μ_naturalityₗ — Mathlib

English

Another formulation of μ-naturality with respect to morphisms on the second variable and their interaction with tensoring.

Русский

Другая форма μ-натурализма относительно морфизмов на второй переменной и их взаимодействие с тензорованием.

LaTeX

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

Lean4

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

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