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.

@[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).toPrefunctor.obj K).X₂ = K.X j

@[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).toPrefunctor.map f).τ₁ = f.f 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 : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor' C c i j k).toPrefunctor.obj K).g = K.d j 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).toPrefunctor.map f).τ₃ = f.f k

@[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).toPrefunctor.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).toPrefunctor.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 : ι) (j : ι) (k : ι) (K : HomologicalComplex C c) : ((HomologicalComplex.shortComplexFunctor' C c i j k).toPrefunctor.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).toPrefunctor.map f).τ₂ = f.f j

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_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).toPrefunctor.obj K).X₁ = K.X (ComplexShape.prev c 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).toPrefunctor.obj K).X₃ = K.X (ComplexShape.next c 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).toPrefunctor.obj K).f = K.d (ComplexShape.prev c i) 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).toPrefunctor.obj K).g = K.d i (ComplexShape.next c 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).toPrefunctor.map f).τ₂ = f.f 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).toPrefunctor.map f).τ₁ = f.f (ComplexShape.prev c 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).toPrefunctor.map f).τ₃ = f.f (ComplexShape.next c 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).toPrefunctor.obj K).X₂ = K.X i

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 (ComplexShape.prev c i) i (ComplexShape.next c i)

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) (X : HomologicalComplex C c) : ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₁ = (HomologicalComplex.XIsoOfEq X hi).hom

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) (X : HomologicalComplex C c) : ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₃ = (HomologicalComplex.XIsoOfEq X hk).inv

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) (X : HomologicalComplex C c) : ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₁ = (HomologicalComplex.XIsoOfEq X 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c 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'_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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) (X : HomologicalComplex C c) : ((HomologicalComplex.natIsoSc' C c i j k hi hk).hom.app X).τ₃ = (HomologicalComplex.XIsoOfEq X hk).hom

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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c 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.

@[inline, reducible]

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

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

@[inline, reducible]

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

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

@[inline, reducible]

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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) : HomologicalComplex.sc K j ≅ HomologicalComplex.sc' K 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

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

@[inline, reducible]

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

• HomologicalComplex.HasHomology K i = CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc K i)

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 : ι) [HomologicalComplex.HasHomology K i] : C

The homology in degree i of a homological complex.

Equations

• HomologicalComplex.homology K i = CategoryTheory.ShortComplex.homology (HomologicalComplex.sc K i)

noncomputable def HomologicalComplex.homology'IsoHomology {ι : Type u_2} {c : ComplexShape ι} {A : Type u_3} [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (K : HomologicalComplex A c) (i : ι) : HomologicalComplex.homology' K i ≅ HomologicalComplex.homology K i

Comparison isomorphism between the homology for the two homology API.

Equations

• HomologicalComplex.homology'IsoHomology K i = CategoryTheory.ShortComplex.homology'IsoHomology (HomologicalComplex.sc K i)

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 : ι) [HomologicalComplex.HasHomology K i] : C

The cycles in degree i of a homological complex.

Equations

• HomologicalComplex.cycles K i = CategoryTheory.ShortComplex.cycles (HomologicalComplex.sc K i)

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 : ι) [HomologicalComplex.HasHomology K i] : HomologicalComplex.cycles K i ⟶ K.X i

The inclusion of the cycles of a homological complex.

Equations

• HomologicalComplex.iCycles K i = CategoryTheory.ShortComplex.iCycles (HomologicalComplex.sc K i)

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 : ι) [HomologicalComplex.HasHomology K i] : HomologicalComplex.cycles K i ⟶ HomologicalComplex.homology K i

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

Equations

• HomologicalComplex.homologyπ K i = CategoryTheory.ShortComplex.homologyπ (HomologicalComplex.sc K i)

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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : ComplexShape.next c i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) : A ⟶ HomologicalComplex.cycles K 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

• HomologicalComplex.liftCycles K k j hj hk = CategoryTheory.ShortComplex.liftCycles (HomologicalComplex.sc K i) k (_ : CategoryTheory.CategoryStruct.comp k (HomologicalComplex.sc K i).g = 0)

@[reducible]

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 : ι} [HomologicalComplex.HasHomology K 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 ⟶ HomologicalComplex.cycles K 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

• HomologicalComplex.liftCycles' K k j hj hk = HomologicalComplex.liftCycles K k j (_ : ComplexShape.next c i = j) hk

@[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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : ComplexShape.next c i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) {Z : C} (h : K.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K k j hj hk) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) h) = CategoryTheory.CategoryStruct.comp k h

@[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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : ComplexShape.next c i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K k j hj hk) (HomologicalComplex.iCycles K i) = k

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 : ι) [HomologicalComplex.HasHomology K j] : K.X i ⟶ HomologicalComplex.cycles K j

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

Equations

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

@[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 : ι) [HomologicalComplex.HasHomology K i] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) (CategoryTheory.CategoryStruct.comp (K.d i j) h) = CategoryTheory.CategoryStruct.comp 0 h

@[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 : ι) [HomologicalComplex.HasHomology K i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) (K.d i j) = 0

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 : ι) [HomologicalComplex.HasHomology K i] (hj : ComplexShape.next c i = j) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (HomologicalComplex.iCycles K i) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) (K.d i j) = 0))

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

Equations

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

@[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 : ι) [HomologicalComplex.HasHomology K j] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.toCycles K i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K j) h) = CategoryTheory.CategoryStruct.comp (K.d i j) h

@[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 : ι) [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.toCycles K i j) (HomologicalComplex.iCycles K j) = K.d i j

instance HomologicalComplex.instMonoCyclesXICycles {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 : ι) [HomologicalComplex.HasHomology K i] : CategoryTheory.Mono (HomologicalComplex.iCycles K i)

Equations

• (_ : CategoryTheory.Mono (HomologicalComplex.iCycles K i)) = (_ : CategoryTheory.Mono (HomologicalComplex.iCycles K i))

instance HomologicalComplex.instEpiCyclesHomologyHomologyπ {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 : ι) [HomologicalComplex.HasHomology K i] : CategoryTheory.Epi (HomologicalComplex.homologyπ K i)

Equations

• (_ : CategoryTheory.Epi (HomologicalComplex.homologyπ K i)) = (_ : CategoryTheory.Epi (HomologicalComplex.homologyπ K i))

@[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 : ι) [HomologicalComplex.HasHomology K k] {Z : C} (h : HomologicalComplex.cycles K k ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.toCycles K j k) h) = CategoryTheory.CategoryStruct.comp 0 h

@[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 : ι) [HomologicalComplex.HasHomology K k] : CategoryTheory.CategoryStruct.comp (K.d i j) (HomologicalComplex.toCycles K j k) = 0

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 : ι} [HomologicalComplex.HasHomology K i] {A' : C} {A : C} (k : A ⟶ K.X i) (j : ι) (hj : ComplexShape.next c i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (α : A' ⟶ A) {Z : C} (h : HomologicalComplex.cycles K i ⟶ Z) : CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K k j hj hk) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K (CategoryTheory.CategoryStruct.comp α k) j hj (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α k) (K.d i j) = 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 : ι} [HomologicalComplex.HasHomology K i] {A' : C} {A : C} (k : A ⟶ K.X i) (j : ι) (hj : ComplexShape.next c i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (α : A' ⟶ A) : CategoryTheory.CategoryStruct.comp α (HomologicalComplex.liftCycles K k j hj hk) = HomologicalComplex.liftCycles K (CategoryTheory.CategoryStruct.comp α k) j hj (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α k) (K.d i j) = 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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : ComplexShape.next c i = j) {i' : ι} (x : A ⟶ K.X i') (hx : k = CategoryTheory.CategoryStruct.comp x (K.d i' i)) {Z : C} (h : HomologicalComplex.homology K i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K k j hj (_ : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i) h) = CategoryTheory.CategoryStruct.comp 0 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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : ComplexShape.next c i = j) {i' : ι} (x : A ⟶ K.X i') (hx : k = CategoryTheory.CategoryStruct.comp x (K.d i' i)) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K k j hj (_ : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0)) (HomologicalComplex.homologyπ K i) = 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 : ι) [HomologicalComplex.HasHomology K j] {Z : C} (h : HomologicalComplex.homology K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.toCycles K i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K j) 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 : ι) [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.toCycles K i j) (HomologicalComplex.homologyπ K j) = 0

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 : ι) [HomologicalComplex.HasHomology K i] (hi : ComplexShape.prev c j = i) [HomologicalComplex.HasHomology K j] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (HomologicalComplex.homologyπ K j) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.toCycles K i j) (HomologicalComplex.homologyπ K j) = 0))

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

Equations

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

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 : ι) [HomologicalComplex.HasHomology K i] : C

The opcycles in degree i of a homological complex.

Equations

• HomologicalComplex.opcycles K i = CategoryTheory.ShortComplex.opcycles (HomologicalComplex.sc K i)

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 : ι) [HomologicalComplex.HasHomology K i] : K.X i ⟶ HomologicalComplex.opcycles K i

The projection to the opcycles of a homological complex.

Equations

• HomologicalComplex.pOpcycles K i = CategoryTheory.ShortComplex.pOpcycles (HomologicalComplex.sc K i)

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 : ι) [HomologicalComplex.HasHomology K i] : HomologicalComplex.homology K i ⟶ HomologicalComplex.opcycles K i

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

Equations

• HomologicalComplex.homologyι K i = CategoryTheory.ShortComplex.homologyι (HomologicalComplex.sc K i)

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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : ComplexShape.prev c i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) : HomologicalComplex.opcycles K 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

• HomologicalComplex.descOpcycles K k j hj hk = CategoryTheory.ShortComplex.descOpcycles (HomologicalComplex.sc K i) k (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.sc K i).f k = 0)

@[reducible]

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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : c.Rel j i) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) : HomologicalComplex.opcycles K 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

• HomologicalComplex.descOpcycles' K k j hj hk = HomologicalComplex.descOpcycles K k j (_ : ComplexShape.prev c i = j) hk

@[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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : ComplexShape.prev c i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.descOpcycles K k j hj hk) h) = CategoryTheory.CategoryStruct.comp k h

@[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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : ComplexShape.prev c i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (HomologicalComplex.descOpcycles K k j hj hk) = k

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 : ι) [HomologicalComplex.HasHomology K i] : HomologicalComplex.opcycles K i ⟶ K.X j

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

Equations

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

@[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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] {Z : C} (h : HomologicalComplex.opcycles K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K j) h) = CategoryTheory.CategoryStruct.comp 0 h

@[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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (K.d i j) (HomologicalComplex.pOpcycles K j) = 0

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 : ι) [HomologicalComplex.HasHomology K i] (hi : ComplexShape.prev c j = i) [HomologicalComplex.HasHomology K j] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (HomologicalComplex.pOpcycles K j) (_ : CategoryTheory.CategoryStruct.comp (K.d i j) (HomologicalComplex.pOpcycles K j) = 0))

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_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 : ι) [HomologicalComplex.HasHomology K i] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.fromOpcycles K i j) h) = CategoryTheory.CategoryStruct.comp (K.d i j) h

@[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 : ι) [HomologicalComplex.HasHomology K i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (HomologicalComplex.fromOpcycles K i j) = K.d i j

instance HomologicalComplex.instEpiXOpcyclesPOpcycles {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 : ι) [HomologicalComplex.HasHomology K i] : CategoryTheory.Epi (HomologicalComplex.pOpcycles K i)

Equations

• (_ : CategoryTheory.Epi (HomologicalComplex.pOpcycles K i)) = (_ : CategoryTheory.Epi (HomologicalComplex.pOpcycles K i))

instance HomologicalComplex.instMonoHomologyOpcyclesHomologyι {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 : ι) [HomologicalComplex.HasHomology K i] : CategoryTheory.Mono (HomologicalComplex.homologyι K i)

Equations

• (_ : CategoryTheory.Mono (HomologicalComplex.homologyι K i)) = (_ : CategoryTheory.Mono (HomologicalComplex.homologyι K i))

@[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 : ι) [HomologicalComplex.HasHomology K i] {Z : C} (h : K.X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.fromOpcycles K i j) (CategoryTheory.CategoryStruct.comp (K.d j k) h) = CategoryTheory.CategoryStruct.comp 0 h

@[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 : ι) [HomologicalComplex.HasHomology K i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.fromOpcycles K i j) (K.d j k) = 0

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 : ι} [HomologicalComplex.HasHomology K i] {A : C} {A' : C} (k : K.X i ⟶ A) (j : ι) (hj : ComplexShape.prev c i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) (α : A ⟶ A') {Z : C} (h : A' ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.descOpcycles K k j hj hk) (CategoryTheory.CategoryStruct.comp α h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.descOpcycles K (CategoryTheory.CategoryStruct.comp k α) j hj (_ : CategoryTheory.CategoryStruct.comp (K.d j i) (CategoryTheory.CategoryStruct.comp k α) = 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 : ι} [HomologicalComplex.HasHomology K i] {A : C} {A' : C} (k : K.X i ⟶ A) (j : ι) (hj : ComplexShape.prev c i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) (α : A ⟶ A') : CategoryTheory.CategoryStruct.comp (HomologicalComplex.descOpcycles K k j hj hk) α = HomologicalComplex.descOpcycles K (CategoryTheory.CategoryStruct.comp k α) j hj (_ : CategoryTheory.CategoryStruct.comp (K.d j i) (CategoryTheory.CategoryStruct.comp k α) = 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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : ComplexShape.prev c 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 (HomologicalComplex.homologyι K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.descOpcycles K k j hj (_ : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0)) h) = CategoryTheory.CategoryStruct.comp 0 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 : ι} [HomologicalComplex.HasHomology K i] {A : C} (k : K.X i ⟶ A) (j : ι) (hj : ComplexShape.prev c i = j) {i' : ι} (x : K.X i' ⟶ A) (hx : k = CategoryTheory.CategoryStruct.comp (K.d i i') x) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (HomologicalComplex.descOpcycles K k j hj (_ : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0)) = 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 : ι) [HomologicalComplex.HasHomology K i] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.fromOpcycles K i j) 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 : ι) [HomologicalComplex.HasHomology K i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (HomologicalComplex.fromOpcycles K i j) = 0

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 : ι) [HomologicalComplex.HasHomology K i] (hi : ComplexShape.next c i = j) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (HomologicalComplex.homologyι K i) (_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (HomologicalComplex.fromOpcycles K i j) = 0))

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

Equations

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

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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] : HomologicalComplex.homology K i ⟶ HomologicalComplex.homology L 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).toPrefunctor.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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] : HomologicalComplex.cycles K i ⟶ HomologicalComplex.cycles L 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).toPrefunctor.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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] : HomologicalComplex.opcycles K i ⟶ HomologicalComplex.opcycles L 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).toPrefunctor.map φ)

@[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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] {Z : C} (h : L.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles L i) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) (CategoryTheory.CategoryStruct.comp (φ.f i) h)

@[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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (HomologicalComplex.iCycles L i) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) (φ.f 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] {Z : C} (h : HomologicalComplex.opcycles L i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) h) = CategoryTheory.CategoryStruct.comp (φ.f i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles L 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (HomologicalComplex.opcyclesMap φ i) = CategoryTheory.CategoryStruct.comp (φ.f i) (HomologicalComplex.pOpcycles L i)

instance HomologicalComplex.instMonoCyclesCyclesMap {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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] [CategoryTheory.Mono (φ.f i)] : CategoryTheory.Mono (HomologicalComplex.cyclesMap φ i)

Equations

• (_ : CategoryTheory.Mono (HomologicalComplex.cyclesMap φ i)) = (_ : CategoryTheory.Mono (HomologicalComplex.cyclesMap φ i))

instance HomologicalComplex.instEpiOpcyclesOpcyclesMap {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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] [CategoryTheory.Epi (φ.f i)] : CategoryTheory.Epi (HomologicalComplex.opcyclesMap φ i)

Equations

• (_ : CategoryTheory.Epi (HomologicalComplex.opcyclesMap φ i)) = (_ : CategoryTheory.Epi (HomologicalComplex.opcyclesMap φ i))

@[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 : ι) [HomologicalComplex.HasHomology K i] : HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.id K) i = CategoryTheory.CategoryStruct.id (HomologicalComplex.homology K 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 : ι) [HomologicalComplex.HasHomology K i] : HomologicalComplex.cyclesMap (CategoryTheory.CategoryStruct.id K) i = CategoryTheory.CategoryStruct.id (HomologicalComplex.cycles K 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 : ι) [HomologicalComplex.HasHomology K i] : HomologicalComplex.opcyclesMap (CategoryTheory.CategoryStruct.id K) i = CategoryTheory.CategoryStruct.id (HomologicalComplex.opcycles K 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] [HomologicalComplex.HasHomology M i] {Z : C} (h : HomologicalComplex.homology M 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.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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] [HomologicalComplex.HasHomology M i] : HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.comp φ ψ) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (HomologicalComplex.homologyMap ψ 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] [HomologicalComplex.HasHomology M i] {Z : C} (h : HomologicalComplex.cycles M 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.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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] [HomologicalComplex.HasHomology M i] : HomologicalComplex.cyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (HomologicalComplex.cyclesMap ψ 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] [HomologicalComplex.HasHomology M i] {Z : C} (h : HomologicalComplex.opcycles M 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)

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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] [HomologicalComplex.HasHomology M i] : HomologicalComplex.opcyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (HomologicalComplex.opcyclesMap ψ i)

@[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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] : HomologicalComplex.opcyclesMap 0 i = 0

@[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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] {Z : C} (h : HomologicalComplex.homology L i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ L 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i) (HomologicalComplex.homologyMap φ i) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (HomologicalComplex.homologyπ L 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] {Z : C} (h : HomologicalComplex.opcycles L i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι L i) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (HomologicalComplex.homologyι L i) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (HomologicalComplex.opcyclesMap φ 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 : ι) [HomologicalComplex.HasHomology K i] {Z : C} (h : HomologicalComplex.opcycles K i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K 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 : ι) [HomologicalComplex.HasHomology K i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i) (HomologicalComplex.homologyι K i) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) (HomologicalComplex.pOpcycles K i)

@[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 : ι} [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] {A : C} (k : L.X i ⟶ A) (j : ι) (hj : ComplexShape.prev c 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 (HomologicalComplex.descOpcycles L k j hj hk) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.descOpcycles K (CategoryTheory.CategoryStruct.comp (φ.f i) k) j hj (_ : CategoryTheory.CategoryStruct.comp (K.d j i) (CategoryTheory.CategoryStruct.comp (φ.f i) k) = 0)) 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 : ι} [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] {A : C} (k : L.X i ⟶ A) (j : ι) (hj : ComplexShape.prev c i = j) (hk : CategoryTheory.CategoryStruct.comp (L.d j i) k = 0) (φ : K ⟶ L) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i) (HomologicalComplex.descOpcycles L k j hj hk) = HomologicalComplex.descOpcycles K (CategoryTheory.CategoryStruct.comp (φ.f i) k) j hj (_ : CategoryTheory.CategoryStruct.comp (K.d j i) (CategoryTheory.CategoryStruct.comp (φ.f i) k) = 0)

@[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 : ι} [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : ComplexShape.next c i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (φ : K ⟶ L) {Z : C} (h : HomologicalComplex.cycles L i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K k j hj hk) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles L (CategoryTheory.CategoryStruct.comp k (φ.f i)) j hj (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp k (φ.f i)) (L.d i j) = 0)) 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 : ι} [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] {A : C} (k : A ⟶ K.X i) (j : ι) (hj : ComplexShape.next c i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (φ : K ⟶ L) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K k j hj hk) (HomologicalComplex.cyclesMap φ i) = HomologicalComplex.liftCycles L (CategoryTheory.CategoryStruct.comp k (φ.f i)) j hj (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp k (φ.f i)) (L.d i j) = 0)

@[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).toPrefunctor.obj K = HomologicalComplex.homology K 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).toPrefunctor.map f = HomologicalComplex.homologyMap f i

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.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).toPrefunctor.obj K i = HomologicalComplex.homology K 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).toPrefunctor.map f i = 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.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).toPrefunctor.obj K = HomologicalComplex.cycles K i

@[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).toPrefunctor.map f = HomologicalComplex.cyclesMap 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.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).toPrefunctor.map f = HomologicalComplex.opcyclesMap f i

@[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).toPrefunctor.obj K = HomologicalComplex.opcycles K 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.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 = HomologicalComplex.homologyπ K 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 = CategoryTheory.NatTrans.mk fun (K : HomologicalComplex C c) => HomologicalComplex.homologyπ K i

@[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 = HomologicalComplex.homologyι K 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 = CategoryTheory.NatTrans.mk fun (K : HomologicalComplex C c) => HomologicalComplex.homologyι K 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 (HomologicalComplex.homology X 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 (HomologicalComplex.homology X 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 ≅ CategoryTheory.Functor.comp (HomologicalComplex.shortComplexFunctor C c i) (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)

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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) : HomologicalComplex.homologyFunctor C c j ≅ CategoryTheory.Functor.comp (HomologicalComplex.shortComplexFunctor' C c i j k) (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.instPreservesZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexInstHasZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexHomologyFunctor (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.PreservesZeroMorphisms (HomologicalComplex.homologyFunctor C c i)

Equations

• (_ : CategoryTheory.Functor.PreservesZeroMorphisms (HomologicalComplex.homologyFunctor C c i)) = (_ : CategoryTheory.Functor.PreservesZeroMorphisms (HomologicalComplex.homologyFunctor C c i))

instance HomologicalComplex.instPreservesZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexInstHasZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexOpcyclesFunctor (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.PreservesZeroMorphisms (HomologicalComplex.opcyclesFunctor C c i)

Equations

• (_ : CategoryTheory.Functor.PreservesZeroMorphisms (HomologicalComplex.opcyclesFunctor C c i)) = (_ : CategoryTheory.Functor.PreservesZeroMorphisms (HomologicalComplex.opcyclesFunctor C c i))

instance HomologicalComplex.instPreservesZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexInstHasZeroMorphismsHomologicalComplexInstCategoryHomologicalComplexCyclesFunctor (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.PreservesZeroMorphisms (HomologicalComplex.cyclesFunctor C c i)

Equations

• (_ : CategoryTheory.Functor.PreservesZeroMorphisms (HomologicalComplex.cyclesFunctor C c i)) = (_ : CategoryTheory.Functor.PreservesZeroMorphisms (HomologicalComplex.cyclesFunctor C c i))

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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] : CategoryTheory.IsIso (HomologicalComplex.iCycles K 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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] : (HomologicalComplex.iCyclesIso K i j hj h).hom = HomologicalComplex.iCycles K 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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] : HomologicalComplex.cycles K i ≅ K.X i

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

Equations

• HomologicalComplex.iCyclesIso K i j hj h = let_fun this := (_ : CategoryTheory.IsIso (HomologicalComplex.iCycles K i)); CategoryTheory.asIso (HomologicalComplex.iCycles K 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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] {Z : C} (h : HomologicalComplex.cycles K i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCyclesIso K i j hj h✝).inv h) = h

@[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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) (HomologicalComplex.iCyclesIso K i j hj h).inv = CategoryTheory.CategoryStruct.id (HomologicalComplex.cycles K 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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] {Z : C} (h : K.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCyclesIso K i j hj h✝).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K i) 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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCyclesIso K i j hj h).inv (HomologicalComplex.iCycles K i) = CategoryTheory.CategoryStruct.id (K.X i)

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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] : CategoryTheory.IsIso (HomologicalComplex.homologyι K 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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] : (HomologicalComplex.isoHomologyι K i j hj h).hom = HomologicalComplex.homologyι K 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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] : HomologicalComplex.homology K i ≅ HomologicalComplex.opcycles K i

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

Equations

• HomologicalComplex.isoHomologyι K i j hj h = let_fun this := (_ : CategoryTheory.IsIso (HomologicalComplex.homologyι K i)); CategoryTheory.asIso (HomologicalComplex.homologyι K 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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] {Z : C} (h : HomologicalComplex.homology K i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.isoHomologyι K i j hj h✝).inv h) = h

@[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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) (HomologicalComplex.isoHomologyι K i j hj h).inv = CategoryTheory.CategoryStruct.id (HomologicalComplex.homology K 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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] {Z : C} (h : HomologicalComplex.opcycles K i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.isoHomologyι K i j hj h✝).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K i) 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 : ComplexShape.next c i = j) (h : K.d i j = 0) [HomologicalComplex.HasHomology K i] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.isoHomologyι K i j hj h).inv (HomologicalComplex.homologyι K i) = CategoryTheory.CategoryStruct.id (HomologicalComplex.opcycles K i)

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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] : CategoryTheory.IsIso (HomologicalComplex.pOpcycles K 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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] : (HomologicalComplex.pOpcyclesIso K i j hi h).hom = HomologicalComplex.pOpcycles K 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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] : K.X j ≅ HomologicalComplex.opcycles K j

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

Equations

• HomologicalComplex.pOpcyclesIso K i j hi h = let_fun this := (_ : CategoryTheory.IsIso (HomologicalComplex.pOpcycles K j)); CategoryTheory.asIso (HomologicalComplex.pOpcycles K 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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcyclesIso K i j hi h✝).inv h) = h

@[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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K j) (HomologicalComplex.pOpcyclesIso K i j hi h).inv = CategoryTheory.CategoryStruct.id (K.X 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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] {Z : C} (h : HomologicalComplex.opcycles K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcyclesIso K i j hi h✝).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K j) 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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcyclesIso K i j hi h).inv (HomologicalComplex.pOpcycles K j) = CategoryTheory.CategoryStruct.id (HomologicalComplex.opcycles K j)

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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] : CategoryTheory.IsIso (HomologicalComplex.homologyπ K 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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] : (HomologicalComplex.isoHomologyπ K i j hi h).hom = HomologicalComplex.homologyπ K 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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] : HomologicalComplex.cycles K j ≅ HomologicalComplex.homology K j

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

Equations

• HomologicalComplex.isoHomologyπ K i j hi h = let_fun this := (_ : CategoryTheory.IsIso (HomologicalComplex.homologyπ K j)); CategoryTheory.asIso (HomologicalComplex.homologyπ K 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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] {Z : C} (h : HomologicalComplex.cycles K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.isoHomologyπ K i j hi h✝).inv h) = h

@[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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K j) (HomologicalComplex.isoHomologyπ K i j hi h).inv = CategoryTheory.CategoryStruct.id (HomologicalComplex.cycles K 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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] {Z : C} (h : HomologicalComplex.homology K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.isoHomologyπ K i j hi h✝).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K j) 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 : ComplexShape.prev c j = i) (h : K.d i j = 0) [HomologicalComplex.HasHomology K j] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.isoHomologyπ K i j hi h).inv (HomologicalComplex.homologyπ K j) = CategoryTheory.CategoryStruct.id (HomologicalComplex.homology K 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

• HomologicalComplex.ExactAt K i = CategoryTheory.ShortComplex.Exact (HomologicalComplex.sc K 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 : ι) : HomologicalComplex.ExactAt K i ↔ CategoryTheory.ShortComplex.Exact (HomologicalComplex.sc K 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) : HomologicalComplex.ExactAt K j ↔ CategoryTheory.ShortComplex.Exact (HomologicalComplex.sc' K i j k)

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 : ι) [HomologicalComplex.HasHomology K i] : HomologicalComplex.ExactAt K i ↔ CategoryTheory.Limits.IsZero (HomologicalComplex.homology K 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

• (_ : CategoryTheory.IsIso (HomologicalComplex.homologyι K 0)) = (_ : CategoryTheory.IsIso (HomologicalComplex.homologyι K 0))

@[inline, reducible]

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

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

@[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 (ChainComplex.isoHomologyι₀ K).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ 0) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ 0) (CategoryTheory.CategoryStruct.comp (ChainComplex.isoHomologyι₀ L).inv h)

@[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 (ChainComplex.isoHomologyι₀ K).inv (HomologicalComplex.homologyMap φ 0) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ 0) (ChainComplex.isoHomologyι₀ L).inv

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

• (_ : CategoryTheory.IsIso (HomologicalComplex.homologyπ K 0)) = (_ : CategoryTheory.IsIso (HomologicalComplex.homologyπ K 0))

@[inline, reducible]

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

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

@[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 (CochainComplex.isoHomologyπ₀ L).inv h) = CategoryTheory.CategoryStruct.comp (CochainComplex.isoHomologyπ₀ K).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ 0) h)

@[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) (CochainComplex.isoHomologyπ₀ L).inv = CategoryTheory.CategoryStruct.comp (CochainComplex.isoHomologyπ₀ K).inv (HomologicalComplex.cyclesMap φ 0)

@[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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L 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 : ι) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology L i] : HomologicalComplex.homologyMap (φ - ψ) i = HomologicalComplex.homologyMap φ i - HomologicalComplex.homologyMap ψ i

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

Equations

• (_ : CategoryTheory.Functor.Additive (HomologicalComplex.homologyFunctor C c i)) = (_ : CategoryTheory.Functor.Additive (HomologicalComplex.homologyFunctor C c i))

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 (_ : ComplexShape.next (ComplexShape.up ℕ) 0 = 1) hφ) ↔ CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.mk φ (K.d 0 1) hφ) ∧ 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 (_ : ComplexShape.prev (ComplexShape.down ℕ) 0 = 1) hφ) ↔ CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.mk (K.d 1 0) φ hφ) ∧ 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : HomologicalComplex.cycles K j ≅ CategoryTheory.ShortComplex.cycles (HomologicalComplex.sc' K i j k)

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

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

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] {Z : C} (h : (HomologicalComplex.sc' K i j k).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesIsoSc' K i j k hi hk).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles (HomologicalComplex.sc' K i j k)) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K j) h

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesIsoSc' K i j k hi hk).hom (CategoryTheory.ShortComplex.iCycles (HomologicalComplex.sc' K i j k)) = HomologicalComplex.iCycles K j

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] {Z : C} (h : K.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesIsoSc' K i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles K j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles (HomologicalComplex.sc' K i j k)) 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesIsoSc' K i j k hi hk).inv (HomologicalComplex.iCycles K j) = CategoryTheory.ShortComplex.iCycles (HomologicalComplex.sc' K i j k)

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] {Z : C} (h : CategoryTheory.ShortComplex.cycles (HomologicalComplex.sc' K i j k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.toCycles K i j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesIsoSc' K i j k hi hk).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.toCycles (HomologicalComplex.sc' K i j k)) 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.toCycles K i j) (HomologicalComplex.cyclesIsoSc' K i j k hi hk).hom = CategoryTheory.ShortComplex.toCycles (HomologicalComplex.sc' K i j k)

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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : HomologicalComplex.opcycles K j ≅ CategoryTheory.ShortComplex.opcycles (HomologicalComplex.sc' K i j k)

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

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

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] {Z : C} (h : HomologicalComplex.opcycles K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles (HomologicalComplex.sc' K i j k)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesIsoSc' K i j k hi hk).inv h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K j) h

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles (HomologicalComplex.sc' K i j k)) (HomologicalComplex.opcyclesIsoSc' K i j k hi hk).inv = HomologicalComplex.pOpcycles K j

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] {Z : C} (h : CategoryTheory.ShortComplex.opcycles (HomologicalComplex.sc' K i j k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesIsoSc' K i j k hi hk).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.pOpcycles (HomologicalComplex.sc' K i j k)) 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K j) (HomologicalComplex.opcyclesIsoSc' K i j k hi hk).hom = CategoryTheory.ShortComplex.pOpcycles (HomologicalComplex.sc' K i j k)

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] {Z : C} (h : K.X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesIsoSc' K i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.fromOpcycles K j k) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.fromOpcycles (HomologicalComplex.sc' K i j k)) 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesIsoSc' K i j k hi hk).inv (HomologicalComplex.fromOpcycles K j k) = CategoryTheory.ShortComplex.fromOpcycles (HomologicalComplex.sc' K i j k)

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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : HomologicalComplex.homology K j ≅ CategoryTheory.ShortComplex.homology (HomologicalComplex.sc' K i j k)

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

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

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] {Z : C} (h : CategoryTheory.ShortComplex.homology (HomologicalComplex.sc' K i j k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyIsoSc' K i j k hi hk).hom h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesIsoSc' K i j k hi hk).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ (HomologicalComplex.sc' K i j k)) 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K j) (HomologicalComplex.homologyIsoSc' K i j k hi hk).hom = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesIsoSc' K i j k hi hk).hom (CategoryTheory.ShortComplex.homologyπ (HomologicalComplex.sc' K i j k))

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] {Z : C} (h : HomologicalComplex.homology K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ (HomologicalComplex.sc' K i j k)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyIsoSc' K i j k hi hk).inv h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesIsoSc' K i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K j) 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyπ (HomologicalComplex.sc' K i j k)) (HomologicalComplex.homologyIsoSc' K i j k hi hk).inv = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesIsoSc' K i j k hi hk).inv (HomologicalComplex.homologyπ K j)

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] {Z : C} (h : CategoryTheory.ShortComplex.opcycles (HomologicalComplex.sc' K i j k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyIsoSc' K i j k hi hk).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι (HomologicalComplex.sc' K i j k)) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K j) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesIsoSc' K i j k hi hk).hom 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyIsoSc' K i j k hi hk).hom (CategoryTheory.ShortComplex.homologyι (HomologicalComplex.sc' K i j k)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K j) (HomologicalComplex.opcyclesIsoSc' K i j k hi hk).hom

@[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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] {Z : C} (h : HomologicalComplex.opcycles K j ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyIsoSc' K i j k hi hk).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyι K j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι (HomologicalComplex.sc' K i j k)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesIsoSc' K i j k hi hk).inv 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 : ComplexShape.prev c j = i) (hk : ComplexShape.next c j = k) [HomologicalComplex.HasHomology K j] [CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyIsoSc' K i j k hi hk).inv (HomologicalComplex.homologyι K j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyι (HomologicalComplex.sc' K i j k)) (HomologicalComplex.opcyclesIsoSc' K i j k hi hk).inv