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

ink

class CategoryTheory.Functorial {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C → D) : 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.

ink

def CategoryTheory.map {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C → D) [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

• CategoryTheory.map F f = CategoryTheory.Functorial.map' f

ink

@[simp]

theorem CategoryTheory.map'_as_map {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C → D} [inst : CategoryTheory.Functorial F] {X : C} {Y : C} {f : X ⟶ Y} : CategoryTheory.Functorial.map' f = CategoryTheory.map F f

ink

@[simp]

theorem CategoryTheory.Functorial.map_id {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C → D} [inst : CategoryTheory.Functorial F] {X : C} : CategoryTheory.map F (𝟙 X) = 𝟙 (F X)

ink

@[simp]

theorem CategoryTheory.Functorial.map_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C → D} [inst : CategoryTheory.Functorial F] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} : CategoryTheory.map F (f ≫ g) = CategoryTheory.map F f ≫ CategoryTheory.map F g

ink

def CategoryTheory.Functor.of {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C → D) [I : CategoryTheory.Functorial F] : C ⥤ D

Bundle a functorial function as a functor.

Equations

• CategoryTheory.Functor.of F = CategoryTheory.Functor.mk { obj := F, map := fun {X Y} => CategoryTheory.map F }

ink

instance CategoryTheory.instFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctor {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) : CategoryTheory.Functorial F.toPrefunctor.obj

Equations

• CategoryTheory.instFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctor F = CategoryTheory.Functorial.mk fun {X Y} => Prefunctor.map F.toPrefunctor

ink

@[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

ink

instance CategoryTheory.functorial_id {C : Type u₁} [inst : CategoryTheory.Category C] : CategoryTheory.Functorial id

Equations

• CategoryTheory.functorial_id = CategoryTheory.Functorial.mk fun {X Y} f => f

ink

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 : C → D) [inst : CategoryTheory.Functorial F] (G : D → E) [inst : CategoryTheory.Functorial G] : CategoryTheory.Functorial (G ∘ F)

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.