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 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 HomologicalComplex.instCategory HomologicalComplex.quasiIso CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid CochainComplex.instHasShiftInt	DFunLike.coe Equiv CategoryTheory.Localization.SmallShiftedHom 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 HomologicalComplex.quasiIso 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 CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.ShiftedHom DerivedCategory instCategoryDerivedCategory 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 AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom AddEquiv.instEquivLike AddEquiv.symm CochainComplex.HomComplex.Cocycle.equivHomShift	—	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 CategoryTheory.categoryWithHomology_of_abelian AddRightCancelSemigroup.toIsRightCancelAdd DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp
toSmallShiftedHom_mk 📖	mathematical	CategoryTheory.Localization.HasSmallLocalizedShiftedHom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 HomologicalComplex.instCategory HomologicalComplex.quasiIso CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid CochainComplex.instHasShiftInt	toSmallShiftedHom CategoryTheory.Abelian.toPreadditive CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 HomologicalComplex.quasiIso 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 CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid CochainComplex.instHasShiftInt DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm CochainComplex.HomComplex.Cocycle.equivHomShift	—	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 CategoryTheory.categoryWithHomology_of_abelian

---

← Back to Index