mateEquiv_apply' — Mathlib

English

The mateEquiv bijection applied to α equals a specified composite built from adjunctions and whiskering.

Русский

Применение биекции mateEquiv к α равно определённой композиции, построенной из адъюнкций и подстановок.

LaTeX

$$$\\mathrm{mateEquiv}\\ adj_1 adj_2 \\alpha = \\text{(explicit composite)}$$$

Lean4

theorem mateEquiv_apply' (α : g ≫ l₂ ⟶ l₁ ≫ h) :
    mateEquiv adj₁ adj₂ α = 𝟙 _ ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 _ :=
  by
  rw [mateEquiv_apply, Adjunction.homEquiv₂_apply, Adjunction.homEquiv₁_apply]
  bicategory

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