conjugateEquiv_apply' — Mathlib

English

A variant of conjugateEquiv_apply giving a more expanded composite form.

Русский

Вариант conjugateEquiv_apply, дающий более развёртую форму композиции.

LaTeX

$$$\\mathrm{conjugateEquiv\\_apply'} (\\alpha) = (\\rho_{r_1}).inv \\circ (r_1 \\curvearrowleft adj_2.unit) \\circ (r_1 \\curvearrowleft \\alpha \\curvearrowright 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₂ α =
      (ρ_ _).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ _ _ _).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ _).hom :=
  by
  rw [conjugateEquiv_apply, mateEquiv_apply']
  bicategory

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