conjugateEquiv_symm_comm — Mathlib

English

For α: R1 → R2 and β: R2 → R3, the symmetric conjugation satisfies (conjugateEquiv adj2 adj1).symm(β) ∘ (conjugateEquiv adj1 adj2).symm(α) = (conjugateEquiv adj1 adj3).symm (α ∘ β).

Русский

Для α: R1 → R2 и β: R2 → R3 справедливо (conjugateEquiv adj2 adj1)^{-1}(β) ∘ (conjugateEquiv adj1 adj2)^{-1}(α) = (conjugateEquiv adj1 adj3)^{-1}(α ∘ β).

LaTeX

$$$(\\text{conjugateEquiv } adj_2 adj_1)^{-1}(\\beta) \\circ (\\text{conjugateEquiv } adj_1 adj_2)^{-1}(\\alpha) = (\\text{conjugateEquiv } adj_1 adj_3)^{-1}(\\alpha \\circ \\beta)$$$

Lean4

theorem conjugateEquiv_symm_comm {α : R₁ ⟶ R₂} {β : R₂ ⟶ R₁} (αβ : α ≫ β = 𝟙 _) :
    (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 _ := by
  rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]

Похожие утверждения