conjugateEquiv_counit_symm — Mathlib

English

Symmetric counit compatibility for the conjugateEquiv.

Русский

Симметричное согласование counit для conjugateEquiv.

LaTeX

$$$$ (conjugateEquiv adj1 adj2).symm \\; \\text{on } \\alpha \\; \\Rightarrow \\text{counit relations} $$$$

Lean4

/-- A component of a transposed form of the inverse conjugation definition. -/
theorem conjugateEquiv_counit_symm (α : R₁ ⟶ R₂) (d : D) :
    L₂.map (α.app _) ≫ adj₂.counit.app d = ((conjugateEquiv adj₁ adj₂).symm α).app _ ≫ adj₁.counit.app d :=
  by
  conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]
  exact (conjugateEquiv_counit adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) d)

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