inverse — Mathlib

English

Extensionality principle for Action morphisms: equality of underlying maps implies equality of morphisms.

Русский

Принцип экстенсивности для морфизмов действия: равенство подлежащих отображений влечёт равенство морфизмов.

LaTeX

$$$\forall \phi_1 \phi_2 : M \to N, \ (\phi_1.hom = \phi_2.hom) \Rightarrow \phi_1 = \phi_2$$$

Lean4

/-- Auxiliary definition for `functorCategoryEquivalence`. -/
@[simps]
def inverse : (SingleObj G ⥤ V) ⥤ Action V G
    where
  obj
    F :=
    { V := F.obj PUnit.unit
      ρ :=
        { toFun := fun g => F.map g
          map_one' := F.map_id PUnit.unit
          map_mul' := fun g h => F.map_comp h g } }
  map
    f :=
    { hom := f.app PUnit.unit
      comm := fun g => f.naturality g }

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