fix

mbkybky · Oct 25, 2024 · d3d7ff3 · d3d7ff3
1 parent 5ec90ed
commit d3d7ff3
Showing 1 changed file with 17 additions and 12 deletions.
diff --git a/ModuleLocalProperties/MissingLemmas/Integral.lean b/ModuleLocalProperties/MissingLemmas/Integral.lean
@@ -6,25 +6,30 @@ Authors: SiHan Su
 import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
 import Mathlib.RingTheory.Localization.AsSubring
 
-open Localization
-lemma Localization.IsIntegrallyClosed {R : Type*} [CommRing R] [IsDomain R]
-    (int : IsIntegrallyClosed R) (S : Submonoid R) (hs : 0 ∉ S):
-    IsIntegrallyClosed (Localization S) := by
+open Localization IsLocalization
+
+lemma IsLocalization.isIntegrallyClosed {R A : Type*} [CommRing R] [IsDomain R] (S : Submonoid R)
+    [CommRing A] [Algebra R A] [IsLocalization S A] (int : IsIntegrallyClosed R) (hs : 0 ∉ S) :
+    IsIntegrallyClosed A := by
   have le := le_nonZeroDivisors_of_noZeroDivisors hs
-  letI alg := (mapToFractionRing (FractionRing R) S (Localization S) le).toAlgebra
-  letI : IsFractionRing (Localization S) (FractionRing R) :=
+  letI alg := (mapToFractionRing (FractionRing R) S A le).toAlgebra
+  letI : IsFractionRing A (FractionRing R) :=
     IsFractionRing.isFractionRing_of_isLocalization S _ _ le
   apply (isIntegrallyClosed_iff (FractionRing R)).mpr
   intro x hx
   obtain ⟨r, hr⟩ := IsIntegral.exists_multiple_integral_of_isLocalization S _ hx
   obtain ⟨y, eqy⟩ := (isIntegrallyClosed_iff (FractionRing R)).mp int hr
-  use (y • mk 1 r)
+  use (y • mk' A 1 r)
   calc
-    _ = ((algebraMap R _) y) * (algebraMap _ _) (mk 1 r) := by
-      rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R (Localization S) (FractionRing R),
+    _ = ((algebraMap R _) y) * (algebraMap _ _) (mk' A 1 r) := by
+      rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R A (FractionRing R),
         _root_.map_mul]
     _ = _ := by
       have : r • x = r.1 • x := rfl
-      rw [eqy, this, Algebra.smul_def, IsScalarTower.algebraMap_apply R (Localization S) _,
-        mul_comm, ← mul_assoc, ← _root_.map_mul, ← mk_one_eq_algebraMap, mk_mul]
-      simp only [mk_self, one_mul, mul_one, map_one]
+      rw [eqy, this, Algebra.smul_def, IsScalarTower.algebraMap_apply R A _,
+        mul_comm, ← mul_assoc, ← _root_.map_mul, mk'_spec, map_one, map_one, one_mul]
+
+lemma Localization.isIntegrallyClosed {R : Type*} [CommRing R] [IsDomain R]
+    (int : IsIntegrallyClosed R) (S : Submonoid R) (hs : 0 ∉ S):
+    IsIntegrallyClosed (Localization S) :=
+  IsLocalization.isIntegrallyClosed S int hs