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 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomotopyCategory.instPreadditive HomotopyCategory.subcategoryAcyclic CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory HomotopyCategory.quotient	—	AddRightCancelSemigroup.toIsRightCancelAdd HomotopyCategory.quotient_obj_surjective CategoryTheory.Functor.map_surjective HomotopyCategory.instFullHomologicalComplexQuotient 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 Quiver.Hom HomologicalComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomotopyCategory.instPreadditive HomotopyCategory.subcategoryAcyclic CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory HomotopyCategory.quotient	—	AddRightCancelSemigroup.toIsRightCancelAdd 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 Quiver.Hom HomologicalComplex 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