English
The iterated mates equivalence commutes with conjugation: mateEquiv_adj1_adj3 (leftSquareConjugate.vcomp α β) equals conjugateEquiv (adj1 adj4) (adj3 adj2) α etc.
Русский
Совместимость итеративных mate с сопряжением.
LaTeX
$$$$ \\text{mateEquiv } adj_1 adj_3 (\\text{leftAdjointConjugateSquare.vcomp } α β) = \\text{conjugateEquiv } (adj_1 adj_4) (adj_3 adj_2) α. $$$$
Lean4
/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`. -/
theorem mateEquiv_conjugateEquiv_vcomp (α : g ≫ l₂ ⟶ l₁ ≫ h) (β : l₃ ⟶ l₂) :
(mateEquiv adj₁ adj₃) (leftAdjointSquareConjugate.vcomp α β) =
rightAdjointSquareConjugate.vcomp (mateEquiv adj₁ adj₂ α) (conjugateEquiv adj₂ adj₃ β) :=
by
symm
calc
_ =
𝟙 _ ⊗≫
rightAdjointSquare.vcomp (mateEquiv adj₁ adj₂ α) (mateEquiv adj₂ adj₃ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫
𝟙 _ :=
by
dsimp only [conjugateEquiv_apply, rightAdjointSquareConjugate.vcomp, rightAdjointSquare.vcomp]
bicategory
_ = _ := by
rw [← mateEquiv_vcomp]
simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointSquareConjugate.vcomp]
bicategory
