enrichedFunctorTypeEquivFunctor — Mathlib

English

There is an equivalence between enriched functors from Type v to C and ordinary functors C→D; in particular, enriching over Type v collapses to ordinary functors.

Русский

Существует эквивалентость между обогащёнными функторaми от Type v в C и обычными функторaми C→D; обогащение над Type v приводится к обычным функторaм.

LaTeX

$$$\\text{enrichedFunctorTypeEquivFunctor}:\\; \\text{EnrichedFunctor}(\\mathrm{Type}(v),C,D) \\simeq C \\to D$$$

Lean4

/-- We verify that an enriched functor between `Type v` enriched categories
is just the same thing as an honest functor.
-/
@[simps]
def enrichedFunctorTypeEquivFunctor {C : Type u₁} [𝒞 : EnrichedCategory (Type v) C] {D : Type u₂}
    [𝒟 : EnrichedCategory (Type v) D] : EnrichedFunctor (Type v) C D ≃ C ⥤ D
    where
  toFun
    F :=
    { obj := fun X => F.obj X
      map := fun f => F.map _ _ f
      map_id := fun X => congr_fun (F.map_id X) PUnit.unit
      map_comp := fun f g => congr_fun (F.map_comp _ _ _) ⟨f, g⟩ }
  invFun
    F :=
    { obj := fun X => F.obj X
      map := fun _ _ f => F.map f
      map_id := fun X => by ext ⟨⟩; exact F.map_id X
      map_comp := fun X Y Z => by ext ⟨f, g⟩; exact F.map_comp f g }

Похожие утверждения