lift_fieldRange_eq_of_range_eq — Mathlib

English

The same consequence as above, using a slightly different presentation; if hg injective and g.range = Subring.closure s, then (lift hg).fieldRange = Subfield.closure s.

Русский

Та же зависимость: если hg инъективно и g.range = Subring.closure s, то (lift hg).fieldRange = Subfield.closure s.

LaTeX

$$$ (\mathrm{lift} \; hg).fieldRange = \operatorname{Subfield.closure} s $$$

Lean4

/-- The image of `IsFractionRing.lift` is the subfield generated by `s`, if the image
of the ring hom is the subring generated by `s`. -/
theorem lift_fieldRange_eq_of_range_eq (hg : Injective g) {s : Set L} (hs : g.range = Subring.closure s) :
    (lift hg : K →+* L).fieldRange = Subfield.closure s :=
  ringHom_fieldRange_eq_of_comp_eq_of_range_eq (by ext; simp) hs

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