The short complexes attached to homological complexes

In this file, we define a functor shortComplexFunctor C c i : HomologicalComplex C c ⥤ ShortComplex C. By definition, the image of a homological complex K by this functor is the short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

The homology K.homology i of a homological complex K in degree i is defined as the homology of the short complex (shortComplexFunctor C c i).obj K, which can be abbreviated as K.sc i.

def HomologicalComplex.shortComplexFunctor' (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) : CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.ShortComplex C)

The functor HomologicalComplex C c ⥤ ShortComplex C which sends a homological complex K to the short complex K.X i ⟶ K.X j ⟶ K.X k for arbitrary indices i, j and k.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomologicalComplex.shortComplexFunctor'_map_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) : ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₁ = f.f i

@[simp]

theorem HomologicalComplex.shortComplexFunctor'_obj_X₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₂ = K.X j

@[simp]

theorem HomologicalComplex.shortComplexFunctor'_obj_f (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).f = K.d i j

@[simp]

theorem HomologicalComplex.shortComplexFunctor'_obj_X₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₃ = K.X k

@[simp]

theorem HomologicalComplex.shortComplexFunctor'_map_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) : ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₃ = f.f k

@[simp]

theorem HomologicalComplex.shortComplexFunctor'_obj_g (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).g = K.d j k

@[simp]

theorem HomologicalComplex.shortComplexFunctor'_obj_X₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₁ = K.X i

@[simp]

theorem HomologicalComplex.shortComplexFunctor'_map_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) : ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor' C c i j k).map f).τ₂ = f.f j

noncomputable def HomologicalComplex.shortComplexFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) : CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.ShortComplex C)

The functor HomologicalComplex C c ⥤ ShortComplex C which sends a homological complex K to the short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

Equations

• HomologicalComplex.shortComplexFunctor C c i = HomologicalComplex.shortComplexFunctor' C c (c.prev i) i (c.next i)

@[simp]

theorem HomologicalComplex.shortComplexFunctor_map_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) : ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₃ = f.f (c.next i)

@[simp]

theorem HomologicalComplex.shortComplexFunctor_obj_g (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor C c i).obj K).g = K.d i (c.next i)

@[simp]

theorem HomologicalComplex.shortComplexFunctor_map_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) : ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₂ = f.f i

@[simp]

theorem HomologicalComplex.shortComplexFunctor_obj_f (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor C c i).obj K).f = K.d (c.prev i) i

@[simp]

theorem HomologicalComplex.shortComplexFunctor_obj_X₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor C c i).obj K).X₂ = K.X i

@[simp]

theorem HomologicalComplex.shortComplexFunctor_obj_X₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor C c i).obj K).X₁ = K.X (c.prev i)

@[simp]

theorem HomologicalComplex.shortComplexFunctor_obj_X₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor C c i).obj K).X₃ = K.X (c.next i)

@[simp]

theorem HomologicalComplex.shortComplexFunctor_map_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) : ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₁ = f.f (c.prev i)

noncomputable def HomologicalComplex.natIsoSc' (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) : HomologicalComplex.shortComplexFunctor C c j ≅ HomologicalComplex.shortComplexFunctor' C c i j k

The natural isomorphism shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k when c.prev j = i and c.next j = k.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomologicalComplex.natIsoSc'_inv_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) : ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₂ = CategoryTheory.CategoryStruct.id (X.X j)

@[simp]

theorem HomologicalComplex.natIsoSc'_inv_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) : ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₁ = (X.XIsoOfEq hi).inv

@[simp]

theorem HomologicalComplex.natIsoSc'_hom_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) : ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₃ = (X.XIsoOfEq hk).hom

@[simp]

theorem HomologicalComplex.natIsoSc'_hom_app_τ₂ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) : ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₂ = CategoryTheory.CategoryStruct.id (X.X j)

@[simp]

theorem HomologicalComplex.natIsoSc'_inv_app_τ₃ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) : ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₃ = (X.XIsoOfEq hk).inv

@[simp]

theorem HomologicalComplex.natIsoSc'_hom_app_τ₁ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c) : ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₁ = (X.XIsoOfEq hi).hom

@[reducible, inline]

abbrev HomologicalComplex.sc' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) : CategoryTheory.ShortComplex C

The short complex K.X i ⟶ K.X j ⟶ K.X k for arbitrary indices i, j and k.

Equations

• K.sc' i j k = (HomologicalComplex.shortComplexFunctor' C c i j k).obj K

@[reducible, inline]

noncomputable abbrev HomologicalComplex.sc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) : CategoryTheory.ShortComplex C

The short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i).

Equations

• K.sc i = (HomologicalComplex.shortComplexFunctor C c i).obj K

@[reducible, inline]

noncomputable abbrev HomologicalComplex.isoSc' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) : K.sc j ≅ K.sc' i j k

The canonical isomorphism K.sc j ≅ K.sc' i j k when c.prev j = i and c.next j = k.

Equations

• K.isoSc' i j k hi hk = (HomologicalComplex.natIsoSc' C c i j k hi hk).app K

@[reducible, inline]

abbrev HomologicalComplex.HasHomology {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) : Prop

A homological complex K has homology in degree i if the associated short complex K.sc i has.

Equations

• K.HasHomology i = (K.sc i).HasHomology

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

The homology in degree i of a homological complex.

Equations

• K.homology i = (K.sc i).homology

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

The cycles in degree i of a homological complex.

Equations

• K.cycles i = (K.sc i).cycles

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

The inclusion of the cycles of a homological complex.

Equations

• K.iCycles i = (K.sc i).iCycles

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

The homology class map from cycles to the homology of a homological complex.

Equations

• K.homologyπ i = (K.sc i).homologyπ

noncomputable def HomologicalComplex.liftCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) : A ⟶ K.cycles i

The morphism to K.cycles i that is induced by a "cycle", i.e. a morphism to K.X i whose postcomposition with the differential is zero.

Equations

• K.liftCycles k j hj hk = (K.sc i).liftCycles k ⋯

@[reducible, inline]

noncomputable abbrev HomologicalComplex.liftCycles' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.Rel i j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) : A ⟶ K.cycles i

The morphism to K.cycles i that is induced by a "cycle", i.e. a morphism to K.X i whose postcomposition with the differential is zero.

Equations

• K.liftCycles' k j hj hk = K.liftCycles k j ⋯ hk

@[simp]

theorem HomologicalComplex.liftCycles_i {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) : CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) (K.iCycles i) = k

@[simp]

theorem HomologicalComplex.liftCycles_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) {Z : C} (h : K.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) (CategoryTheory.CategoryStruct.comp (K.iCycles i) h) = CategoryTheory.CategoryStruct.comp k h

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

The map K.X i ⟶ K.cycles j induced by the differential K.d i j.

Equations

• K.toCycles i j = K.liftCycles (K.d i j) (c.next j) ⋯ ⋯

@[simp]

theorem HomologicalComplex.iCycles_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.iCycles i) (K.d i j) = 0

@[simp]

theorem HomologicalComplex.iCycles_d_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.iCycles i) (CategoryTheory.CategoryStruct.comp (K.d i j) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def HomologicalComplex.cyclesIsKernel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] (hj : c.next i = j) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (K.iCycles i) ⋯)

K.cycles i is the kernel of K.d i j when c.next i = j.

Equations

• K.cyclesIsKernel i j hj = hj ▸ (K.sc i).cyclesIsKernel

@[simp]

theorem HomologicalComplex.toCycles_i {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.toCycles i j) (K.iCycles j) = K.d i j

@[simp]

theorem HomologicalComplex.toCycles_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology j] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.toCycles i j) (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) = CategoryTheory.CategoryStruct.comp (K.d i j) h

instance HomologicalComplex.instMonoICycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] : CategoryTheory.Mono (K.iCycles i)

Equations

• ⋯ = ⋯

instance HomologicalComplex.instEpiHomologyπ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] : CategoryTheory.Epi (K.homologyπ i)

Equations

• ⋯ = ⋯

@[simp]

theorem HomologicalComplex.d_toCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) [K.HasHomology k] : CategoryTheory.CategoryStruct.comp (K.d i j) (K.toCycles j k) = 0

@[simp]

theorem HomologicalComplex.d_toCycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) [K.HasHomology k] {Z : C} (h : K.cycles k ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d i j) (CategoryTheory.CategoryStruct.comp (K.toCycles j k) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem HomologicalComplex.comp_liftCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A' : C} {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (α : A' ⟶ A) : CategoryTheory.CategoryStruct.comp α (K.liftCycles k j hj hk) = K.liftCycles (CategoryTheory.CategoryStruct.comp α k) j hj ⋯

theorem HomologicalComplex.comp_liftCycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A' : C} {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (α : A' ⟶ A) {Z : C} (h : K.cycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) h) = CategoryTheory.CategoryStruct.comp (K.liftCycles (CategoryTheory.CategoryStruct.comp α k) j hj ⋯) h

theorem HomologicalComplex.liftCycles_homologyπ_eq_zero_of_boundary {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) {i' : ι} (x : A ⟶ K.X i') (hx : k = CategoryTheory.CategoryStruct.comp x (K.d i' i)) : CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj ⋯) (K.homologyπ i) = 0

theorem HomologicalComplex.liftCycles_homologyπ_eq_zero_of_boundary_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) {i' : ι} (x : A ⟶ K.X i') (hx : k = CategoryTheory.CategoryStruct.comp x (K.d i' i)) {Z : C} (h : K.homology i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj ⋯) (CategoryTheory.CategoryStruct.comp (K.homologyπ i) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex.toCycles_comp_homologyπ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.toCycles i j) (K.homologyπ j) = 0

@[simp]

theorem HomologicalComplex.toCycles_comp_homologyπ_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology j] {Z : C} (h : K.homology j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.toCycles i j) (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def HomologicalComplex.homologyIsCokernel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) [K.HasHomology j] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (K.homologyπ j) ⋯)

K.homology j is the cokernel of K.toCycles i j : K.X i ⟶ K.cycles j when c.prev j = i.

Equations

• K.homologyIsCokernel i j hi = hi ▸ (K.sc j).homologyIsCokernel

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

The opcycles in degree i of a homological complex.

Equations

• K.opcycles i = (K.sc i).opcycles

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

The projection to the opcycles of a homological complex.

Equations

• K.pOpcycles i = (K.sc i).pOpcycles

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

The inclusion map of the homology of a homological complex into its opcycles.

Equations

• K.homologyι i = (K.sc i).homologyι

noncomputable def HomologicalComplex.descOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) : K.opcycles i ⟶ A

The morphism from K.opcycles i that is induced by an "opcycle", i.e. a morphism from K.X i whose precomposition with the differential is zero.

Equations

• K.descOpcycles k j hj hk = (K.sc i).descOpcycles k ⋯

@[reducible, inline]

noncomputable abbrev HomologicalComplex.descOpcycles' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : c.Rel j i) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) : K.opcycles i ⟶ A

The morphism from K.opcycles i that is induced by an "opcycle", i.e. a morphism from K.X i whose precomposition with the differential is zero.

Equations

• K.descOpcycles' k j hj hk = K.descOpcycles k j ⋯ hk

@[simp]

theorem HomologicalComplex.p_descOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) : CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.descOpcycles k j hj hk) = k

@[simp]

theorem HomologicalComplex.p_descOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (K.descOpcycles k j hj hk) h) = CategoryTheory.CategoryStruct.comp k h

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

The map K.opcycles i ⟶ K.X j induced by the differential K.d i j.

Equations

• K.fromOpcycles i j = K.descOpcycles (K.d i j) (c.prev i) ⋯ ⋯

@[simp]

theorem HomologicalComplex.d_pOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.d i j) (K.pOpcycles j) = 0

@[simp]

theorem HomologicalComplex.d_pOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] [K.HasHomology j] {Z : C} (h : K.opcycles j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d i j) (CategoryTheory.CategoryStruct.comp (K.pOpcycles j) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def HomologicalComplex.opcyclesIsCokernel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] (hi : c.prev j = i) [K.HasHomology j] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (K.pOpcycles j) ⋯)

K.opcycles j is the cokernel of K.d i j when c.prev j = i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomologicalComplex.p_fromOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (K.fromOpcycles i j) = K.d i j

@[simp]

theorem HomologicalComplex.p_fromOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) h) = CategoryTheory.CategoryStruct.comp (K.d i j) h

instance HomologicalComplex.instEpiPOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] : CategoryTheory.Epi (K.pOpcycles i)

Equations

• ⋯ = ⋯

instance HomologicalComplex.instMonoHomologyι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] : CategoryTheory.Mono (K.homologyι i)

Equations

• ⋯ = ⋯

@[simp]

theorem HomologicalComplex.fromOpcycles_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) [K.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) (K.d j k) = 0

@[simp]

theorem HomologicalComplex.fromOpcycles_d_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) [K.HasHomology i] {Z : C} (h : K.X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) (CategoryTheory.CategoryStruct.comp (K.d j k) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem HomologicalComplex.descOpcycles_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} {A' : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) (α : A ⟶ A') : CategoryTheory.CategoryStruct.comp (K.descOpcycles k j hj hk) α = K.descOpcycles (CategoryTheory.CategoryStruct.comp k α) j hj ⋯

theorem HomologicalComplex.descOpcycles_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} {A' : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) (α : A ⟶ A') {Z : C} (h : A' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.descOpcycles k j hj hk) (CategoryTheory.CategoryStruct.comp α h) = CategoryTheory.CategoryStruct.comp (K.descOpcycles (CategoryTheory.CategoryStruct.comp k α) j hj ⋯) h

theorem HomologicalComplex.homologyι_descOpcycles_eq_zero_of_boundary {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) {i' : ι} (x : K.X i' ⟶ A) (hx : k = CategoryTheory.CategoryStruct.comp (K.d i i') x) : CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.descOpcycles k j hj ⋯) = 0

theorem HomologicalComplex.homologyι_descOpcycles_eq_zero_of_boundary_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [K.HasHomology i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) {i' : ι} (x : K.X i' ⟶ A) (hx : k = CategoryTheory.CategoryStruct.comp (K.d i i') x) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.homologyι i) (CategoryTheory.CategoryStruct.comp (K.descOpcycles k j hj ⋯) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem HomologicalComplex.homologyι_comp_fromOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.fromOpcycles i j) = 0

@[simp]

theorem HomologicalComplex.homologyι_comp_fromOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.homologyι i) (CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def HomologicalComplex.homologyIsKernel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) [K.HasHomology i] (hi : c.next i = j) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (K.homologyι i) ⋯)

K.homology i is the kernel of K.fromOpcycles i j : K.opcycles i ⟶ K.X j when c.next i = j.

Equations

• K.homologyIsKernel i j hi = hi ▸ (K.sc i).homologyIsKernel

noncomputable def HomologicalComplex.homologyMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : K.homology i ⟶ L.homology i

The map K.homology i ⟶ L.homology i induced by a morphism in HomologicalComplex.

Equations

• HomologicalComplex.homologyMap φ i = CategoryTheory.ShortComplex.homologyMap ((HomologicalComplex.shortComplexFunctor C c i).map φ)

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

The map K.cycles i ⟶ L.cycles i induced by a morphism in HomologicalComplex.

Equations

• HomologicalComplex.cyclesMap φ i = CategoryTheory.ShortComplex.cyclesMap ((HomologicalComplex.shortComplexFunctor C c i).map φ)

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

The map K.opcycles i ⟶ L.opcycles i induced by a morphism in HomologicalComplex.

Equations

• HomologicalComplex.opcyclesMap φ i = CategoryTheory.ShortComplex.opcyclesMap ((HomologicalComplex.shortComplexFunctor C c i).map φ)

@[simp]

theorem HomologicalComplex.cyclesMap_i {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (L.iCycles i) = CategoryTheory.CategoryStruct.comp (K.iCycles i) (φ.f i)

@[simp]

theorem HomologicalComplex.cyclesMap_i_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] {Z : C} (h : L.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (CategoryTheory.CategoryStruct.comp (L.iCycles i) h) = CategoryTheory.CategoryStruct.comp (K.iCycles i) (CategoryTheory.CategoryStruct.comp (φ.f i) h)

@[simp]

theorem HomologicalComplex.p_opcyclesMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (HomologicalComplex.opcyclesMap φ i) = CategoryTheory.CategoryStruct.comp (φ.f i) (L.pOpcycles i)

@[simp]

theorem HomologicalComplex.p_opcyclesMap_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] {Z : C} (h : L.opcycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) h) = CategoryTheory.CategoryStruct.comp (φ.f i) (CategoryTheory.CategoryStruct.comp (L.pOpcycles i) h)

instance HomologicalComplex.instMonoCyclesMapOfF {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [CategoryTheory.Mono (φ.f i)] : CategoryTheory.Mono (HomologicalComplex.cyclesMap φ i)

Equations

• ⋯ = ⋯

instance HomologicalComplex.instEpiOpcyclesMapOfF {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [CategoryTheory.Epi (φ.f i)] : CategoryTheory.Epi (HomologicalComplex.opcyclesMap φ i)

Equations

• ⋯ = ⋯

@[simp]

theorem HomologicalComplex.homologyMap_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] : HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.id K) i = CategoryTheory.CategoryStruct.id (K.homology i)

@[simp]

theorem HomologicalComplex.cyclesMap_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] : HomologicalComplex.cyclesMap (CategoryTheory.CategoryStruct.id K) i = CategoryTheory.CategoryStruct.id (K.cycles i)

@[simp]

theorem HomologicalComplex.opcyclesMap_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] : HomologicalComplex.opcyclesMap (CategoryTheory.CategoryStruct.id K) i = CategoryTheory.CategoryStruct.id (K.opcycles i)

theorem HomologicalComplex.homologyMap_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] : HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.comp φ ψ) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (HomologicalComplex.homologyMap ψ i)

theorem HomologicalComplex.homologyMap_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] {Z : C} (h : M.homology i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.comp φ ψ) i) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ψ i) h)

theorem HomologicalComplex.cyclesMap_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] : HomologicalComplex.cyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (HomologicalComplex.cyclesMap ψ i)

theorem HomologicalComplex.cyclesMap_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] {Z : C} (h : M.cycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) i) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap ψ i) h)

theorem HomologicalComplex.opcyclesMap_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] : HomologicalComplex.opcyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (HomologicalComplex.opcyclesMap ψ i)

theorem HomologicalComplex.opcyclesMap_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] {Z : C} (h : M.opcycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) i) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ψ i) h)

@[simp]

theorem HomologicalComplex.homologyMap_zero {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (L : HomologicalComplex C c) (i : ι) [K.HasHomology i] [L.HasHomology i] : HomologicalComplex.homologyMap 0 i = 0

@[simp]

theorem HomologicalComplex.cyclesMap_zero {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (L : HomologicalComplex C c) (i : ι) [K.HasHomology i] [L.HasHomology i] : HomologicalComplex.cyclesMap 0 i = 0

@[simp]

theorem HomologicalComplex.opcyclesMap_zero {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (L : HomologicalComplex C c) (i : ι) [K.HasHomology i] [L.HasHomology i] : HomologicalComplex.opcyclesMap 0 i = 0

@[simp]

theorem HomologicalComplex.homologyπ_naturality {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.homologyπ i) (HomologicalComplex.homologyMap φ i) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (L.homologyπ i)

@[simp]

theorem HomologicalComplex.homologyπ_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] {Z : C} (h : L.homology i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.homologyπ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (CategoryTheory.CategoryStruct.comp (L.homologyπ i) h)

@[simp]

theorem HomologicalComplex.homologyι_naturality {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (L.homologyι i) = CategoryTheory.CategoryStruct.comp (K.homologyι i) (HomologicalComplex.opcyclesMap φ i)

@[simp]

theorem HomologicalComplex.homologyι_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] {Z : C} (h : L.opcycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (CategoryTheory.CategoryStruct.comp (L.homologyι i) h) = CategoryTheory.CategoryStruct.comp (K.homologyι i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) h)

@[simp]

theorem HomologicalComplex.homology_π_ι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} (i : ι) [K.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.homologyπ i) (K.homologyι i) = CategoryTheory.CategoryStruct.comp (K.iCycles i) (K.pOpcycles i)

@[simp]

theorem HomologicalComplex.homology_π_ι_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} (i : ι) [K.HasHomology i] {Z : C} (h : K.opcycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.homologyπ i) (CategoryTheory.CategoryStruct.comp (K.homologyι i) h) = CategoryTheory.CategoryStruct.comp (K.iCycles i) (CategoryTheory.CategoryStruct.comp (K.pOpcycles i) h)

@[simp]

theorem HomologicalComplex.opcyclesMap_comp_descOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {i : ι} [K.HasHomology i] [L.HasHomology i] {A : C} (k : L.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (L.d j i) k = 0) (φ : K ⟶ L) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (L.descOpcycles k j hj hk) = K.descOpcycles (CategoryTheory.CategoryStruct.comp (φ.f i) k) j hj ⋯

@[simp]

theorem HomologicalComplex.opcyclesMap_comp_descOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {i : ι} [K.HasHomology i] [L.HasHomology i] {A : C} (k : L.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (L.d j i) k = 0) (φ : K ⟶ L) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (CategoryTheory.CategoryStruct.comp (L.descOpcycles k j hj hk) h) = CategoryTheory.CategoryStruct.comp (K.descOpcycles (CategoryTheory.CategoryStruct.comp (φ.f i) k) j hj ⋯) h

@[simp]

theorem HomologicalComplex.liftCycles_comp_cyclesMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {i : ι} [K.HasHomology i] [L.HasHomology i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (φ : K ⟶ L) : CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) (HomologicalComplex.cyclesMap φ i) = L.liftCycles (CategoryTheory.CategoryStruct.comp k (φ.f i)) j hj ⋯

@[simp]

theorem HomologicalComplex.liftCycles_comp_cyclesMap_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {i : ι} [K.HasHomology i] [L.HasHomology i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (φ : K ⟶ L) {Z : C} (h : L.cycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) h) = CategoryTheory.CategoryStruct.comp (L.liftCycles (CategoryTheory.CategoryStruct.comp k (φ.f i)) j hj ⋯) h

noncomputable def HomologicalComplex.homologyFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : CategoryTheory.Functor (HomologicalComplex C c) C

The ith homology functor HomologicalComplex C c ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomologicalComplex.homologyFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c) : (HomologicalComplex.homologyFunctor C c i).obj K = K.homology i

@[simp]

theorem HomologicalComplex.homologyFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), (HomologicalComplex.homologyFunctor C c i).map f = HomologicalComplex.homologyMap f i

noncomputable def HomologicalComplex.gradedHomologyFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.CategoryWithHomology C] : CategoryTheory.Functor (HomologicalComplex C c) (CategoryTheory.GradedObject ι C)

The homology functor to graded objects.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomologicalComplex.gradedHomologyFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c) (i : ι) : (HomologicalComplex.gradedHomologyFunctor C c).obj K i = K.homology i

@[simp]

theorem HomologicalComplex.gradedHomologyFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.CategoryWithHomology C] : ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y) (i : ι), (HomologicalComplex.gradedHomologyFunctor C c).map f i = HomologicalComplex.homologyMap f i

noncomputable def HomologicalComplex.cyclesFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : CategoryTheory.Functor (HomologicalComplex C c) C

The ith cycles functor HomologicalComplex C c ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomologicalComplex.cyclesFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), (HomologicalComplex.cyclesFunctor C c i).map f = HomologicalComplex.cyclesMap f i

@[simp]

theorem HomologicalComplex.cyclesFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c) : (HomologicalComplex.cyclesFunctor C c i).obj K = K.cycles i

noncomputable def HomologicalComplex.opcyclesFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : CategoryTheory.Functor (HomologicalComplex C c) C

The ith opcycles functor HomologicalComplex C c ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HomologicalComplex.opcyclesFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c) : (HomologicalComplex.opcyclesFunctor C c i).obj K = K.opcycles i

@[simp]

theorem HomologicalComplex.opcyclesFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y), (HomologicalComplex.opcyclesFunctor C c i).map f = HomologicalComplex.opcyclesMap f i

noncomputable def HomologicalComplex.natTransHomologyπ (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : HomologicalComplex.cyclesFunctor C c i ⟶ HomologicalComplex.homologyFunctor C c i

The natural transformation K.homologyπ i : K.cycles i ⟶ K.homology i for all K : HomologicalComplex C c.

Equations

• HomologicalComplex.natTransHomologyπ C c i = { app := fun (K : HomologicalComplex C c) => K.homologyπ i, naturality := ⋯ }

@[simp]

theorem HomologicalComplex.natTransHomologyπ_app (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c) : (HomologicalComplex.natTransHomologyπ C c i).app K = K.homologyπ i

noncomputable def HomologicalComplex.natTransHomologyι (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : HomologicalComplex.homologyFunctor C c i ⟶ HomologicalComplex.opcyclesFunctor C c i

The natural transformation K.homologyι i : K.homology i ⟶ K.opcycles i for all K : HomologicalComplex C c.

Equations

• HomologicalComplex.natTransHomologyι C c i = { app := fun (K : HomologicalComplex C c) => K.homologyι i, naturality := ⋯ }

@[simp]

theorem HomologicalComplex.natTransHomologyι_app (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c) : (HomologicalComplex.natTransHomologyι C c i).app K = K.homologyι i

noncomputable def HomologicalComplex.homologyFunctorIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : HomologicalComplex.homologyFunctor C c i ≅ (HomologicalComplex.shortComplexFunctor C c i).comp (CategoryTheory.ShortComplex.homologyFunctor C)

The natural isomorphism K.homology i ≅ (K.sc i).homology for all homological complexes K.

Equations

• HomologicalComplex.homologyFunctorIso C c i = CategoryTheory.Iso.refl (HomologicalComplex.homologyFunctor C c i)

@[simp]

theorem HomologicalComplex.homologyFunctorIso_hom_app (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] (X : HomologicalComplex C c) : (HomologicalComplex.homologyFunctorIso C c i).hom.app X = CategoryTheory.CategoryStruct.id (X.homology i)

@[simp]

theorem HomologicalComplex.homologyFunctorIso_inv_app (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] (X : HomologicalComplex C c) : (HomologicalComplex.homologyFunctorIso C c i).inv.app X = CategoryTheory.CategoryStruct.id (X.homology i)

noncomputable def HomologicalComplex.homologyFunctorIso' (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) (j : ι) (k : ι) [CategoryTheory.CategoryWithHomology C] (hi : c.prev j = i) (hk : c.next j = k) : HomologicalComplex.homologyFunctor C c j ≅ (HomologicalComplex.shortComplexFunctor' C c i j k).comp (CategoryTheory.ShortComplex.homologyFunctor C)

The natural isomorphism K.homology j ≅ (K.sc' i j k).homology for all homological complexes K when c.prev j = i and c.next j = k.

Equations

• One or more equations did not get rendered due to their size.

instance HomologicalComplex.instPreservesZeroMorphismsHomologyFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : (HomologicalComplex.homologyFunctor C c i).PreservesZeroMorphisms

Equations

• ⋯ = ⋯

instance HomologicalComplex.instPreservesZeroMorphismsOpcyclesFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : (HomologicalComplex.opcyclesFunctor C c i).PreservesZeroMorphisms

Equations

• ⋯ = ⋯

instance HomologicalComplex.instPreservesZeroMorphismsCyclesFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [CategoryTheory.CategoryWithHomology C] : (HomologicalComplex.cyclesFunctor C c i).PreservesZeroMorphisms

Equations

• ⋯ = ⋯

theorem HomologicalComplex.isIso_iCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] : CategoryTheory.IsIso (K.iCycles i)

noncomputable def HomologicalComplex.iCyclesIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] : K.cycles i ≅ K.X i

The canonical isomorphism K.cycles i ≅ K.X i when the differential from i is zero.

Equations

• K.iCyclesIso i j hj h = CategoryTheory.asIso (K.iCycles i)

@[simp]

theorem HomologicalComplex.iCyclesIso_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] : (K.iCyclesIso i j hj h).hom = K.iCycles i

@[simp]

theorem HomologicalComplex.iCyclesIso_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.iCycles i) (K.iCyclesIso i j hj h).inv = CategoryTheory.CategoryStruct.id (K.cycles i)

@[simp]

theorem HomologicalComplex.iCyclesIso_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] {Z : C} (h : K.cycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.iCycles i) (CategoryTheory.CategoryStruct.comp (K.iCyclesIso i j hj h✝).inv h) = h

@[simp]

theorem HomologicalComplex.iCyclesIso_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.iCyclesIso i j hj h).inv (K.iCycles i) = CategoryTheory.CategoryStruct.id (K.X i)

@[simp]

theorem HomologicalComplex.iCyclesIso_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] {Z : C} (h : K.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.iCyclesIso i j hj h✝).inv (CategoryTheory.CategoryStruct.comp (K.iCycles i) h) = h

theorem HomologicalComplex.isIso_homologyι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] : CategoryTheory.IsIso (K.homologyι i)

noncomputable def HomologicalComplex.isoHomologyι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] : K.homology i ≅ K.opcycles i

The canonical isomorphism K.homology i ≅ K.opcycles i when the differential from i is zero.

Equations

• K.isoHomologyι i j hj h = CategoryTheory.asIso (K.homologyι i)

@[simp]

theorem HomologicalComplex.isoHomologyι_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] : (K.isoHomologyι i j hj h).hom = K.homologyι i

@[simp]

theorem HomologicalComplex.isoHomologyι_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.homologyι i) (K.isoHomologyι i j hj h).inv = CategoryTheory.CategoryStruct.id (K.homology i)

@[simp]

theorem HomologicalComplex.isoHomologyι_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] {Z : C} (h : K.homology i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.homologyι i) (CategoryTheory.CategoryStruct.comp (K.isoHomologyι i j hj h✝).inv h) = h

@[simp]

theorem HomologicalComplex.isoHomologyι_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] : CategoryTheory.CategoryStruct.comp (K.isoHomologyι i j hj h).inv (K.homologyι i) = CategoryTheory.CategoryStruct.id (K.opcycles i)

@[simp]

theorem HomologicalComplex.isoHomologyι_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hj : c.next i = j) (h : K.d i j = 0) [K.HasHomology i] {Z : C} (h : K.opcycles i ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.isoHomologyι i j hj h✝).inv (CategoryTheory.CategoryStruct.comp (K.homologyι i) h) = h

theorem HomologicalComplex.isIso_pOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] : CategoryTheory.IsIso (K.pOpcycles j)

noncomputable def HomologicalComplex.pOpcyclesIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] : K.X j ≅ K.opcycles j

The canonical isomorphism K.X j ≅ K.opCycles j when the differential to j is zero.

Equations

• K.pOpcyclesIso i j hi h = CategoryTheory.asIso (K.pOpcycles j)

@[simp]

theorem HomologicalComplex.pOpcyclesIso_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] : (K.pOpcyclesIso i j hi h).hom = K.pOpcycles j

@[simp]

theorem HomologicalComplex.pOpcyclesIso_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (K.pOpcyclesIso i j hi h).inv = CategoryTheory.CategoryStruct.id (K.X j)

@[simp]

theorem HomologicalComplex.pOpcyclesIso_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (CategoryTheory.CategoryStruct.comp (K.pOpcyclesIso i j hi h✝).inv h) = h

@[simp]

theorem HomologicalComplex.pOpcyclesIso_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.pOpcyclesIso i j hi h).inv (K.pOpcycles j) = CategoryTheory.CategoryStruct.id (K.opcycles j)

@[simp]

theorem HomologicalComplex.pOpcyclesIso_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] {Z : C} (h : K.opcycles j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.pOpcyclesIso i j hi h✝).inv (CategoryTheory.CategoryStruct.comp (K.pOpcycles j) h) = h

theorem HomologicalComplex.isIso_homologyπ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] : CategoryTheory.IsIso (K.homologyπ j)

noncomputable def HomologicalComplex.isoHomologyπ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] : K.cycles j ≅ K.homology j

The canonical isomorphism K.cycles j ≅ K.homology j when the differential to j is zero.

Equations

• K.isoHomologyπ i j hi h = CategoryTheory.asIso (K.homologyπ j)

@[simp]

theorem HomologicalComplex.isoHomologyπ_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] : (K.isoHomologyπ i j hi h).hom = K.homologyπ j

@[simp]

theorem HomologicalComplex.isoHomologyπ_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.homologyπ j) (K.isoHomologyπ i j hi h).inv = CategoryTheory.CategoryStruct.id (K.cycles j)

@[simp]

theorem HomologicalComplex.isoHomologyπ_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] {Z : C} (h : K.cycles j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.homologyπ j) (CategoryTheory.CategoryStruct.comp (K.isoHomologyπ i j hi h✝).inv h) = h

@[simp]

theorem HomologicalComplex.isoHomologyπ_inv_hom_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] : CategoryTheory.CategoryStruct.comp (K.isoHomologyπ i j hi h).inv (K.homologyπ j) = CategoryTheory.CategoryStruct.id (K.homology j)

@[simp]

theorem HomologicalComplex.isoHomologyπ_inv_hom_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (hi : c.prev j = i) (h : K.d i j = 0) [K.HasHomology j] {Z : C} (h : K.homology j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.isoHomologyπ i j hi h✝).inv (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h) = h

theorem HomologicalComplex.epi_homologyMap_of_epi_of_not_rel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [CategoryTheory.Epi (φ.f i)] (hi : ∀ (j : ι), ¬c.Rel i j) : CategoryTheory.Epi (HomologicalComplex.homologyMap φ i)

theorem HomologicalComplex.mono_homologyMap_of_mono_of_not_rel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (j : ι) [K.HasHomology j] [L.HasHomology j] [CategoryTheory.Mono (φ.f j)] (hj : ∀ (i : ι), ¬c.Rel i j) : CategoryTheory.Mono (HomologicalComplex.homologyMap φ j)

def HomologicalComplex.ExactAt {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) : Prop

A homological complex K is exact at i if the short complex K.sc i is exact.

Equations

• K.ExactAt i = (K.sc i).Exact

theorem HomologicalComplex.exactAt_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) : K.ExactAt i ↔ (K.sc i).Exact

theorem HomologicalComplex.ExactAt.of_iso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {i : ι} (hK : K.ExactAt i) {L : HomologicalComplex C c} (e : K ≅ L) : L.ExactAt i

theorem HomologicalComplex.exactAt_iff' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) : K.ExactAt j ↔ (K.sc' i j k).Exact

theorem HomologicalComplex.exactAt_iff_isZero_homology {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [K.HasHomology i] : K.ExactAt i ↔ CategoryTheory.Limits.IsZero (K.homology i)

instance ChainComplex.isIso_homologyι₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : ChainComplex C ℕ) [HomologicalComplex.HasHomology K 0] : CategoryTheory.IsIso (HomologicalComplex.homologyι K 0)

Equations

• ⋯ = ⋯

@[reducible, inline]

noncomputable abbrev ChainComplex.isoHomologyι₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : ChainComplex C ℕ) [HomologicalComplex.HasHomology K 0] : HomologicalComplex.homology K 0 ≅ HomologicalComplex.opcycles K 0

The canonical isomorphism K.homology 0 ≅ K.opcycles 0 for a chain complex K indexed by ℕ.

Equations

• K.isoHomologyι₀ = HomologicalComplex.isoHomologyι K 0 ((ComplexShape.down ℕ).next 0) ChainComplex.isoHomologyι₀.proof_1 ⋯

@[simp]

theorem ChainComplex.isoHomologyι₀_inv_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : ChainComplex C ℕ} (φ : K ⟶ L) [HomologicalComplex.HasHomology K 0] [HomologicalComplex.HasHomology L 0] : CategoryTheory.CategoryStruct.comp K.isoHomologyι₀.inv (HomologicalComplex.homologyMap φ 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ 0) L.isoHomologyι₀.inv

@[simp]

theorem ChainComplex.isoHomologyι₀_inv_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : ChainComplex C ℕ} {L : ChainComplex C ℕ} (φ : K ⟶ L) [HomologicalComplex.HasHomology K 0] [HomologicalComplex.HasHomology L 0] {Z : C} (h : HomologicalComplex.homology L 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp K.isoHomologyι₀.inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ 0) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ 0) (CategoryTheory.CategoryStruct.comp L.isoHomologyι₀.inv h)

instance CochainComplex.isIso_homologyπ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℕ) [HomologicalComplex.HasHomology K 0] : CategoryTheory.IsIso (HomologicalComplex.homologyπ K 0)

Equations

• ⋯ = ⋯

@[reducible, inline]

noncomputable abbrev CochainComplex.isoHomologyπ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℕ) [HomologicalComplex.HasHomology K 0] : HomologicalComplex.cycles K 0 ≅ HomologicalComplex.homology K 0

The canonical isomorphism K.cycles 0 ≅ K.homology 0 for a cochain complex K indexed by ℕ.

Equations

• K.isoHomologyπ₀ = HomologicalComplex.isoHomologyπ K ((ComplexShape.up ℕ).prev 0) 0 CochainComplex.isoHomologyπ₀.proof_1 ⋯

@[simp]

theorem CochainComplex.isoHomologyπ₀_inv_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : CochainComplex C ℕ} {L : CochainComplex C ℕ} (φ : K ⟶ L) [HomologicalComplex.HasHomology K 0] [HomologicalComplex.HasHomology L 0] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ 0) L.isoHomologyπ₀.inv = CategoryTheory.CategoryStruct.comp K.isoHomologyπ₀.inv (HomologicalComplex.cyclesMap φ 0)

@[simp]

theorem CochainComplex.isoHomologyπ₀_inv_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : CochainComplex C ℕ} {L : CochainComplex C ℕ} (φ : K ⟶ L) [HomologicalComplex.HasHomology K 0] [HomologicalComplex.HasHomology L 0] {Z : C} (h : HomologicalComplex.cycles L 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ 0) (CategoryTheory.CategoryStruct.comp L.isoHomologyπ₀.inv h) = CategoryTheory.CategoryStruct.comp K.isoHomologyπ₀.inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ 0) h)

@[simp]

theorem HomologicalComplex.homologyMap_neg {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : HomologicalComplex.homologyMap (-φ) i = -HomologicalComplex.homologyMap φ i

@[simp]

theorem HomologicalComplex.homologyMap_add {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (ψ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : HomologicalComplex.homologyMap (φ + ψ) i = HomologicalComplex.homologyMap φ i + HomologicalComplex.homologyMap ψ i

@[simp]

theorem HomologicalComplex.homologyMap_sub {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (φ : K ⟶ L) (ψ : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] : HomologicalComplex.homologyMap (φ - ψ) i = HomologicalComplex.homologyMap φ i - HomologicalComplex.homologyMap ψ i

instance HomologicalComplex.instAdditiveHomologyFunctor {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} (i : ι) [CategoryTheory.CategoryWithHomology C] : (HomologicalComplex.homologyFunctor C c i).Additive

Equations

• ⋯ = ⋯

theorem CochainComplex.isIso_liftCycles_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (K : CochainComplex C ℕ) {X : C} (φ : X ⟶ K.X 0) [HomologicalComplex.HasHomology K 0] (hφ : CategoryTheory.CategoryStruct.comp φ (K.d 0 1) = 0) : CategoryTheory.IsIso (HomologicalComplex.liftCycles K φ 1 ⋯ hφ) ↔ (CategoryTheory.ShortComplex.mk φ (K.d 0 1) hφ).Exact ∧ CategoryTheory.Mono φ

theorem ChainComplex.isIso_descOpcycles_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (K : ChainComplex C ℕ) {X : C} (φ : K.X 0 ⟶ X) [HomologicalComplex.HasHomology K 0] (hφ : CategoryTheory.CategoryStruct.comp (K.d 1 0) φ = 0) : CategoryTheory.IsIso (HomologicalComplex.descOpcycles K φ 1 ⋯ hφ) ↔ (CategoryTheory.ShortComplex.mk (K.d 1 0) φ hφ).Exact ∧ CategoryTheory.Epi φ

noncomputable def HomologicalComplex.cyclesIsoSc' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : K.cycles j ≅ (K.sc' i j k).cycles

The cycles of a homological complex in degree j can be computed by specifying a choice of c.prev j and c.next j.

Equations

• K.cyclesIsoSc' i j k hi hk = CategoryTheory.ShortComplex.cyclesMapIso (K.isoSc' i j k hi hk)

@[simp]

theorem HomologicalComplex.cyclesIsoSc'_hom_iCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom (K.sc' i j k).iCycles = K.iCycles j

@[simp]

theorem HomologicalComplex.cyclesIsoSc'_hom_iCycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom (CategoryTheory.CategoryStruct.comp (K.sc' i j k).iCycles h) = CategoryTheory.CategoryStruct.comp (K.iCycles j) h

@[simp]

theorem HomologicalComplex.cyclesIsoSc'_inv_iCycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv (K.iCycles j) = (K.sc' i j k).iCycles

@[simp]

theorem HomologicalComplex.cyclesIsoSc'_inv_iCycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (K.iCycles j) h) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).iCycles h

@[simp]

theorem HomologicalComplex.toCycles_cyclesIsoSc'_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : CategoryTheory.CategoryStruct.comp (K.toCycles i j) (K.cyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).toCycles

@[simp]

theorem HomologicalComplex.toCycles_cyclesIsoSc'_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).cycles ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.toCycles i j) (CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom h) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).toCycles h

noncomputable def HomologicalComplex.opcyclesIsoSc' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : K.opcycles j ≅ (K.sc' i j k).opcycles

The homology of a homological complex in degree j can be computed by specifying a choice of c.prev j and c.next j.

Equations

• K.opcyclesIsoSc' i j k hi hk = CategoryTheory.ShortComplex.opcyclesMapIso (K.isoSc' i j k hi hk)

@[simp]

theorem HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : CategoryTheory.CategoryStruct.comp (K.sc' i j k).pOpcycles (K.opcyclesIsoSc' i j k hi hk).inv = K.pOpcycles j

@[simp]

theorem HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : K.opcycles j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.sc' i j k).pOpcycles (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv h) = CategoryTheory.CategoryStruct.comp (K.pOpcycles j) h

@[simp]

theorem HomologicalComplex.pOpcycles_opcyclesIsoSc'_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (K.opcyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).pOpcycles

@[simp]

theorem HomologicalComplex.pOpcycles_opcyclesIsoSc'_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).opcycles ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.pOpcycles j) (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).hom h) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).pOpcycles h

@[simp]

theorem HomologicalComplex.opcyclesIsoSc'_inv_fromOpcycles {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv (K.fromOpcycles j k) = (K.sc' i j k).fromOpcycles

@[simp]

theorem HomologicalComplex.opcyclesIsoSc'_inv_fromOpcycles_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : K.X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (K.fromOpcycles j k) h) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).fromOpcycles h

noncomputable def HomologicalComplex.homologyIsoSc' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : K.homology j ≅ (K.sc' i j k).homology

The opcycles of a homological complex in degree j can be computed by specifying a choice of c.prev j and c.next j.

Equations

• K.homologyIsoSc' i j k hi hk = CategoryTheory.ShortComplex.homologyMapIso (K.isoSc' i j k hi hk)

@[simp]

theorem HomologicalComplex.π_homologyIsoSc'_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : CategoryTheory.CategoryStruct.comp (K.homologyπ j) (K.homologyIsoSc' i j k hi hk).hom = CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom (K.sc' i j k).homologyπ

@[simp]

theorem HomologicalComplex.π_homologyIsoSc'_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).homology ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.homologyπ j) (CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).hom h) = CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).hom (CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyπ h)

@[simp]

theorem HomologicalComplex.π_homologyIsoSc'_inv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyπ (K.homologyIsoSc' i j k hi hk).inv = CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv (K.homologyπ j)

@[simp]

theorem HomologicalComplex.π_homologyIsoSc'_inv_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : K.homology j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyπ (CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).inv h) = CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h)

@[simp]

theorem HomologicalComplex.homologyIsoSc'_hom_ι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).hom (K.sc' i j k).homologyι = CategoryTheory.CategoryStruct.comp (K.homologyι j) (K.opcyclesIsoSc' i j k hi hk).hom

@[simp]

theorem HomologicalComplex.homologyIsoSc'_hom_ι_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).opcycles ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).hom (CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyι h) = CategoryTheory.CategoryStruct.comp (K.homologyι j) (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).hom h)

@[simp]

theorem HomologicalComplex.homologyIsoSc'_inv_ι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] : CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).inv (K.homologyι j) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyι (K.opcyclesIsoSc' i j k hi hk).inv

@[simp]

theorem HomologicalComplex.homologyIsoSc'_inv_ι_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) (j : ι) (k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [(K.sc' i j k).HasHomology] {Z : C} (h : K.opcycles j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (K.homologyι j) h) = CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyι (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv h)