conjugateEquiv_adjunction_id_symm

English

Symmetry of the previous identity: conjugateEquiv_adjunction_id_symm states (conjugateEquiv adj (Adjunction.id c)).symm α = adj.unit ≫ l ▷ α ≫ (ρ_ _).hom for α: 𝟙 c ⟶ l.

Русский

Симметричная версия: (conjugateEquiv adj (Adjunction.id c)).symm α = adj.unit ≫ l ◁ α ≫ (ρ_ _).hom, для α: 𝟙 c ⟶ l.

LaTeX

$$$$ (\\text{conjugateEquiv } adj (Adjunction.id\\ c)).\\mathrm{symm} \\ α = adj.unit \\,\\gg\\, l \\triangleleft α \\,\\gg\\, (\\rho_\\_).hom. $$$$

Lean4

theorem conjugateEquiv_adjunction_id_symm {l r : c ⟶ c} (adj : l ⊣ r) (α : r ⟶ 𝟙 c) :
    (conjugateEquiv adj (Adjunction.id c)).symm α = adj.unit ≫ l ◁ α ≫ (ρ_ _).hom :=
  by
  rw [conjugateEquiv_symm_apply, mateEquiv_symm_apply']
  dsimp [Adjunction.id]
  bicategory

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