coe_toAlgHom — Mathlib

English

In a tower of algebras R → S → A, the canonical S-algebra map from S to A coincides with the structure map algebraMap S A.

Русский

В башне алгебр R → S → A каноническое S-алгебраическое отображение S → A совпадает с базовым отображением алгебраMap S A.

LaTeX

$$$ \uparrow\bigl(toAlgHom\, R\, S\, A\bigr) = algebraMap\ S\ A$$

Lean4

@[simp]
theorem coe_toAlgHom : ↑(toAlgHom R S A) = algebraMap S A :=
  RingHom.ext fun _ => rfl

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