leftAdjointUniq_refl — Mathlib

English

For any adjunction F ⊣ G, the leftAdjointUniq taken with itself yields the identity: (leftAdjointUniq adj1 adj1).hom = 𝟙.

Русский

Для любой сопряжённости F ⊣ G отражение левогоUniq в самом себе даёт тождественный гомоморфизм: (leftAdjointUniq adj1 adj1).hom = 𝟙.

LaTeX

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

Lean4

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

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