range_lift — Mathlib

English

For a linear map f: M → A (A an R-algebra), the range of the lifted map lift R f equals the algebra generated by the range of f.

Русский

Для линейного отображения f: M → A (A — R-алгебра) множество образ lift R f равно алгебральной порождающей мощностью образа f.

LaTeX

$$$\\operatorname{range}(\\mathrm{lift}\\ R\\ f) = \\operatorname{adjoin}_R(\\operatorname{range}(f))$$$

Lean4

@[simp]
theorem range_lift {A : Type*} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) :
    (lift R f).range = Algebra.adjoin R (Set.range f) := by
  simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp, Function.comp_def, lift_ι_apply]

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