Theorems · Inductive type · category theory
HomologicalComplex.HasHomotopyCofiber
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.Preadditive C] →
{ι : Type u_2} → {c : ComplexShape ι} → {F G : HomologicalComplex C c} → (F ⟶ G) → PropA morphism of homological complexes φ : F ⟶ G has a homotopy cofiber if for all
indices i and j such that c.Rel i j, the binary biproduct F.X j ⊞ G.X i exists.
- Defined in
- Mathlib.Algebra.Homology.HomotopyCofiber
- Cited by
- 225 results in Mathlib
- Foundations
- Depth 18 from the axioms, rests on 198 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.Preadditivestatement · cited by 3,309
- HomologicalComplexstatement · cited by 1,691
- ComplexShapestatement · cited by 1,684
Cited by274
Results whose statement or proof uses this declaration.
- CochainComplex.mappingConestatement and proof · cited by 181
- CochainComplex.mappingCone.inrstatement and proof · cited by 79
- CochainComplex.mappingCone.inlstatement and proof · cited by 61
- HomologicalComplex.homotopyCofiber.Xstatement and proof · cited by 59
- CochainComplex.mappingCone.fststatement and proof · cited by 51
- CochainComplex.mappingCone.sndstatement and proof · cited by 49
- CochainComplex.mappingCoconestatement and proof · cited by 46
- HomologicalComplex.homotopyCofiber.inrXstatement and proof · cited by 33
- HomologicalComplex.homotopyCofiberstatement and proof · cited by 31
- HomologicalComplex.homotopyCofiber.inlXstatement and proof · cited by 29
- HomologicalComplex.HasCylinderproof · cited by 27
- HomologicalComplex.homotopyCofiber.sndXstatement and proof · cited by 27
Showing the 200 most cited of 274.