KProjective

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

Statistics

Metric	Count
Definitions IsKProjective, homotopyZero	2
Theorems homotopyZero_def, leftOrthogonal, nonempty_homotopy_zero, instIsKProjectiveObjIntShiftFunctor, isKProjective_iff_leftOrthogonal, isKProjective_iff_of_iso, isKProjective_of_iso, isKProjective_of_op, isKProjective_of_projective, isKProjective_shift_iff, isKProjective	11
Total	13

CochainComplex

Definitions

Name	Category	Theorems
IsKProjective 📖	CompData	9 math math: CategoryTheory.ProjectiveResolution.instIsKProjectiveCochainComplex, isKProjective_of_projective, instIsKProjectiveObjIntShiftFunctor, HomotopyEquiv.isKProjective, isKProjective_iff_leftOrthogonal, isKProjective_iff_of_iso, isKProjective_shift_iff, isKProjective_of_op, isKProjective_of_iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsKProjectiveObjIntShiftFunctor 📖	mathematical	—	IsKProjective 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 isKProjective_iff_leftOrthogonal CategoryTheory.ObjectProperty.prop_of_iso CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsLeftOrthogonal CategoryTheory.ObjectProperty.le_shift CategoryTheory.ObjectProperty.IsStableUnderShift.isStableUnderShiftBy CategoryTheory.ObjectProperty.instIsStableUnderShiftLeftOrthogonal CategoryTheory.ObjectProperty.IsTriangulated.toIsStableUnderShift HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic
isKProjective_iff_leftOrthogonal 📖	mathematical	—	IsKProjective CategoryTheory.ObjectProperty.leftOrthogonal 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 AddRightCancelSemigroup.toIsRightCancelAdd HomotopyCategory.eq_of_homotopy HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomotopyCategory.instAdditiveHomologicalComplexQuotient
isKProjective_iff_of_iso 📖	mathematical	—	IsKProjective	—	AddRightCancelSemigroup.toIsRightCancelAdd isKProjective_of_iso
isKProjective_of_iso 📖	mathematical	—	IsKProjective	—	AddRightCancelSemigroup.toIsRightCancelAdd HomotopyEquiv.isKProjective
isKProjective_of_op 📖	mathematical	—	IsKProjective	—	AddRightCancelSemigroup.toIsRightCancelAdd acyclic_op CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object CategoryTheory.Limits.hasZeroObject_op HomologicalComplex.instHasZeroObject CategoryTheory.Abelian.hasZeroObject CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit CategoryTheory.Equivalence.isEquivalence_functor HomologicalComplex.instHasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasTerminal_op_of_hasInitial CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits Finite.of_fintype
isKProjective_of_projective 📖	mathematical	CategoryTheory.Projective 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	IsKProjective	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Injective.instOppositeOpOfProjective isStrictlyGE_iff CategoryTheory.Limits.IsZero.op isZero_of_isStrictlyLE isKProjective_of_op isKInjective_of_injective
isKProjective_shift_iff 📖	mathematical	—	IsKProjective 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 isKProjective_of_iso instIsKProjectiveObjIntShiftFunctor

CochainComplex.IsKProjective

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
leftOrthogonal 📖	mathematical	—	CategoryTheory.ObjectProperty.leftOrthogonal 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.isKProjective_iff_leftOrthogonal
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	—	—

HomotopyEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isKProjective 📖	mathematical	—	CochainComplex.IsKProjective	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Limits.comp_zero

---

← Back to Index