unit_naturality — Mathlib

English

Naturalness of the unit with respect to morphisms f: x → x' and g: y → y' expresses commutativity of the unit with respect to the Day convolution map, i.e., the unit is compatible with maps in both variables.

Русский

Натуральность единицы по отношению к отображениям f: x → x' и g: y → y' выражает совместимость единицы с отображениями в обеих переменных для Day-конволюции.

LaTeX

$$$ (F.map f \\otimes G.map g) \\; \\circ \\; (\\text{unit } F G)_{(x',y')} = (\\text{unit } F G)_{(x,y)} \\circ (F \\⊛ G)_{(f,g)} $$$

Lean4

@[reassoc (attr := simp)]
theorem unit_naturality (f : x ⟶ x') (g : y ⟶ y') :
    (F.map f ⊗ₘ G.map g) ≫ (unit F G).app (x', y') = (unit F G).app (x, y) ≫ (F ⊛ G).map (f ⊗ₘ g) := by
  simpa [tensorHom_def] using (unit F G).naturality (f ×ₘ g)

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