Documentation Verification Report

KInjective

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

Statistics

Metric	Count
Definitions `IsKInjective`, `homotopyZero`	2
Theorems `homotopyZero_def`, `nonempty_homotopy_zero`, `rightOrthogonal`, `instIsKInjectiveObjIntShiftFunctor`, `isKInjective_iff_of_iso`, `isKInjective_iff_rightOrthogonal`, `isKInjective_of_injective`, `isKInjective_of_injective_aux`, `isKInjective_of_iso`, `isKInjective_shift_iff`, `isKInjective`	11
Total	13

CochainComplex

Definitions

Name	Category	Theorems
`IsKInjective` 📖	CompData	8 math math: `isKInjective_of_injective`, `isKInjective_shift_iff`, `instIsKInjectiveObjIntShiftFunctor`, `isKInjective_of_iso`, `HomotopyEquiv.isKInjective`, `isKInjective_iff_of_iso`, `CategoryTheory.InjectiveResolution.instIsKInjectiveCochainComplex`, `isKInjective_iff_rightOrthogonal`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsKInjectiveObjIntShiftFunctor` 📖	mathematical	—	`IsKInjective` `CategoryTheory.Functor.obj` `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.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `isKInjective_iff_rightOrthogonal` `CategoryTheory.ObjectProperty.prop_of_iso` `CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsRightOrthogonal` `CategoryTheory.ObjectProperty.le_shift` `CategoryTheory.ObjectProperty.IsStableUnderShift.isStableUnderShiftBy` `CategoryTheory.ObjectProperty.instIsStableUnderShiftRightOrthogonal` `CategoryTheory.ObjectProperty.IsTriangulated.toIsStableUnderShift` `HomotopyCategory.instHasZeroObject` `CategoryTheory.Abelian.hasZeroObject` `HomotopyCategory.instAdditiveIntUpShiftFunctor` `CategoryTheory.Abelian.hasBinaryBiproducts` `HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic`
`isKInjective_iff_of_iso` 📖	mathematical	—	`IsKInjective`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `isKInjective_of_iso`
`isKInjective_iff_rightOrthogonal` 📖	mathematical	—	`IsKInjective` `CategoryTheory.ObjectProperty.rightOrthogonal` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomotopyCategory.instPreadditive` `HomotopyCategory.subcategoryAcyclic` `CategoryTheory.Functor.obj` `HomologicalComplex` `HomologicalComplex.instCategory` `HomotopyCategory.quotient`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `HomotopyCategory.quotient_obj_surjective` `CategoryTheory.Functor.map_surjective` `HomotopyCategory.instFullHomologicalComplexQuotient` `HomotopyCategory.eq_of_homotopy` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic` `CategoryTheory.Functor.map_zero` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `HomotopyCategory.instAdditiveHomologicalComplexQuotient`
`isKInjective_of_injective` 📖	mathematical	`CategoryTheory.Injective` `HomologicalComplex.X` `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`	`IsKInjective`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Limits.IsZero.eq_of_tgt` `isZero_of_isStrictlyGE` `isKInjective_of_injective_aux` `add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `HomComplex.Cochain.single_v_eq_zero` `HomComplex.Cochain.ofHom_zero` `add_zero` `HomComplex.Cochain.ext₀` `neg_add_cancel` `HomComplex.δ_v` `HomComplex.Cochain.InductionUp.limitSequence_eqUpTo`
`isKInjective_of_injective_aux` 📖	mathematical	`HomologicalComplex.ExactAt` `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` `HomComplex.Cochain.EqUpTo` `HomComplex.δ` `HomComplex.Cochain.ofHom`	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `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` `HomComplex.Cochain.EqUpTo` `HomComplex.δ` `HomComplex.Cochain` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `HomComplex.instAddCommGroupCochain` `HomComplex.Cochain.single` `HomComplex.Cochain.ofHom`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `add_zero` `le_refl` `CategoryTheory.Preadditive.comp_sub` `neg_add_cancel` `HomologicalComplex.Hom.comm` `HomComplex.δ_v` `one_smul` `HomComplex.Cochain.ofHom_v` `CategoryTheory.Preadditive.add_comp` `CategoryTheory.Category.assoc` `HomologicalComplex.d_comp_d` `CategoryTheory.Limits.comp_zero` `zero_add` `sub_self` `HomologicalComplex.d_comp_d_assoc` `CategoryTheory.Limits.zero_comp` `HomologicalComplex.exactAt_iff'` `prev` `add_sub_cancel_right` `next` `CategoryTheory.ShortComplex.Exact.comp_descToInjective` `LE.le.lt_or_eq` `HomComplex.δ_add` `HomComplex.Cochain.add_v` `add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `HomComplex.Cochain.single_v_eq_zero` `smul_zero` `HomComplex.Cochain.single_v` `CategoryTheory.Preadditive.comp_add` `add_sub_cancel`
`isKInjective_of_iso` 📖	mathematical	—	`IsKInjective`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomotopyEquiv.isKInjective`
`isKInjective_shift_iff` 📖	mathematical	—	`IsKInjective` `CategoryTheory.Functor.obj` `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.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `isKInjective_of_iso` `instIsKInjectiveObjIntShiftFunctor`

CochainComplex.IsKInjective

Definitions

Name	Category	Theorems
`homotopyZero` 📖	CompOp	1 math math: `homotopyZero_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homotopyZero_def` 📖	mathematical	`HomologicalComplex.Acyclic` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	`homotopyZero` `Nonempty.some` `Homotopy` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `Quiver.Hom` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.instZeroHom_1` `nonempty_homotopy_zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `nonempty_homotopy_zero`
`nonempty_homotopy_zero` 📖	mathematical	`HomologicalComplex.Acyclic` `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`	`Homotopy` `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` `Quiver.Hom` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.instZeroHom_1`	—	—
`rightOrthogonal` 📖	mathematical	—	`CategoryTheory.ObjectProperty.rightOrthogonal` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomotopyCategory.instPreadditive` `HomotopyCategory.subcategoryAcyclic` `CategoryTheory.Functor.obj` `HomologicalComplex` `HomologicalComplex.instCategory` `HomotopyCategory.quotient`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `CochainComplex.isKInjective_iff_rightOrthogonal`

HomotopyEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isKInjective` 📖	mathematical	—	`CochainComplex.IsKInjective`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.zero_comp`

---

← Back to Index