English
For algebra hom g lifts to f on the fraction field, the field range equals the subalgebra generated by g.range.
Русский
Для алгебраического гомофона g, который поднимается до f на дробном поле, образ поля равен подалгебре, порождаемой диапазоном g.
LaTeX
$$$f.fieldRange = \operatorname{IntermediateField.adjoin}_F (g.range)$$$
Lean4
/-- If `F` is a field, `A` is an `F`-algebra with fraction field `K`, `L` is a field,
`g : A →ₐ[F] L` lifts to `f : K →ₐ[F] L`,
then the image of `f` is the field generated by the image of `g`.
Note: this does not require `IsScalarTower F A K`. -/
theorem algHom_fieldRange_eq_of_comp_eq (h : RingHom.comp f (algebraMap A K) = (g : A →+* L)) :
f.fieldRange = IntermediateField.adjoin F g.range :=
by
apply IntermediateField.toSubfield_injective
simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]
convert ringHom_fieldRange_eq_of_comp_eq h using 2
exact Set.union_eq_self_of_subset_left fun _ ⟨x, hx⟩ ↦ ⟨algebraMap F A x, by simp [← hx]⟩
