coev_ev — Mathlib

English

The coevaluation and evaluation compose to the identity, forming the other triangle identity of the adjunction ihom.

Русский

Кооценка и оценка композиционно составляют тождество, образуя другую сторону треугольного тождества сопряжения ihom.

LaTeX

$$$ (coev A).app (A ⟶[C] B) \\circ (ev A).app B = \\mathrm{id} (A ⟶[C] B) $$$

Lean4

@[reassoc (attr := simp)]
theorem coev_ev : (coev A).app (A ⟶[C] B) ≫ (ihom A).map ((ev A).app B) = 𝟙 (A ⟶[C] B) :=
  Adjunction.right_triangle_components (ihom.adjunction A) _

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