Documentation Verification Report

Resolution

📁 Source: Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean

Statistics

Metric	Count
Definitions `mapProjectiveResolution`, `HasProjectiveResolution`, `HasProjectiveResolutions`, `ProjectiveResolution`, `hom`, `cokernelCofork`, `complex`, `isColimitCokernelCofork`, `self`, `π`	10
Theorems `mapProjectiveResolution_complex`, `mapProjectiveResolution_π`, `out`, `out`, `hom_comp_π`, `hom_comp_π_assoc`, `hom_f_zero_comp_π_f_zero`, `hom_f_zero_comp_π_f_zero_assoc`, `complex_d_comp_π_f_zero`, `complex_d_comp_π_f_zero_assoc`, `complex_d_succ_comp`, `complex_exactAt_succ`, `exact_succ`, `hasHomology`, `instEpiFNatπ`, `projective`, `quasiIso`, `self_complex`, `self_π`, `π_f_succ`	20
Total	30

CategoryTheory

Definitions

Name	Category	Theorems
`HasProjectiveResolution` 📖	CompData	2 math math: `HasProjectiveResolutions.out`, `ProjectiveResolution.instHasProjectiveResolution`
`HasProjectiveResolutions` 📖	CompData	1 math math: `ProjectiveResolution.instHasProjectiveResolutions`
`ProjectiveResolution` 📖	CompData	1 math math: `HasProjectiveResolution.out`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`mapProjectiveResolution` 📖	CompOp	2 math math: `mapProjectiveResolution_π`, `mapProjectiveResolution_complex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapProjectiveResolution_complex` 📖	mathematical	—	`CategoryTheory.ProjectiveResolution.complex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `obj` `mapProjectiveResolution` `HomologicalComplex` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `mapHomologicalComplex` `preservesZeroMorphisms_of_additive`	—	`preservesZeroMorphisms_of_additive`
`mapProjectiveResolution_π` 📖	mathematical	—	`CategoryTheory.ProjectiveResolution.π` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `obj` `mapProjectiveResolution` `CategoryTheory.CategoryStruct.comp` `ChainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `HomologicalComplex` `mapHomologicalComplex` `preservesZeroMorphisms_of_additive` `CategoryTheory.ProjectiveResolution.complex` `ChainComplex.single₀` `map` `CategoryTheory.NatTrans.app` `comp` `HomologicalComplex.single` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `HomologicalComplex.singleMapHomologicalComplex`	—	`preservesZeroMorphisms_of_additive`

CategoryTheory.HasProjectiveResolution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	—	`CategoryTheory.ProjectiveResolution`	—	—

CategoryTheory.HasProjectiveResolutions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	—	`CategoryTheory.HasProjectiveResolution`	—	—

CategoryTheory.ProjectiveResolution

Definitions

Name	Category	Theorems
`cokernelCofork` 📖	CompOp	—
`complex` 📖	CompOp	47 math math: `quasiIso`, `lift_commutes_zero_assoc`, `homotopyEquiv_inv_π_assoc`, `homotopyEquiv_hom_π`, `cochainComplex_d`, `CategoryTheory.Functor.mapProjectiveResolution_π`, `CategoryTheory.Functor.mapProjectiveResolution_complex`, `Hom.hom_comp_π_assoc`, `Rep.barResolution_complex`, `Hom.hom'_f_assoc`, `pOpcycles_comp_fromLeftDerivedZero'_assoc`, `homotopyEquiv_inv_π`, `instIsIsoFromLeftDerivedZero'Self`, `π'_f_zero_assoc`, `π_f_succ`, `Hom.hom'_f`, `pOpcycles_comp_fromLeftDerivedZero'`, `Hom.hom_f_zero_comp_π_f_zero_assoc`, `lift_commutes_zero`, `leftDerived_app_eq`, `lift_commutes`, `homotopyEquiv_hom_π_assoc`, `complex_d_comp_π_f_zero`, `Hom.hom_comp_π`, `exact_succ`, `π'_f_zero`, `complex_d_succ_comp`, `hasHomology`, `extMk_zero`, `self_complex`, `lift_commutes_assoc`, `leftDerivedToHomotopyCategory_app_eq`, `Rep.FiniteCyclicGroup.resolution_complex`, `Hom.hom_f_zero_comp_π_f_zero`, `Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply`, `Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply`, `exact₀`, `projective`, `liftFOne_zero_comm`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply`, `instEpiFNatπ`, `complex_d_comp_π_f_zero_assoc`, `cochainComplex_d_assoc`, `fromLeftDerivedZero_eq`, `complex_exactAt_succ`, `CategoryTheory.instIsIsoFromLeftDerivedZero'`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply`
`isColimitCokernelCofork` 📖	CompOp	—
`self` 📖	CompOp	3 math math: `self_π`, `instIsIsoFromLeftDerivedZero'Self`, `self_complex`
`π` 📖	CompOp	25 math math: `quasiIso`, `lift_commutes_zero_assoc`, `homotopyEquiv_inv_π_assoc`, `homotopyEquiv_hom_π`, `self_π`, `CategoryTheory.Functor.mapProjectiveResolution_π`, `Hom.hom_comp_π_assoc`, `pOpcycles_comp_fromLeftDerivedZero'_assoc`, `homotopyEquiv_inv_π`, `π'_f_zero_assoc`, `π_f_succ`, `pOpcycles_comp_fromLeftDerivedZero'`, `Hom.hom_f_zero_comp_π_f_zero_assoc`, `lift_commutes_zero`, `lift_commutes`, `homotopyEquiv_hom_π_assoc`, `complex_d_comp_π_f_zero`, `Hom.hom_comp_π`, `π'_f_zero`, `lift_commutes_assoc`, `Hom.hom_f_zero_comp_π_f_zero`, `exact₀`, `instEpiFNatπ`, `complex_d_comp_π_f_zero_assoc`, `Rep.FiniteCyclicGroup.resolution_π`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complex_d_comp_π_f_zero` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `HomologicalComplex.d` `HomologicalComplex.Hom.f` `π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.Hom.comm` `HomologicalComplex.single_obj_d` `CategoryTheory.Limits.comp_zero`
`complex_d_comp_π_f_zero_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `HomologicalComplex.d` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `HomologicalComplex.Hom.f` `π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `complex_d_comp_π_f_zero`
`complex_d_succ_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.shape` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `CategoryTheory.Limits.comp_zero`
`complex_exactAt_succ` 📖	mathematical	—	`HomologicalComplex.ExactAt` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `hasHomology` `HomologicalComplex.instHasHomologyObjSingle` `quasiIsoAt_iff_exactAt'` `ChainComplex.exactAt_succ_single_obj` `QuasiIso.quasiIsoAt` `quasiIso`
`exact_succ` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `HomologicalComplex.d` `HomologicalComplex.d_comp_d`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.exactAt_iff'` `ChainComplex.prev` `ChainComplex.next_nat_succ` `complex_exactAt_succ`
`hasHomology` 📖	mathematical	—	`HomologicalComplex.HasHomology` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex`	—	—
`instEpiFNatπ` 📖	mathematical	—	`CategoryTheory.Epi` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `HomologicalComplex.Hom.f` `π`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Limits.epi_of_isColimit_cofork` `π_f_succ` `CategoryTheory.Limits.HasZeroObject.instEpi`
`projective` 📖	mathematical	—	`CategoryTheory.Projective` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex`	—	—
`quasiIso` 📖	mathematical	—	`QuasiIso` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `π` `hasHomology` `HomologicalComplex.instHasHomologyObjSingle`	—	—
`self_complex` 📖	mathematical	—	`complex` `self` `CategoryTheory.Functor.obj` `ChainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `ChainComplex.single₀`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`self_π` 📖	mathematical	—	`π` `self` `CategoryTheory.CategoryStruct.id` `ChainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `CategoryTheory.Functor.obj` `ChainComplex.single₀`	—	—
`π_f_succ` 📖	mathematical	—	`HomologicalComplex.Hom.f` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `complex` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `π` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Limits.IsZero.eq_of_tgt` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.isZero_single_obj_X`

CategoryTheory.ProjectiveResolution.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	7 math math: `hom_comp_π_assoc`, `CategoryTheory.ProjectiveResolution.mk₀_comp_extMk`, `hom'_f_assoc`, `hom'_f`, `hom_f_zero_comp_π_f_zero_assoc`, `hom_comp_π`, `hom_f_zero_comp_π_f_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_comp_π` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ProjectiveResolution.complex` `CategoryTheory.Functor.obj` `ChainComplex.single₀` `hom` `CategoryTheory.ProjectiveResolution.π` `CategoryTheory.Functor.map`	—	`HomologicalComplex.to_single_hom_ext` `AddRightCancelSemigroup.toIsRightCancelAdd` `hom_f_zero_comp_π_f_zero` `ChainComplex.single₀_map_f_zero`
`hom_comp_π_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ChainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.ProjectiveResolution.complex` `hom` `CategoryTheory.Functor.obj` `ChainComplex.single₀` `CategoryTheory.ProjectiveResolution.π` `CategoryTheory.Functor.map`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `hom_comp_π`
`hom_f_zero_comp_π_f_zero` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.ProjectiveResolution.complex` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `HomologicalComplex.Hom.f` `hom` `CategoryTheory.ProjectiveResolution.π` `CategoryTheory.Functor.map`	—	—
`hom_f_zero_comp_π_f_zero_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `ComplexShape.down` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `AddRightCancelSemigroup.toIsRightCancelAdd` `Nat.instOne` `CategoryTheory.ProjectiveResolution.complex` `HomologicalComplex.Hom.f` `hom` `CategoryTheory.Functor.obj` `ChainComplex` `HomologicalComplex.instCategory` `ChainComplex.single₀` `CategoryTheory.ProjectiveResolution.π` `CategoryTheory.Functor.map`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `hom_f_zero_comp_π_f_zero`

---

← Back to Index