Structures · Category theory
CategoryTheory.Preadditive
A category is called preadditive if P ⟶ Q is an abelian group such that composition is
linear in both variables.
- Defined in
- Mathlib.CategoryTheory.Preadditive.Basic
- Shape
- One type argument · adds homGroup, add_comp, comp_add
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances38
- CategoryTheory.Functor
- ModuleCat
- HomologicalComplex
- Action
- AddCommGrpCat
- CategoryTheory.ObjectProperty.FullSubcategory
- CategoryTheory.ShrinkHoms
- Rep
- CategoryTheory.Quotient
- SheafOfModules
- CategoryTheory.Ind
- CategoryTheory.Comma
- HomotopyCategory
- PresheafOfModules
- CategoryTheory.MorphismProperty.Localization
- CategoryTheory.InducedCategory
- DerivedCategory
- CategoryTheory.Arrow
- CategoryTheory.ShortComplex
- CategoryTheory.Comonad.Coalgebra
- CategoryTheory.Monad.Algebra
- CategoryTheory.SingleObj
- TopModuleCat
- CategoryTheory.Pretriangulated.Triangle
- CategoryTheory.Idempotents.Karoubi
- CategoryTheory.Mat_
- TopRep
- CategoryTheory.Endofunctor.Coalgebra
- CategoryTheory.Endofunctor.Algebra
- CategoryTheory.OppositeShift
- CategoryTheory.MorphismProperty.Localization'
- CategoryTheory.PullbackShift
- CategoryTheory.Mat
- CategoryTheory.Free
- CategoryTheory.Preadditive.RightFreyd
- CategoryTheory.AsSmall
- SemiNormedGrp
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by4,720
- CochainComplex.HomComplex.Cochain
- CochainComplex.HomComplex.Cochain.v
- CochainComplex.mappingCone
- AlgebraicTopology.AlternatingFaceMapComplex.obj
- HomotopyCategory
- CochainComplex.HomComplex.Cocycle
- CochainComplex.HomComplex.Cochain.ofHom
- CochainComplex.HomComplex.Cochain.comp
- CochainComplex.singleFunctor
- HomologicalComplex.mapBifunctor
- HomotopyCategory.quotient
- CochainComplex.HomComplex.cocycle
- HomologicalComplex₂.HasTotal
- HomologicalComplex.HasMapBifunctor
- CochainComplex.HomComplex.δ
- AlgebraicTopology.DoldKan.PInfty
- CategoryTheory.Triangulated.TStructure.truncGE
- CategoryTheory.Preadditive.add_comp
- CochainComplex.mappingCone.inr
- CategoryTheory.Triangulated.TStructure.truncLT
- HomologicalComplex₂.total
- CategoryTheory.Preadditive.comp_add
- CategoryTheory.Triangulated.TStructure.eTruncLT
- CochainComplex.mappingCone.inl
- HomologicalComplex.homotopyCofiber.X
- CategoryTheory.Triangulated.TStructure.eTruncGE
- CategoryTheory.Triangulated.TStructure.truncGEπ
- CochainComplex.mappingCone.fst
- CochainComplex.shiftFunctor
- CochainComplex.HomComplex.CohomologyClass
- CategoryTheory.Triangulated.TStructure.truncLTι
- CochainComplex.mappingCone.snd
- CochainComplex.mappingCone.triangle
- Homotopy.hom
- CochainComplex.mappingCocone
- CategoryTheory.Triangulated.TStructure.truncLE
- SSet.chainComplex
- CochainComplex.HomComplex.Cochain.ofHom_v
- HomotopyEquiv.hom
- CategoryTheory.Pretriangulated.Triangle.rotate
- HomologicalComplex₂.ιTotal
- AlgebraicTopology.DoldKan.N₁
- CochainComplex.shiftFunctorObjXIso
- CategoryTheory.Pretriangulated.Triangle.invRotate
- HomologicalComplex.ιMapBifunctor
- AlgebraicTopology.DoldKan.P
- CochainComplex.HomComplex.Cochain.v.congr_simp
- CategoryTheory.Linear.comp_units_smul
- CategoryTheory.Triangulated.TStructure.eTruncLTι
- HomotopyCategory.homologyFunctor
Ancestors0
No ancestors.