comp_hvcomp — Mathlib

English

There is a bijection between squares built from adjunctions that are composed horizontally (a square of squares).

Русский

Существует биекция между квадратами, построенными из adjunctions, которые композиционно образуют квадрат сверху вниз.

LaTeX

$$$\\mathrm{mateEquiv\\_square} : (\\text{adjoints}) \\Rightarrow (\\text{adjoints})$$$

Lean4

/-- Horizontal and vertical composition of squares commutes. -/
theorem comp_hvcomp : comp α β γ δ = hcomp (vcomp α γ) (vcomp β δ) :=
  by
  dsimp only [comp, vcomp, hcomp]
  calc
    _ = 𝟙 _ ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 _ := by bicategory
    _ = _ := by
      rw [← whisker_exchange]
      bicategory

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