range — Mathlib

English

The range of an algebra homomorphism φ: A →ₐ[R] B is a subalgebra of B, consisting of all elements that are images of elements of A under φ, with the algebra structure induced from B.

Русский

Образ гомоморфизма алгебры φ: A →ₐ[R] B образует подалгебру B, состоящую из элементов вида φ(a), a ∈ A, со структурой алгебры, индуцированной из B.

LaTeX

$$$\operatorname{range}(\varphi) = \{ φ(a) : a \in A \}$ является подалгеброй B$$

Lean4

/-- Range of an `AlgHom` as a subalgebra. -/
@[simps! coe toSubsemiring]
protected def range (φ : A →ₐ[R] B) : Subalgebra R B :=
  { φ.toRingHom.rangeS with algebraMap_mem' := fun r => ⟨algebraMap R A r, φ.commutes r⟩ }

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