English
Given an injective g, the image of liftAlgHom has fieldRange equal to the adjoin of g.range.
Русский
Пусть g инъективен, тогда образ liftAlgHom имеет fieldRange, равное адъюнкту g.range.
LaTeX
$$$\operatorname{IsFractionRing.liftAlgHom hg}.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`,
`s` is a set such that the image of `g` is the subalgebra generated by `s`,
then the image of `f` is the intermediate field generated by `s`.
Note: this does not require `IsScalarTower F A K`. -/
theorem algHom_fieldRange_eq_of_comp_eq_of_range_eq (h : RingHom.comp f (algebraMap A K) = (g : A →+* L)) {s : Set L}
(hs : g.range = Algebra.adjoin F s) : f.fieldRange = IntermediateField.adjoin F s :=
by
apply IntermediateField.toSubfield_injective
simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]
refine ringHom_fieldRange_eq_of_comp_eq_of_range_eq h ?_
rw [← Algebra.adjoin_eq_ring_closure, ← hs]; rfl
