English
The mates equivalence preserves vertical composition of squares (vcomp) in a particular arrangement.
Русский
Эквивалентность мэйтов сохраняет вертикальную композицию квадратов.
LaTeX
$$$\\mathrm{mateEquiv\\_vcomp}$ preserves $\\mathrm{vcomp}$$$
Lean4
/-- The mates equivalence commutes with composition of squares of squares. These results form the
basis for an isomorphism of double categories to be proven later.
-/
theorem mateEquiv_square (α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) (β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) (γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂)
(δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂) :
(mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) (leftAdjointSquare.comp α β γ δ) =
rightAdjointSquare.comp (mateEquiv adj₁ adj₃ α) (mateEquiv adj₂ adj₄ β) (mateEquiv adj₃ adj₅ γ)
(mateEquiv adj₄ adj₆ δ) :=
by
have vcomp :=
mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆) (leftAdjointSquare.hcomp α β)
(leftAdjointSquare.hcomp γ δ)
have hcomp1 := mateEquiv_hcomp adj₁ adj₃ adj₂ adj₄ α β
have hcomp2 := mateEquiv_hcomp adj₃ adj₅ adj₄ adj₆ γ δ
rw [hcomp1, hcomp2] at vcomp
exact vcomp
