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

---

← Back to Index