rightAdjointUniq_refl — Mathlib

English

For any adjunction F ⊣ G, the rightAdjointUniq hom is the identity when both arguments are equal: (rightAdjointUniq adj1 adj1).hom = 𝟙.

Русский

Для любой пары F ⊣ G, если обе стороны совпадают, то правый уникальный морфизм является тождественным: (rightAdjointUniq adj1 adj1).hom = 𝟙.

LaTeX

$$$$ (rightAdjointUniq adj1 adj1).hom = \mathrm{Id}, $$$$

Lean4

@[simp]
theorem rightAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) : (rightAdjointUniq adj1 adj1).hom = 𝟙 _ :=
  by
  delta rightAdjointUniq
  simp

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