subalgebraMap — Mathlib

English

There is a canonical restriction of an algebra homomorphism to any subalgebra S of the domain, yielding an algebra homomorphism from S onto its image S.map f.

Русский

Существует каноническое ограничение алгебра-хомоморфизма на любую подалгебру S пространства домена, образующее алгебра-хомоморфизм S → S.map f.

LaTeX

$$$\mathrm{AlgHom.subalgebraMap}(S,f) : S \toₐ[R] S.map f$$$

Lean4

/-- An `AlgHom` between two rings restricts to an `AlgHom` from any subalgebra of the
domain onto the image of that subalgebra. -/
def _root_.AlgHom.subalgebraMap : S →ₐ[R] S.map f :=
  (f.comp S.val).codRestrict _ fun x ↦ ⟨_, x.2, rfl⟩

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