Additive Functors #
A functor between two preadditive categories is called additive provided that the induced map on hom types is a morphism of abelian groups.
An additive functor between preadditive categories creates and preserves biproducts.
Conversely, if F : C ⥤ D
is a functor between preadditive categories, where C
has binary
biproducts, and if F
preserves binary biproducts, then F
is additive.
We also define the category of bundled additive functors.
Implementation details #
Functor.Additive
is a Prop
-valued class, defined by saying that for every two objects X
and
Y
, the map F.map : (X ⟶ Y) → (F.obj X ⟶ F.obj Y)
is a morphism of abelian groups.
A functor F
is additive provided F.map
is an additive homomorphism.
the addition of two morphisms is mapped to the sum of their images
Instances
the addition of two morphisms is mapped to the sum of their images
F.mapAddHom
is an additive homomorphism whose underlying function is F.map
.
Equations
- F.mapAddHom = AddMonoidHom.mk' (fun (f : X ⟶ Y) => F.map f) ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
Bundled additive functors.
Equations
- (C ⥤+ D) = CategoryTheory.FullSubcategory fun (F : CategoryTheory.Functor C D) => F.Additive
Equations
- CategoryTheory.instCategoryAdditiveFunctor C D = CategoryTheory.FullSubcategory.category fun (F : CategoryTheory.Functor C D) => F.Additive
the category of additive functors is denoted C ⥤+ D
Equations
- CategoryTheory.«term_⥤+_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_⥤+_ 26 27 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤+ ") (Lean.ParserDescr.cat `term 26))
Equations
- CategoryTheory.instPreadditiveAdditiveFunctor C D = CategoryTheory.Preadditive.inducedCategory CategoryTheory.FullSubcategory.obj
An additive functor is in particular a functor.
Equations
- CategoryTheory.AdditiveFunctor.forget C D = CategoryTheory.fullSubcategoryInclusion fun (F : CategoryTheory.Functor C D) => F.Additive
Equations
- ⋯ = ⋯
Turn an additive functor into an object of the category AdditiveFunctor C D
.
Equations
- CategoryTheory.AdditiveFunctor.of F = { obj := F, property := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Turn a left exact functor into an additive functor.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Turn a right exact functor into an additive functor.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Turn an exact functor into an additive functor.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯