range_mapAlgHom — Mathlib

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]

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