KProjective

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

Statistics

Metric	Count
Definitions equivOfIsKProjective	1
Theorems bijective_toSmallShiftedHom_of_isKProjective, equivOfIsKProjective_apply, equivOfIsKProjective_symm_apply, Qh_map_bijective	4
Total	5

CochainComplex.HomComplex.CohomologyClass

Definitions

Name	Category	Theorems
equivOfIsKProjective 📖	CompOp	2 math math: equivOfIsKProjective_symm_apply, equivOfIsKProjective_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_toSmallShiftedHom_of_isKProjective 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.quasiIso CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid CochainComplex.instHasShiftInt	Function.Bijective CochainComplex.HomComplex.CohomologyClass CategoryTheory.Localization.SmallShiftedHom toSmallShiftedHom	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp Function.Bijective.of_comp_iff' Equiv.bijective mk_surjective CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_app_assoc CategoryTheory.NatTrans.naturality Function.Bijective.comp CochainComplex.IsKProjective.Qh_map_bijective toHom_bijective
equivOfIsKProjective_apply 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.quasiIso CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid CochainComplex.instHasShiftInt	DFunLike.coe Equiv CochainComplex.HomComplex.CohomologyClass CategoryTheory.Localization.SmallShiftedHom EquivLike.toFunLike Equiv.instEquivLike equivOfIsKProjective toSmallShiftedHom	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor
equivOfIsKProjective_symm_apply 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.quasiIso CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid CochainComplex.instHasShiftInt	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom CochainComplex.HomComplex.CohomologyClass EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivOfIsKProjective Function.surjInv toSmallShiftedHom Function.Bijective.surjective bijective_toSmallShiftedHom_of_isKProjective	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian

CochainComplex.IsKProjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Qh_map_bijective 📖	mathematical	—	Function.Bijective Quiver.Hom HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryHomotopyCategory CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup HomologicalComplex.instCategory HomotopyCategory.quotient DerivedCategory DerivedCategory.instCategory DerivedCategory.Qh CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ObjectProperty.leftOrthogonal.map_bijective_of_isTriangulated HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic HomotopyCategory.instIsTriangulatedIntUp leftOrthogonal DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic

---

← Back to Index