conjugateEquiv_counit — Mathlib

English

If you take conjugateEquiv with the identity adjunction, it reduces to the identity on L.

Русский

Если взять conjugateEquiv с тождественной сопряженностью, получаем тождественный изоморфизм.

LaTeX

$$$$\\big(\\text{conjugateEquiv } adj \\; Adjunction.id \\; \\text{on } \\alpha\\big) = \\alpha.$$$$

Lean4

/-- A component of a transposed form of the conjugation definition. -/
theorem conjugateEquiv_counit (α : L₂ ⟶ L₁) (d : D) :
    L₂.map ((conjugateEquiv adj₁ adj₂ α).app _) ≫ adj₂.counit.app d = α.app _ ≫ adj₁.counit.app d := by simp

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