conjugateEquiv_comm — Mathlib

English

If we have a square of four left adjoints, the iterated mates coincide with the single conjugate: mateEquiv adj4 adj3 (mateEquiv adj1 adj2 α) = conjugateEquiv (adj1.adj4) (adj3.adj2) α.

Русский

Для квадрата из четырех левых сопряжённых итеративные mate совпадают с одной конъюгированной: …

LaTeX

$$$$ \\operatorname{mateEquiv} adj_4 adj_3 (\\operatorname{mateEquiv} adj_1 adj_2 \\alpha) = \\operatorname{conjugateEquiv} (adj_1 \\cdot adj_4) (adj_3 \\cdot adj_2) \\alpha. $$$$

Lean4

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

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