conjugateEquiv_comm — Mathlib

English

If α: L2 → L1 and β: L1 → L2 with βα = id, then the conjugates compose to the identity.

Русский

Если α: L2 → L1 и β: L1 → L2 удовлетворяют βα = id, то сопряжённые они образуют тождественный морфизм.

LaTeX

$$$\\text{conjugateEquiv } adj_1 adj_2(\\alpha) \\circ \\text{conjugateEquiv } adj_2 adj_1(\\beta) = \\mathrm{id}_{L_1}$$$

Lean4

theorem conjugateEquiv_comm {α : L₂ ⟶ L₁} {β : L₁ ⟶ L₂} (βα : β ≫ α = 𝟙 _) :
    conjugateEquiv adj₁ adj₂ α ≫ conjugateEquiv adj₂ adj₁ β = 𝟙 _ := by rw [conjugateEquiv_comp, βα, conjugateEquiv_id]

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