δ_natural — Mathlib

English

In an oplax monoidal setting, the coherence morphism δ is natural with respect to tensoring on either side.

Русский

В условии оплакс-монодального функторa δ естественно по отношению к тензорованию слева и справа.

LaTeX

$$$δ F X X' \\;\\circ (f ⊗ f') = F.map (f ⊗ f') \\circ δ F Y Y'$$$

Lean4

@[reassoc (attr := simp)]
theorem δ_natural {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
    δ F X X' ≫ (F.map f ⊗ₘ F.map g) = F.map (f ⊗ₘ g) ≫ δ F Y Y' := by simp [tensorHom_def]

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