English
Let adjunctions adj1: L1 ⊣ R1, adj2: L2 ⊣ R2, adj3: L3 ⊣ R3 be given. For α: R1 → R2 and β: R2 → R3, the symmetric conjugation satisfies (conjugateEquiv adj2 adj3).symm(β) ∘ (conjugateEquiv adj1 adj2).symm(α) = (conjugateEquiv adj1 adj3).symm(α ∘ β).
Русский
Пусть заданы сопряжения adj1: L1 ⊣ R1, adj2: L2 ⊣ R2, adj3: L3 ⊣ R3. Для α: R1 → R2 и β: R2 → R3 верно, что (conjugateEquiv adj2 adj3)^{-1}(β) ∘ (conjugateEquiv adj1 adj2)^{-1}(α) = (conjugateEquiv adj1 adj3)^{-1}(α ∘ β).
LaTeX
$$$\\big(\\text{conjugateEquiv } adj_2 adj_3\\big)^{-1}(\\beta) \\circ \\big(\\text{conjugateEquiv } adj_1 adj_2\\big)^{-1}(\\alpha) = \\big(\\text{conjugateEquiv } adj_1 adj_3\\big)^{-1}(\\alpha \\circ \\beta)$$$
Lean4
@[simp]
theorem conjugateEquiv_symm_comp (α : R₁ ⟶ R₂) (β : R₂ ⟶ R₃) :
(conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = (conjugateEquiv adj₁ adj₃).symm (α ≫ β) :=
by
rw [Equiv.eq_symm_apply, ← conjugateEquiv_comp _ adj₂]
simp only [Equiv.apply_symm_apply]
