Documentation

TauCeti.Algebra.Homology.HomologicalComplex.ZeroDifferential

Complexes with zero differentials #

A family of objects E i forms a homological complex HomologicalComplex.graded c E with zero differentials. It has homology in every degree, and each of its terms consists of cycles (Mathlib's HomologicalComplex.iCyclesIso). Hence a family of morphisms e i : E i ⟶ K.cycles i into the cycles of a complex K defines a morphism of complexes K.fromGraded e, which induces e i on cycles (HomologicalComplex.iCyclesIso_inv_cyclesMap_fromGraded). It is surjective on homology when every e i is an epimorphism (HomologicalComplex.epi_homologyMap_fromGraded), and a quasi-isomorphism when every e i ≫ K.homologyπ i is an isomorphism (HomologicalComplex.quasiIso_fromGraded). Such morphisms are the first step in the construction of resolutions by attaching cells.

More generally, the homology of any complex in a degree where both differentials vanish is the term in that degree (HomologicalComplex.XIsoHomologyOfDEqZero), so it is projective when that term is (HomologicalComplex.projective_homology_of_d_eq_zero).

source
@[reducible, inline]
abbrev HomologicalComplex.graded {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι) (E : ι → C) :
HomologicalComplex C c

The homological complex with terms E i and zero differentials.

Instances For
    source
    @[simp]
    theorem HomologicalComplex.graded_d {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι) (E : ι → C) (x✝ x✝¹ : ι) :
    (graded c E).d x✝ x✝¹ = 0
    source
    @[simp]
    theorem HomologicalComplex.graded_X {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι) (E : ι → C) (a✝ : ι) :
    (graded c E).X a✝ = E a✝
    source
    instance HomologicalComplex.hasHomology_graded {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι) (E : ι → C) (i : ι) :
    (graded c E).HasHomology i

    A complex with zero differentials has homology in every degree.

    source
    noncomputable def HomologicalComplex.XIsoHomologyOfDEqZero {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] (h₁ : K.d (c.prev i) i = 0) (h₂ : K.d i (c.next i) = 0) :
    K.X i ≅ K.homology i

    If the differentials into and out of degree i vanish, the term in degree i is isomorphic to the homology in degree i: every element is a cycle, and none but zero is a boundary.

    Instances For
      source
      @[simp]
      theorem HomologicalComplex.XIsoHomologyOfDEqZero_hom {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] (h₁ : K.d (c.prev i) i = 0) (h₂ : K.d i (c.next i) = 0) :
      (K.XIsoHomologyOfDEqZero i h₁ h₂).hom = CategoryTheory.CategoryStruct.comp (K.iCyclesIso i (c.next i) ⋯ h₂).inv (K.homologyπ i)

      The isomorphism K.XIsoHomologyOfDEqZero i h₁ h₂ sends a term to the class of the corresponding cycle.

      source
      theorem HomologicalComplex.XIsoHomologyOfDEqZero_hom_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] (h₁ : K.d (c.prev i) i = 0) (h₂ : K.d i (c.next i) = 0) {Z : C} (h : K.homology i ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (K.XIsoHomologyOfDEqZero i h₁ h₂).hom h = CategoryTheory.CategoryStruct.comp (K.iCyclesIso i (c.next i) ⋯ h₂).inv (CategoryTheory.CategoryStruct.comp (K.homologyπ i) h)

      The isomorphism K.XIsoHomologyOfDEqZero i h₁ h₂ sends a term to the class of the corresponding cycle.

      source
      @[simp]
      theorem HomologicalComplex.XIsoHomologyOfDEqZero_inv {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] (h₁ : K.d (c.prev i) i = 0) (h₂ : K.d i (c.next i) = 0) :
      (K.XIsoHomologyOfDEqZero i h₁ h₂).inv = CategoryTheory.CategoryStruct.comp (K.isoHomologyπ (c.prev i) i ⋯ h₁).inv (K.iCycles i)

      The inverse of K.XIsoHomologyOfDEqZero i h₁ h₂ sends a homology class to its unique representing cycle, viewed as a term.

      source
      theorem HomologicalComplex.XIsoHomologyOfDEqZero_inv_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] (h₁ : K.d (c.prev i) i = 0) (h₂ : K.d i (c.next i) = 0) {Z : C} (h : K.X i ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (K.XIsoHomologyOfDEqZero i h₁ h₂).inv h = CategoryTheory.CategoryStruct.comp (K.isoHomologyπ (c.prev i) i ⋯ h₁).inv (CategoryTheory.CategoryStruct.comp (K.iCycles i) h)

      The inverse of K.XIsoHomologyOfDEqZero i h₁ h₂ sends a homology class to its unique representing cycle, viewed as a term.

      source
      theorem HomologicalComplex.projective_homology_of_d_eq_zero {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] [CategoryTheory.Projective (K.X i)] (h₁ : K.d (c.prev i) i = 0) (h₂ : K.d i (c.next i) = 0) :
      CategoryTheory.Projective (K.homology i)

      If the differentials into and out of degree i vanish, the homology in degree i is the term in degree i, so it is projective when that term is.

      source
      @[reducible, inline]
      noncomputable abbrev HomologicalComplex.fromGraded {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) [∀ (i : ι), K.HasHomology i] {E : ι → C} (e : (i : ι) → E i ⟶ K.cycles i) :
      graded c E ⟶ K

      The morphism to K from the complex with zero differentials on a family of objects mapping to the cycles of K.

      Instances For
        source
        @[simp]
        theorem HomologicalComplex.fromGraded_f {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) [∀ (i : ι), K.HasHomology i] {E : ι → C} (e : (i : ι) → E i ⟶ K.cycles i) (i : ι) :
        (K.fromGraded e).f i = CategoryTheory.CategoryStruct.comp (e i) (K.iCycles i)
        source
        theorem HomologicalComplex.iCyclesIso_inv_cyclesMap_fromGraded {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) [∀ (i : ι), K.HasHomology i] {E : ι → C} (e : (i : ι) → E i ⟶ K.cycles i) (i : ι) :
        CategoryTheory.CategoryStruct.comp ((graded c E).iCyclesIso i (c.next i) ⋯ ⋯).inv (cyclesMap (K.fromGraded e) i) = e i

        On cycles, the morphism K.fromGraded e is given by e.

        source
        theorem HomologicalComplex.iCyclesIso_inv_cyclesMap_fromGraded_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) [∀ (i : ι), K.HasHomology i] {E : ι → C} (e : (i : ι) → E i ⟶ K.cycles i) (i : ι) {Z : C} (h : K.cycles i ⟶ Z) :
        CategoryTheory.CategoryStruct.comp ((graded c E).iCyclesIso i (c.next i) ⋯ ⋯).inv (CategoryTheory.CategoryStruct.comp (cyclesMap (K.fromGraded e) i) h) = CategoryTheory.CategoryStruct.comp (e i) h

        On cycles, the morphism K.fromGraded e is given by e.

        source
        theorem HomologicalComplex.epi_homologyMap_fromGraded {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) [∀ (i : ι), K.HasHomology i] {E : ι → C} (e : (i : ι) → E i ⟶ K.cycles i) [∀ (i : ι), CategoryTheory.Epi (e i)] (i : ι) :
        CategoryTheory.Epi (homologyMap (K.fromGraded e) i)

        If every e i is an epimorphism, then K.fromGraded e is surjective on homology.

        source
        theorem HomologicalComplex.quasiIso_fromGraded {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) [∀ (i : ι), K.HasHomology i] {E : ι → C} (e : (i : ι) → E i ⟶ K.cycles i) (he : ∀ (i : ι), CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (e i) (K.homologyπ i))) :
        QuasiIso (K.fromGraded e)

        If every e i ≫ K.homologyπ i is an isomorphism, for instance when each e i is a section of K.homologyπ i, then K.fromGraded e is a quasi-isomorphism.