Homological complexes.

A HomologicalComplex V c with a "shape" controlled by c : ComplexShape ι has chain groups X i (objects in V) indexed by i : ι, and a differential d i j whenever c.Rel i j.

We in fact ask for differentials d i j for all i j : ι, but have a field shape requiring that these are zero when not allowed by c. This avoids a lot of dependent type theory hell!

The composite of any two differentials d i j ≫ d j k must be zero.

We provide ChainComplex V α for α-indexed chain complexes in which d i j ≠ 0 only if j + 1 = i, and similarly CochainComplex V α, with i = j + 1.

There is a category structure, where morphisms are chain maps.

For C : HomologicalComplex V c, we define C.xNext i, which is either C.X j for some arbitrarily chosen j such that c.r i j, or C.X i if there is no such j. Similarly we have C.xPrev j. Defined in terms of these we have C.dFrom i : C.X i ⟶ C.xNext i and C.dTo j : C.xPrev j ⟶ C.X j, which are either defined as C.d i j, or zero, as needed.

structure HomologicalComplex {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) : Type (max (max u u_1) v)

A HomologicalComplex V c with a "shape" controlled by c : ComplexShape ι has chain groups X i (objects in V) indexed by i : ι, and a differential d i j whenever c.Rel i j.

We in fact ask for differentials d i j for all i j : ι, but have a field shape requiring that these are zero when not allowed by c. This avoids a lot of dependent type theory hell!

The composite of any two differentials d i j ≫ d j k must be zero.

• X : ι → V
• d (i j : ι) : self.X i ⟶ self.X j
• shape (i j : ι) : ¬c.Rel i j → self.d i j = 0
• d_comp_d' (i j k : ι) : c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (self.d i j) (self.d j k) = 0

@[simp]

theorem HomologicalComplex.d_comp_d {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i j k : ι) : CategoryTheory.CategoryStruct.comp (C.d i j) (C.d j k) = 0

@[simp]

theorem HomologicalComplex.d_comp_d_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i j k : ι) {Z : V} (h : C.X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.d i j) (CategoryTheory.CategoryStruct.comp (C.d j k) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem HomologicalComplex.ext {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (h_X : C₁.X = C₂.X) (h_d : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (C₁.d i j) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (C₂.d i j)) : C₁ = C₂

def HomologicalComplex.XIsoOfEq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p q : ι} (h : p = q) : K.X p ≅ K.X q

The obvious isomorphism K.X p ≅ K.X q when p = q.

@[simp]

theorem HomologicalComplex.XIsoOfEq_rfl {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) (p : ι) : K.XIsoOfEq ⋯ = CategoryTheory.Iso.refl (K.X p)

@[simp]

theorem HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₁₂ : p₁ = p₂) (h₂₃ : p₂ = p₃) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom

@[simp]

theorem HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₁₂ : p₁ = p₂) (h₂₃ : p₂ = p₃) {Z : V} (h : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₃).hom h) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h

@[simp]

theorem HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_inv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₁₂ : p₁ = p₂) (h₃₂ : p₃ = p₂) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom

@[simp]

theorem HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_inv_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₁₂ : p₁ = p₂) (h₃₂ : p₃ = p₂) {Z : V} (h : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₁₂).hom (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₃₂).inv h) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h

@[simp]

theorem HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₂₁ : p₂ = p₁) (h₂₃ : p₂ = p₃) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq ⋯).hom

@[simp]

theorem HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_hom_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₂₁ : p₂ = p₁) (h₂₃ : p₂ = p₃) {Z : V} (h : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₃).hom h) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h

@[simp]

theorem HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_inv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₂₁ : p₂ = p₁) (h₃₂ : p₃ = p₂) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom

@[simp]

theorem HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_inv_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι} (h₂₁ : p₂ = p₁) (h₃₂ : p₃ = p₂) {Z : V} (h : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₃₂).inv h) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h

@[simp]

theorem HomologicalComplex.XIsoOfEq_hom_comp_d {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ : ι} (h : p₁ = p₂) (p₃ : ι) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (K.d p₂ p₃) = K.d p₁ p₃

@[simp]

theorem HomologicalComplex.XIsoOfEq_hom_comp_d_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ : ι} (h : p₁ = p₂) (p₃ : ι) {Z : V} (h✝ : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (CategoryTheory.CategoryStruct.comp (K.d p₂ p₃) h✝) = CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h✝

@[simp]

theorem HomologicalComplex.XIsoOfEq_inv_comp_d {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₁ : ι} (h : p₂ = p₁) (p₃ : ι) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (K.d p₂ p₃) = K.d p₁ p₃

@[simp]

theorem HomologicalComplex.XIsoOfEq_inv_comp_d_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₁ : ι} (h : p₂ = p₁) (p₃ : ι) {Z : V} (h✝ : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (CategoryTheory.CategoryStruct.comp (K.d p₂ p₃) h✝) = CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h✝

@[simp]

theorem HomologicalComplex.d_comp_XIsoOfEq_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₂ = p₃) (p₁ : ι) : CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (K.XIsoOfEq h).hom = K.d p₁ p₃

@[simp]

theorem HomologicalComplex.d_comp_XIsoOfEq_hom_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₂ = p₃) (p₁ : ι) {Z : V} (h✝ : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom h✝) = CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h✝

@[simp]

theorem HomologicalComplex.d_comp_XIsoOfEq_inv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₃ = p₂) (p₁ : ι) : CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (K.XIsoOfEq h).inv = K.d p₁ p₃

@[simp]

theorem HomologicalComplex.d_comp_XIsoOfEq_inv_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₃ = p₂) (p₁ : ι) {Z : V} (h✝ : K.X p₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv h✝) = CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h✝

@[reducible, inline]

abbrev ChainComplex (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (α : Type u_2) [AddRightCancelSemigroup α] [One α] : Type (max (max u_2 u) v)

An α-indexed chain complex is a HomologicalComplex in which d i j ≠ 0 only if j + 1 = i.

@[reducible, inline]

abbrev CochainComplex (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (α : Type u_2) [AddRightCancelSemigroup α] [One α] : Type (max (max u_2 u) v)

An α-indexed cochain complex is a HomologicalComplex in which d i j ≠ 0 only if i + 1 = j.

@[simp]

theorem ChainComplex.prev (α : Type u_2) [AddRightCancelSemigroup α] [One α] (i : α) : (ComplexShape.down α).prev i = i + 1

@[simp]

theorem ChainComplex.next (α : Type u_2) [AddGroup α] [One α] (i : α) : (ComplexShape.down α).next i = i - 1

@[simp]

theorem ChainComplex.next_nat_zero : (ComplexShape.down ℕ).next 0 = 0

@[simp]

theorem ChainComplex.next_nat_succ (i : ℕ) : (ComplexShape.down ℕ).next (i + 1) = i

@[simp]

theorem CochainComplex.prev (α : Type u_2) [AddGroup α] [One α] (i : α) : (ComplexShape.up α).prev i = i - 1

@[simp]

theorem CochainComplex.next (α : Type u_2) [AddRightCancelSemigroup α] [One α] (i : α) : (ComplexShape.up α).next i = i + 1

@[simp]

theorem CochainComplex.prev_nat_zero : (ComplexShape.up ℕ).prev 0 = 0

@[simp]

theorem CochainComplex.prev_nat_succ (i : ℕ) : (ComplexShape.up ℕ).prev (i + 1) = i

structure HomologicalComplex.Hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (A B : HomologicalComplex V c) : Type (max u_1 v)

A morphism of homological complexes consists of maps between the chain groups, commuting with the differentials.

• f (i : ι) : A.X i ⟶ B.X i
• comm' (i j : ι) : c.Rel i j → CategoryTheory.CategoryStruct.comp (self.f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (self.f j)

theorem HomologicalComplex.Hom.ext_iff {ι : Type u_1} {V : Type u} {inst✝ : CategoryTheory.Category.{v, u} V} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms V} {c : ComplexShape ι} {A B : HomologicalComplex V c} {x y : A.Hom B} : x = y ↔ x.f = y.f

theorem HomologicalComplex.Hom.ext {ι : Type u_1} {V : Type u} {inst✝ : CategoryTheory.Category.{v, u} V} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms V} {c : ComplexShape ι} {A B : HomologicalComplex V c} {x y : A.Hom B} (f : x.f = y.f) : x = y

@[simp]

theorem HomologicalComplex.Hom.comm {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c} (f : A.Hom B) (i j : ι) : CategoryTheory.CategoryStruct.comp (f.f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f.f j)

@[simp]

theorem HomologicalComplex.Hom.comm_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c} (f : A.Hom B) (i j : ι) {Z : V} (h : B.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.f i) (CategoryTheory.CategoryStruct.comp (B.d i j) h) = CategoryTheory.CategoryStruct.comp (A.d i j) (CategoryTheory.CategoryStruct.comp (f.f j) h)

@[implicit_reducible]

instance HomologicalComplex.instInhabitedHom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (A B : HomologicalComplex V c) : Inhabited (A.Hom B)

def HomologicalComplex.id {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (A : HomologicalComplex V c) : A.Hom A

Identity chain map.

def HomologicalComplex.comp {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (A B C : HomologicalComplex V c) (φ : A.Hom B) (ψ : B.Hom C) : A.Hom C

Composition of chain maps.

@[implicit_reducible]

instance HomologicalComplex.instCategory {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} : CategoryTheory.Category.{max u_1 v, max (max u_1 u) v} (HomologicalComplex V c)

theorem HomologicalComplex.hom_ext {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D) (h : ∀ (i : ι), f.f i = g.f i) : f = g

theorem HomologicalComplex.hom_ext_iff {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} : f = g ↔ ∀ (i : ι), f.f i = g.f i

@[simp]

theorem HomologicalComplex.id_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i : ι) : (CategoryTheory.CategoryStruct.id C).f i = CategoryTheory.CategoryStruct.id (C.X i)

@[simp]

theorem HomologicalComplex.comp_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) : (CategoryTheory.CategoryStruct.comp f g).f i = CategoryTheory.CategoryStruct.comp (f.f i) (g.f i)

theorem HomologicalComplex.comp_f_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) {Z : V} (h : C₃.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).f i) h = CategoryTheory.CategoryStruct.comp (f.f i) (CategoryTheory.CategoryStruct.comp (g.f i) h)

@[simp]

theorem HomologicalComplex.eqToHom_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (h : C₁ = C₂) (n : ι) : (CategoryTheory.eqToHom h).f n = CategoryTheory.eqToHom ⋯

theorem HomologicalComplex.hom_f_injective {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} : Function.Injective fun (f : C₁.Hom C₂) => f.f

@[implicit_reducible]

instance HomologicalComplex.instZeroHom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (X Y : HomologicalComplex V c) : Zero (X ⟶ Y)

@[simp]

theorem HomologicalComplex.zero_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C D : HomologicalComplex V c) (i : ι) : Hom.f 0 i = 0

@[implicit_reducible]

instance HomologicalComplex.instHasZeroMorphisms {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} : CategoryTheory.Limits.HasZeroMorphisms (HomologicalComplex V c)

noncomputable def HomologicalComplex.zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroObject V] : HomologicalComplex V c

The zero complex

theorem HomologicalComplex.isZero_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Limits.IsZero zero

instance HomologicalComplex.instHasZeroObject {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroObject V] : CategoryTheory.Limits.HasZeroObject (HomologicalComplex V c)

@[implicit_reducible]

noncomputable instance HomologicalComplex.instInhabitedOfHasZeroObject {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroObject V] : Inhabited (HomologicalComplex V c)

theorem HomologicalComplex.congr_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (w : f = g) (i : ι) : f.f i = g.f i

theorem HomologicalComplex.mono_of_mono_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) (hφ : ∀ (i : ι), CategoryTheory.Mono (φ.f i)) : CategoryTheory.Mono φ

theorem HomologicalComplex.epi_of_epi_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) (hφ : ∀ (i : ι), CategoryTheory.Epi (φ.f i)) : CategoryTheory.Epi φ

def HomologicalComplex.eval {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) : CategoryTheory.Functor (HomologicalComplex V c) V

The functor picking out the i-th object of a complex.

@[simp]

theorem HomologicalComplex.eval_obj {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) (C : HomologicalComplex V c) : (eval V c i).obj C = C.X i

@[simp]

theorem HomologicalComplex.eval_map {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) {X✝ Y✝ : HomologicalComplex V c} (f : X✝ ⟶ Y✝) : (eval V c i).map f = f.f i

instance HomologicalComplex.instPreservesZeroMorphismsEval {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) : (eval V c i).PreservesZeroMorphisms

def HomologicalComplex.forget {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) : CategoryTheory.Functor (HomologicalComplex V c) (CategoryTheory.GradedObject ι V)

The functor forgetting the differential in a complex, obtaining a graded object.

@[simp]

theorem HomologicalComplex.forget_obj {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (C : HomologicalComplex V c) (a✝ : ι) : (forget V c).obj C a✝ = C.X a✝

@[simp]

theorem HomologicalComplex.forget_map {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) {X✝ Y✝ : HomologicalComplex V c} (f : X✝ ⟶ Y✝) (i : ι) : (forget V c).map f i = f.f i

instance HomologicalComplex.instFaithfulGradedObjectForget {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) : (forget V c).Faithful

def HomologicalComplex.forgetEval {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) : (forget V c).comp (CategoryTheory.GradedObject.eval i) ≅ eval V c i

Forgetting the differentials than picking out the i-th object is the same as just picking out the i-th object.

@[simp]

theorem HomologicalComplex.forgetEval_hom_app {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) (X : HomologicalComplex V c) : (forgetEval V c i).hom.app X = CategoryTheory.CategoryStruct.id (X.X i)

@[simp]

theorem HomologicalComplex.forgetEval_inv_app {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) (X : HomologicalComplex V c) : (forgetEval V c i).inv.app X = CategoryTheory.CategoryStruct.id (X.X i)

theorem HomologicalComplex.XIsoOfEq_hom_naturality {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') : CategoryTheory.CategoryStruct.comp (φ.f n) (L.XIsoOfEq h).hom = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (φ.f n')

theorem HomologicalComplex.XIsoOfEq_hom_naturality_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') {Z : V} (h✝ : L.X n' ⟶ Z) : CategoryTheory.CategoryStruct.comp (φ.f n) (CategoryTheory.CategoryStruct.comp (L.XIsoOfEq h).hom h✝) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom (CategoryTheory.CategoryStruct.comp (φ.f n') h✝)

theorem HomologicalComplex.XIsoOfEq_inv_naturality {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') : CategoryTheory.CategoryStruct.comp (φ.f n') (L.XIsoOfEq h).inv = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (φ.f n)

theorem HomologicalComplex.XIsoOfEq_inv_naturality_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') {Z : V} (h✝ : L.X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (φ.f n') (CategoryTheory.CategoryStruct.comp (L.XIsoOfEq h).inv h✝) = CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (CategoryTheory.CategoryStruct.comp (φ.f n) h✝)

@[simp]

theorem HomologicalComplex.d_comp_eqToHom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j j' : ι} (rij : c.Rel i j) (rij' : c.Rel i j') : CategoryTheory.CategoryStruct.comp (C.d i j') (CategoryTheory.eqToHom ⋯) = C.d i j

If C.d i j and C.d i j' are both allowed, then we must have j = j', and so the differentials only differ by an eqToHom.

@[simp]

theorem HomologicalComplex.eqToHom_comp_d {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i i' j : ι} (rij : c.Rel i j) (rij' : c.Rel i' j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (C.d i' j) = C.d i j

If C.d i j and C.d i' j are both allowed, then we must have i = i', and so the differentials only differ by an eqToHom.

theorem HomologicalComplex.kernel_eq_kernel {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] {i j j' : ι} (r : c.Rel i j) (r' : c.Rel i j') : CategoryTheory.Limits.kernelSubobject (C.d i j) = CategoryTheory.Limits.kernelSubobject (C.d i j')

theorem HomologicalComplex.image_eq_image {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i i' j : ι} (r : c.Rel i j) (r' : c.Rel i' j) : CategoryTheory.Limits.imageSubobject (C.d i j) = CategoryTheory.Limits.imageSubobject (C.d i' j)

@[reducible, inline]

noncomputable abbrev HomologicalComplex.xPrev {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (j : ι) : V

Either C.X i, if there is some i with c.Rel i j, or C.X j.

noncomputable def HomologicalComplex.xPrevIso {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : C.xPrev j ≅ C.X i

If c.Rel i j, then C.xPrev j is isomorphic to C.X i.

noncomputable def HomologicalComplex.xPrevIsoSelf {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι} (h : ¬c.Rel (c.prev j) j) : C.xPrev j ≅ C.X j

If there is no i so c.Rel i j, then C.xPrev j is isomorphic to C.X j.

@[reducible, inline]

noncomputable abbrev HomologicalComplex.xNext {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i : ι) : V

Either C.X j, if there is some j with c.rel i j, or C.X i.

noncomputable def HomologicalComplex.xNextIso {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : C.xNext i ≅ C.X j

If c.Rel i j, then C.xNext i is isomorphic to C.X j.

noncomputable def HomologicalComplex.xNextIsoSelf {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι} (h : ¬c.Rel i (c.next i)) : C.xNext i ≅ C.X i

If there is no j so c.Rel i j, then C.xNext i is isomorphic to C.X i.

@[reducible, inline]

noncomputable abbrev HomologicalComplex.dTo {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (j : ι) : C.xPrev j ⟶ C.X j

The differential mapping into C.X j, or zero if there isn't one.

@[reducible, inline]

noncomputable abbrev HomologicalComplex.dFrom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (i : ι) : C.X i ⟶ C.xNext i

The differential mapping out of C.X i, or zero if there isn't one.

theorem HomologicalComplex.dTo_eq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : C.dTo j = CategoryTheory.CategoryStruct.comp (C.xPrevIso r).hom (C.d i j)

theorem HomologicalComplex.dTo_eq_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι} (h : ¬c.Rel (c.prev j) j) : C.dTo j = 0

theorem HomologicalComplex.dFrom_eq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : C.dFrom i = CategoryTheory.CategoryStruct.comp (C.d i j) (C.xNextIso r).inv

theorem HomologicalComplex.dFrom_eq_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι} (h : ¬c.Rel i (c.next i)) : C.dFrom i = 0

@[simp]

theorem HomologicalComplex.xPrevIso_comp_dTo {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : CategoryTheory.CategoryStruct.comp (C.xPrevIso r).inv (C.dTo j) = C.d i j

@[simp]

theorem HomologicalComplex.xPrevIso_comp_dTo_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) {Z : V} (h : C.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.xPrevIso r).inv (CategoryTheory.CategoryStruct.comp (C.dTo j) h) = CategoryTheory.CategoryStruct.comp (C.d i j) h

theorem HomologicalComplex.xPrevIsoSelf_comp_dTo {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι} (h : ¬c.Rel (c.prev j) j) : CategoryTheory.CategoryStruct.comp (C.xPrevIsoSelf h).inv (C.dTo j) = 0

theorem HomologicalComplex.xPrevIsoSelf_comp_dTo_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι} (h : ¬c.Rel (c.prev j) j) {Z : V} (h✝ : C.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.xPrevIsoSelf h).inv (CategoryTheory.CategoryStruct.comp (C.dTo j) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem HomologicalComplex.dFrom_comp_xNextIso {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) : CategoryTheory.CategoryStruct.comp (C.dFrom i) (C.xNextIso r).hom = C.d i j

@[simp]

theorem HomologicalComplex.dFrom_comp_xNextIso_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι} (r : c.Rel i j) {Z : V} (h : C.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.dFrom i) (CategoryTheory.CategoryStruct.comp (C.xNextIso r).hom h) = CategoryTheory.CategoryStruct.comp (C.d i j) h

theorem HomologicalComplex.dFrom_comp_xNextIsoSelf {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι} (h : ¬c.Rel i (c.next i)) : CategoryTheory.CategoryStruct.comp (C.dFrom i) (C.xNextIsoSelf h).hom = 0

theorem HomologicalComplex.dFrom_comp_xNextIsoSelf_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι} (h : ¬c.Rel i (c.next i)) {Z : V} (h✝ : C.X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.dFrom i) (CategoryTheory.CategoryStruct.comp (C.xNextIsoSelf h).hom h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem HomologicalComplex.dTo_comp_dFrom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) (j : ι) : CategoryTheory.CategoryStruct.comp (C.dTo j) (C.dFrom j) = 0

theorem HomologicalComplex.kernel_from_eq_kernel {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasKernels V] {i j : ι} (r : c.Rel i j) : CategoryTheory.Limits.kernelSubobject (C.dFrom i) = CategoryTheory.Limits.kernelSubobject (C.d i j)

theorem HomologicalComplex.image_to_eq_image {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasEqualizers V] {i j : ι} (r : c.Rel i j) : CategoryTheory.Limits.imageSubobject (C.dTo j) = CategoryTheory.Limits.imageSubobject (C.d i j)

def HomologicalComplex.Hom.isoApp {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ≅ C₂) (i : ι) : C₁.X i ≅ C₂.X i

The i-th component of an isomorphism of chain complexes.

@[simp]

theorem HomologicalComplex.Hom.isoApp_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ≅ C₂) (i : ι) : (isoApp f i).hom = f.hom.f i

@[simp]

theorem HomologicalComplex.Hom.isoApp_inv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ≅ C₂) (i : ι) : (isoApp f i).inv = f.inv.f i

def HomologicalComplex.Hom.isoOfComponents {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : (i : ι) → C₁.X i ≅ C₂.X i) (hf : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) = CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom := by cat_disch) : C₁ ≅ C₂

Construct an isomorphism of chain complexes from isomorphism of the objects which commute with the differentials.

@[simp]

theorem HomologicalComplex.Hom.isoOfComponents_hom_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : (i : ι) → C₁.X i ≅ C₂.X i) (hf : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) = CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom := by cat_disch) (i : ι) : (isoOfComponents f hf).hom.f i = (f i).hom

@[simp]

theorem HomologicalComplex.Hom.isoOfComponents_inv_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : (i : ι) → C₁.X i ≅ C₂.X i) (hf : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) = CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom := by cat_disch) (i : ι) : (isoOfComponents f hf).inv.f i = (f i).inv

@[simp]

theorem HomologicalComplex.Hom.isoOfComponents_app {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : (i : ι) → C₁.X i ≅ C₂.X i) (hf : ∀ (i j : ι), c.Rel i j → CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) = CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom) (i : ι) : isoApp (isoOfComponents f hf) i = f i

theorem HomologicalComplex.Hom.isIso_of_components {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁ ⟶ C₂) [∀ (n : ι), CategoryTheory.IsIso (f.f n)] : CategoryTheory.IsIso f

Lemmas relating chain maps and dTo/dFrom.

@[reducible, inline]

noncomputable abbrev HomologicalComplex.Hom.prev {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) : C₁.xPrev j ⟶ C₂.xPrev j

f.prev j is f.f i if there is some r i j, and f.f j otherwise.

theorem HomologicalComplex.Hom.prev_eq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) {i j : ι} (w : c.Rel i j) : f.prev j = CategoryTheory.CategoryStruct.comp (C₁.xPrevIso w).hom (CategoryTheory.CategoryStruct.comp (f.f i) (C₂.xPrevIso w).inv)

@[reducible, inline]

noncomputable abbrev HomologicalComplex.Hom.next {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) : C₁.xNext i ⟶ C₂.xNext i

f.next i is f.f j if there is some r i j, and f.f j otherwise.

theorem HomologicalComplex.Hom.next_eq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) {i j : ι} (w : c.Rel i j) : f.next i = CategoryTheory.CategoryStruct.comp (C₁.xNextIso w).hom (CategoryTheory.CategoryStruct.comp (f.f j) (C₂.xNextIso w).inv)

theorem HomologicalComplex.Hom.comm_from {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) : CategoryTheory.CategoryStruct.comp (f.f i) (C₂.dFrom i) = CategoryTheory.CategoryStruct.comp (C₁.dFrom i) (f.next i)

theorem HomologicalComplex.Hom.comm_from_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) {Z : V} (h : C₂.xNext i ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.f i) (CategoryTheory.CategoryStruct.comp (C₂.dFrom i) h) = CategoryTheory.CategoryStruct.comp (C₁.dFrom i) (CategoryTheory.CategoryStruct.comp (f.next i) h)

@[simp]

theorem HomologicalComplex.Hom.comm_from_apply {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) {F : V → V → Type uF} {carrier : V → Type w} {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory V F] (x : carrier (C₁.X i)) : (CategoryTheory.ConcreteCategory.hom (C₂.dFrom i)) ((CategoryTheory.ConcreteCategory.hom (f.f i)) x) = (CategoryTheory.ConcreteCategory.hom (f.next i)) ((CategoryTheory.ConcreteCategory.hom (C₁.dFrom i)) x)

theorem HomologicalComplex.Hom.comm_to {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) : CategoryTheory.CategoryStruct.comp (f.prev j) (C₂.dTo j) = CategoryTheory.CategoryStruct.comp (C₁.dTo j) (f.f j)

theorem HomologicalComplex.Hom.comm_to_assoc {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) {Z : V} (h : C₂.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.prev j) (CategoryTheory.CategoryStruct.comp (C₂.dTo j) h) = CategoryTheory.CategoryStruct.comp (C₁.dTo j) (CategoryTheory.CategoryStruct.comp (f.f j) h)

@[simp]

theorem HomologicalComplex.Hom.comm_to_apply {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) {F : V → V → Type uF} {carrier : V → Type w} {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory V F] (x : carrier (C₁.xPrev j)) : (CategoryTheory.ConcreteCategory.hom (C₂.dTo j)) ((CategoryTheory.ConcreteCategory.hom (f.prev j)) x) = (CategoryTheory.ConcreteCategory.hom (f.f j)) ((CategoryTheory.ConcreteCategory.hom (C₁.dTo j)) x)

noncomputable def HomologicalComplex.Hom.sqFrom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) : CategoryTheory.Arrow.mk (C₁.dFrom i) ⟶ CategoryTheory.Arrow.mk (C₂.dFrom i)

A morphism of chain complexes induces a morphism of arrows of the differentials out of each object.

@[simp]

theorem HomologicalComplex.Hom.sqFrom_left {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) : (f.sqFrom i).left = f.f i

@[simp]

theorem HomologicalComplex.Hom.sqFrom_right {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (i : ι) : (f.sqFrom i).right = f.next i

@[simp]

theorem HomologicalComplex.Hom.sqFrom_id {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C₁ : HomologicalComplex V c) (i : ι) : sqFrom (CategoryTheory.CategoryStruct.id C₁) i = CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk (C₁.dFrom i))

@[simp]

theorem HomologicalComplex.Hom.sqFrom_comp {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c} (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) : sqFrom (CategoryTheory.CategoryStruct.comp f g) i = CategoryTheory.CategoryStruct.comp (sqFrom f i) (sqFrom g i)

noncomputable def HomologicalComplex.Hom.sqTo {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) : CategoryTheory.Arrow.mk (C₁.dTo j) ⟶ CategoryTheory.Arrow.mk (C₂.dTo j)

A morphism of chain complexes induces a morphism of arrows of the differentials into each object.

@[simp]

theorem HomologicalComplex.Hom.sqTo_left {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) : (f.sqTo j).left = f.prev j

@[simp]

theorem HomologicalComplex.Hom.sqTo_right {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (f : C₁.Hom C₂) (j : ι) : (f.sqTo j).right = f.f j

def ChainComplex.of {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d : (n : α) → X (n + 1) ⟶ X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) : ChainComplex V α

Construct an α-indexed chain complex from a dependently-typed differential.

@[simp]

theorem ChainComplex.of_x {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d : (n : α) → X (n + 1) ⟶ X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) (n : α) : (of X d sq).X n = X n

@[simp]

theorem ChainComplex.of_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d : (n : α) → X (n + 1) ⟶ X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) (j : α) : (of X d sq).d (j + 1) j = d j

theorem ChainComplex.of_d_ne {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d : (n : α) → X (n + 1) ⟶ X n) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d (n + 1)) (d n) = 0) {i j : α} (h : i ≠ j + 1) : (of X d sq).d i j = 0

def ChainComplex.ofHom {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d_X : (n : α) → X (n + 1) ⟶ X n) (sq_X : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_X (n + 1)) (d_X n) = 0) (Y : α → V) (d_Y : (n : α) → Y (n + 1) ⟶ Y n) (sq_Y : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_Y (n + 1)) (d_Y n) = 0) (f : (i : α) → X i ⟶ Y i) (comm : ∀ (i : α), CategoryTheory.CategoryStruct.comp (f (i + 1)) (d_Y i) = CategoryTheory.CategoryStruct.comp (d_X i) (f i)) : of X d_X sq_X ⟶ of Y d_Y sq_Y

A constructor for chain maps between α-indexed chain complexes built using ChainComplex.of, from a dependently typed collection of morphisms.

@[simp]

theorem ChainComplex.ofHom_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d_X : (n : α) → X (n + 1) ⟶ X n) (sq_X : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_X (n + 1)) (d_X n) = 0) (Y : α → V) (d_Y : (n : α) → Y (n + 1) ⟶ Y n) (sq_Y : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_Y (n + 1)) (d_Y n) = 0) (f : (i : α) → X i ⟶ Y i) (comm : ∀ (i : α), CategoryTheory.CategoryStruct.comp (f (i + 1)) (d_Y i) = CategoryTheory.CategoryStruct.comp (d_X i) (f i)) (i : α) : (ofHom X d_X sq_X Y d_Y sq_Y f comm).f i = f i

def ChainComplex.mkAux {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) : ℕ → CategoryTheory.ShortComplex V

Auxiliary definition for mk.

def ChainComplex.mk {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) : ChainComplex V ℕ

An inductive constructor for ℕ-indexed chain complexes.

You provide explicitly the first two differentials, then a function which takes two differentials and the fact they compose to zero, and returns the next object, its differential, and the fact it composes appropriately to zero.

See also mk', which only sees the previous differential in the inductive step.

@[simp]

theorem ChainComplex.mk_X_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) : (mk X₀ X₁ X₂ d₀ d₁ s succ).X 0 = X₀

@[simp]

theorem ChainComplex.mk_X_1 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) : (mk X₀ X₁ X₂ d₀ d₁ s succ).X 1 = X₁

@[simp]

theorem ChainComplex.mk_X_2 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) : (mk X₀ X₁ X₂ d₀ d₁ s succ).X 2 = X₂

@[simp]

theorem ChainComplex.mk_d_1_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀

@[simp]

theorem ChainComplex.mk_d_2_1 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁

theorem ChainComplex.mk_congr_succ_X₃ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) {S S' : CategoryTheory.ShortComplex V} (h : S = S') : (succ S).fst = (succ S').fst

theorem ChainComplex.mk_congr_succ_d₂ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) {S S' : CategoryTheory.ShortComplex V} (h : S = S') : (succ S).snd.fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (succ S').snd.fst (CategoryTheory.eqToHom ⋯))

theorem ChainComplex.mkAux_eq_shortComplex_mk_d_comp_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) (n : ℕ) : mkAux X₀ X₁ X₂ d₀ d₁ s succ n = { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1), X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1), g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }

def ChainComplex.mkXIso {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) (n : ℕ) : (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) ≅ (succ { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1), X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1), g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).fst

The isomorphism from (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) that is given by the inductive construction.

theorem ChainComplex.mk_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) (n : ℕ) : (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 3) (n + 2) = CategoryTheory.CategoryStruct.comp (mkXIso X₀ X₁ X₂ d₀ d₁ s succ n).hom (succ { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1), X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1), g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst

def ChainComplex.mk' {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V) (d : X₁ ⟶ X₀) (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0) : ChainComplex V ℕ

A simpler inductive constructor for ℕ-indexed chain complexes.

You provide explicitly the first differential, then a function which takes a differential, and returns the next object, its differential, and the fact it composes appropriately to zero.

@[simp]

theorem ChainComplex.mk'_X_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V) (d₀ : X₁ ⟶ X₀) (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0) : (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} => succ').X 0 = X₀

@[simp]

theorem ChainComplex.mk'_X_1 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V) (d₀ : X₁ ⟶ X₀) (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0) : (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} => succ').X 1 = X₁

@[simp]

theorem ChainComplex.mk'_d_1_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V) (d₀ : X₁ ⟶ X₀) (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0) : (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} => succ').d 1 0 = d₀

def ChainComplex.mk'XIso {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V) (d₀ : X₁ ⟶ X₀) (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0) (n : ℕ) : (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} => succ').X (n + 2) ≅ (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁ : V} => succ').d (n + 1) n)).fst

The isomorphism from (mk' X₀ X₁ d₀ succ').X (n + 2) that is given by the inductive construction.

theorem ChainComplex.mk'_congr_succ'_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0) {X Y : V} (f g : X ⟶ Y) (h : f = g) : (succ' f).snd.fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (succ' g).snd.fst

theorem ChainComplex.mk'_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V) (d₀ : X₁ ⟶ X₀) (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0) (n : ℕ) : (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} => succ').d (n + 2) (n + 1) = CategoryTheory.CategoryStruct.comp (mk'XIso X₀ X₁ d₀ (fun {X₀ X₁ : V} => succ') n).hom (succ' ((mk' X₀ X₁ d₀ fun {X₀ X₁ : V} => succ').d (n + 1) n)).snd.fst

def ChainComplex.mkHomAux {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (P Q : ChainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1) (one_zero_comm : CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst) (n : ℕ) : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f

An auxiliary construction for mkHom.

Here we build by induction a family of commutative squares, but don't require at the type level that these successive commutative squares actually agree. They do in fact agree, and we then capture that at the type level (i.e. by constructing a chain map) in mkHom.

def ChainComplex.mkHom {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (P Q : ChainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1) (one_zero_comm : CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst) : P ⟶ Q

A constructor for chain maps between ℕ-indexed chain complexes, working by induction on commutative squares.

You need to provide the components of the chain map in degrees 0 and 1, show that these form a commutative square, and then give a construction of each component, and the fact that it forms a commutative square with the previous component, using as an inductive hypothesis the data (and commutativity) of the previous two components.

@[simp]

theorem ChainComplex.mkHom_f_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (P Q : ChainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1) (one_zero_comm : CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst) : (P.mkHom Q zero one one_zero_comm succ).f 0 = zero

@[simp]

theorem ChainComplex.mkHom_f_1 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (P Q : ChainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1) (one_zero_comm : CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst) : (P.mkHom Q zero one one_zero_comm succ).f 1 = one

@[simp]

theorem ChainComplex.mkHom_f_succ_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (P Q : ChainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1) (one_zero_comm : CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst) (n : ℕ) : (P.mkHom Q zero one one_zero_comm succ).f (n + 2) = (succ n ⟨(P.mkHom Q zero one one_zero_comm succ).f n, ⟨(P.mkHom Q zero one one_zero_comm succ).f (n + 1), ⋯⟩⟩).fst

def CochainComplex.of {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d : (n : α) → X n ⟶ X (n + 1)) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0) : CochainComplex V α

Construct an α-indexed cochain complex from a dependently-typed differential.

@[simp]

theorem CochainComplex.of_x {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d : (n : α) → X n ⟶ X (n + 1)) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0) (n : α) : (of X d sq).X n = X n

@[simp]

theorem CochainComplex.of_d {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d : (n : α) → X n ⟶ X (n + 1)) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0) (j : α) : (of X d sq).d j (j + 1) = d j

theorem CochainComplex.of_d_ne {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d : (n : α) → X n ⟶ X (n + 1)) (sq : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0) {i j : α} (h : i + 1 ≠ j) : (of X d sq).d i j = 0

def CochainComplex.ofHom {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d_X : (n : α) → X n ⟶ X (n + 1)) (sq_X : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_X n) (d_X (n + 1)) = 0) (Y : α → V) (d_Y : (n : α) → Y n ⟶ Y (n + 1)) (sq_Y : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_Y n) (d_Y (n + 1)) = 0) (f : (i : α) → X i ⟶ Y i) (comm : ∀ (i : α), CategoryTheory.CategoryStruct.comp (f i) (d_Y i) = CategoryTheory.CategoryStruct.comp (d_X i) (f (i + 1))) : of X d_X sq_X ⟶ of Y d_Y sq_Y

A constructor for chain maps between α-indexed cochain complexes built using CochainComplex.of, from a dependently typed collection of morphisms.

@[simp]

theorem CochainComplex.ofHom_f {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {α : Type u_2} [AddRightCancelSemigroup α] [One α] [DecidableEq α] (X : α → V) (d_X : (n : α) → X n ⟶ X (n + 1)) (sq_X : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_X n) (d_X (n + 1)) = 0) (Y : α → V) (d_Y : (n : α) → Y n ⟶ Y (n + 1)) (sq_Y : ∀ (n : α), CategoryTheory.CategoryStruct.comp (d_Y n) (d_Y (n + 1)) = 0) (f : (i : α) → X i ⟶ Y i) (comm : ∀ (i : α), CategoryTheory.CategoryStruct.comp (f i) (d_Y i) = CategoryTheory.CategoryStruct.comp (d_X i) (f (i + 1))) (i : α) : (ofHom X d_X sq_X Y d_Y sq_Y f comm).f i = f i

def CochainComplex.mkAux {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0) : ℕ → CategoryTheory.ShortComplex V

Auxiliary definition for mk.

def CochainComplex.mk {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0) : CochainComplex V ℕ

An inductive constructor for ℕ-indexed cochain complexes.

You provide explicitly the first two differentials, then a function which takes two differentials and the fact they compose to zero, and returns the next object, its differential, and the fact it composes appropriately to zero.

See also mk', which only sees the previous differential in the inductive step.

@[simp]

theorem CochainComplex.mk_X_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0) : (mk X₀ X₁ X₂ d₀ d₁ s succ).X 0 = X₀

@[simp]

theorem CochainComplex.mk_X_1 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0) : (mk X₀ X₁ X₂ d₀ d₁ s succ).X 1 = X₁

@[simp]

theorem CochainComplex.mk_X_2 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0) : (mk X₀ X₁ X₂ d₀ d₁ s succ).X 2 = X₂

@[simp]

theorem CochainComplex.mk_d_1_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0) : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 0 1 = d₀

@[simp]

theorem CochainComplex.mk_d_2_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0) (succ : (S : CategoryTheory.ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0) : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁

def CochainComplex.mk' {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V) (d : X₀ ⟶ X₁) (succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp f d = 0) : CochainComplex V ℕ

A simpler inductive constructor for ℕ-indexed cochain complexes.

You provide explicitly the first differential, then a function which takes a differential, and returns the next object, its differential, and the fact it composes appropriately to zero.

@[simp]

theorem CochainComplex.mk'_X_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V) (d₀ : X₀ ⟶ X₁) (succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp f d = 0) : (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} => succ').X 0 = X₀

@[simp]

theorem CochainComplex.mk'_X_1 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V) (d₀ : X₀ ⟶ X₁) (succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp f d = 0) : (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} => succ').X 1 = X₁

@[simp]

theorem CochainComplex.mk'_d_1_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V) (d₀ : X₀ ⟶ X₁) (succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp f d = 0) : (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} => succ').d 0 1 = d₀

def CochainComplex.mkHomAux {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (P Q : CochainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1) (one_zero_comm : CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'') (n : ℕ) : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f'

An auxiliary construction for mkHom.

Here we build by induction a family of commutative squares, but don't require at the type level that these successive commutative squares actually agree. They do in fact agree, and we then capture that at the type level (i.e. by constructing a chain map) in mkHom.

def CochainComplex.mkHom {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (P Q : CochainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1) (one_zero_comm : CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'') : P ⟶ Q

A constructor for chain maps between ℕ-indexed cochain complexes, working by induction on commutative squares.

You need to provide the components of the chain map in degrees 0 and 1, show that these form a commutative square, and then give a construction of each component, and the fact that it forms a commutative square with the previous component, using as an inductive hypothesis the data (and commutativity) of the previous two components.

@[simp]

theorem CochainComplex.mkHom_f_0 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (P Q : CochainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1) (one_zero_comm : CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'') : (P.mkHom Q zero one one_zero_comm succ).f 0 = zero

@[simp]

theorem CochainComplex.mkHom_f_1 {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (P Q : CochainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1) (one_zero_comm : CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'') : (P.mkHom Q zero one one_zero_comm succ).f 1 = one

@[simp]

theorem CochainComplex.mkHom_f_succ_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] (P Q : CochainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1) (one_zero_comm : CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one) (succ : (n : ℕ) → (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) = CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') → (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'') (n : ℕ) : (P.mkHom Q zero one one_zero_comm succ).f (n + 2) = (succ n ⟨(P.mkHom Q zero one one_zero_comm succ).f n, ⟨(P.mkHom Q zero one one_zero_comm succ).f (n + 1), ⋯⟩⟩).fst