toAlgHom_unop — Mathlib

English

If f is an R-algebra equivalence between the opposites A^op and B^op, then the unop of f, viewed as an R-algebra equivalence A ≃ B, has the same underlying algebra homomorphism as the unop of f's underlying algebra homomorphism.

Русский

Пусть f является R-алгебраическим изоморфизмом между противоположностями A^op и B^op; тогда несжатый образ f, рассматриваемый как эквиваличность A ≃ B, имеет такое же лежащее в основе алгебро-хомоморфизм, как несжатый образ f.toAlgHom.

LaTeX

$$$ f.unop.toAlgHom = AlgHom.unop f.toAlgHom $$$

Lean4

theorem toAlgHom_unop (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) : f.unop.toAlgHom = AlgHom.unop f.toAlgHom :=
  rfl

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