functor — Mathlib

English

The standard equivalence between Action V G and the functor category is established by certain functors and natural isomorphisms.

Русский

Стандартное эквивалентность между категориальными действиями и категорией функторов устанавливается через соответствующие функторы и естественные изоморфизмы.

LaTeX

$$$\text{Equivalence}(\mathrm{Action}\, V G, \mathrm{Funct}(\mathbf{SingleObj}(G),V))$$$

Lean4

/-- Auxiliary definition for `functorCategoryEquivalence`. -/
@[simps]
def functor : Action V G ⥤ SingleObj G ⥤ V
    where
  obj
    M :=
    { obj := fun _ => M.V
      map := fun g => M.ρ g
      map_id := fun _ => M.ρ.map_one
      map_comp := fun g h => M.ρ.map_mul h g }
  map
    f :=
    { app := fun _ => f.hom
      naturality := fun _ _ g => f.comm g }

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