Functors

Defines a functor between categories, extending a Prefunctor between quivers.

Introduces, in the CategoryTheory scope, notations C ⥤ D for the type of all functors from C to D, 𝟭 for the identity functor and ⋙ for functor composition.

TODO: Switch to using the ⇒ arrow.

structure CategoryTheory.Functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] extends Prefunctor : Type (max v₁ v₂ u₁ u₂)

• obj : C → D
• map : {X Y : C} → (X ⟶ Y) → (s.obj X ⟶ s.obj Y)
• map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)

  A functor preserves identity morphisms.

• map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)

  A functor preserves composition.

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.

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

theorem CategoryTheory.Functor.map_comp_assoc {C : Type u₁} [CategoryTheory.Category.{u_1, u₁} C] {D : Type u₂} [CategoryTheory.Category.{u_2, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {W : D} (h : F.obj Z ⟶ W) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) h)

def CategoryTheory.Functor.id (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Functor C C

𝟭 C is the identity functor on a category C.

Equations

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

def CategoryTheory.«term𝟭» : Lean.ParserDescr

Notation for the identity functor on a category.

Equations

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

instance CategoryTheory.Functor.instInhabitedFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : Inhabited (CategoryTheory.Functor C C)

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

F ⋙ G is the composition of a functor F and a functor G (F first, then G).

Equations

• CategoryTheory.Functor.comp F G = CategoryTheory.Functor.mk { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f) }

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

Notation for composition of functors.

Equations

• CategoryTheory.«term_⋙_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_⋙_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋙ ") (Lean.ParserDescr.cat `term 80))

@[simp]

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

theorem CategoryTheory.Functor.comp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor.comp F (CategoryTheory.Functor.id D) = F

theorem CategoryTheory.Functor.id_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor.comp (CategoryTheory.Functor.id C) F = F

@[simp]

theorem CategoryTheory.Functor.map_dite {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {P : Prop} [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)

@[simp]

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