toRingHom_fromOpposite — Mathlib

English

There is a canonical equivalence between algebra homs A → Bᵐᵒᵖ and Aᵐᵒᵖ → B.

Русский

Существует каноническое эквивалентноe между алгебра-гомоморфизмами A → Bᵐᵒᵖ и Aᵐᵒᵖ → B.

LaTeX

$$AlgHom.opComm : (A →ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ →ₐ[R] B)$$

Lean4

@[simp]
theorem toRingHom_fromOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) :
    (f.fromOpposite hf : Aᵐᵒᵖ →+* B) = (f : A →+* B).fromOpposite hf :=
  rfl

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