toAlgHom

Mathlib.Algebra.Algebra.Tower

URI: https://scilib.ai/kg/mathlib#IsScalarTower.toAlgHom

← MathLib Explorer

English

For any y in S, toAlgHom y = algebraMap_S^A y.

Русский

Для любого y в S, toAlgHom y = algebraMap_S^A y.

LaTeX

$$$\mathrm{toAlgHom}\;R\;S\;A\;y = \mathrm{algebraMap}\;S\;A\;y$$$

Lean4

/-- In a tower, the canonical map from the middle element to the top element is an
algebra homomorphism over the bottom element. -/
def toAlgHom : S →ₐ[R] A :=
  { algebraMap S A with commutes' := fun _ => (algebraMap_apply _ _ _ _).symm }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru