Documentation

Mathlib.CategoryTheory.Functor.Functorial

Unbundled functors, as a typeclass decorating the object-level function. #

class CategoryTheory.Functorial {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : CD) :
Type (maxv₁v₂u₁u₂)
  • A functorial map extends to an action on morphisms.

    map' : {X Y : C} → (X Y) → (F X F Y)
  • A functorial map preserves identities.

    map_id' : autoParam (∀ (X : C), map' X X (𝟙 X) = 𝟙 (F X)) _auto✝
  • A functorial map preserves composition of morphisms.

    map_comp' : autoParam (∀ {X Y Z : C} (f : X Y) (g : Y Z), map' X Z (f g) = map' X Y f map' Y Z g) _auto✝

A unbundled functor.

Instances
    def CategoryTheory.map {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : CD) [inst : CategoryTheory.Functorial F] {X : C} {Y : C} (f : X Y) :
    F X F Y

    If F : C → D→ D (just a function) has [Functorial F], we can write map F f : F X ⟶ F Y⟶ F Y for the action of F on a morphism f : X ⟶ Y⟶ Y.

    Equations
    @[simp]
    theorem CategoryTheory.map'_as_map {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : CD} [inst : CategoryTheory.Functorial F] {X : C} {Y : C} {f : X Y} :
    @[simp]
    theorem CategoryTheory.Functorial.map_id {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : CD} [inst : CategoryTheory.Functorial F] {X : C} :
    @[simp]
    theorem CategoryTheory.Functorial.map_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : CD} [inst : CategoryTheory.Functorial F] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} :
    def CategoryTheory.Functor.of {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : CD) [I : CategoryTheory.Functorial F] :
    C D

    Bundle a functorial function as a functor.

    Equations
    @[simp]
    theorem CategoryTheory.map_functorial_obj {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) {X : C} {Y : C} (f : X Y) :
    CategoryTheory.map F.toPrefunctor.obj f = F.map f
    Equations
    def CategoryTheory.functorial_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : CD) [inst : CategoryTheory.Functorial F] (G : DE) [inst : CategoryTheory.Functorial G] :

    G ∘ F∘ F is a functorial if both F and G are.

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