map_ε_comp_counit_app_unit — Mathlib

English

Compatibility identity between ε and η under the adjunction: F.map(ε G) composed with counit at identity equals η F.

Русский

Совместимость ε и η при сопряжении: F.map(ε G) ∘ counit(Id_D) = η F.

LaTeX

$$$F(\\\\varepsilon_G) \\\\circ adj.counit.app(\\\\mathbf{1}_D) = η F$$$

Lean4

@[reassoc]
theorem map_ε_comp_counit_app_unit : F.map (ε G) ≫ adj.counit.app (𝟙_ D) = η F := by
  rw [IsMonoidal.leftAdjoint_ε (adj := adj), homEquiv_unit, map_comp, assoc, counit_naturality,
    left_triangle_components_assoc]

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