Mathlib.CategoryTheory.Functor.Basic

CategoryTheory.Functor structure

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

Full source

/-- `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. -/
@[stacks 001B]
structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] :
    Type max v₁ v₂ u₁ u₂
    extends Prefunctor C D where
  /-- A functor preserves identity morphisms. -/
  map_id : ∀ X : C, map (𝟙 X) = 𝟙 (obj X) := by aesop_cat
  /-- A functor preserves composition. -/
  map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g := by aesop_cat

Functor between categories

Informal description

A functor $ F $ between categories $ C $ and $ D $ consists of: - A map $ F.obj $ sending objects $ X $ of $ C $ to objects $ F.obj X $ of $ D $. - A map $ F.map $ sending morphisms $ f : X \to Y $ in $ C $ to morphisms $ F.map f : F.obj X \to F.obj Y $ in $ D $. The functor must satisfy: 1. **Identity preservation**: $ F.map (\text{id}_X) = \text{id}_{F.obj X} $ for all objects $ X $ in $ C $. 2. **Composition preservation**: $ F.map (g \circ f) = F.map g \circ F.map f $ for all composable morphisms $ f, g $ in $ C $.

CategoryTheory.term_⥤_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for a functor between categories. -/
-- A functor is basically a function, so give ⥤ a similar precedence to → (25).
-- For example, `C × D ⥤ E` should parse as `(C × D) ⥤ E` not `C × (D ⥤ E)`.
scoped [CategoryTheory] infixr:26 " ⥤ " => Functor

Functor notation (`⥤`)

Informal description

The notation `C ⥤ D` denotes the type of functors from category `C` to category `D`, where a functor is a structure that extends a prefunctor (a map between the underlying quivers) and preserves the categorical structure (composition and identities). The notation has right associativity with precedence level 26, ensuring that expressions like `C × D ⥤ E` are parsed as `(C × D) ⥤ E` rather than `C × (D ⥤ E)`.

CategoryTheory.Functor.map_comp_assoc theorem

 {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : C ⥤ D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {W : D}
  (h : F.obj Z ⟶ W) : (F.map (f ≫ g)) ≫ h = F.map f ≫ F.map g ≫ h

Full source

lemma Functor.map_comp_assoc {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : C ⥤ D)
    {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {W : D} (h : F.obj Z ⟶ W) :
    (F.map (f ≫ g)) ≫ h = F.map f ≫ F.map g ≫ h := by
  rw [F.map_comp, Category.assoc]

Associativity of Functor Composition with Post-Composition

Informal description

Let $ C $ and $ D $ be categories, and let $ F : C \to D $ be a functor. For any objects $ X, Y, Z $ in $ C $ and morphisms $ f : X \to Y $, $ g : Y \to Z $, and any morphism $ h : F(Z) \to W $ in $ D $, the following equality holds: \[ F(f \circ g) \circ h = F(f) \circ F(g) \circ h. \]

CategoryTheory.Functor.id definition

: C ⥤ C

Full source

/-- `𝟭 C` is the identity functor on a category `C`. -/
protected def id : C ⥤ C where
  obj X := X
  map f := f

Identity functor

Informal description

The identity functor on a category $ C $ is the functor that maps every object $ X $ in $ C $ to itself and every morphism $ f $ in $ C $ to itself. It satisfies the functoriality conditions: 1. **Identity preservation**: The identity morphism on $ X $ is mapped to the identity morphism on $ X $. 2. **Composition preservation**: The composition of morphisms $ f $ and $ g $ is mapped to the composition of their images under the functor.

CategoryTheory.term𝟭 definition

: Lean.ParserDescr✝

Full source

/-- Notation for the identity functor on a category. -/
scoped [CategoryTheory] notation "𝟭" => Functor.id

Identity functor notation

Informal description

The notation `𝟭` denotes the identity functor on a category, which maps every object and morphism to itself.

CategoryTheory.Functor.instInhabited instance

: Inhabited (C ⥤ C)

Full source

instance : Inhabited (C ⥤ C) :=
  ⟨Functor.id C⟩

Inhabited Type of Endofunctors on a Category

Informal description

For any category $C$, the type of functors from $C$ to itself is inhabited by the identity functor.

CategoryTheory.Functor.id_obj theorem

(X : C) : (𝟭 C).obj X = X

Full source

@[simp]
theorem id_obj (X : C) : (𝟭 C).obj X = X := rfl

Identity Functor Preserves Objects

Informal description

For any object $X$ in a category $C$, the application of the identity functor $\mathbf{1}_C$ to $X$ yields $X$ itself, i.e., $(\mathbf{1}_C)(X) = X$.

CategoryTheory.Functor.id_map theorem

{X Y : C} (f : X ⟶ Y) : (𝟭 C).map f = f

Full source

@[simp]
theorem id_map {X Y : C} (f : X ⟶ Y) : (𝟭 C).map f = f := rfl

Identity Functor Preserves Morphisms

Informal description

For any morphism $f \colon X \to Y$ in a category $C$, the identity functor $\mathbf{1}_C$ maps $f$ to itself, i.e., $\mathbf{1}_C(f) = f$.

CategoryTheory.Functor.comp definition

(F : C ⥤ D) (G : D ⥤ E) : C ⥤ E

Full source

/-- `F ⋙ G` is the composition of a functor `F` and a functor `G` (`F` first, then `G`).
-/
@[simps obj]
def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E where
  obj X := G.obj (F.obj X)
  map f := G.map (F.map f)
  map_comp := by intros; rw [F.map_comp, G.map_comp]

Composition of functors

Informal description

The composition of two functors $ F : C \to D $ and $ G : D \to E $ is a functor $ F \circ G : C \to E $ defined by: - On objects: $ (F \circ G)(X) = G(F(X)) $ for any object $ X $ in $ C $. - On morphisms: $ (F \circ G)(f) = G(F(f)) $ for any morphism $ f $ in $ C $. This composition preserves identities and composition of morphisms, i.e., it satisfies: 1. $ (F \circ G)(\text{id}_X) = \text{id}_{G(F(X))} $ for all objects $ X $ in $ C $. 2. $ (F \circ G)(g \circ f) = (F \circ G)(g) \circ (F \circ G)(f) $ for all composable morphisms $ f, g $ in $ C $.

CategoryTheory.term_⋙_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for composition of functors. -/
scoped [CategoryTheory] infixr:80 " ⋙ " => Functor.comp

Functor composition

Informal description

The notation `⋙` denotes the composition of functors in category theory. Given two functors `F : C ⥤ D` and `G : D ⥤ E`, the composition `F ⋙ G` is a functor from `C` to `E` that first applies `F` and then applies `G`.

CategoryTheory.Functor.comp_map theorem

(F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) : (F ⋙ G).map f = G.map (F.map f)

Full source

@[simp]
theorem comp_map (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) :
    (F ⋙ G).map f = G.map (F.map f) := rfl

Functor Composition Preserves Morphism Mapping

Informal description

For any functors $F \colon C \to D$ and $G \colon D \to E$, and any morphism $f \colon X \to Y$ in $C$, the action of the composed functor $F \circ G$ on $f$ satisfies $(F \circ G)(f) = G(F(f))$.

CategoryTheory.Functor.comp_id theorem

(F : C ⥤ D) : F ⋙ 𝟭 D = F

Full source

protected theorem comp_id (F : C ⥤ D) : F ⋙ 𝟭 D = F := by cases F; rfl

Right Identity Law for Functor Composition: $F \circ \text{id}_D = F$

Informal description

For any functor $F \colon C \to D$, the composition of $F$ with the identity functor on $D$ is equal to $F$ itself, i.e., $F \circ \text{id}_D = F$.

CategoryTheory.Functor.id_comp theorem

(F : C ⥤ D) : 𝟭 C ⋙ F = F

Full source

protected theorem id_comp (F : C ⥤ D) : 𝟭𝟭 C ⋙ F = F := by cases F; rfl

Identity Functor Left Unit Law: $1_C \circ F = F$

Informal description

For any functor $F \colon C \to D$ between categories, the composition of the identity functor on $C$ with $F$ is equal to $F$ itself, i.e., $1_C \circ F = F$.

CategoryTheory.Functor.map_dite theorem

 (F : C ⥤ D) {X 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)

Full source

@[simp]
theorem map_dite (F : C ⥤ D) {X 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) := by
  aesop_cat

Functoriality of Conditional Morphisms

Informal description

Let $F \colon C \to D$ be a functor between categories, and let $X, Y$ be objects in $C$. For any decidable proposition $P$ and morphisms $f \colon P \to (X \to Y)$ and $g \colon \neg P \to (X \to Y)$, the functor $F$ preserves the conditional morphism construction: \[ F\left(\text{if } h : P \text{ then } f(h) \text{ else } g(h)\right) = \text{if } h : P \text{ then } F(f(h)) \text{ else } F(g(h)). \]

CategoryTheory.Functor.toPrefunctor_comp theorem

(F : C ⥤ D) (G : D ⥤ E) : F.toPrefunctor.comp G.toPrefunctor = (F ⋙ G).toPrefunctor

Full source

@[simp]
theorem toPrefunctor_comp (F : C ⥤ D) (G : D ⥤ E) :
    F.toPrefunctor.comp G.toPrefunctor = (F ⋙ G).toPrefunctor := rfl

Compatibility of Functor Composition with Underlying Prefunctors

Informal description

For any functors $F \colon C \to D$ and $G \colon D \to E$ between categories, the prefunctor obtained by composing the underlying prefunctors of $F$ and $G$ is equal to the underlying prefunctor of the composition $F \circ G \colon C \to E$. In other words, we have: \[ F_{\text{pre}} \circ G_{\text{pre}} = (F \circ G)_{\text{pre}} \] where $F_{\text{pre}}$ and $G_{\text{pre}}$ denote the underlying prefunctors of $F$ and $G$ respectively.