δ_naturality — Mathlib

English

δ is natural with respect to f; the naturality condition aligns δ with the action of F on morphisms in M.

Русский

δ естественно по f; условие натурализма согласует δ с действием F на отображения в M.

LaTeX

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

Lean4

@[reassoc]
theorem δ_naturality {m n : M} {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal] :
    (δ F m n).app X ≫ (F.obj n).map ((F.obj m).map f) = (F.obj _).map f ≫ (δ F m n).app Y := by
  simp
    -- This is not a simp lemma since it could be proved by the lemmas later.

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