Linear

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

Statistics

Metric	Count
Definitions instLinear	1
Theorems instLinearCochainComplexIntQ, instLinearHomotopyCategoryIntUpQh, instLinearShiftFunctorInt, instLinearSingleFunctor	4
Total	5

DerivedCategory

Definitions

Name	Category	Theorems
instLinear 📖	CompOp	8 math math: CategoryTheory.Abelian.Ext.homLinearEquiv_apply, CategoryTheory.Abelian.Ext.smul_hom, instLinearCochainComplexIntQ, instLinearShiftFunctorInt, instLinearSingleFunctor, instLinearHomotopyCategoryIntUpQh, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLinearCochainComplexIntQ 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd instCategoryDerivedCategory HomologicalComplex.instPreadditive instPreadditive HomologicalComplex.instLinear instLinear Q	—	CategoryTheory.Functor.linear_of_iso AddRightCancelSemigroup.toIsRightCancelAdd 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.Functor.instLinearComp HomotopyCategory.instLinearHomologicalComplexQuotient instLinearHomotopyCategoryIntUpQh
instLinearHomotopyCategoryIntUpQh 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring HomotopyCategory 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 DerivedCategory instCategoryHomotopyCategory instCategoryDerivedCategory HomotopyCategory.instPreadditive instPreadditive HomotopyCategory.instLinear instLinear Qh	—	CategoryTheory.Localization.functor_linear 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 instIsLocalizationHomotopyCategoryIntUpQhQuasiIso instAdditiveHomotopyCategoryIntUpQh
instLinearShiftFunctorInt 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring DerivedCategory instCategoryDerivedCategory instPreadditive instLinear CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt	—	CategoryTheory.Shift.linear_of_localization 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 HomotopyCategory.instLinearIntUpShiftFunctor HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic instLinearHomotopyCategoryIntUpQh
instLinearSingleFunctor 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring DerivedCategory instCategoryDerivedCategory CategoryTheory.Abelian.toPreadditive instPreadditive instLinear singleFunctor	—	—

---

← Back to Index