instIsMonoidalCounit — Mathlib

English

If F ⊣ G is an adjunction forming an equivalence e : C ≌ D with monoidal functor and lax monoidal inverse, then the unit morphism is monoidal.

Русский

Если пара F ⊣ G образует эквивалентность e : C ≌ D с моноидальным функтором и лаксомонильной обратной, то единичное отображение моноидально.

LaTeX

$$IsMonoidal(adj.unit)$$

Lean4

instance : NatTrans.IsMonoidal adj.counit
    where
  unit := by
    dsimp
    rw [assoc, map_ε_comp_counit_app_unit adj, ε_η]
  tensor X
    Y := by
    dsimp
    rw [assoc, map_μ_comp_counit_app_tensor, μ_δ_assoc, comp_id]

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