English
If A is a commutative ring with fraction field K, L is a field, and g : A →+* L lifts to f : K →+* L with f ∘ algebraMap A K = g, then the image (fieldRange) of f is the subfield generated by the image of g.
Русский
Пусть A — коммутативное кольцо с полем дробей K, L — поле, и г : A →+* L поднимается до f : K →+* L так, что f ∘ algebraMap A K = g. Тогда образ f есть подполе, порождаемое образом g.
LaTeX
$$$f.fieldRange = \operatorname{Subfield.closure} (g.range)$$$
Lean4
/-- If `A` is a commutative ring with fraction field `K`, `L` is a field, `g : A →+* L` lifts to
`f : K →+* L`, then the image of `f` is the subfield generated by the image of `g`. -/
theorem ringHom_fieldRange_eq_of_comp_eq (h : RingHom.comp f (algebraMap A K) = g) :
f.fieldRange = Subfield.closure g.range := by
rw [f.fieldRange_eq_map, ← closure_range_algebraMap A K, f.map_field_closure, ← Set.range_comp, ← f.coe_comp, h,
g.coe_range]
