conjugateEquiv_symm_id

Mathlib.CategoryTheory.Adjunction.Mates

URI: https://scilib.ai/kg/mathlib#CategoryTheory.conjugateEquiv_symm_id

← MathLib Explorer

English

ConjugateEquiv adj Adjunction.id α yields a certain equality involving counit.

Русский

ConjugateEquiv adj Adjunction.id α даёт равенство, связанное с counit.

LaTeX

$$$$ (\\text{conjugateEquiv } adj Adjunction.id α).app c = α.app (R.obj c) \\\\; $$$$

Lean4

@[simp]
theorem conjugateEquiv_symm_id : (conjugateEquiv adj₁ adj₁).symm (𝟙 _) = 𝟙 _ :=
  by
  rw [Equiv.symm_apply_eq]
  simp only [conjugateEquiv_id]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru