English
Same as above: the range of the algebra-polynomial map equals the submodule generated by the image of the coefficient range.
Русский
То же самое: диапазон отображения от алгебрpolynomial равен подподмножеству образа диапазона коэффициентов.
LaTeX
$$$\\\\mathrm{range}(\\\\mathrm{mapAlgHom} f).toSubmodule = \\\\mathrm{coeffsIn} σ f.range.toSubmodule$$$
Lean4
theorem range_mapAlgHom [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
(mapAlgHom f).range.toSubmodule = coeffsIn σ f.range.toSubmodule :=
by
ext
rw [Subalgebra.mem_toSubmodule, ← SetLike.mem_coe, AlgHom.coe_range, mapAlgHom, AlgHom.coe_mk,
mem_range_map_iff_coeffs_subset, mem_coeffsIn_iff_coeffs_subset]
simp [Set.subset_def]