mateEquiv_id_comp_right — Mathlib

English

Relates the mateEquiv with a right action by identity and composition on the right.

Русский

Связывает биекцию mateEquiv с действием справа через единичную композицию.

LaTeX

$$$\\mathrm{mateEquiv}(\\_) (f \\;\\text{comp} \\; \\mathrm{Id} \\; \\circ l_2) \\;=\\; \\mathrm{mateEquiv}(\\_) (f \\circ (\\lambda_{l_2})^{-1} \\; \\circ \\varphi) \\;\\text{etc}$$$

Lean4

theorem mateEquiv_id_comp_right (φ : f ≫ 𝟙 _ ≫ l₂ ⟶ l₁ ≫ g) :
    mateEquiv adj₁ ((Adjunction.id _).comp adj₂) φ =
      mateEquiv adj₁ adj₂ (f ◁ (λ_ l₂).inv ≫ φ) ≫ (ρ_ _).inv ≫ (α_ _ _ _).hom :=
  by
  simp only [mateEquiv_apply, Adjunction.homEquiv₁_apply, Adjunction.homEquiv₂_apply, Adjunction.id]
  dsimp
  bicategory

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