English
The coeIdeal of the span of a single element equals the span singleton of its image under algebra map.
Русский
Коэффициентный идеал от спана единичного элемента равен spanSingleton образа через алгебраическую маппингу.
LaTeX
$$$(↑(Ideal.span \\{ x \\} : Ideal R) : FractionalIdeal S P) = spanSingleton S (algebraMap R P x)$$$
Lean4
@[simp]
theorem coeIdeal_span_singleton (x : R) :
(↑(Ideal.span { x } : Ideal R) : FractionalIdeal S P) = spanSingleton S (algebraMap R P x) :=
by
ext y
refine (mem_coeIdeal S).trans (Iff.trans ?_ (mem_spanSingleton S).symm)
constructor
· rintro ⟨y', hy', rfl⟩
obtain ⟨x', rfl⟩ := Submodule.mem_span_singleton.mp hy'
use x'
rw [smul_eq_mul, RingHom.map_mul, Algebra.smul_def]
· rintro ⟨y', rfl⟩
refine ⟨y' * x, Submodule.mem_span_singleton.mpr ⟨y', rfl⟩, ?_⟩
rw [RingHom.map_mul, Algebra.smul_def]
