Skip to content

Commit a9802c2

Browse files
tb65536tb65536
committed
attempt
1 parent 3b9fc57 commit a9802c2

13 files changed

Lines changed: 49 additions & 45 deletions

File tree

‎Mathlib/RingTheory/Flat/Localization.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
107107

108108
instance [Module.Flat A B] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p]
109109
[Algebra (Localization.AtPrime p) (Localization.AtPrime P)]
110-
[Localization.AtPrime.IsLiesOverAlgebra p P] :
110+
[IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime P)] :
111111
Module.Flat (Localization.AtPrime p) (Localization.AtPrime P) := by
112112
rw [Module.flat_iff_of_isLocalization (Localization.AtPrime p) p.primeCompl]
113113
exact Module.Flat.trans A B (Localization.AtPrime P)

‎Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean‎

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -69,12 +69,6 @@ abbrev Fiber (p : Ideal R) [p.IsPrime] (S : Type*) [AddCommGroup S] [Module R S]
6969
instance (q : Ideal (p.Fiber S)) [q.IsPrime] : q.LiesOver p :=
7070
.trans _ (⊥ : Ideal p.ResidueField) _
7171

72-
/-- If `q` is a prime ideal of `p.Fiber S`, then the localization `(p.Fiber S)_q` is an algebra
73-
over the localization `R_p` since `p.Fiber S` is already an `R_p`-algebra. This `R_p`-algebra
74-
structure on `(p.Fiber S)_q` agrees with the one coming from the fact that `q` lies over `p`. -/
75-
instance (q : Ideal (p.Fiber S)) [q.IsPrime] : Localization.AtPrime.IsLiesOverAlgebra p q where
76-
algebraMap_eq := (Localization.localRingHom_unique p q _ (Ideal.over_def q p) fun _ ↦ rfl).symm
77-
7872
lemma Fiber.exists_smul_eq_one_tmul (x : p.Fiber S) : ∃ r ∉ p, ∃ s, r • x = 1 ⊗ₜ[R] s := by
7973
obtain ⟨r, hr, s, e⟩ := Ideal.ResidueField.exists_smul_eq_tmul_one _
8074
(Algebra.TensorProduct.comm _ _ _ x)
@@ -136,7 +130,7 @@ noncomputable def Fiber.algEquivAux₂ (q : Ideal (p.Fiber S)) [q.IsPrime] :
136130
/-- The localization of the fiber `p.Fiber S` is isomorphic to a quotient of a localization. -/
137131
noncomputable def Fiber.localizationAlgEquivQuotient (q : Ideal (p.Fiber S)) [q.IsPrime]
138132
[Algebra (Localization.AtPrime p) (Localization.AtPrime (q.comap includeRight))]
139-
[Localization.AtPrime.IsLiesOverAlgebra p (q.comap includeRight)] :
133+
[IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime (q.comap includeRight))] :
140134
letI r := q.comap includeRight
141135
letI Sr := Localization.AtPrime r
142136
Localization.AtPrime q ≃ₐ[Localization.AtPrime p] Sr ⧸ p.map (algebraMap R Sr) :=

‎Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -170,8 +170,10 @@ section
170170
open Localization AtPrime
171171

172172
variable (J : Ideal A) (K : Ideal B) [J.IsPrime] [K.IsPrime]
173-
[J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [IsLiesOverAlgebra I J]
174-
[K.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime K)] [IsLiesOverAlgebra I K]
173+
[J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
174+
[K.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime K)]
175+
[IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime J)]
176+
[IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime K)]
175177

176178
instance : IsLocalHom (algebraMap (Localization.AtPrime I) (Localization.AtPrime J)) := by
177179
rw [IsLiesOverAlgebra.algebraMap_eq]
@@ -200,7 +202,7 @@ instance (p : Ideal R) [p.IsPrime] : Algebra.EssFiniteType R p.ResidueField :=
200202
instance [Algebra.EssFiniteType R A]
201203
(p : Ideal R) [p.IsPrime] (q : Ideal A) [q.IsPrime] [q.LiesOver p]
202204
[Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
203-
[Localization.AtPrime.IsLiesOverAlgebra p q] :
205+
[IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)] :
204206
Algebra.EssFiniteType p.ResidueField q.ResidueField := by
205207
have : Algebra.EssFiniteType R q.ResidueField := .comp _ A _
206208
refine .of_comp R _ _

‎Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ variable (p : Ideal A) (q : Ideal B) [q.LiesOver p]
2323
section maximal
2424

2525
variable [p.IsMaximal] [q.IsMaximal] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
26-
[Localization.AtPrime.IsLiesOverAlgebra p q]
26+
[IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime q)]
2727

2828
attribute [local instance] Ideal.Quotient.field
2929

@@ -59,7 +59,7 @@ end maximal
5959
section prime
6060

6161
variable [p.IsPrime] [q.IsPrime] [Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
62-
[Localization.AtPrime.IsLiesOverAlgebra p q]
62+
[IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime q)]
6363

6464
instance : Algebra.IsAlgebraic (A ⧸ p) p.ResidueField :=
6565
IsLocalization.isAlgebraic _ (nonZeroDivisors (A ⧸ p))

‎Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ open scoped nonZeroDivisors TensorProduct
2626
variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
2727
variable (I : Ideal R) [I.IsPrime] (J : Ideal R[X]) [J.IsPrime] [J.LiesOver I]
2828
[Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
29-
[Localization.AtPrime.IsLiesOverAlgebra I J]
29+
[IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime J)]
3030

3131

3232
/-- `κ(I[X]) ≃ₐ[κ(I)] κ(I)(X)`. -/

‎Mathlib/RingTheory/Localization/AtPrime/Basic.lean‎

Lines changed: 25 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -367,19 +367,23 @@ noncomputable def algebraOfLiesOver
367367

368368
@[deprecated (since := "2026-04-24")] alias instAlgebraOfLiesOver := algebraOfLiesOver
369369

370-
/-- A predicate expressing that `Localization.AtPrime P` is an algebra over `Localization.AtPrime p`
371-
in the natural way when `P` lies over `p`. -/
372-
class IsLiesOverAlgebra (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p]
373-
[Algebra (Localization.AtPrime p) (Localization.AtPrime P)] : Prop where
374-
algebraMap_eq : algebraMap (Localization.AtPrime p) (Localization.AtPrime P) =
375-
Localization.localRingHom p P (algebraMap A B) Ideal.LiesOver.over
376-
377-
instance (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] :
378-
letI := algebraOfLiesOver p P; IsLiesOverAlgebra p P :=
379-
letI := algebraOfLiesOver p P; ⟨rfl⟩
370+
@[deprecated "Use `IsScalarTower` instead." (since := "2026-06-27")]
371+
abbrev IsLiesOverAlgebra (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime]
372+
[Algebra (Localization.AtPrime p) (Localization.AtPrime P)] :=
373+
IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime P)
374+
375+
theorem IsLiesOverAlgebra.algebraMap_eq (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime]
376+
[Algebra (Localization.AtPrime p) (Localization.AtPrime P)]
377+
[IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime P)] [P.LiesOver p] :
378+
algebraMap (Localization.AtPrime p) (Localization.AtPrime P) =
379+
Localization.localRingHom p P (algebraMap A B) Ideal.LiesOver.over := by
380+
symm
381+
apply localRingHom_unique
382+
simp [← IsScalarTower.algebraMap_apply]
380383

381384
instance (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p]
382-
[Algebra (Localization.AtPrime p) (Localization.AtPrime P)] [IsLiesOverAlgebra p P] :
385+
[Algebra (Localization.AtPrime p) (Localization.AtPrime P)]
386+
[IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime P)] :
383387
IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime P) :=
384388
.of_algebraMap_eq <| by
385389
simp [IsScalarTower.algebraMap_apply R A (Localization.AtPrime p),
@@ -388,9 +392,12 @@ instance (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p]
388392

389393
instance (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] (Q : Ideal C)
390394
[Q.IsPrime] [Q.LiesOver P] [Q.LiesOver p]
391-
[Algebra (Localization.AtPrime p) (Localization.AtPrime P)] [IsLiesOverAlgebra p P]
392-
[Algebra (Localization.AtPrime P) (Localization.AtPrime Q)] [IsLiesOverAlgebra P Q]
393-
[Algebra (Localization.AtPrime p) (Localization.AtPrime Q)] [IsLiesOverAlgebra p Q] :
395+
[Algebra (Localization.AtPrime p) (Localization.AtPrime P)]
396+
[Algebra (Localization.AtPrime P) (Localization.AtPrime Q)]
397+
[Algebra (Localization.AtPrime p) (Localization.AtPrime Q)]
398+
[IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime P)]
399+
[IsScalarTower B (Localization.AtPrime P) (Localization.AtPrime Q)]
400+
[IsScalarTower A (Localization.AtPrime p) (Localization.AtPrime Q)] :
394401
IsScalarTower (Localization.AtPrime p) (Localization.AtPrime P) (Localization.AtPrime Q) :=
395402
.of_algebraMap_eq' <| by
396403
simp [IsLiesOverAlgebra.algebraMap_eq, ← localRingHom_comp, ← IsScalarTower.algebraMap_eq]
@@ -423,8 +430,10 @@ section localAlg
423430
open AtPrime
424431

425432
variable {S} [Algebra R P] (J : Ideal S) (K : Ideal P) [J.IsPrime] [K.IsPrime]
426-
[J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)] [IsLiesOverAlgebra I J]
427-
[K.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime K)] [IsLiesOverAlgebra I K]
433+
[J.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime J)]
434+
[K.LiesOver I] [Algebra (Localization.AtPrime I) (Localization.AtPrime K)]
435+
[IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime J)]
436+
[IsScalarTower R (Localization.AtPrime I) (Localization.AtPrime K)]
428437

429438
/-- For an `R`-algebra homomorphism `f : S →ₐ[R] P` and prime ideals `J = f⁻¹(K)` lying over `I`,
430439
the induced algebra homomorphism from the localization of `S` at `J` to the localization of `P` at

‎Mathlib/RingTheory/QuasiFinite/Basic.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -277,7 +277,7 @@ lemma eq_of_le_of_under_eq [QuasiFinite R S] (P Q : Ideal S) [P.IsPrime] [Q.IsPr
277277

278278
instance [QuasiFinite R S] (P : Ideal R) [P.IsPrime] (Q : Ideal S) [Q.IsPrime] [Q.LiesOver P]
279279
[Algebra (Localization.AtPrime P) (Localization.AtPrime Q)]
280-
[Localization.AtPrime.IsLiesOverAlgebra P Q] :
280+
[IsScalarTower R (Localization.AtPrime P) (Localization.AtPrime Q)] :
281281
Module.Finite P.ResidueField Q.ResidueField :=
282282
have : QuasiFinite P.ResidueField Q.ResidueField := .of_restrictScalars R _ _
283283
.of_quasiFinite
@@ -424,7 +424,7 @@ lemma QuasiFiniteAt.eq_of_le_of_under_eq {P Q : Ideal S} [P.IsPrime] [Q.IsPrime]
424424

425425
instance (p : Ideal R) [p.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p] [QuasiFiniteAt R P]
426426
[Algebra (Localization.AtPrime p) (Localization.AtPrime P)]
427-
[Localization.AtPrime.IsLiesOverAlgebra p P] :
427+
[IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime P)] :
428428
Module.Finite p.ResidueField P.ResidueField := by
429429
let m := IsLocalRing.maximalIdeal (Localization.AtPrime P)
430430
let : m.LiesOver p := .trans _ P _
@@ -551,7 +551,7 @@ lemma _root_.Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver
551551
lemma _root_.Ideal.Fiber.lift_residueField_surjective [Algebra.FiniteType R S]
552552
(p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime] [q.LiesOver p] [Algebra.QuasiFiniteAt R q]
553553
[Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
554-
[Localization.AtPrime.IsLiesOverAlgebra p q] :
554+
[IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)] :
555555
Function.Surjective (Algebra.TensorProduct.lift (Algebra.ofId _ _)
556556
(IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _ :
557557
p.Fiber S →ₐ[p.ResidueField] q.ResidueField) := by

‎Mathlib/RingTheory/QuasiFinite/Weakly.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,7 @@ instance comap_algEquiv (p : Ideal S) [p.IsPrime]
121121
lemma finite_residueField
122122
[p.IsPrime] [q.LiesOver p] [WeaklyQuasiFiniteAt R q]
123123
[Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
124-
[Localization.AtPrime.IsLiesOverAlgebra p q] :
124+
[IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)] :
125125
Module.Finite p.ResidueField q.ResidueField := by
126126
let r := q.map (Ideal.Quotient.mk ((q.under R).map (algebraMap R S)))
127127
have : r.LiesOver q :=

‎Mathlib/RingTheory/RamificationInertia/Inertia.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ noncomputable def inertiaDeg' : ℕ :=
4747

4848
theorem inertiaDeg'_def [hq : q.IsPrime]
4949
[Algebra (Localization.AtPrime (q.under R)) (Localization.AtPrime q)]
50-
[Localization.AtPrime.IsLiesOverAlgebra (q.under R) q] :
50+
[IsScalarTower R (Localization.AtPrime (q.under R)) (Localization.AtPrime q)] :
5151
q.inertiaDeg' R = Module.finrank (q.under R).ResidueField q.ResidueField := by
5252
convert! dif_pos hq
5353
simp [Algebra.algebra_ext_iff, Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq]
@@ -70,7 +70,7 @@ variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
7070

7171
theorem inertiaDeg'_eq [q.LiesOver p] [q.IsPrime] [p.IsPrime]
7272
[Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
73-
[Localization.AtPrime.IsLiesOverAlgebra p q] :
73+
[IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q)] :
7474
q.inertiaDeg' R = Module.finrank p.ResidueField q.ResidueField := by
7575
have := Ideal.over_def q p
7676
subst this

‎Mathlib/RingTheory/RamificationInertia/Ramification.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -145,8 +145,7 @@ theorem ramificationIdx_eq_ramificationIdx'
145145
/-- See `ramificationIdx'_tower` for a version that does not assume primality. -/
146146
theorem ramificationIdx'_tower' [q.IsPrime] [r.IsPrime] [r.LiesOver q]
147147
[Algebra (Localization.AtPrime q) (Localization.AtPrime r)]
148-
[Localization.AtPrime.IsLiesOverAlgebra q r]
149-
[Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)] :
148+
[IsScalarTower S (Localization.AtPrime q) (Localization.AtPrime r)] :
150149
r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S := by
151150
have : q.LiesOver (r.under R) := LiesOver.tower_bot r q (r.under R)
152151
let f := (Ideal.quotientEquivAlgOfEq (Localization.AtPrime r)

0 commit comments

Comments
 (0)