map_μ_comp_counit_app_tensor — Mathlib

English

Compatibility of μ with counit on tensor: F.map(μ_G X Y) composed with counit at X⊗Y equals δ_F X Y followed by counit factors.

Русский

Совместимость μ с counit на тензоре: F.map(μ_G X Y) ∘ counit(X⊗Y) = δ F X Y ∘ (counit X ⊗ counit Y).

LaTeX

$$$F.map(\\\\mu_G X Y) \\\\circ adj.counit.app(X \\otimes Y) = δ F X Y \\\\circ (adj.counit.app X \\otimes_? adj.counit.app Y)$$$

Lean4

@[reassoc]
theorem map_μ_comp_counit_app_tensor (X Y : D) :
    F.map (μ G X Y) ≫ adj.counit.app (X ⊗ Y) = δ F _ _ ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y) :=
  by
  rw [IsMonoidal.leftAdjoint_μ (adj := adj), homEquiv_unit]
  simp

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