English
The mates equivalence commutes with vertical composition of squares.
Русский
Эквивалентность мэйтов коммутирует с вертикальной композицией квадратов.
LaTeX
$$$\\mathrm{mateEquiv\\_vcomp} (\\alpha) (\\beta) = \\text{the vertical composition under mates}$$$
Lean4
/-- The mates equivalence commutes with vertical composition. -/
theorem mateEquiv_vcomp (α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁) (β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂) :
mateEquiv adj₁ adj₃ (leftAdjointSquare.vcomp α β) =
rightAdjointSquare.vcomp (mateEquiv adj₁ adj₂ α) (mateEquiv adj₂ adj₃ β) :=
by
simp only [leftAdjointSquare.vcomp, mateEquiv_apply', rightAdjointSquare.vcomp]
symm
calc
_ =
𝟙 _ ⊗≫
r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
((adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ 𝟙 e)) ≫ 𝟙 b ◁ (h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit)) ⊗≫
h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ :=
by bicategory
_ =
𝟙 _ ⊗≫
r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
(r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit)) ⊗≫
((adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃) ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ :=
by
rw [← whisker_exchange]
bicategory
_ =
𝟙 _ ⊗≫
r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
(r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃) ⊗≫
(adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ :=
by
rw [← whisker_exchange, ← whisker_exchange]
bicategory
_ =
𝟙 _ ⊗≫
r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ :=
by
rw [← whisker_exchange, ← whisker_exchange, ← whisker_exchange]
bicategory
_ =
𝟙 _ ⊗≫
r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
((r₁ ≫ g₁) ◁ leftZigzag adj₂.unit adj₂.counit ▷ (h₂ ≫ r₃)) ⊗≫
r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 _ :=
by
rw [← whisker_exchange, ← whisker_exchange]
bicategory
_ = _ := by
rw [adj₂.left_triangle]
bicategory
