μ_naturality — Mathlib

English

μ satisfies a naturality condition with respect to morphisms in M: the map commutes with F.map f appropriately.

Русский

μ удовлетворяет условию естественности по отображениям в M: отображение commute с F.map f корректно.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem μ_naturality {m n : M} {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] :
    (F.obj n).map ((F.obj m).map f) ≫ (μ F m n).app Y = (μ F m n).app X ≫ (F.obj _).map f :=
  (μ F m n).naturality f

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