comp_hvcomp — Mathlib

English

Horizontal and vertical composition commute for squares in a left adjoint square; the composition equals the horizontal composite of the two compositions.

Русский

Горизонтальная и вертикальная композиции квадратов в левой квадратной схеме согласуются; композиция равна горизонтальной композиции двух композиций.

LaTeX

$$$\\text{comp}_{\\text{hv}}(\\alpha,\\beta,\\gamma,\\delta) = \\text{hcomp}(vcomp(\\alpha,\\gamma), vcomp(\\beta,\\delta))$$$

Lean4

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

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