Commit 2024-11-14 18:07 2ee23a34

View on Github →

feat: add some result on IsFractionRing and fieldRange (#18984) In Mathlib/RingTheory/Localization/FractionRing.lean:

  • IsFractionRing.closure_range_algebraMap: if A is a ring with fraction field K, then the subfield of K generated by the image of algebraMap A K is equal to the whole field K.
  • IsFractionRing.ringHom_fieldRange_eq_of_comp_eq[_of_range_eq]: if A is a ring with fraction field K, L is a field, g : A →+* L lifts to f : K →+* L, then the image of f is the field generated by the image of g. In Mathlib/FieldTheory/Adjoin.lean:
  • IsFractionRing.algHom_fieldRange_eq_of_comp_eq[_of_range_eq]: 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.

Estimated changes