mateEquiv_comp_id_right — Mathlib

English

The mates equivalence is compatible with composing two adjunction squares into a bigger square.

Русский

Эквивалентность мэйтов совместима с композицией двух квадратов сопряжений в больший квадрат.

LaTeX

$$$\\mathrm{mateEquiv}\\ (adj_1\\,\\, adj_3)\\ (adj_2\\,\\, adj_4) \\bigl( \\mathrm{leftAdjointSquare.comp} \\alpha \\beta \\gamma \\delta \\bigr) = \\mathrm{rightAdjointSquare.comp} (\\mathrm{mateEquiv}\\ adj_1 adj_2 \\alpha) (\\mathrm{mateEquiv}\\ adj_3 adj_4 \\beta) (\\mathrm{mateEquiv}\\ adj_2 adj_3 \\gamma) (\\mathrm{mateEquiv}\\ adj_4 adj_6 \\delta)$$$$

Lean4

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

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