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 : C → D)
:
Type (maxv₁v₂u₁u₂)
A functorial map extends to an action on morphisms.
A functorial map preserves identities.
A functorial map preserves composition of morphisms.
A unbundled functor.
Instances
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
@[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}
:
@[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)
@[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
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 }
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
@[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
- CategoryTheory.functorial_id = CategoryTheory.Functorial.mk fun {X Y} f => f
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.