CM5a

📁 Source: Mathlib/Algebra/Homology/Factorizations/CM5a.lean

Statistics

Metric	Count
Definitions cofFib, isIsoLE, quasiIsoLE	3
Theorems step	1
Total	4

CochainComplex.Plus.modelCategoryQuillen.cm5a_cof

Definitions

Name	Category	Theorems
cofFib 📖	CompOp	1 math math: step
isIsoLE 📖	CompOp	1 math math: step
quasiIsoLE 📖	CompOp	1 math math: step

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
step 📖	mathematical	QuasiIsoAt CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc	CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Factorisation CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Factorisation.instCategory cofFib quasiIsoLE isIsoLE	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Factorisation.ι_π_assoc CategoryTheory.Factorisation.ι_π CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.IsIso.comp_isIso

---

← Back to Index