Mathlib Map

Structures · Category theory

CategoryTheory.Functor.Additive

A functor F is additive provided F.map is an additive homomorphism.

Defined in
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Shape
One type argument · adds map_add
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances39

  • CategoryTheory.Functor
  • ModuleCat
  • HomologicalComplex
  • Action
  • AddCommGrpCat
  • CategoryTheory.ObjectProperty.FullSubcategory
  • CategoryTheory.ShrinkHoms
  • Rep
  • SheafOfModules
  • CategoryTheory.Comma
  • HomotopyCategory
  • PresheafOfModules
  • CategoryTheory.MorphismProperty.Localization
  • CategoryTheory.Sheaf
  • CategoryTheory.InducedCategory
  • DerivedCategory
  • AlgebraicGeometry.Scheme.Modules
  • TopCat.Presheaf
  • CategoryTheory.Arrow
  • TopCat.Sheaf
  • CategoryTheory.ShortComplex
  • CategoryTheory.Comonad.Coalgebra
  • CategoryTheory.Monad.Algebra
  • CategoryTheory.Idempotents.Karoubi
  • CategoryTheory.Mat_
  • TopRep
  • CategoryTheory.Endofunctor.Coalgebra
  • CategoryTheory.Endofunctor.Algebra
  • CategoryTheory.OppositeShift
  • CategoryTheory.MorphismProperty.Localization'
  • CategoryTheory.PullbackShift
  • FGModuleCat
  • CategoryTheory.Free
  • CochainComplex
  • CategoryTheory.SimplicialObject
  • CategoryTheory.AsSmall
  • SemiNormedGrp
  • CategoryTheory.AdditiveFunctor
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by1,665

Ancestors0

No ancestors.