ev_coev — Mathlib

English

The evaluation and coevaluation satisfy a standard triangle identity in the adjunction ihom A.

Русский

Оценка и кооценка удовлетворяют стандартному треугольному тождеству в сопряжении ihom A.

LaTeX

$$$ \\text{ev}_A \\circ (coev_A) = \\mathrm{id} $$$

Lean4

@[reassoc (attr := simp)]
theorem ev_coev : (A ◁ (coev A).app B) ≫ (ev A).app (A ⊗ B) = 𝟙 (A ⊗ B) :=
  (ihom.adjunction A).left_triangle_components _

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