Documentation

Mathlib.CategoryTheory.Functor.Functorial

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

class CategoryTheory.Functorial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CD) :
Type (max v₁ v₂ u₁ u₂)

An unbundled functor.

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

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

    Equations
    Instances For

      Bundle a functorial function as a functor.

      Equations
      Instances For
        Equations
        Equations
        • CategoryTheory.functorial_id = { map' := fun {X Y : C} (f : X Y) => f, map_id' := , map_comp' := }

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

        Equations
        Instances For