English
The conjugation and mate operations commute with vcomp in the left and right conjugation squares.
Русский
Сопряжение и mate-компоновки взаимно commute через левый и правый квадрат сопряжений.
LaTeX
$$$$ \\text{conjugateEquiv_mateEquiv_vcomp} = \\text{...}. $$$$
Lean4
/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`. -/
theorem conjugateEquiv_mateEquiv_vcomp (α : l₂ ⟶ l₁) (β : g ≫ l₃ ⟶ l₂ ≫ h) :
(mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β) =
rightAdjointConjugateSquare.vcomp (conjugateEquiv adj₁ adj₂ α) (mateEquiv adj₂ adj₃ β) :=
by
symm
calc
_ =
𝟙 _ ⊗≫
rightAdjointSquare.vcomp (mateEquiv adj₁ adj₂ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv)) (mateEquiv adj₂ adj₃ β) ⊗≫
𝟙 _ :=
by
dsimp only [conjugateEquiv_apply, rightAdjointConjugateSquare.vcomp, rightAdjointSquare.vcomp]
bicategory
_ = _ := by
rw [← mateEquiv_vcomp]
simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointConjugateSquare.vcomp]
bicategory
