chore(Mathlib/RingTheory/LocalProperties): split LocalProperties.lean (…

…#16879)

Split the section on local properties in general and the properties that satisfy local properties in `LocalProperties.lean` into separate files.

See the discussions [here](#16558 (comment)).



Co-authored-by: Hu Yongle <[email protected]>
Co-authored-by: Yongle Hu <[email protected]>

Mathlib.lean

@@ -3920,7 +3920,9 @@ import Mathlib.RingTheory.Kaehler.CotangentComplex
 import Mathlib.RingTheory.Kaehler.Polynomial
 import Mathlib.RingTheory.LaurentSeries
 import Mathlib.RingTheory.LittleWedderburn
-import Mathlib.RingTheory.LocalProperties
+import Mathlib.RingTheory.LocalProperties.Basic
+import Mathlib.RingTheory.LocalProperties.IntegrallyClosed
+import Mathlib.RingTheory.LocalProperties.Reduced
 import Mathlib.RingTheory.LocalRing.Basic
 import Mathlib.RingTheory.LocalRing.Defs
 import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

@@ -95,11 +95,11 @@ theorem spec_of_surjective {R S : CommRingCat} (f : R ⟶ S) (h : Function.Surje
   surj_on_stalks x := by
     haveI : (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f)).RespectsIso := by
       rw [← RingHom.toMorphismProperty_respectsIso_iff]
-      exact surjective_respectsIso
+      exact RingHom.surjective_respectsIso
     apply (MorphismProperty.arrow_mk_iso_iff
       (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f))
       (Scheme.arrowStalkMapSpecIso f x)).mpr
-    exact surjective_localRingHom_of_surjective f h x.asIdeal
+    exact RingHom.surjective_localRingHom_of_surjective f h x.asIdeal
 
 /-- For any ideal `I` in a commutative ring `R`, the quotient map `specObj R ⟶ specObj (R ⧸ I)`
 is a closed immersion. -/

Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
-import Mathlib.RingTheory.LocalProperties
+import Mathlib.RingTheory.RingHom.Surjective
 
 /-!
 
@@ -52,7 +52,7 @@ lemma isPreimmersion_eq_inf :
 /-- Being surjective on stalks is local at the target. -/
 instance isSurjectiveOnStalks_isLocalAtTarget : IsLocalAtTarget
     (stalkwise (Function.Surjective ·)) :=
-  stalkwiseIsLocalAtTarget_of_respectsIso surjective_respectsIso
+  stalkwiseIsLocalAtTarget_of_respectsIso RingHom.surjective_respectsIso
 
 namespace IsPreimmersion
 

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.AlgebraicGeometry.Morphisms.Basic
-import Mathlib.RingTheory.LocalProperties
+import Mathlib.RingTheory.LocalProperties.Basic
 
 /-!
 

Mathlib/AlgebraicGeometry/Properties.lean

@@ -4,10 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.AlgebraicGeometry.AffineScheme
-import Mathlib.RingTheory.Nilpotent.Lemmas
-import Mathlib.Topology.Sheaves.SheafCondition.Sites
-import Mathlib.Algebra.Category.Ring.Constructions
-import Mathlib.RingTheory.LocalProperties
+import Mathlib.RingTheory.LocalProperties.Reduced
 
 /-!
 # Basic properties of schemes

Mathlib/RingTheory/Ideal/Norm.lean

@@ -12,7 +12,7 @@ import Mathlib.LinearAlgebra.FreeModule.Determinant
 import Mathlib.LinearAlgebra.FreeModule.IdealQuotient
 import Mathlib.RingTheory.DedekindDomain.PID
 import Mathlib.RingTheory.Ideal.Basis
-import Mathlib.RingTheory.LocalProperties
+import Mathlib.RingTheory.LocalProperties.Basic
 import Mathlib.RingTheory.Localization.NormTrace
 
 /-!

Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

@@ -3,11 +3,11 @@ Copyright (c) 2023 Andrew Yang, Patrick Lutz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
-import Mathlib.RingTheory.LocalProperties
-import Mathlib.RingTheory.Localization.NormTrace
-import Mathlib.RingTheory.Localization.LocalizationLocalization
 import Mathlib.RingTheory.DedekindDomain.IntegralClosure
+import Mathlib.RingTheory.RingHom.Finite
+import Mathlib.RingTheory.Localization.LocalizationLocalization
+import Mathlib.RingTheory.Localization.NormTrace
+
 /-!
 # Restriction of various maps between fields to integrally closed subrings.
 

Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import Mathlib.RingTheory.Localization.Integral
-import Mathlib.RingTheory.Localization.LocalizationLocalization
 
 /-!
 # Integrally closed rings
@@ -278,44 +277,7 @@ end integralClosure
 
 /-- Any field is integral closed. -/
 /- Although `infer_instance` can find this if you import Mathlib, in this file they have not been
-  proven yet. However, the next theorem is a fundamental property of `IsIntegrallyClosed`,
+  proven yet. However, it is used to prove a fundamental property of `IsIntegrallyClosed`,
   and it is not desirable to involve more content from other files. -/
 instance Field.instIsIntegrallyClosed (K : Type*) [Field K] : IsIntegrallyClosed K :=
   (isIntegrallyClosed_iff K).mpr fun {x} _ ↦ ⟨x, rfl⟩
-
-open Localization Ideal IsLocalization in
-/-- An integral domain `R` is integral closed if `Rₘ` is integral closed
-for any maximal ideal `m` of `R`. -/
-theorem IsIntegrallyClosed.of_localization_maximal {R : Type*} [CommRing R] [IsDomain R]
-    (h : ∀ p : Ideal R, p ≠ ⊥ → [p.IsMaximal] → IsIntegrallyClosed (Localization.AtPrime p)) :
-    IsIntegrallyClosed R := by
-  by_cases hf : IsField R
-  · exact hf.toField.instIsIntegrallyClosed
-  apply (isIntegrallyClosed_iff (FractionRing R)).mpr
-  rintro ⟨x⟩ hx
-  let I : Ideal R := span {x.2.1} / span {x.1}
-  have h1 : 1 ∈ I := by
-    apply I.eq_top_iff_one.mp
-    by_contra hn
-    rcases I.exists_le_maximal hn with ⟨p, hpm, hpi⟩
-    have hic := h p (Ring.ne_bot_of_isMaximal_of_not_isField hpm hf)
-    have hxp : IsIntegral (Localization.AtPrime p) (mk x.1 x.2) := hx.tower_top
-    /- `x.1 / x.2.1 ∈ Rₚ` since it is integral over `Rₚ` and `Rₚ` is integrally closed.
-      More precisely, `x.1 / x.2.1 = y.1 / y.2.1` where `y.1, y.2.1 ∈ R` and `y.2.1 ∉ p`. -/
-    rcases (isIntegrallyClosed_iff (FractionRing R)).mp hic hxp with ⟨⟨y⟩, hy⟩
-    /- `y.2.1 ∈ I` since for all `a ∈ Ideal.span {x.1}`, say `a = b * x.1`,
-      we have `y.2 * a = b * x.1 * y.2 = b * y.1 * x.2.1 ∈ Ideal.span {x.2.1}`. -/
-    have hyi : y.2.1 ∈ I := by
-      intro a ha
-      rcases mem_span_singleton'.mp ha with ⟨b, hb⟩
-      apply mem_span_singleton'.mpr ⟨b * y.1, _⟩
-      rw [← hb, ← mul_assoc, mul_comm y.2.1 b, mul_assoc, mul_assoc]
-      exact congrArg (HMul.hMul b) <| (mul_comm y.1 x.2.1).trans <|
-        NoZeroSMulDivisors.algebraMap_injective R (Localization R⁰) <| mk'_eq_iff_eq.mp <|
-          (mk'_eq_algebraMap_mk'_of_submonoid_le _ _ p.primeCompl_le_nonZeroDivisors y.1 y.2).trans
-            <| show algebraMap (Localization.AtPrime p) _ (mk' _ y.1 y.2) = mk' _ x.1 x.2
-              by simpa only [← mk_eq_mk', ← hy] using by rfl
-    -- `y.2.1 ∈ I` implies `y.2.1 ∈ p` since `I ⊆ p`, which contradicts to the choice of `y`.
-    exact y.2.2 (hpi hyi)
-  rcases mem_span_singleton'.mp (h1 x.1 (mem_span_singleton_self x.1)) with ⟨y, hy⟩
-  exact ⟨y, (eq_mk'_of_mul_eq (hy.trans (one_mul x.1))).trans (mk_eq_mk'_apply x.1 x.2).symm⟩