δ_naturalityᵣ — Mathlib

English

A left-compatibility form of δ with respect to a morphism f and X in C.

Русский

Левая совместимость δ с отображением f и X.

LaTeX

$$$ (\\delta F m n).app X \\circ (F.obj n).map ((F.map f).app X) = (F.map (m ▷ g)).app X \\circ (\\delta F m' n).app X $$$

Lean4

@[reassoc (attr := simp)]
theorem δ_naturalityᵣ {m n n' : M} (g : n ⟶ n') (X : C) [F.OplaxMonoidal] :
    (δ F m n).app X ≫ (F.map g).app ((F.obj m).obj X) = (F.map (m ◁ g)).app X ≫ (δ F m n').app X :=
  congr_app (δ_natural_right F m g) X

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