Ramification index

Let S/R be an extension of rings, and let q be a prime ideal of S lying over a prime ideal p of R. Let Sq be the localization of S and q, and let pSq be the image of p in Sq. Then the ramification index of q over R is defined to be the length of the quotient Sq/pSq as an Sq-module.

Main definitions

• Ideal.ramificationIdx' q R: The ramification index of q over R.

Main statements

• ramificationIdx_eq_ramificationIdx': The ramification index agrees with the usual definition in the case of Dedekind domains.
• ramificationIdx'_tower: Ramification index is multiplicative in towers.

noncomputable def Ideal.ramificationIdx' {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] : ℕ

Let S/R be an extension of rings, and let q be a prime ideal of S lying over a prime ideal p of R. Let Sq be the localization of S and q, and let pSq be the image of p in Sq. Then the ramification index of q over R is defined to be the length of the quotient Sq/pSq as an Sq-module.

When q is not prime, we use a junk value of 0.

This will eventually replace the existing definition of Ideal.ramificationIdx.

Equations

• One or more equations did not get rendered due to their size.

theorem Ideal.ramificationIdx'_def {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] [q.IsPrime] : q.ramificationIdx' R = (Module.length (Localization.AtPrime q) (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))).toNat

theorem Ideal.ramificationIdx'_of_not_isPrime {S : Type u_1} [CommRing S] (q : Ideal S) (R : Type u_2) [CommRing R] [Algebra R S] (hq : ¬q.IsPrime) : q.ramificationIdx' R = 0

theorem Ideal.ramificationIdx'_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [q.LiesOver p] [q.IsPrime] : q.ramificationIdx' R = (Module.length (Localization.AtPrime q) (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) p)).toNat

theorem Ideal.ramificationIdx_eq_ramificationIdx' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) (q : Ideal S) [IsDomain R] [IsDedekindDomain S] [Module.IsTorsionFree R S] [q.LiesOver p] [hq : q.IsPrime] (hp : p ≠ ⊥) : p.ramificationIdx q = q.ramificationIdx' R

theorem Ideal.ramificationIdx'_tower' {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [q.IsPrime] [r.IsPrime] [r.LiesOver q] [Algebra (Localization.AtPrime q) (Localization.AtPrime r)] [Localization.AtPrime.IsLiesOverAlgebra q r] [Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)] : r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S

See ramificationIdx'_tower for a version that does not assume primality.

theorem Ideal.ramificationIdx'_tower {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T) [r.LiesOver q] [Module.Flat S T] : r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S

See ramificationIdx'_tower' for a version that only assumes local flatness.