Preadditive

📁 Source: Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean

Statistics

Metric	Count
Definitions add, neg, add, comp, compLeft, compRight, equivSubZero, h₀, h₁, h₂, h₃, neg, ofEq, ofNullHomotopic, op, refl, sub, trans, unop, HomotopyEquiv, hom, homotopyHomInvId, homotopyInvHomId, inv, refl, trans, add, neg, ofNullHomotopic, add, neg, ofNullHomotopic, instAddCommGroupHom, instAddHom, instNegHom, instPreadditive, instSubHom, nullHomotopic	38
Theorems add_left, add_right, neg_left, neg_right, add_h₀, add_h₁, add_h₂, add_h₃, comm₁, comm₂, comm₃, compLeft_h₀, compLeft_h₁, compLeft_h₂, compLeft_h₃, compRight_h₀, compRight_h₁, compRight_h₂, compRight_h₃, comp_h₀, comp_h₁, comp_h₂, comp_h₃, eq_add_nullHomotopic, equivSubZero_apply, equivSubZero_symm_apply, ext, ext_iff, g_h₃, g_h₃_assoc, homologyMap'_congr, homologyMap_congr, h₀_f, h₀_f_assoc, leftHomologyMap'_congr, leftHomologyMap_congr, neg_h₀, neg_h₁, neg_h₂, neg_h₃, ofEq_h₀, ofEq_h₁, ofEq_h₂, ofEq_h₃, ofNullHomotopic_h₀, ofNullHomotopic_h₁, ofNullHomotopic_h₂, ofNullHomotopic_h₃, op_h₀, op_h₁, op_h₂, op_h₃, refl_h₀, refl_h₁, refl_h₂, refl_h₃, rightHomologyMap'_congr, rightHomologyMap_congr, sub_h₀, sub_h₁, sub_h₂, sub_h₃, symm_h₀, symm_h₁, symm_h₂, symm_h₃, trans_h₀, trans_h₁, trans_h₂, trans_h₃, unop_h₀, unop_h₁, unop_h₂, unop_h₃, ext, ext_iff, refl_hom, refl_homotopyHomInvId, refl_homotopyInvHomId, refl_inv, symm_hom, symm_homotopyHomInvId, symm_homotopyInvHomId, symm_inv, trans_hom, trans_homotopyHomInvId, trans_homotopyInvHomId, trans_inv, add_φH, add_φK, neg_φH, neg_φK, add_φH, add_φQ, neg_φH, neg_φQ, add_liftCycles, add_τ₁, add_τ₂, add_τ₃, cyclesFunctor_additive, cyclesMap'_add, cyclesMap'_neg, cyclesMap'_sub, cyclesMap_add, cyclesMap_neg, cyclesMap_sub, homologyFunctor_additive, homologyMap'_add, homologyMap'_neg, homologyMap'_nullHomotopic, homologyMap'_sub, homologyMap_add, homologyMap_neg, homologyMap_nullHomotopic, homologyMap_sub, leftHomologyFunctor_additive, leftHomologyMap'_add, leftHomologyMap'_neg, leftHomologyMap'_nullHomotopic, leftHomologyMap'_sub, leftHomologyMap_add, leftHomologyMap_neg, leftHomologyMap_nullHomotopic, leftHomologyMap_sub, neg_τ₁, neg_τ₂, neg_τ₃, nullHomotopic_τ₁, nullHomotopic_τ₂, nullHomotopic_τ₃, opcyclesFunctor_additive, opcyclesMap'_add, opcyclesMap'_neg, opcyclesMap'_sub, opcyclesMap_add, opcyclesMap_neg, opcyclesMap_sub, rightHomologyFunctor_additive, rightHomologyMap'_add, rightHomologyMap'_neg, rightHomologyMap'_nullHomotopic, rightHomologyMap'_sub, rightHomologyMap_add, rightHomologyMap_neg, rightHomologyMap_nullHomotopic, rightHomologyMap_sub, sub_liftCycles, sub_τ₁, sub_τ₂, sub_τ₃	151
Total	189

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
HomotopyEquiv 📖	CompData	—
instAddCommGroupHom 📖	CompOp	1 math math: Homotopy.equivSubZero_symm_apply
instAddHom 📖	CompOp	25 math math: homologyMap_add, HomologyMapData.add_left, Homotopy.add_h₁, homologyMap'_add, add_τ₃, opcyclesMap_add, leftHomologyMap_add, Homotopy.equivSubZero_symm_apply, rightHomologyMap'_add, LeftHomologyMapData.add_φH, Homotopy.add_h₀, HomologyMapData.add_right, add_τ₂, rightHomologyMap_add, Homotopy.add_h₂, Homotopy.eq_add_nullHomotopic, RightHomologyMapData.add_φH, cyclesMap'_add, LeftHomologyMapData.add_φK, Homotopy.add_h₃, opcyclesMap'_add, add_τ₁, leftHomologyMap'_add, RightHomologyMapData.add_φQ, cyclesMap_add
instNegHom 📖	CompOp	23 math math: RightHomologyMapData.neg_φH, RightHomologyMapData.neg_φQ, leftHomologyMap'_neg, cyclesMap_neg, HomologyMapData.neg_left, Homotopy.neg_h₁, homologyMap'_neg, LeftHomologyMapData.neg_φH, opcyclesMap_neg, homologyMap_neg, Homotopy.neg_h₃, neg_τ₂, Homotopy.neg_h₀, HomologyMapData.neg_right, LeftHomologyMapData.neg_φK, rightHomologyMap_neg, rightHomologyMap'_neg, neg_τ₁, Homotopy.neg_h₂, cyclesMap'_neg, neg_τ₃, opcyclesMap'_neg, leftHomologyMap_neg
instPreadditive 📖	CompOp	10 math math: cyclesFunctor_linear, opcyclesFunctor_linear, rightHomologyFunctor_linear, leftHomologyFunctor_additive, rightHomologyFunctor_additive, opcyclesFunctor_additive, cyclesFunctor_additive, homologyFunctor_linear, leftHomologyFunctor_linear, homologyFunctor_additive
instSubHom 📖	CompOp	19 math math: leftHomologyMap'_sub, Homotopy.sub_h₀, leftHomologyMap_sub, opcyclesMap_sub, opcyclesMap'_sub, cyclesMap_sub, cyclesMap'_sub, homologyMap'_sub, Homotopy.sub_h₁, Homotopy.equivSubZero_symm_apply, Homotopy.sub_h₃, sub_τ₁, rightHomologyMap_sub, Homotopy.equivSubZero_apply, sub_τ₂, rightHomologyMap'_sub, homologyMap_sub, Homotopy.sub_h₂, sub_τ₃
nullHomotopic 📖	CompOp	14 math math: homologyMap'_nullHomotopic, Homotopy.ofNullHomotopic_h₀, Homotopy.ofNullHomotopic_h₁, Homotopy.ofNullHomotopic_h₂, nullHomotopic_τ₁, leftHomologyMap_nullHomotopic, nullHomotopic_τ₂, nullHomotopic_τ₃, rightHomologyMap'_nullHomotopic, leftHomologyMap'_nullHomotopic, rightHomologyMap_nullHomotopic, Homotopy.eq_add_nullHomotopic, homologyMap_nullHomotopic, Homotopy.ofNullHomotopic_h₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_liftCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup liftCycles X₂	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Preadditive.add_comp liftCycles_i
add_τ₁ 📖	mathematical	—	Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom X₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
add_τ₂ 📖	mathematical	—	Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom X₂ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
add_τ₃ 📖	mathematical	—	Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom X₃ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
cyclesFunctor_additive 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategory instPreadditive cyclesFunctor	—	cyclesMap_add
cyclesMap'_add 📖	mathematical	—	cyclesMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom LeftHomologyData.K AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	LeftHomologyMapData.cyclesMap'_eq
cyclesMap'_neg 📖	mathematical	—	cyclesMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom LeftHomologyData.K NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	LeftHomologyMapData.cyclesMap'_eq
cyclesMap'_sub 📖	mathematical	—	cyclesMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom LeftHomologyData.K SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	sub_eq_add_neg cyclesMap'_add cyclesMap'_neg
cyclesMap_add 📖	mathematical	—	cyclesMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom cycles AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	cyclesMap'_add
cyclesMap_neg 📖	mathematical	—	cyclesMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom cycles NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	cyclesMap'_neg
cyclesMap_sub 📖	mathematical	—	cyclesMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom cycles SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	cyclesMap'_sub
homologyFunctor_additive 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategory instPreadditive homologyFunctor	—	CategoryTheory.CategoryWithHomology.hasHomology homologyMap_add
homologyMap'_add 📖	mathematical	—	homologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom LeftHomologyData.H HomologyData.left AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	leftHomologyMap'_add
homologyMap'_neg 📖	mathematical	—	homologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom LeftHomologyData.H HomologyData.left NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	leftHomologyMap'_neg
homologyMap'_nullHomotopic 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero X₃ g	homologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopic Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct LeftHomologyData.H HomologyData.left CategoryTheory.Limits.HasZeroMorphisms.zero	—	leftHomologyMap'_nullHomotopic
homologyMap'_sub 📖	mathematical	—	homologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom LeftHomologyData.H HomologyData.left SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	leftHomologyMap'_sub
homologyMap_add 📖	mathematical	—	homologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom homology AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	homologyMap'_add
homologyMap_neg 📖	mathematical	—	homologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom homology NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	homologyMap'_neg
homologyMap_nullHomotopic 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero X₃ g	homologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopic Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Limits.HasZeroMorphisms.zero	—	homologyMap'_nullHomotopic
homologyMap_sub 📖	mathematical	—	homologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom homology SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	homologyMap'_sub
leftHomologyFunctor_additive 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategory instPreadditive leftHomologyFunctor	—	leftHomologyMap_add
leftHomologyMap'_add 📖	mathematical	—	leftHomologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom LeftHomologyData.H AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	LeftHomologyMapData.leftHomologyMap'_eq
leftHomologyMap'_neg 📖	mathematical	—	leftHomologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom LeftHomologyData.H NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	LeftHomologyMapData.leftHomologyMap'_eq
leftHomologyMap'_nullHomotopic 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero X₃ g	leftHomologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopic Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct LeftHomologyData.H CategoryTheory.Limits.HasZeroMorphisms.zero	—	LeftHomologyMapData.leftHomologyMap'_eq
leftHomologyMap'_sub 📖	mathematical	—	leftHomologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom LeftHomologyData.H SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	sub_eq_add_neg leftHomologyMap'_add leftHomologyMap'_neg
leftHomologyMap_add 📖	mathematical	—	leftHomologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom leftHomology AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	leftHomologyMap'_add
leftHomologyMap_neg 📖	mathematical	—	leftHomologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom leftHomology NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	leftHomologyMap'_neg
leftHomologyMap_nullHomotopic 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero X₃ g	leftHomologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopic Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct leftHomology CategoryTheory.Limits.HasZeroMorphisms.zero	—	leftHomologyMap'_nullHomotopic
leftHomologyMap_sub 📖	mathematical	—	leftHomologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom leftHomology SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	leftHomologyMap'_sub
neg_τ₁ 📖	mathematical	—	Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom X₁ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_τ₂ 📖	mathematical	—	Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom X₂ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_τ₃ 📖	mathematical	—	Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom X₃ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
nullHomotopic_τ₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero X₃ g	Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopic Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp X₂ f	—	—
nullHomotopic_τ₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero X₃ g	Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopic Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp X₁ f X₃ g	—	—
nullHomotopic_τ₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero X₃ g	Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopic Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₃ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp X₂ g	—	—
opcyclesFunctor_additive 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategory instPreadditive opcyclesFunctor	—	opcyclesMap_add
opcyclesMap'_add 📖	mathematical	—	opcyclesMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom RightHomologyData.Q AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	RightHomologyMapData.opcyclesMap'_eq
opcyclesMap'_neg 📖	mathematical	—	opcyclesMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom RightHomologyData.Q NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	RightHomologyMapData.opcyclesMap'_eq
opcyclesMap'_sub 📖	mathematical	—	opcyclesMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom RightHomologyData.Q SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	sub_eq_add_neg opcyclesMap'_add opcyclesMap'_neg
opcyclesMap_add 📖	mathematical	—	opcyclesMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom opcycles AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	opcyclesMap'_add
opcyclesMap_neg 📖	mathematical	—	opcyclesMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom opcycles NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	opcyclesMap'_neg
opcyclesMap_sub 📖	mathematical	—	opcyclesMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom opcycles SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	opcyclesMap'_sub
rightHomologyFunctor_additive 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategory instPreadditive rightHomologyFunctor	—	rightHomologyMap_add
rightHomologyMap'_add 📖	mathematical	—	rightHomologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom RightHomologyData.H AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	RightHomologyMapData.rightHomologyMap'_eq
rightHomologyMap'_neg 📖	mathematical	—	rightHomologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom RightHomologyData.H NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	RightHomologyMapData.rightHomologyMap'_eq
rightHomologyMap'_nullHomotopic 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero X₃ g	rightHomologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopic Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct RightHomologyData.H CategoryTheory.Limits.HasZeroMorphisms.zero	—	RightHomologyMapData.rightHomologyMap'_eq
rightHomologyMap'_sub 📖	mathematical	—	rightHomologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom RightHomologyData.H SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	sub_eq_add_neg rightHomologyMap'_add rightHomologyMap'_neg
rightHomologyMap_add 📖	mathematical	—	rightHomologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instAddHom rightHomology AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	rightHomologyMap'_add
rightHomologyMap_neg 📖	mathematical	—	rightHomologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instNegHom rightHomology NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	rightHomologyMap'_neg
rightHomologyMap_nullHomotopic 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero X₃ g	rightHomologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms nullHomotopic Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct rightHomology CategoryTheory.Limits.HasZeroMorphisms.zero	—	rightHomologyMap'_nullHomotopic
rightHomologyMap_sub 📖	mathematical	—	rightHomologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom rightHomology SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	rightHomologyMap'_sub
sub_liftCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup liftCycles X₂	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Preadditive.sub_comp liftCycles_i
sub_τ₁ 📖	mathematical	—	Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom X₁ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
sub_τ₂ 📖	mathematical	—	Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom X₂ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
sub_τ₃ 📖	mathematical	—	Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSubHom X₃ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—

CategoryTheory.ShortComplex.HomologyMapData

Definitions

Name	Category	Theorems
add 📖	CompOp	2 math math: add_left, add_right
neg 📖	CompOp	2 math math: neg_left, neg_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_left 📖	mathematical	—	left CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom add CategoryTheory.ShortComplex.LeftHomologyMapData.add CategoryTheory.ShortComplex.HomologyData.left	—	—
add_right 📖	mathematical	—	right CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom add CategoryTheory.ShortComplex.RightHomologyMapData.add CategoryTheory.ShortComplex.HomologyData.right	—	—
neg_left 📖	mathematical	—	left CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instNegHom neg CategoryTheory.ShortComplex.LeftHomologyMapData.neg CategoryTheory.ShortComplex.HomologyData.left	—	—
neg_right 📖	mathematical	—	right CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instNegHom neg CategoryTheory.ShortComplex.RightHomologyMapData.neg CategoryTheory.ShortComplex.HomologyData.right	—	—

CategoryTheory.ShortComplex.Homotopy

Definitions

Name	Category	Theorems
add 📖	CompOp	5 math math: add_h₁, equivSubZero_symm_apply, add_h₀, add_h₂, add_h₃
comp 📖	CompOp	4 math math: comp_h₃, comp_h₁, comp_h₀, comp_h₂
compLeft 📖	CompOp	6 math math: compLeft_h₂, CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyHomInvId, compLeft_h₃, compLeft_h₀, CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyInvHomId, compLeft_h₁
compRight 📖	CompOp	6 math math: compRight_h₀, compRight_h₁, compRight_h₂, compRight_h₃, CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyHomInvId, CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyInvHomId
equivSubZero 📖	CompOp	2 math math: equivSubZero_symm_apply, equivSubZero_apply
h₀ 📖	CompOp	21 math math: h₀_f_assoc, refl_h₀, comm₁, sub_h₀, op_h₀, ofNullHomotopic_h₀, unop_h₃, compRight_h₀, smul_h₀, ofEq_h₀, symm_h₀, add_h₀, op_h₃, trans_h₀, neg_h₀, eq_add_nullHomotopic, comp_h₀, compLeft_h₀, ext_iff, unop_h₀, h₀_f
h₁ 📖	CompOp	20 math math: comm₁, smul_h₁, unop_h₂, op_h₂, add_h₁, sub_h₁, neg_h₁, compRight_h₁, ofNullHomotopic_h₁, refl_h₁, comp_h₁, unop_h₁, eq_add_nullHomotopic, trans_h₁, comm₂, ofEq_h₁, op_h₁, ext_iff, symm_h₁, compLeft_h₁
h₂ 📖	CompOp	20 math math: unop_h₂, compLeft_h₂, op_h₂, smul_h₂, refl_h₂, ofEq_h₂, comm₃, compRight_h₂, ofNullHomotopic_h₂, trans_h₂, unop_h₁, add_h₂, eq_add_nullHomotopic, symm_h₂, sub_h₂, comm₂, op_h₁, ext_iff, comp_h₂, neg_h₂
h₃ 📖	CompOp	21 math math: comp_h₃, op_h₀, g_h₃_assoc, refl_h₃, unop_h₃, smul_h₃, comm₃, compRight_h₃, symm_h₃, sub_h₃, op_h₃, trans_h₃, neg_h₃, compLeft_h₃, eq_add_nullHomotopic, g_h₃, ext_iff, ofEq_h₃, ofNullHomotopic_h₃, add_h₃, unop_h₀
neg 📖	CompOp	4 math math: neg_h₁, neg_h₃, neg_h₀, neg_h₂
ofEq 📖	CompOp	10 math math: CategoryTheory.ShortComplex.HomotopyEquiv.refl_homotopyHomInvId, ofEq_h₂, ofEq_h₀, equivSubZero_symm_apply, CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyHomInvId, equivSubZero_apply, ofEq_h₁, ofEq_h₃, CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyInvHomId, CategoryTheory.ShortComplex.HomotopyEquiv.refl_homotopyInvHomId
ofNullHomotopic 📖	CompOp	4 math math: ofNullHomotopic_h₀, ofNullHomotopic_h₁, ofNullHomotopic_h₂, ofNullHomotopic_h₃
op 📖	CompOp	4 math math: op_h₀, op_h₂, op_h₃, op_h₁
refl 📖	CompOp	6 math math: refl_h₀, refl_h₃, refl_h₂, equivSubZero_symm_apply, refl_h₁, equivSubZero_apply
sub 📖	CompOp	5 math math: sub_h₀, sub_h₁, sub_h₃, equivSubZero_apply, sub_h₂
trans 📖	CompOp	8 math math: equivSubZero_symm_apply, trans_h₂, CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyHomInvId, equivSubZero_apply, trans_h₃, trans_h₀, trans_h₁, CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyInvHomId
unop 📖	CompOp	4 math math: unop_h₂, unop_h₃, unop_h₁, unop_h₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_h₀ 📖	mathematical	—	h₀ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom add CategoryTheory.ShortComplex.X₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
add_h₁ 📖	mathematical	—	h₁ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom add CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
add_h₂ 📖	mathematical	—	h₂ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom add CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₂ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
add_h₃ 📖	mathematical	—	h₃ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom add CategoryTheory.ShortComplex.X₃ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
comm₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f h₁ h₀	—	—
comm₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g h₂ CategoryTheory.ShortComplex.X₁ h₁ CategoryTheory.ShortComplex.f	—	—
comm₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup h₃ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.X₂ h₂ CategoryTheory.ShortComplex.g	—	—
compLeft_h₀ 📖	mathematical	—	h₀ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory compLeft CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.Hom.τ₁	—	—
compLeft_h₁ 📖	mathematical	—	h₁ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory compLeft CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.Hom.τ₂	—	—
compLeft_h₂ 📖	mathematical	—	h₂ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory compLeft CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.Hom.τ₃	—	—
compLeft_h₃ 📖	mathematical	—	h₃ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory compLeft CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.Hom.τ₃	—	—
compRight_h₀ 📖	mathematical	—	h₀ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory compRight CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.Hom.τ₁	—	—
compRight_h₁ 📖	mathematical	—	h₁ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory compRight CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.Hom.τ₁	—	—
compRight_h₂ 📖	mathematical	—	h₂ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory compRight CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.Hom.τ₂	—	—
compRight_h₃ 📖	mathematical	—	h₃ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory compRight CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.Hom.τ₃	—	—
comp_h₀ 📖	mathematical	—	h₀ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ShortComplex.X₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.ShortComplex.Hom.τ₁	—	—
comp_h₁ 📖	mathematical	—	h₁ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.ShortComplex.Hom.τ₂	—	—
comp_h₂ 📖	mathematical	—	h₂ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₂ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.ShortComplex.Hom.τ₃	—	—
comp_h₃ 📖	mathematical	—	h₃ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.ShortComplex.X₃ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.ShortComplex.Hom.τ₃	—	—
eq_add_nullHomotopic 📖	mathematical	—	Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom CategoryTheory.ShortComplex.nullHomotopic h₀ h₀_f h₁ h₂ h₃ g_h₃	—	CategoryTheory.ShortComplex.hom_ext h₀_f g_h₃ comm₁ Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero comm₂ comm₃
equivSubZero_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.ShortComplex.Homotopy Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instSubHom CategoryTheory.ShortComplex.instZeroHom EquivLike.toFunLike Equiv.instEquivLike equivSubZero trans sub refl ofEq	—	—
equivSubZero_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.ShortComplex.Homotopy Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instSubHom CategoryTheory.ShortComplex.instZeroHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivSubZero trans CategoryTheory.ShortComplex.instAddHom AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.ShortComplex.instAddCommGroupHom SubNegMonoid.toSub ofEq add refl	—	—
ext 📖	—	h₀ h₁ h₂ h₃	—	—	—
ext_iff 📖	mathematical	—	h₀ h₁ h₂ h₃	—	ext
g_h₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g h₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
g_h₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g h₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' g_h₃
homologyMap'_congr 📖	mathematical	—	CategoryTheory.ShortComplex.homologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	h₀_f g_h₃ eq_add_nullHomotopic CategoryTheory.ShortComplex.homologyMap'_add CategoryTheory.ShortComplex.homologyMap'_nullHomotopic add_zero
homologyMap_congr 📖	mathematical	—	CategoryTheory.ShortComplex.homologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	homologyMap'_congr
h₀_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₂ h₀ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
h₀_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms h₀ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h₀_f
leftHomologyMap'_congr 📖	mathematical	—	CategoryTheory.ShortComplex.leftHomologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	h₀_f g_h₃ eq_add_nullHomotopic CategoryTheory.ShortComplex.leftHomologyMap'_add CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic add_zero
leftHomologyMap_congr 📖	mathematical	—	CategoryTheory.ShortComplex.leftHomologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	leftHomologyMap'_congr
neg_h₀ 📖	mathematical	—	h₀ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instNegHom neg CategoryTheory.ShortComplex.X₁ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_h₁ 📖	mathematical	—	h₁ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instNegHom neg CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₁ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_h₂ 📖	mathematical	—	h₂ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instNegHom neg CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₂ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_h₃ 📖	mathematical	—	h₃ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instNegHom neg CategoryTheory.ShortComplex.X₃ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
ofEq_h₀ 📖	mathematical	—	h₀ ofEq Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
ofEq_h₁ 📖	mathematical	—	h₁ ofEq Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₁ CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
ofEq_h₂ 📖	mathematical	—	h₂ ofEq Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
ofEq_h₃ 📖	mathematical	—	h₃ ofEq Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
ofNullHomotopic_h₀ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	h₀ CategoryTheory.ShortComplex.nullHomotopic Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instZeroHom ofNullHomotopic	—	—
ofNullHomotopic_h₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	h₁ CategoryTheory.ShortComplex.nullHomotopic Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instZeroHom ofNullHomotopic	—	—
ofNullHomotopic_h₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	h₂ CategoryTheory.ShortComplex.nullHomotopic Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instZeroHom ofNullHomotopic	—	—
ofNullHomotopic_h₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	h₃ CategoryTheory.ShortComplex.nullHomotopic Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instZeroHom ofNullHomotopic	—	—
op_h₀ 📖	mathematical	—	h₀ Opposite CategoryTheory.Category.opposite CategoryTheory.instPreadditiveOpposite CategoryTheory.ShortComplex.op CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.opMap op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ h₃	—	—
op_h₁ 📖	mathematical	—	h₁ Opposite CategoryTheory.Category.opposite CategoryTheory.instPreadditiveOpposite CategoryTheory.ShortComplex.op CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.opMap op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₂ h₂	—	—
op_h₂ 📖	mathematical	—	h₂ Opposite CategoryTheory.Category.opposite CategoryTheory.instPreadditiveOpposite CategoryTheory.ShortComplex.op CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.opMap op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₁ h₁	—	—
op_h₃ 📖	mathematical	—	h₃ Opposite CategoryTheory.Category.opposite CategoryTheory.instPreadditiveOpposite CategoryTheory.ShortComplex.op CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.opMap op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ h₀	—	—
refl_h₀ 📖	mathematical	—	h₀ refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
refl_h₁ 📖	mathematical	—	h₁ refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₁ CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
refl_h₂ 📖	mathematical	—	h₂ refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
refl_h₃ 📖	mathematical	—	h₃ refl Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
rightHomologyMap'_congr 📖	mathematical	—	CategoryTheory.ShortComplex.rightHomologyMap' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	h₀_f g_h₃ eq_add_nullHomotopic CategoryTheory.ShortComplex.rightHomologyMap'_add CategoryTheory.ShortComplex.rightHomologyMap'_nullHomotopic add_zero
rightHomologyMap_congr 📖	mathematical	—	CategoryTheory.ShortComplex.rightHomologyMap CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	rightHomologyMap'_congr
sub_h₀ 📖	mathematical	—	h₀ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instSubHom sub CategoryTheory.ShortComplex.X₁ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
sub_h₁ 📖	mathematical	—	h₁ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instSubHom sub CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₁ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
sub_h₂ 📖	mathematical	—	h₂ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instSubHom sub CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.X₂ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
sub_h₃ 📖	mathematical	—	h₃ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instSubHom sub CategoryTheory.ShortComplex.X₃ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	—
symm_h₀ 📖	mathematical	—	h₀ symm Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
symm_h₁ 📖	mathematical	—	h₁ symm Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₁ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
symm_h₂ 📖	mathematical	—	h₂ symm Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₂ NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
symm_h₃ 📖	mathematical	—	h₃ symm Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
trans_h₀ 📖	mathematical	—	h₀ trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
trans_h₁ 📖	mathematical	—	h₁ trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
trans_h₂ 📖	mathematical	—	h₂ trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.X₂ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
trans_h₃ 📖	mathematical	—	h₃ trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
unop_h₀ 📖	mathematical	—	h₀ CategoryTheory.ShortComplex.unop CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.unopMap unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ Opposite CategoryTheory.Category.opposite CategoryTheory.instPreadditiveOpposite h₃	—	—
unop_h₁ 📖	mathematical	—	h₁ CategoryTheory.ShortComplex.unop CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.unopMap unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₃ Opposite CategoryTheory.Category.opposite CategoryTheory.instPreadditiveOpposite CategoryTheory.ShortComplex.X₂ h₂	—	—
unop_h₂ 📖	mathematical	—	h₂ CategoryTheory.ShortComplex.unop CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.unopMap unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ Opposite CategoryTheory.Category.opposite CategoryTheory.instPreadditiveOpposite CategoryTheory.ShortComplex.X₁ h₁	—	—
unop_h₃ 📖	mathematical	—	h₃ CategoryTheory.ShortComplex.unop CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.ShortComplex.unopMap unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ Opposite CategoryTheory.Category.opposite CategoryTheory.instPreadditiveOpposite h₀	—	—

CategoryTheory.ShortComplex.HomotopyEquiv

Definitions

Name	Category	Theorems
hom 📖	CompOp	7 math math: trans_hom, refl_hom, ext_iff, trans_homotopyHomInvId, trans_homotopyInvHomId, symm_hom, symm_inv
homotopyHomInvId 📖	CompOp	5 math math: refl_homotopyHomInvId, symm_homotopyHomInvId, symm_homotopyInvHomId, ext_iff, trans_homotopyHomInvId
homotopyInvHomId 📖	CompOp	5 math math: symm_homotopyHomInvId, symm_homotopyInvHomId, ext_iff, trans_homotopyInvHomId, refl_homotopyInvHomId
inv 📖	CompOp	7 math math: refl_inv, ext_iff, trans_homotopyHomInvId, trans_inv, trans_homotopyInvHomId, symm_hom, symm_inv
refl 📖	CompOp	4 math math: refl_homotopyHomInvId, refl_hom, refl_inv, refl_homotopyInvHomId
trans 📖	CompOp	4 math math: trans_hom, trans_homotopyHomInvId, trans_inv, trans_homotopyInvHomId

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom inv CategoryTheory.ShortComplex.Homotopy CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.CategoryStruct.id homotopyHomInvId homotopyInvHomId	—	—	—
ext_iff 📖	mathematical	—	hom inv CategoryTheory.ShortComplex.Homotopy CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.CategoryStruct.id homotopyHomInvId homotopyInvHomId	—	ext
refl_hom 📖	mathematical	—	hom refl CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory	—	—
refl_homotopyHomInvId 📖	mathematical	—	homotopyHomInvId refl CategoryTheory.ShortComplex.Homotopy.ofEq CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.CategoryStruct.id	—	—
refl_homotopyInvHomId 📖	mathematical	—	homotopyInvHomId refl CategoryTheory.ShortComplex.Homotopy.ofEq CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.CategoryStruct.id	—	—
refl_inv 📖	mathematical	—	inv refl CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory	—	—
symm_hom 📖	mathematical	—	hom symm inv	—	—
symm_homotopyHomInvId 📖	mathematical	—	homotopyHomInvId symm homotopyInvHomId	—	—
symm_homotopyInvHomId 📖	mathematical	—	homotopyInvHomId symm homotopyHomInvId	—	—
symm_inv 📖	mathematical	—	inv symm hom	—	—
trans_hom 📖	mathematical	—	hom trans CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory	—	—
trans_homotopyHomInvId 📖	mathematical	—	homotopyHomInvId trans CategoryTheory.ShortComplex.Homotopy.trans CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory hom inv CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex.Homotopy.ofEq CategoryTheory.ShortComplex.Homotopy.compLeft CategoryTheory.ShortComplex.Homotopy.compRight	—	—
trans_homotopyInvHomId 📖	mathematical	—	homotopyInvHomId trans CategoryTheory.ShortComplex.Homotopy.trans CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory inv hom CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex.Homotopy.ofEq CategoryTheory.ShortComplex.Homotopy.compLeft CategoryTheory.ShortComplex.Homotopy.compRight	—	—
trans_inv 📖	mathematical	—	inv trans CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory	—	—

CategoryTheory.ShortComplex.LeftHomologyMapData

Definitions

Name	Category	Theorems
add 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.add_left, add_φH, add_φK
neg 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.neg_left, neg_φH, neg_φK
ofNullHomotopic 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_φH 📖	mathematical	—	φH CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom add CategoryTheory.ShortComplex.LeftHomologyData.H AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
add_φK 📖	mathematical	—	φK CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom add CategoryTheory.ShortComplex.LeftHomologyData.K AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_φH 📖	mathematical	—	φH CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instNegHom neg CategoryTheory.ShortComplex.LeftHomologyData.H NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_φK 📖	mathematical	—	φK CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instNegHom neg CategoryTheory.ShortComplex.LeftHomologyData.K NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—

CategoryTheory.ShortComplex.RightHomologyMapData

Definitions

Name	Category	Theorems
add 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.add_right, add_φH, add_φQ
neg 📖	CompOp	3 math math: neg_φH, neg_φQ, CategoryTheory.ShortComplex.HomologyMapData.neg_right
ofNullHomotopic 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_φH 📖	mathematical	—	φH CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom add CategoryTheory.ShortComplex.RightHomologyData.H AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
add_φQ 📖	mathematical	—	φQ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instAddHom add CategoryTheory.ShortComplex.RightHomologyData.Q AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_φH 📖	mathematical	—	φH CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instNegHom neg CategoryTheory.ShortComplex.RightHomologyData.H NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
neg_φQ 📖	mathematical	—	φQ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instNegHom neg CategoryTheory.ShortComplex.RightHomologyData.Q NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—

---

← Back to Index