Documentation

Mathlib.Algebra.Homology.HomologySequence

The homology sequence #

If 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 is a short exact sequence in a category of complexes HomologicalComplex C c in an abelian category (i.e. S is a short complex in that category and satisfies hS : S.ShortExact), then whenever i and j are degrees such that hij : c.Rel i j, then there is a long exact sequence : ... ⟶ S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j ⟶ .... The connecting homomorphism S.X₃.homology i ⟶ S.X₁.homology j is hS.δ i j hij, and the exactness is asserted as lemmas hS.homology_exact₁, hS.homology_exact₂ and hS.homology_exact₃.

The proof is based on the snake lemma, similarly as it was originally done in the Liquid Tensor Experiment.

References #

noncomputable def HomologicalComplex.opcyclesToCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] :
K.opcycles i K.cycles j

The morphism K.opcycles i ⟶ K.cycles j that is induced by K.d i j.

Equations
  • K.opcyclesToCycles i j = K.liftCycles (K.fromOpcycles i j) (c.next j)
Instances For
    @[simp]
    theorem HomologicalComplex.opcyclesToCycles_iCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.X j Z) :
    CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) = CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) h
    @[simp]
    theorem HomologicalComplex.opcyclesToCycles_iCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] :
    CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.iCycles j) = K.fromOpcycles i j
    theorem HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.X j Z) :
    theorem HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] :
    CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.iCycles j)) = K.d i j
    @[simp]
    theorem HomologicalComplex.pOpcycles_opcyclesToCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.cycles j Z) :
    @[simp]
    theorem HomologicalComplex.pOpcycles_opcyclesToCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] :
    CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.opcyclesToCycles i j) = K.toCycles i j
    @[simp]
    theorem HomologicalComplex.homologyι_opcyclesToCycles_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.cycles j Z) :
    @[simp]
    theorem HomologicalComplex.homologyι_opcyclesToCycles {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] :
    CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.opcyclesToCycles i j) = 0
    @[simp]
    theorem HomologicalComplex.opcyclesToCycles_homologyπ_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.homology j Z) :
    @[simp]
    theorem HomologicalComplex.opcyclesToCycles_homologyπ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] :
    CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.homologyπ j) = 0
    @[simp]
    theorem HomologicalComplex.opcyclesToCycles_naturality_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] [L.HasHomology i] [L.HasHomology j] {Z : C} (h : L.cycles j Z) :
    @[simp]
    theorem HomologicalComplex.opcyclesToCycles_naturality {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K L) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] [L.HasHomology i] [L.HasHomology j] :

    The natural transformation K.opcyclesToCycles i j : K.opcycles i ⟶ K.cycles j for all K : HomologicalComplex C c.

    Equations
    Instances For
      noncomputable def HomologicalComplex.HomologySequence.composableArrows₃ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] :

      The diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j.

      Equations
      Instances For

        The diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j is exact when c.Rel i j.

        The functor HomologicalComplex C c ⥤ ComposableArrows C 3 that maps K to the diagram K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem HomologicalComplex.opcycles_right_exact {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) (hS : S.Exact) [CategoryTheory.Epi S.g] (i : ι) [S.X₁.HasHomology i] [S.X₂.HasHomology i] [S.X₃.HasHomology i] :

          If X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 is an exact sequence of homological complexes, then X₁.opcycles i ⟶ X₂.opcycles i ⟶ X₃.opcycles i ⟶ 0 is exact. This lemma states the exactness at X₂.opcycles i, while the fact that X₂.opcycles i ⟶ X₃.opcycles i is an epi is an instance.

          theorem HomologicalComplex.cycles_left_exact {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) (hS : S.Exact) [CategoryTheory.Mono S.f] (i : ι) [S.X₁.HasHomology i] [S.X₂.HasHomology i] [S.X₃.HasHomology i] :

          If 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ is an exact sequence of homological complex, then 0 ⟶ X₁.cycles i ⟶ X₂.cycles i ⟶ X₃.cycles i is exact. This lemma states the exactness at X₂.cycles i, while the fact that X₁.cycles i ⟶ X₂.cycles i is a mono is an instance.

          @[simp]
          theorem HomologicalComplex.HomologySequence.snakeInput_L₁ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) :
          @[simp]
          theorem HomologicalComplex.HomologySequence.snakeInput_L₀ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) :
          @[simp]
          theorem HomologicalComplex.HomologySequence.snakeInput_L₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) :
          @[simp]
          theorem HomologicalComplex.HomologySequence.snakeInput_L₃ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) :

          Given a short exact short complex S : HomologicalComplex C c, and degrees i and j such that c.Rel i j, this is the snake diagram whose four lines are respectively obtained by applying the functors homologyFunctor C c i, opcyclesFunctor C c i, cyclesFunctor C c j, homologyFunctor C c j to S. Applying the snake lemma to this gives the homology sequence of S.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            noncomputable def CategoryTheory.ShortComplex.ShortExact.δ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) :
            S.X₃.homology i S.X₁.homology j

            The connecting homoomorphism S.X₃.homology i ⟶ S.X₁.homology j for a short exact short complex S.

            Equations
            Instances For
              @[simp]
              @[simp]
              theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₁ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) :

              Exactness of S.X₃.homology i ⟶ S.X₁.homology j ⟶ S.X₂.homology j.

              Exactness of S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i.

              theorem CategoryTheory.ShortComplex.ShortExact.homology_exact₃ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) :

              Exactness of S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j.

              theorem CategoryTheory.ShortComplex.ShortExact.δ_eq' {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) {A : C} (x₃ : A S.X₃.homology i) (x₂ : A S.X₂.opcycles i) (x₁ : A S.X₁.cycles j) (h₂ : CategoryTheory.CategoryStruct.comp x₂ (HomologicalComplex.opcyclesMap S.g i) = CategoryTheory.CategoryStruct.comp x₃ (S.X₃.homologyι i)) (h₁ : CategoryTheory.CategoryStruct.comp x₁ (HomologicalComplex.cyclesMap S.f j) = CategoryTheory.CategoryStruct.comp x₂ (S.X₂.opcyclesToCycles i j)) :
              CategoryTheory.CategoryStruct.comp x₃ (hS i j hij) = CategoryTheory.CategoryStruct.comp x₁ (S.X₁.homologyπ j)
              theorem CategoryTheory.ShortComplex.ShortExact.δ_eq {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) {A : C} (x₃ : A S.X₃.X i) (hx₃ : CategoryTheory.CategoryStruct.comp x₃ (S.X₃.d i j) = 0) (x₂ : A S.X₂.X i) (hx₂ : CategoryTheory.CategoryStruct.comp x₂ (S.g.f i) = x₃) (x₁ : A S.X₁.X j) (hx₁ : CategoryTheory.CategoryStruct.comp x₁ (S.f.f j) = CategoryTheory.CategoryStruct.comp x₂ (S.X₂.d i j)) (k : ι) (hk : c.next j = k) :
              CategoryTheory.CategoryStruct.comp (S.X₃.liftCycles x₃ j hx₃) (CategoryTheory.CategoryStruct.comp (S.X₃.homologyπ i) (hS i j hij)) = CategoryTheory.CategoryStruct.comp (S.X₁.liftCycles x₁ k hk ) (S.X₁.homologyπ j)