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.)

ink

structure CategoryTheory.Functor (C : Type u₁) [inst : CategoryTheory.Category C] (D : Type u₂) [inst : CategoryTheory.Category D] extends Prefunctor : Type (maxv₁v₂u₁u₂)

• 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.

ink

def CategoryTheory.unexpandFunctorObj : Lean.PrettyPrinter.Unexpander

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.

ink

def CategoryTheory.unexpandFunctorMap : Lean.PrettyPrinter.Unexpander

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.

ink

def CategoryTheory.«term_⥤_» : Lean.TrailingParserDescr

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))

ink

theorem CategoryTheory.Functor.map_comp_assoc {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (self : C ⥤ D) {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z : D} (h : self.obj Z ⟶ Z) : self.map (f ≫ g) ≫ h = self.map f ≫ self.map g ≫ h

ink

def CategoryTheory.Functor.id (C : Type u₁) [inst : CategoryTheory.Category C] : C ⥤ C

𝟭 C is the identity functor on a category C.

Equations

• 𝟭 C = CategoryTheory.Functor.mk { obj := fun X => X, map := fun {X Y} f => f }

ink

def CategoryTheory.Functor.«term𝟭» : Lean.ParserDescr

Notation for the identity functor on a category.

Equations

• CategoryTheory.Functor.«term𝟭» = Lean.ParserDescr.node `CategoryTheory.Functor.term𝟭 1024 (Lean.ParserDescr.symbol "𝟭")

ink

instance CategoryTheory.Functor.instInhabitedFunctor (C : Type u₁) [inst : CategoryTheory.Category C] : Inhabited (C ⥤ C)

Equations

• CategoryTheory.Functor.instInhabitedFunctor C = { default := 𝟭 C }

ink

@[simp]

theorem CategoryTheory.Functor.id_obj {C : Type u₁} [inst : CategoryTheory.Category C] (X : C) : (𝟭 C).obj X = X

ink

@[simp]

theorem CategoryTheory.Functor.id_map {C : Type u₁} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X ⟶ Y) : (𝟭 C).map f = f

ink

@[simp]

theorem CategoryTheory.Functor.comp_obj {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C ⥤ D) (G : D ⥤ E) (X : C) : (F ⋙ G).obj X = G.obj (F.obj X)

ink

def CategoryTheory.Functor.comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E

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) }

ink

def CategoryTheory.Functor.«term_⋙_» : Lean.TrailingParserDescr

Notation for composition of functors.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem CategoryTheory.Functor.comp_map {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C ⥤ D) (G : D ⥤ E) {X : C} {Y : C} (f : X ⟶ Y) : (F ⋙ G).map f = G.map (F.map f)

ink

theorem CategoryTheory.Functor.comp_id {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) : F ⋙ 𝟭 D = F

ink

theorem CategoryTheory.Functor.id_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) : 𝟭 C ⋙ F = F

ink

@[simp]

theorem CategoryTheory.Functor.map_dite {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) {X : C} {Y : C} {P : Prop} [inst : Decidable P] (f : P → (X ⟶ Y)) (g : ¬P → (X ⟶ Y)) : F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)

ink

@[simp]

theorem CategoryTheory.Functor.toPrefunctor_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C ⥤ D) (G : D ⥤ E) : F.toPrefunctor ⋙q G.toPrefunctor = (F ⋙ G).toPrefunctor