HomotopyCofiber

📁 Source: Mathlib/Algebra/Homology/HomotopyCofiber.lean

Statistics

Metric	Count
Definitions HasHomotopyCofiber, cylinder, desc, homotopyEquiv, homotopy₀₁, inlX, inrX, ι₀, ι₁, π, πCompι₀Homotopy, nullHomotopicMap, nullHomotopy, homotopyCofiber, X, XIso, XIsoBiprod, d, desc, descEquiv, fstX, inlX, inr, inrCompHomotopy, inrX, sndX	26
Theorems hasBinaryBiproduct, inlX_π, inlX_π_assoc, inrX_π, inrX_π_assoc, map_ι₀_eq_map_ι₁, ι₀_desc, ι₀_desc_assoc, ι₀_π, ι₀_π_assoc, ι₁_desc, ι₁_desc_assoc, ι₁_π, ι₁_π_assoc, inlX_nullHomotopy_f, inrX_nullHomotopy_f, nullHomotopicMap_eq, d_fstX, d_fstX_assoc, d_sndX, d_sndX_assoc, descSigma_ext_iff, desc_f, desc_f', eq_desc, ext_from_X, ext_from_X', ext_to_X, ext_to_X', inlX_d, inlX_d', inlX_d'_assoc, inlX_d_assoc, inlX_desc_f, inlX_desc_f_assoc, inlX_fstX, inlX_fstX_assoc, inlX_sndX, inlX_sndX_assoc, inrCompHomotopy_hom, inrCompHomotopy_hom_desc_hom, inrCompHomotopy_hom_desc_hom_assoc, inrCompHomotopy_hom_eq_zero, inrX_d, inrX_d_assoc, inrX_desc_f, inrX_desc_f_assoc, inrX_fstX, inrX_fstX_assoc, inrX_sndX, inrX_sndX_assoc, inr_desc, inr_desc_assoc, inr_f, shape, sndX_inrX, sndX_inrX_assoc, homotopyCofiber_X, homotopyCofiber_d, instHasHomotopyCofiberOfHasBinaryBiproducts, map_eq_of_inverts_homotopyEquivalences	61
Total	87

HomologicalComplex

Definitions

Name	Category	Theorems
HasHomotopyCofiber 📖	CompData	2 math math: CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat, instHasHomotopyCofiberOfHasBinaryBiproducts
cylinder 📖	CompOp	16 math math: cylinder.πCompι₀Homotopy.nullHomotopicMap_eq, cylinder.ι₁_π, cylinder.inrX_π_assoc, cylinder.inlX_π, cylinder.ι₀_π, cylinder.inlX_π_assoc, cylinder.ι₀_π_assoc, cylinder.ι₁_π_assoc, cylinder.ι₀_desc, cylinder.inrX_π, cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f, cylinder.ι₁_desc_assoc, cylinder.map_ι₀_eq_map_ι₁, cylinder.ι₁_desc, cylinder.ι₀_desc_assoc, cylinder.πCompι₀Homotopy.inlX_nullHomotopy_f
homotopyCofiber 📖	CompOp	16 math math: homotopyCofiber.inrCompHomotopy_hom_desc_hom_assoc, homotopyCofiber.desc_f', homotopyCofiber_X, homotopyCofiber.inrCompHomotopy_hom, homotopyCofiber.inrCompHomotopy_hom_desc_hom, homotopyCofiber.inr_desc, homotopyCofiber.inr_desc_assoc, homotopyCofiber.inlX_desc_f_assoc, homotopyCofiber.eq_desc, homotopyCofiber.inrX_desc_f, homotopyCofiber.inrCompHomotopy_hom_eq_zero, homotopyCofiber_d, homotopyCofiber.desc_f, homotopyCofiber.inlX_desc_f, homotopyCofiber.inr_f, homotopyCofiber.inrX_desc_f_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homotopyCofiber_X 📖	mathematical	—	X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms homotopyCofiber homotopyCofiber.X	—	—
homotopyCofiber_d 📖	mathematical	—	d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms homotopyCofiber homotopyCofiber.d	—	—
instHasHomotopyCofiberOfHasBinaryBiproducts 📖	mathematical	—	HasHomotopyCofiber	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct

HomologicalComplex.HasHomotopyCofiber

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasBinaryBiproduct 📖	mathematical	ComplexShape.Rel	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	—	—

HomologicalComplex.cylinder

Definitions

Name	Category	Theorems
desc 📖	CompOp	4 math math: ι₀_desc, ι₁_desc_assoc, ι₁_desc, ι₀_desc_assoc
homotopyEquiv 📖	CompOp	—
homotopy₀₁ 📖	CompOp	—
inlX 📖	CompOp	3 math math: inlX_π, inlX_π_assoc, πCompι₀Homotopy.inlX_nullHomotopy_f
inrX 📖	CompOp	3 math math: inrX_π_assoc, inrX_π, πCompι₀Homotopy.inrX_nullHomotopy_f
ι₀ 📖	CompOp	8 math math: πCompι₀Homotopy.nullHomotopicMap_eq, ι₀_π, ι₀_π_assoc, ι₀_desc, πCompι₀Homotopy.inrX_nullHomotopy_f, map_ι₀_eq_map_ι₁, ι₀_desc_assoc, πCompι₀Homotopy.inlX_nullHomotopy_f
ι₁ 📖	CompOp	5 math math: ι₁_π, ι₁_π_assoc, ι₁_desc_assoc, map_ι₀_eq_map_ι₁, ι₁_desc
π 📖	CompOp	11 math math: πCompι₀Homotopy.nullHomotopicMap_eq, ι₁_π, inrX_π_assoc, inlX_π, ι₀_π, inlX_π_assoc, ι₀_π_assoc, ι₁_π_assoc, inrX_π, πCompι₀Homotopy.inrX_nullHomotopy_f, πCompι₀Homotopy.inlX_nullHomotopy_f
πCompι₀Homotopy 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inlX_π 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.cylinder inlX HomologicalComplex.Hom.f π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.instHasBinaryBiproduct Homotopy.zero HomologicalComplex.homotopyCofiber.inlX_desc_f add_zero
inlX_π_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.cylinder inlX HomologicalComplex.Hom.f π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inlX_π
inrX_π 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.instHasBinaryBiproduct HomologicalComplex.cylinder inrX HomologicalComplex.Hom.f π CategoryTheory.Limits.biprod.desc CategoryTheory.CategoryStruct.id	—	HomologicalComplex.instHasBinaryBiproduct HomologicalComplex.homotopyCofiber.inrX_desc_f
inrX_π_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.instHasBinaryBiproduct HomologicalComplex.cylinder inrX HomologicalComplex.Hom.f π CategoryTheory.Limits.biprod.desc CategoryTheory.CategoryStruct.id	—	HomologicalComplex.instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inrX_π
map_ι₀_eq_map_ι₁ 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X ComplexShape.Rel CategoryTheory.MorphismProperty.IsInvertedBy HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.homotopyEquivalences	CategoryTheory.Functor.map HomologicalComplex.cylinder ι₀ ι₁	—	HomologicalComplex.instHasBinaryBiproduct CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Functor.map_comp ι₀_π CategoryTheory.Functor.map_id ι₁_π
ι₀_desc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.cylinder ι₀ desc	—	HomologicalComplex.instHasBinaryBiproduct CategoryTheory.Category.assoc HomologicalComplex.homotopyCofiber.inr_desc CategoryTheory.Limits.biprod.inl_desc
ι₀_desc_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.cylinder ι₀ desc	—	HomologicalComplex.instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₀_desc
ι₀_π 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.cylinder ι₀ π CategoryTheory.CategoryStruct.id	—	HomologicalComplex.instHasBinaryBiproduct ι₀_desc
ι₀_π_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.cylinder ι₀ π	—	HomologicalComplex.instHasBinaryBiproduct CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ι₀_π
ι₁_desc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.cylinder ι₁ desc	—	HomologicalComplex.instHasBinaryBiproduct CategoryTheory.Category.assoc HomologicalComplex.homotopyCofiber.inr_desc CategoryTheory.Limits.biprod.inr_desc
ι₁_desc_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.cylinder ι₁ desc	—	HomologicalComplex.instHasBinaryBiproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₁_desc
ι₁_π 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.cylinder ι₁ π CategoryTheory.CategoryStruct.id	—	HomologicalComplex.instHasBinaryBiproduct ι₁_desc
ι₁_π_assoc 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.cylinder ι₁ π	—	HomologicalComplex.instHasBinaryBiproduct CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ι₁_π

HomologicalComplex.cylinder.πCompι₀Homotopy

Definitions

Name	Category	Theorems
nullHomotopicMap 📖	CompOp	3 math math: nullHomotopicMap_eq, inrX_nullHomotopy_f, inlX_nullHomotopy_f
nullHomotopy 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inlX_nullHomotopy_f 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.cylinder HomologicalComplex.cylinder.inlX HomologicalComplex.Hom.f nullHomotopicMap Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instCategory HomologicalComplex.instSubHom HomologicalComplex.cylinder.π HomologicalComplex.cylinder.ι₀ CategoryTheory.CategoryStruct.id	—	HomologicalComplex.instHasBinaryBiproduct Homotopy.nullHomotopicMap'_f HomologicalComplex.homotopyCofiber.d_sndX_assoc CategoryTheory.Preadditive.add_comp CategoryTheory.Category.assoc CategoryTheory.Limits.biprod.lift_snd CategoryTheory.Preadditive.neg_comp CategoryTheory.Category.id_comp CategoryTheory.Preadditive.comp_add HomologicalComplex.homotopyCofiber.inlX_fstX_assoc HomologicalComplex.homotopyCofiber.inlX_sndX_assoc CategoryTheory.Limits.zero_comp add_zero CategoryTheory.Preadditive.comp_sub HomologicalComplex.cylinder.inlX_π_assoc CategoryTheory.Category.comp_id zero_sub Homotopy.nullHomotopicMap'_f_of_not_rel_right
inrX_nullHomotopy_f 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biprod HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.instHasBinaryBiproduct HomologicalComplex.cylinder HomologicalComplex.cylinder.inrX HomologicalComplex.Hom.f nullHomotopicMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instSubHom HomologicalComplex.cylinder.π HomologicalComplex.cylinder.ι₀ CategoryTheory.CategoryStruct.id	—	HomologicalComplex.instHasBinaryBiproduct CategoryTheory.Limits.biprod.hom_ext CategoryTheory.Limits.biprod.lift_fst CategoryTheory.Preadditive.sub_comp CategoryTheory.Limits.BinaryBicone.inl_fst CategoryTheory.Limits.BinaryBicone.inr_fst sub_zero CategoryTheory.Limits.biprod.lift_snd CategoryTheory.Limits.BinaryBicone.inl_snd CategoryTheory.Limits.BinaryBicone.inr_snd zero_sub Homotopy.nullHomotopicMap'_f CategoryTheory.Category.assoc HomologicalComplex.homotopyCofiber.inlX_d CategoryTheory.Preadditive.comp_add CategoryTheory.Preadditive.comp_neg HomologicalComplex.homotopyCofiber.inrX_d_assoc HomologicalComplex.homotopyCofiber.inrX_sndX_assoc add_neg_cancel_left CategoryTheory.Preadditive.comp_sub HomologicalComplex.cylinder.inrX_π_assoc CategoryTheory.Category.comp_id CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.biprod.hom_ext' HomologicalComplex.inl_biprodXIso_inv_assoc HomologicalComplex.biprod_inl_snd_f_assoc CategoryTheory.Limits.zero_comp HomologicalComplex.biprod_inl_desc_f_assoc CategoryTheory.Category.id_comp sub_self HomologicalComplex.inr_biprodXIso_inv_assoc HomologicalComplex.biprod_inr_snd_f_assoc HomologicalComplex.biprod_inr_desc_f_assoc Homotopy.nullHomotopicMap'_f_of_not_rel_left HomologicalComplex.homotopyCofiber.inlX_d'
nullHomotopicMap_eq 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X ComplexShape.Rel	nullHomotopicMap Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.cylinder HomologicalComplex.instSubHom CategoryTheory.CategoryStruct.comp HomologicalComplex.cylinder.π HomologicalComplex.cylinder.ι₀ CategoryTheory.CategoryStruct.id	—	HomologicalComplex.instHasBinaryBiproduct HomologicalComplex.hom_ext HomologicalComplex.homotopyCofiber.ext_from_X inlX_nullHomotopy_f inrX_nullHomotopy_f HomologicalComplex.homotopyCofiber.ext_from_X'

HomologicalComplex.homotopyCofiber

Definitions

Name	Category	Theorems
X 📖	CompOp	28 math math: inlX_fstX, inrX_fstX_assoc, inrX_sndX_assoc, desc_f', HomologicalComplex.homotopyCofiber_X, inrX_d_assoc, inlX_sndX_assoc, inrX_fstX, sndX_inrX_assoc, inlX_desc_f_assoc, d_fstX, inrX_desc_f, inlX_sndX, inlX_d, shape, inlX_d'_assoc, d_sndX, inlX_d', inlX_fstX_assoc, inrX_d, inlX_d_assoc, desc_f, sndX_inrX, inlX_desc_f, d_sndX_assoc, inrX_sndX, d_fstX_assoc, inrX_desc_f_assoc
XIso 📖	CompOp	—
XIsoBiprod 📖	CompOp	—
d 📖	CompOp	12 math math: inrX_d_assoc, d_fstX, inlX_d, shape, inlX_d'_assoc, d_sndX, inlX_d', inrX_d, inlX_d_assoc, HomologicalComplex.homotopyCofiber_d, d_sndX_assoc, d_fstX_assoc
desc 📖	CompOp	11 math math: inrCompHomotopy_hom_desc_hom_assoc, desc_f', inrCompHomotopy_hom_desc_hom, inr_desc, inr_desc_assoc, inlX_desc_f_assoc, eq_desc, inrX_desc_f, desc_f, inlX_desc_f, inrX_desc_f_assoc
descEquiv 📖	CompOp	—
fstX 📖	CompOp	9 math math: inlX_fstX, inrX_fstX_assoc, inrX_fstX, d_fstX, d_sndX, inlX_fstX_assoc, desc_f, d_sndX_assoc, d_fstX_assoc
inlX 📖	CompOp	11 math math: inlX_fstX, inrCompHomotopy_hom, inlX_sndX_assoc, inlX_desc_f_assoc, inlX_sndX, inlX_d, inlX_d'_assoc, inlX_d', inlX_fstX_assoc, inlX_d_assoc, inlX_desc_f
inr 📖	CompOp	8 math math: inrCompHomotopy_hom_desc_hom_assoc, inrCompHomotopy_hom, inrCompHomotopy_hom_desc_hom, inr_desc, inr_desc_assoc, eq_desc, inrCompHomotopy_hom_eq_zero, inr_f
inrCompHomotopy 📖	CompOp	5 math math: inrCompHomotopy_hom_desc_hom_assoc, inrCompHomotopy_hom, inrCompHomotopy_hom_desc_hom, eq_desc, inrCompHomotopy_hom_eq_zero
inrX 📖	CompOp	15 math math: inrX_fstX_assoc, inrX_sndX_assoc, inrX_d_assoc, inrX_fstX, sndX_inrX_assoc, inrX_desc_f, inlX_d, inlX_d'_assoc, inlX_d', inrX_d, inlX_d_assoc, sndX_inrX, inrX_sndX, inr_f, inrX_desc_f_assoc
sndX 📖	CompOp	10 math math: inrX_sndX_assoc, desc_f', inlX_sndX_assoc, sndX_inrX_assoc, inlX_sndX, d_sndX, desc_f, sndX_inrX, d_sndX_assoc, inrX_sndX

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_fstX 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms d fstX Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup HomologicalComplex.d	—	CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.neg_comp CategoryTheory.Category.assoc inlX_fstX CategoryTheory.Category.comp_id inrX_fstX CategoryTheory.Limits.comp_zero add_zero ComplexShape.next_eq'
d_fstX_assoc 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms fstX Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup HomologicalComplex.d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_fstX
d_sndX 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms d sndX Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup fstX HomologicalComplex.Hom.f HomologicalComplex.d	—	CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.neg_comp CategoryTheory.Category.assoc inlX_sndX CategoryTheory.Limits.comp_zero neg_zero inrX_sndX CategoryTheory.Category.comp_id zero_add
d_sndX_assoc 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms sndX Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup fstX HomologicalComplex.Hom.f HomologicalComplex.d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_sndX
descSigma_ext_iff 📖	mathematical	—	Quiver.Hom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory Homotopy CategoryTheory.CategoryStruct.comp HomologicalComplex.instZeroHom_1 Homotopy.hom	—	Homotopy.ext Homotopy.zero
desc_f 📖	mathematical	ComplexShape.Rel	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.homotopyCofiber desc Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp fstX Homotopy.hom HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instZeroHom_1 sndX	—	ComplexShape.next_eq'
desc_f' 📖	mathematical	ComplexShape.Rel ComplexShape.next	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.homotopyCofiber desc CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X HomologicalComplex.X sndX	—	—
eq_desc 📖	mathematical	ComplexShape.Rel	desc CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.homotopyCofiber inr Homotopy.trans Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1 Homotopy.ofEq Homotopy.compRight inrCompHomotopy	—	HomologicalComplex.hom_ext ext_from_X inlX_desc_f inrCompHomotopy_hom add_zero zero_add inrX_desc_f ext_from_X'
ext_from_X 📖	—	ComplexShape.Rel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX inrX	—	—	HomologicalComplex.HasHomotopyCofiber.hasBinaryBiproduct CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.biprod.hom_ext' CategoryTheory.Category.assoc ComplexShape.next_eq'
ext_from_X' 📖	—	ComplexShape.Rel ComplexShape.next CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inrX	—	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv
ext_to_X 📖	—	ComplexShape.Rel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms fstX sndX	—	—	HomologicalComplex.HasHomotopyCofiber.hasBinaryBiproduct CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.biprod.hom_ext CategoryTheory.Category.assoc ComplexShape.next_eq'
ext_to_X' 📖	—	ComplexShape.Rel ComplexShape.next CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms sndX	—	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom
inlX_d 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HomologicalComplex.d HomologicalComplex.Hom.f inrX	—	ext_to_X CategoryTheory.Category.assoc d_fstX CategoryTheory.Preadditive.comp_neg inlX_fstX_assoc CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.neg_comp inlX_fstX CategoryTheory.Category.comp_id inrX_fstX CategoryTheory.Limits.comp_zero add_zero d_sndX CategoryTheory.Preadditive.comp_add inlX_sndX_assoc CategoryTheory.Limits.zero_comp inlX_sndX neg_zero inrX_sndX zero_add
inlX_d' 📖	mathematical	ComplexShape.Rel ComplexShape.next	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX d HomologicalComplex.Hom.f inrX	—	ext_to_X' CategoryTheory.Category.assoc d_sndX CategoryTheory.Preadditive.comp_add inlX_fstX_assoc inlX_sndX_assoc CategoryTheory.Limits.zero_comp add_zero inrX_sndX CategoryTheory.Category.comp_id
inlX_d'_assoc 📖	mathematical	ComplexShape.Rel ComplexShape.next	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX d HomologicalComplex.Hom.f inrX	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inlX_d'
inlX_d_assoc 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HomologicalComplex.d HomologicalComplex.Hom.f inrX	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inlX_d
inlX_desc_f 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX HomologicalComplex.Hom.f HomologicalComplex.homotopyCofiber desc Homotopy.hom HomologicalComplex HomologicalComplex.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	—	CategoryTheory.Preadditive.comp_add inlX_fstX_assoc inlX_sndX_assoc CategoryTheory.Limits.zero_comp add_zero ComplexShape.next_eq'
inlX_desc_f_assoc 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX HomologicalComplex.Hom.f HomologicalComplex.homotopyCofiber desc Homotopy.hom HomologicalComplex HomologicalComplex.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inlX_desc_f
inlX_fstX 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX fstX CategoryTheory.CategoryStruct.id	—	HomologicalComplex.HasHomotopyCofiber.hasBinaryBiproduct CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.BinaryBicone.inl_fst
inlX_fstX_assoc 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX fstX	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inlX_fstX
inlX_sndX 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX sndX Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.HasHomotopyCofiber.hasBinaryBiproduct CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.BinaryBicone.inl_snd ComplexShape.next_eq'
inlX_sndX_assoc 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inlX sndX Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inlX_sndX
inrCompHomotopy_hom 📖	mathematical	ComplexShape.Rel	Homotopy.hom HomologicalComplex.homotopyCofiber CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory inr Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1 inrCompHomotopy inlX	—	—
inrCompHomotopy_hom_desc_hom 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.homotopyCofiber Homotopy.hom HomologicalComplex HomologicalComplex.instCategory inr Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1 inrCompHomotopy HomologicalComplex.Hom.f desc	—	inrCompHomotopy_hom desc_f CategoryTheory.Preadditive.comp_add inlX_fstX_assoc inlX_sndX_assoc CategoryTheory.Limits.zero_comp add_zero Homotopy.zero
inrCompHomotopy_hom_desc_hom_assoc 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.homotopyCofiber Homotopy.hom HomologicalComplex HomologicalComplex.instCategory inr Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1 inrCompHomotopy HomologicalComplex.Hom.f desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inrCompHomotopy_hom_desc_hom
inrCompHomotopy_hom_eq_zero 📖	mathematical	ComplexShape.Rel	Homotopy.hom HomologicalComplex.homotopyCofiber CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory inr Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1 inrCompHomotopy HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
inrX_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inrX d HomologicalComplex.d	—	ext_to_X CategoryTheory.Category.assoc d_fstX CategoryTheory.Preadditive.comp_neg inrX_fstX_assoc CategoryTheory.Limits.zero_comp neg_zero inrX_fstX CategoryTheory.Limits.comp_zero d_sndX CategoryTheory.Preadditive.comp_add inrX_sndX_assoc zero_add inrX_sndX CategoryTheory.Category.comp_id ext_to_X' shape HomologicalComplex.shape
inrX_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inrX d HomologicalComplex.d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inrX_d
inrX_desc_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inrX HomologicalComplex.Hom.f HomologicalComplex.homotopyCofiber desc	—	CategoryTheory.Preadditive.comp_add inrX_fstX_assoc CategoryTheory.Limits.zero_comp inrX_sndX_assoc zero_add
inrX_desc_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inrX HomologicalComplex.Hom.f HomologicalComplex.homotopyCofiber desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inrX_desc_f
inrX_fstX 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inrX fstX Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.HasHomotopyCofiber.hasBinaryBiproduct CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.BinaryBicone.inr_fst ComplexShape.next_eq'
inrX_fstX_assoc 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inrX fstX Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inrX_fstX
inrX_sndX 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inrX sndX CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.BinaryBicone.inr_snd CategoryTheory.Iso.inv_hom_id
inrX_sndX_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X inrX sndX	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inrX_sndX
inr_desc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.homotopyCofiber inr desc	—	HomologicalComplex.hom_ext inrX_desc_f
inr_desc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.homotopyCofiber inr desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_desc
inr_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.homotopyCofiber inr inrX	—	—
shape 📖	mathematical	ComplexShape.Rel	d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
sndX_inrX 📖	mathematical	ComplexShape.Rel ComplexShape.next	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms sndX inrX CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
sndX_inrX_assoc 📖	mathematical	ComplexShape.Rel ComplexShape.next	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms sndX inrX	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' sndX_inrX

Homotopy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_eq_of_inverts_homotopyEquivalences 📖	mathematical	ComplexShape.Rel CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X CategoryTheory.MorphismProperty.IsInvertedBy HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.homotopyEquivalences	CategoryTheory.Functor.map	—	HomologicalComplex.instHasBinaryBiproduct HomologicalComplex.cylinder.ι₀_desc CategoryTheory.Functor.map_comp HomologicalComplex.cylinder.map_ι₀_eq_map_ι₁ HomologicalComplex.cylinder.ι₁_desc

---

← Back to Index