Functors #
Defines a functor between categories, extending a Prefunctor
between quivers.
Introduces notation C ⥤ D⥤ D
for the type of all functors from C
to D
.
(Unfortunately the ⇒⇒
arrow (\functor
) is taken by core,
but in mathlib4 we should switch to this.)
A functor preserves identity morphisms.
map_id : autoParam (∀ (X : C), Prefunctor.map toPrefunctor (𝟙 X) = 𝟙 (Prefunctor.obj toPrefunctor X)) _auto✝A functor preserves composition.
map_comp : autoParam (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), Prefunctor.map toPrefunctor (f ≫ g) = Prefunctor.map toPrefunctor f ≫ Prefunctor.map toPrefunctor g) _auto✝
Functor C D
represents a functor between categories C
and D
.
To apply a functor F
to an object use F.obj X
, and to a morphism use F.map f
.
The axiom map_id
expresses preservation of identities, and
map_comp
expresses functoriality.
See https://stacks.math.columbia.edu/tag/001B.
Instances For
This unexpander will pretty print F.obj X
properly.
Without this, we would have Prefunctor.obj F.toPrefunctor X
.
Equations
- One or more equations did not get rendered due to their size.
This unexpander will pretty print F.map f
properly.
Without this, we would have Prefunctor.map F.toPrefunctor f
.
Equations
- One or more equations did not get rendered due to their size.
Notation for a functor between categories.
Equations
- CategoryTheory.«term_⥤_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_⥤_ 26 27 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤ ") (Lean.ParserDescr.cat `term 26))
𝟭 C
is the identity functor on a category C
.
Equations
- 𝟭 C = CategoryTheory.Functor.mk { obj := fun X => X, map := fun {X Y} f => f }
Notation for the identity functor on a category.
Equations
- CategoryTheory.Functor.«term𝟭» = Lean.ParserDescr.node `CategoryTheory.Functor.term𝟭 1024 (Lean.ParserDescr.symbol "𝟭")
Equations
- CategoryTheory.Functor.instInhabitedFunctor C = { default := 𝟭 C }
F ⋙ G⋙ G
is the composition of a functor F
and a functor G
(F
first, then G
).
Equations
- F ⋙ G = CategoryTheory.Functor.mk { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }
Notation for composition of functors.
Equations
- One or more equations did not get rendered due to their size.