unit_app_tensor_comp_map_δ — Mathlib

English

In a monoidal adjunction, the unit at X⊗Y composed with G.map(δ F X Y) equals (unit at X ⊗ unit at Y) composed with μ G X Y.

Русский

В моноидальном сопряжении единица на X⊗Y, затем композиция через G.map(δ F X Y), равна (единица X ⊗ единица Y) затем μ_G X Y.

LaTeX

$$$\\mathrm{adj}.\\mathrm{unit}.app(X \\otimes Y) \\circ G(\\\\delta F X Y) = (\\\\mathrm{adj}.\\mathrm{unit}.app X \\otimes_ M \\\\mathrm{adj}.\\mathrm{unit}.app Y) \\circ μ G X Y$$$

Lean4

@[reassoc]
theorem unit_app_tensor_comp_map_δ (X Y : C) :
    adj.unit.app (X ⊗ Y) ≫ G.map (δ F X Y) = (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G _ _ :=
  by
  rw [IsMonoidal.leftAdjoint_μ (adj := adj), homEquiv_unit]
  dsimp
  simp [← adj.unit_naturality_assoc, ← Functor.map_comp, ← δ_natural_assoc]

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