Documentation Verification Report

SingleFunctors

📁 Source: Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean

Statistics

Metric	Count
Definitions `mapCochainComplexSingleFunctor`, `singleFunctor`, `singleFunctors`, `singleFunctor`, `singleFunctorPostcompQuotientIso`, `singleFunctors`, `singleFunctorsPostcompQuotientIso`	7
Theorems `instAdditiveIntFunctorSingleFunctors`, `instFaithfulIntSingleFunctor`, `instFullIntSingleFunctor`, `instLinearIntFunctorSingleFunctors`, `singleFunctor_obj_d`, `instAdditiveIntUpSingleFunctor`, `instLinearIntUpSingleFunctor`, `quotient_obj_singleFunctors_obj`	8
Total	15

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`mapCochainComplexSingleFunctor` 📖	CompOp	—

CochainComplex

Definitions

Name	Category	Theorems
`singleFunctor` 📖	CompOp	84 math math: `CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁`, `HomComplex.Cochain.fromSingleMk_neg`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add`, `HomComplex.Cocycle.fromSingleMk_add`, `CategoryTheory.InjectiveResolution.ι'_f_zero`, `HomComplex.Cochain.fromSingleEquiv_fromSingleMk`, `HomComplex.Cochain.δ_fromSingleMk`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub`, `HomComplex.Cochain.toSingleMk_neg`, `HomComplex.Cochain.toSingleMk_v`, `HomComplex.Cochain.toSingleMk_add`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub`, `HomComplex.Cochain.fromSingleMk_postcomp`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero`, `CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply`, `HomComplex.Cochain.toSingleMk_v_eq_zero`, `DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective`, `isSplitEpi_to_singleFunctor_obj_of_projective`, `HomComplex.Cocycle.toSingleMk_add`, `HomComplex.Cocycle.toSingleMk_mem_coboundaries_iff`, `CategoryTheory.ProjectiveResolution.extMk_hom`, `HomComplex.Cochain.fromSingleMk_v`, `HomComplex.Cochain.fromSingleMk_add`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg`, `HomComplex.Cocycle.toSingleMk_zero`, `CategoryTheory.ProjectiveResolution.π'_f_zero_assoc`, `HomComplex.Cocycle.toSingleMk_coe`, `CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'`, `singleFunctor_obj_d`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero`, `HomComplex.Cochain.fromSingleMk_zero`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero`, `CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'_assoc`, `HomComplex.Cocycle.fromSingleMk_coe`, `CategoryTheory.ProjectiveResolution.π'_f_zero`, `HomComplex.Cocycle.fromSingleMk_neg`, `HomComplex.Cochain.δ_toSingleMk`, `HomComplex.Cochain.fromSingleMk_precomp`, `HomComplex.Cocycle.fromSingleMk_zero`, `CategoryTheory.InjectiveResolution.ι'_f_zero_assoc`, `CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt`, `CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'_assoc`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add`, `isSplitMono_from_singleFunctor_obj_of_injective`, `HomComplex.Cochain.fromSingleMk_sub`, `DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective`, `CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply`, `HomComplex.Cocycle.toSingleMk_sub`, `CategoryTheory.InjectiveResolution.extMk_hom`, `HomComplex.Cocycle.fromSingleMk_sub`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg`, `instFullIntSingleFunctor`, `HomComplex.Cochain.toSingleMk_zero`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk`, `CategoryTheory.InjectiveResolution.instQuasiIsoIntι'`, `HomComplex.Cocycle.toSingleMk_neg`, `HomComplex.Cocycle.fromSingleMk_precomp`, `HomComplex.Cochain.toSingleMk_postcomp`, `CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ'`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add`, `HomotopyCategory.quotient_obj_singleFunctors_obj`, `HomComplex.Cochain.fromSingleMk_v_eq_zero`, `HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iff`, `instIsStrictlyLEObjIntSingleFunctor`, `instIsStrictlyGEObjIntSingleFunctor`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk`, `HomComplex.Cocycle.toSingleMk_postcomp`, `HomComplex.Cochain.toSingleEquiv_toSingleMk`, `HomComplex.Cocycle.fromSingleMk_postcomp`, `HomComplex.Cocycle.toSingleMk_precomp`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom`, `HomComplex.Cochain.toSingleMk_sub`, `CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'`, `CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply`, `HomComplex.Cochain.toSingleMk_precomp`, `instFaithfulIntSingleFunctor`, `CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg`
`singleFunctors` 📖	CompOp	10 math math: `instLinearIntFunctorSingleFunctors`, `DerivedCategory.singleFunctorsPostcompQIso_inv_hom`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁`, `instAdditiveIntFunctorSingleFunctors`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂`, `DerivedCategory.singleFunctorsPostcompQIso_hom_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAdditiveIntFunctorSingleFunctors` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `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` `HomologicalComplex.instPreadditive` `CategoryTheory.SingleFunctors.functor` `Int.instAddMonoid` `instHasShiftInt` `singleFunctors`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instAdditiveSingle`
`instFaithfulIntSingleFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `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` `singleFunctor`	—	`HomologicalComplex.instFaithfulSingle`
`instFullIntSingleFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `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` `singleFunctor`	—	`HomologicalComplex.instFullSingle`
`instLinearIntFunctorSingleFunctors` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `Ring.toSemiring` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `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` `HomologicalComplex.instPreadditive` `HomologicalComplex.instLinear` `CategoryTheory.SingleFunctors.functor` `Int.instAddMonoid` `instHasShiftInt` `singleFunctors`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Linear.smul_comp` `CategoryTheory.Linear.comp_smul` `HomologicalComplex.hom_ext` `smul_dite` `smul_zero`
`singleFunctor_obj_d` 📖	mathematical	—	`HomologicalComplex.d` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `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.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `singleFunctor` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

HomotopyCategory

Definitions

Name	Category	Theorems
`singleFunctor` 📖	CompOp	3 math math: `instLinearIntUpSingleFunctor`, `instAdditiveIntUpSingleFunctor`, `quotient_obj_singleFunctors_obj`
`singleFunctorPostcompQuotientIso` 📖	CompOp	—
`singleFunctors` 📖	CompOp	1 math math: `DerivedCategory.Qh_obj_singleFunctors_obj`
`singleFunctorsPostcompQuotientIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAdditiveIntUpSingleFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `HomotopyCategory` `ComplexShape.up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `instPreadditive` `singleFunctor`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.instAdditiveComp` `CochainComplex.instAdditiveIntFunctorSingleFunctors` `instAdditiveHomologicalComplexQuotient`
`instLinearIntUpSingleFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `Ring.toSemiring` `HomotopyCategory` `ComplexShape.up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `instPreadditive` `instLinear` `singleFunctor`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.instLinearComp` `CochainComplex.instLinearIntFunctorSingleFunctors` `instLinearHomologicalComplexQuotient`
`quotient_obj_singleFunctors_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `HomotopyCategory` `instCategoryHomotopyCategory` `quotient` `CochainComplex` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `CochainComplex.singleFunctor` `singleFunctor`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

---

← Back to Index