map_δ_μ — Mathlib

English

Let F: C → D be a monoidal functor and G: D → C′ any functor. Then for all objects X, Y in C, the composite G.map(δ F X Y) followed by G.map(μ F X Y) is the identity on G(F(X ⊗ Y)).

Русский

Пусть F: C → D — моноидальный функтор, G: D → C′ произвольный функтор. Тогда для любых объектов X, Y в C композиция G.map(δ F X Y) затем G.map(μ F X Y) даёт тождество на G(F(X ⊗ Y)).

LaTeX

$$$$ G\\big(\\delta_F(X,Y)\\big) \\circ G\\big(\\mu_F(X,Y)\\big) = \\mathrm{id}_{G\\big(F(X \\otimes Y)\\big)} $$$$

Lean4

@[reassoc (attr := simp)]
theorem map_δ_μ (G : D ⥤ C') (X Y : C) : G.map (δ F X Y) ≫ G.map (μ F X Y) = 𝟙 _ :=
  (μIso F X Y).map_inv_hom_id G

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