English
If A is a commutative ring with fraction field K, L is a field, g lifts to f, and s is a set with g.range = Subring.closure s, then the image of f equals the subfield generated by s.
Русский
Пусть A — коммутативное кольцо с полем дробей K, L — поле, g поднимается до f, и существует множество s, для которого g.range = Subring.closure s. Тогда образ f равен подполю, порождаемому s.
LaTeX
$$$f.fieldRange = \operatorname{Subfield.closure} s$$$
Lean4
/-- If `A` is a commutative ring with fraction field `K`, `L` is a field, `g : A →+* L` lifts to
`f : K →+* L`, `s` is a set such that the image of `g` is the subring generated by `s`,
then the image of `f` is the subfield generated by `s`. -/
theorem ringHom_fieldRange_eq_of_comp_eq_of_range_eq (h : RingHom.comp f (algebraMap A K) = g) {s : Set L}
(hs : g.range = Subring.closure s) : f.fieldRange = Subfield.closure s :=
by
rw [ringHom_fieldRange_eq_of_comp_eq h, hs]
ext
simp_rw [Subfield.mem_closure_iff, Subring.closure_eq]
