conjugateEquiv_apply — Mathlib

English

Applies conjugateEquiv to α to give an explicit composite in terms of adjunctions and units/counits.

Русский

Применяет conjugateEquiv к α, получая явную композицию через adjunction и единицы/ counit.

LaTeX

$$$\\mathrm{conjugateEquiv}\\ adj_1\\ adj_2 \\alpha = (\\rho_{r_1}).inv \\circ (r_1 \\curvearrowleft adj_2.unit) \\circ (r_1 \\curvearrowleft \\alpha \\rangle r_2) \\circ (\\alpha_{d c d}).inv \\circ (adj_1.counit \\curvearrowright r_2) \\circ (\\lambda_{r_2}).hom$$$

Lean4

theorem conjugateEquiv_apply (α : l₂ ⟶ l₁) :
    conjugateEquiv adj₁ adj₂ α = (ρ_ r₁).inv ≫ mateEquiv adj₁ adj₂ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫ (λ_ r₂).hom :=
  rfl

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