ext — Mathlib

English

Two adjunctions with the same unit are equal.

Русский

Две сопряжённости с одинаковой единицей равны.

LaTeX

$$$\forall \text{adj}, \text{adj'}: F \dashv G,\ adj.unit = adj'.unit \Rightarrow adj = adj'$$$

Lean4

@[ext]
theorem ext {F : C ⥤ D} {G : D ⥤ C} {adj adj' : F ⊣ G} (h : adj.unit = adj'.unit) : adj = adj' :=
  by
  suffices h' : adj.counit = adj'.counit by cases adj; cases adj'; aesop
  ext X
  apply (adj.homEquiv _ _).injective
  rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit, Adjunction.right_triangle_components, h,
    Adjunction.right_triangle_components]

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