feat: IsFractionRing R R if R is a field. (#8641)

Mathlib/RingTheory/Localization/Away/Basic.lean

@@ -117,30 +117,10 @@ section AtUnits
 
 variable (R) (S)
 
-/-- The localization at a module of units is isomorphic to the ring. -/
-noncomputable def atUnits (H : ∀ x : M, IsUnit (x : R)) : R ≃ₐ[R] S := by
-  refine' AlgEquiv.ofBijective (Algebra.ofId R S) ⟨_, _⟩
-  · intro x y hxy
-    obtain ⟨c, eq⟩ := (IsLocalization.eq_iff_exists M S).mp hxy
-    obtain ⟨u, hu⟩ := H c
-    rwa [← hu, Units.mul_right_inj] at eq
-  · intro y
-    obtain ⟨⟨x, s⟩, eq⟩ := IsLocalization.surj M y
-    obtain ⟨u, hu⟩ := H s
-    use x * u.inv
-    dsimp [Algebra.ofId, RingHom.toFun_eq_coe, AlgHom.coe_mks]
-    rw [RingHom.map_mul, ← eq, ← hu, mul_assoc, ← RingHom.map_mul]
-    simp
-#align is_localization.at_units IsLocalization.atUnits
-
 /-- The localization away from a unit is isomorphic to the ring. -/
-noncomputable def atUnit (x : R) (e : IsUnit x) [IsLocalization.Away x S] : R ≃ₐ[R] S := by
-  apply atUnits R (Submonoid.powers x)
-  rintro ⟨xn, n, hxn⟩
-  obtain ⟨u, hu⟩ := e
-  rw [isUnit_iff_exists_inv]
-  use u.inv ^ n
-  simp [← hxn, ← hu, ← mul_pow]
+noncomputable def atUnit (x : R) (e : IsUnit x) [IsLocalization.Away x S] : R ≃ₐ[R] S :=
+  atUnits R (Submonoid.powers x)
+    (by rwa [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff])
 #align is_localization.at_unit IsLocalization.atUnit
 
 /-- The localization at one is isomorphic to the ring. -/

Mathlib/RingTheory/Localization/Basic.lean

@@ -436,6 +436,12 @@ theorem smul_mk' (x y : R) (m : M) : x • mk' S y m = mk' S (x * y) m := by
     (m : R) • mk' S r m = algebraMap R S r := by
   rw [smul_mk', mk'_mul_cancel_left]
 
+@[simps]
+instance invertible_mk'_one (s : M) : Invertible (IsLocalization.mk' S (1 : R) s) where
+  invOf := algebraMap R S s
+  invOf_mul_self := by simp
+  mul_invOf_self := by simp
+
 section
 
 variable (M)
@@ -748,6 +754,34 @@ theorem algEquiv_symm_mk' (x : R) (y : M) : (algEquiv M S Q).symm (mk' Q x y) =
 
 end AlgEquiv
 
+section at_units
+
+lemma at_units {R : Type*} [CommSemiring R] (S : Submonoid R)
+    (hS : S ≤ IsUnit.submonoid R) : IsLocalization S R where
+  map_units' y := hS y.prop
+  surj' := fun s ↦ ⟨⟨s, 1⟩, by simp⟩
+  exists_of_eq := fun {x y} (e : x = y) ↦ ⟨1, e ▸ rfl⟩
+
+variable (R M)
+
+/-- The localization at a module of units is isomorphic to the ring. -/
+noncomputable def atUnits (H : M ≤ IsUnit.submonoid R) : R ≃ₐ[R] S := by
+  refine' AlgEquiv.ofBijective (Algebra.ofId R S) ⟨_, _⟩
+  · intro x y hxy
+    obtain ⟨c, eq⟩ := (IsLocalization.eq_iff_exists M S).mp hxy
+    obtain ⟨u, hu⟩ := H c.prop
+    rwa [← hu, Units.mul_right_inj] at eq
+  · intro y
+    obtain ⟨⟨x, s⟩, eq⟩ := IsLocalization.surj M y
+    obtain ⟨u, hu⟩ := H s.prop
+    use x * u.inv
+    dsimp [Algebra.ofId, RingHom.toFun_eq_coe, AlgHom.coe_mks]
+    rw [RingHom.map_mul, ← eq, ← hu, mul_assoc, ← RingHom.map_mul]
+    simp
+#align is_localization.at_units IsLocalization.atUnits
+
+end at_units
+
 end IsLocalization
 
 section

Mathlib/RingTheory/Localization/FractionRing.lean

@@ -44,6 +44,9 @@ abbrev IsFractionRing [CommRing K] [Algebra R K] :=
   IsLocalization (nonZeroDivisors R) K
 #align is_fraction_ring IsFractionRing
 
+instance {R : Type*} [Field R] : IsFractionRing R R :=
+  IsLocalization.at_units _ (fun _ ↦ isUnit_of_mem_nonZeroDivisors)
+
 /-- The cast from `Int` to `Rat` as a `FractionRing`. -/
 instance Rat.isFractionRing : IsFractionRing ℤ ℚ where
   map_units' := by
@@ -314,8 +317,7 @@ noncomputable def liftAlgebra [IsDomain R] [Field K] [Algebra R K]
   RingHom.toAlgebra (IsFractionRing.lift (NoZeroSMulDivisors.algebraMap_injective R _))
 
 -- Porting note: had to fill in the `_` by hand for this instance
-/-- Should be introduced locally after introducing `FractionRing.liftAlgebra` -/
-theorem isScalarTower_liftAlgebra [IsDomain R] [Field K] [Algebra R K] [NoZeroSMulDivisors R K] :
+instance isScalarTower_liftAlgebra [IsDomain R] [Field K] [Algebra R K] [NoZeroSMulDivisors R K] :
     by letI := liftAlgebra R K; exact IsScalarTower R (FractionRing R) K := by
   letI := liftAlgebra R K
   exact IsScalarTower.of_algebraMap_eq fun x =>