toTop — Mathlib

English

The top subalgebra is canonically isomorphic to the ambient algebra A; there is an algebra isomorphism between ⊤ and A.

Русский

Верхняя подалгебра естественным образом изоморфна самой области A; существует алгебраическое изоморфизм между ⊤ и A.

LaTeX

$$$ \\text{topEquiv} : (\\top : \\mathrm{Subalgebra} R A) \\simeq_{\\! R} A $$$

Lean4

/-- `AlgHom` to `⊤ : Subalgebra R A`. -/
def toTop : A →ₐ[R] (⊤ : Subalgebra R A) :=
  (AlgHom.id R A).codRestrict ⊤ fun _ => mem_top

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