liftAlgHom_fieldRange_eq_of_range_eq

English

If the range of g equals the algebraic adjoin of s, then the field range of liftAlgHom equals the adjoin of s.

Русский

Если образ g равен алгебраическому адъюнкту множества s, тогда образ поля liftAlgHom равен адъюнкту s.

LaTeX

$$f.fieldRange = \operatorname{IntermediateField.adjoin}_F (s)$$

Lean4

/-- The image of `IsFractionRing.liftAlgHom` is the intermediate field generated by `s`,
if the image of the algebra hom is the subalgebra generated by `s`. -/
theorem liftAlgHom_fieldRange_eq_of_range_eq (hg : Function.Injective g) {s : Set L}
    (hs : g.range = Algebra.adjoin F s) : (liftAlgHom hg : K →ₐ[F] L).fieldRange = IntermediateField.adjoin F s :=
  algHom_fieldRange_eq_of_comp_eq_of_range_eq (by ext; simp) hs

Похожие утверждения