conjugateEquiv_adjunction_id — Mathlib

English

Symmetry of conjugateEquiv with identity adjunction for the symmetrized map.

Русский

Симметрия conjugateEquiv с тождественной сопряжённостью для симметризированной карты.

LaTeX

$$$$ (conjugateEquiv adj Adjunction.id).symm (id) = id $$$$

Lean4

theorem conjugateEquiv_adjunction_id {L R : C ⥤ C} (adj : L ⊣ R) (α : 𝟭 C ⟶ L) (c : C) :
    (conjugateEquiv adj Adjunction.id α).app c = α.app (R.obj c) ≫ adj.counit.app c := by
  simp [conjugateEquiv, mateEquiv, Adjunction.id]

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