SmallShiftedHom

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

Statistics

Metric	Count
Definitions toSmallShiftedHom	1
Theorems equiv_toSmallShiftedHom_mk, toSmallShiftedHom_mk	2
Total	3

CochainComplex.HomComplex.CohomologyClass

Definitions

Name	Category	Theorems
toSmallShiftedHom 📖	CompOp	8 math math: equivOfIsKInjective_apply, bijective_toSmallShiftedHom_of_isKProjective, bijective_toSmallShiftedHom_of_isKInjective, toSmallShiftedHom_mk, equivOfIsKInjective_symm_apply, equiv_toSmallShiftedHom_mk, equivOfIsKProjective_symm_apply, equivOfIsKProjective_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_toSmallShiftedHom_mk 📖	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 AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShiftedHom DerivedCategory DerivedCategory.instCategory DerivedCategory.instHasShiftInt CategoryTheory.Functor.obj DerivedCategory.Q EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Localization.SmallShiftedHom.equiv DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp DerivedCategory.instCommShiftCochainComplexIntQ toSmallShiftedHom CategoryTheory.ShiftedHom.map AddEquiv CochainComplex.HomComplex.Cocycle Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom AddEquiv.instEquivLike AddEquiv.symm CochainComplex.HomComplex.Cocycle.equivHomShift	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp
toSmallShiftedHom_mk 📖	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	toSmallShiftedHom CochainComplex AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm CochainComplex.HomComplex.Cocycle.equivHomShift	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian

---

← Back to Index