curriedAction — Mathlib

English

Let x be an object of C and f : y → z in D be an isomorphism. The inverse of the right action morphism x ⊴ᵣ f equals x ⊴ᵣ inv f.

Русский

Пусть x — объект C, а f : y → z в D — изоморфизм. Обратное к правому отображению действия равно x ⊴ᵣ inv f.

LaTeX

$$inv (x ⊴ᵣ f) = x ⊴ᵣ inv f$$

Lean4

/-- Bundle the action of `C` on `D` as a functor `C ⥤ D ⥤ D`. -/
@[simps!]
def curriedAction : C ⥤ D ⥤ D
    where
  obj
    x :=
    { obj y := x ⊙ₗ y
      map f := x ⊴ₗ f }
  map
    f :=
    { app y := f ⊵ₗ y
      naturality _ _ _ := by simp [action_exchange] }

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