conjugateEquiv_adjunction_id — Mathlib

English

For left adjoint l and right adjoint r with adjunction, conjugating with the identity adjunction yields a simple expression: conjugateEquiv adj (Id c) α = (ρ_ _).hom ≫ r ◁ α ≫ adj.counit when α is a morphism 𝟙_c ⟶ l.

Русский

При сопряжении adj и идентичности дают простое выражение: conjugateEquiv adj (Id c) α = (ρ_ _).hom ≫ r ◁ α ≫ adj.counit для α: 𝟙_c ⟶ l.

LaTeX

$$$$ \\text{conjugateEquiv } adj\\ (Adjunction.id\\ c)\\ α = (\\rho_\\_).hom \\; ∘\\; (r \\triangleleft α) \\; ∘\\; adj.counit. $$$$

Lean4

theorem conjugateEquiv_adjunction_id {l r : c ⟶ c} (adj : l ⊣ r) (α : 𝟙 c ⟶ l) :
    (conjugateEquiv adj (Adjunction.id c) α) = (ρ_ _).inv ≫ r ◁ α ≫ adj.counit :=
  by
  rw [conjugateEquiv_apply, mateEquiv_apply']
  dsimp [Adjunction.id]
  bicategory

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