unit_conjugateEquiv_symm — Mathlib

English

The inverse of conjugateEquiv with itself is the identity.

Русский

Обратное к conjugateEquiv в случае самого себя равно тождественному отображению.

LaTeX

$$$$ (conjugateEquiv adj1 adj1).symm (\\mathrm{id}) = \\mathrm{id} $$$$

Lean4

/-- A component of a transposed form of the inverse conjugation definition. -/
theorem unit_conjugateEquiv_symm (α : R₁ ⟶ R₂) (c : C) :
    adj₁.unit.app _ ≫ α.app _ = adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app _) :=
  by
  conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]
  exact (unit_conjugateEquiv adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) c)

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