English
Conjugation commutes with symm composition: (conjugateEquiv adj2 adj3).symm β ≫ (conjugateEquiv adj1 adj2).symm α = (conjugateEquiv adj1 adj3).symm (α ≫ β).
Русский
Сопряжение сохраняет симм-компоновку: (conjugateEquiv adj2 adj3).symm β ≫ (conjugateEquiv adj1 adj2).symm α = (conjugateEquiv adj1 adj3).symm (α ≫ β).
LaTeX
$$$$ (conjugateEquiv adj_2 adj_3)\\!^{-1} β \\;\\circ\\; (conjugateEquiv adj_1 adj_2)\\!^{-1} α = (conjugateEquiv adj_1 adj_3)\\!^{-1} (α \\circ β). $$$$
Lean4
@[simp]
theorem conjugateEquiv_comp (α : l₂ ⟶ l₁) (β : l₃ ⟶ l₂) :
conjugateEquiv adj₁ adj₂ α ≫ conjugateEquiv adj₂ adj₃ β = conjugateEquiv adj₁ adj₃ (β ≫ α) :=
by
simp only [conjugateEquiv_apply]
calc
_ =
𝟙 r₁ ⊗≫
rightAdjointSquare.vcomp (mateEquiv adj₁ adj₂ ((λ_ _).hom ≫ α ≫ (ρ_ _).inv))
(mateEquiv adj₂ adj₃ ((λ_ _).hom ≫ β ≫ (ρ_ _).inv)) ⊗≫
𝟙 r₃ :=
by
dsimp only [rightAdjointSquare.vcomp]
bicategory
_ = _ := by
rw [← mateEquiv_vcomp]
simp only [leftAdjointSquare.vcomp, mateEquiv_apply']
bicategory
