feat(RingTheory): etale local structure of quasi-finite algebras (leanprover-community#35036)

Author: erdOne

Mathlib/RingTheory/Etale/Basic.lean

@@ -242,6 +242,8 @@ theorem of_isLocalizationAway (r : R) [IsLocalization.Away r A] : Etale R A wher
   formallyEtale := Algebra.FormallyEtale.of_isLocalization (Submonoid.powers r)
   finitePresentation := IsLocalization.Away.finitePresentation r
 
+instance (s : A) [Algebra.Etale R A] : Algebra.Etale R (Localization.Away s) where
+
 @[deprecated (since := "2025-11-03")] alias of_isLocalization_Away := of_isLocalizationAway
 
 end Etale

Mathlib/RingTheory/Etale/QuasiFinite.lean

@@ -250,6 +250,9 @@ theorem ne_bot_of_liesOver_of_ne_bot (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver
 
 end CommRing
 
+instance {K A : Type*} [Field K] [Semiring A] [Algebra K A] (P : Ideal A) [P.IsPrime] :
+    P.LiesOver (⊥ : Ideal K) :=
+  ⟨((IsSimpleOrder.eq_bot_or_eq_top _).resolve_right Ideal.IsPrime.ne_top').symm⟩
 namespace Quotient
 
 variable (R : Type*) [CommSemiring R] {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]

Mathlib/RingTheory/Ideal/Over.lean

@@ -48,8 +48,11 @@ theorem isPrime_iff {I : Ideal α} : IsPrime I ↔ I ≠ ⊤ ∧ ∀ {x y : α},
 theorem IsPrime.ne_top {I : Ideal α} (hI : I.IsPrime) : I ≠ ⊤ :=
   hI.1
 
+lemma notMem_of_isUnit (I : Ideal α) [I.IsPrime] {x : α} (hx : IsUnit x) : x ∉ I :=
+  fun h ↦ ‹I.IsPrime›.ne_top (eq_top_of_isUnit_mem _ h hx)
+
 theorem IsPrime.one_notMem {I : Ideal α} (hI : I.IsPrime) : 1 ∉ I :=
-  mt (eq_top_iff_one I).2 hI.1
+  notMem_of_isUnit _ isUnit_one
 
 theorem one_notMem (I : Ideal α) [hI : I.IsPrime] : 1 ∉ I :=
   hI.one_notMem

Mathlib/RingTheory/Ideal/Prime.lean

@@ -63,6 +63,9 @@ and the actual set-theoretic fiber of `PrimeSpectrum S → PrimeSpectrum R` at `
 abbrev Ideal.Fiber (p : Ideal R) [p.IsPrime] (S : Type*) [CommRing S] [Algebra R S] : Type _ :=
   p.ResidueField ⊗[R] S
 
+instance (p : Ideal R) [p.IsPrime] (q : Ideal (p.Fiber S)) [q.IsPrime] : q.LiesOver p :=
+  .trans _ (⊥ : Ideal p.ResidueField) _
+
 lemma Ideal.Fiber.exists_smul_eq_one_tmul (x : p.Fiber S) : ∃ r ∉ p, ∃ s, r • x = 1 ⊗ₜ[R] s := by
   obtain ⟨r, hr, s, e⟩ := Ideal.ResidueField.exists_smul_eq_tmul_one _
     (Algebra.TensorProduct.comm _ _ _ x)

Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean

@@ -89,6 +89,9 @@ noncomputable instance : Algebra (R ⧸ I) I.ResidueField :=
 instance (I : Ideal A) [I.IsPrime] : IsScalarTower R (A ⧸ I) I.ResidueField :=
   .of_algebraMap_eq' rfl
 
+instance (I : Ideal R) [I.IsPrime] : (⊥ : Ideal I.ResidueField).LiesOver I :=
+  ⟨I.ker_algebraMap_residueField.symm⟩
+
 @[simp]
 lemma Ideal.algebraMap_quotient_residueField_mk (x) :
     algebraMap (R ⧸ I) I.ResidueField (Ideal.Quotient.mk _ x) =

Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean

@@ -366,7 +366,20 @@ end AtUnits
 
 section Prod
 
-lemma away_of_isIdempotentElem_of_mul {R S} [CommSemiring R] [CommSemiring S] [Algebra R S]
+lemma Away.algebraMap_surjective_of_isIdempotentElem
+    (e : R) (he : IsIdempotentElem e) [IsLocalization.Away e S] :
+    Function.Surjective (algebraMap R S) := by
+  intro x
+  obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers e) x
+  suffices ∃ a k, e ^ k * (a * e ^ n) = e ^ k * x by
+    simpa [IsLocalization.eq_mk'_iff_mul_eq, ← map_pow, ← map_mul,
+      IsLocalization.eq_iff_exists (.powers e), Submonoid.mem_powers_iff]
+  refine ⟨x, 1, ?_⟩
+  trans e ^ (n + 1) * x
+  · ring
+  · rw [he.pow_succ_eq]; ring
+
+lemma away_of_isIdempotentElem_of_mul
     {e : R} (he : IsIdempotentElem e)
     (H : ∀ x y, algebraMap R S x = algebraMap R S y ↔ e * x = e * y)
     (H' : Function.Surjective (algebraMap R S)) :
@@ -502,6 +515,22 @@ lemma awayMap_bijective_of_dvd {R : Type*} [CommRing R] (f : R →+* S)
     Function.Bijective (awayMap f b) :=
   ⟨awayMap_injective_of_dvd f h H.1, awayMap_surjective_of_dvd f h H.2⟩
 
+omit [Algebra R S] in
+lemma awayMap_awayMap_surjective (f : R →+* S) (a b : R)
+    (H : Function.Surjective (awayMap f (a * b))) :
+    Function.Surjective (awayMap (awayMap f a) (algebraMap _ _ b)) := by
+  rw [awayMap_surjective_iff] at H ⊢
+  suffices ∀ (s : S) (n : ℕ), ∃ c l m k, f (a ^ (k + n) * c) =
+      f (a ^ (k + l) * b ^ m) * s by
+    simpa [Function.Surjective, (IsLocalization.mk'_surjective (.powers (f a))).forall, ← map_pow,
+      (IsLocalization.mk'_surjective (.powers a)).exists, Submonoid.mem_powers_iff, pow_add,
+      Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_mk', ← mul_assoc,
+      IsLocalization.mk'_eq_iff_eq, ← map_mul, IsLocalization.eq_iff_exists (.powers (f a)),
+      IsLocalization.mul_mk'_eq_mk'_of_mul]
+  intro s n
+  obtain ⟨c, m, e⟩ := H s
+  exact ⟨c, n + m, m, 0, by simp [e, pow_add]; ring⟩
+
 variable {A : Type*} [CommSemiring A] [Algebra R A]
 variable {B : Type*} [CommSemiring B] [Algebra R B]