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₂)
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.
- obj : C → D
- map_id : ∀ (X : C), self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
A functor preserves identity morphisms.
- map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
A functor preserves composition.
@[simp]
theorem
CategoryTheory.Functor.map_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(self : CategoryTheory.Functor C D)
(X : C)
:
self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
A functor preserves identity morphisms.
@[simp]
theorem
CategoryTheory.Functor.map_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(self : CategoryTheory.Functor C D)
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
A functor preserves composition.
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)
𝟭 C is the identity functor on a category C.
Equations
- CategoryTheory.Functor.id C = { obj := fun (X : C) => X, map := fun {X Y : C} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }
Notation for the identity functor on a category.
Equations
- CategoryTheory.«term𝟭» = Lean.ParserDescr.node `CategoryTheory.term𝟭 1024 (Lean.ParserDescr.symbol "𝟭")
Equations
- CategoryTheory.Functor.instInhabited 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)
:
(F.comp 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)
:
F ⋙ G is the composition of a functor F and a functor G (F first, then G).
Equations
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)
:
(F.comp 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)
:
F.comp (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.id C).comp 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)
: