range — Mathlib

English

The range of a nonunital algebra homomorphism φ is a nonunital subalgebra of B consisting exactly of the elements φ(x) as x ranges over A.

Русский

Образ гомоморфизма φ — это немонолитная подалгебра B, состоящая ровно из элементов φ(x).

LaTeX

$$$\\mathrm{range}(\\phi) = \\{ \\phi(x) \\mid x \\in A \\}$ as a NonUnitalSubalgebra of B$$

Lean4

/-- Range of an `NonUnitalAlgHom` as a non-unital subalgebra. -/
protected def range (φ : F) : NonUnitalSubalgebra R B
    where
  toNonUnitalSubsemiring := NonUnitalRingHom.srange (φ : A →ₙ+* B)
  smul_mem' := fun r a => by rintro ⟨a, rfl⟩; exact ⟨r • a, map_smul φ r a⟩

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