KInjective

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

Statistics

Metric	Count
Definitions equivOfIsKInjective	1
Theorems bijective_toSmallShiftedHom_of_isKInjective, equivOfIsKInjective_apply, equivOfIsKInjective_symm_apply, Qh_map_bijective	4
Total	5

CochainComplex.HomComplex.CohomologyClass

Definitions

Name	Category	Theorems
equivOfIsKInjective 📖	CompOp	2 math math: equivOfIsKInjective_apply, equivOfIsKInjective_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_toSmallShiftedHom_of_isKInjective 📖	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.IsKInjective.Qh_map_bijective CochainComplex.instIsKInjectiveObjIntShiftFunctor toHom_bijective
equivOfIsKInjective_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 equivOfIsKInjective toSmallShiftedHom	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Localization.HasSmallLocalizedHom.small CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor
equivOfIsKInjective_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 equivOfIsKInjective Function.surjInv toSmallShiftedHom Function.Bijective.surjective bijective_toSmallShiftedHom_of_isKInjective	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian

CochainComplex.IsKInjective

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 HomologicalComplex.instCategory HomotopyCategory.quotient DerivedCategory DerivedCategory.instCategory DerivedCategory.Qh CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ObjectProperty.rightOrthogonal.map_bijective_of_isTriangulated HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic HomotopyCategory.instIsTriangulatedIntUp rightOrthogonal DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic

---

← Back to Index