μ_naturalityᵣ — Mathlib

English

Left-naturality of μ with respect to a morphism f on the left factor and X in C.

Русский

Левая натурализм μ по отношению к морфизму f слева и X в C.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem μ_naturalityᵣ {m n n' : M} (g : n ⟶ n') (X : C) [F.LaxMonoidal] :
    (F.map g).app ((F.obj m).obj X) ≫ (μ F m n').app X = (μ F m n).app X ≫ (F.map (m ◁ g)).app X :=
  by
  rw [← id_tensorHom, ← μ_naturality₂ F (𝟙 m) g X]
  simp

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