Ramification index

Given P : Ideal S lying over p : Ideal R for the ring extension f : R →+* S (assuming P and p are prime or maximal where needed), the ramification index Ideal.ramificationIdx p P is the multiplicity of P in map f p.

Implementation notes

Often the above theory is set up in the case where:

• R is the ring of integers of a number field K,
• L is a finite separable extension of K,
• S is the integral closure of R in L,
• p and P are maximal ideals,
• P is an ideal lying over p. We will try to relax the above hypotheses as much as possible.

Notation

In this file, e stands for the ramification index of P over p, leaving p and P implicit.

noncomputable def Ideal.ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) : ℕ

The ramification index of P over p is the largest exponent n such that p is contained in P^n.

In particular, if p is not contained in P^n, then the ramification index is 0.

If there is no largest such n (e.g. because p = ⊥), then ramificationIdx is defined to be 0.

Equations

• p.ramificationIdx P = sSup {n : ℕ | Ideal.map (algebraMap R S) p ≤ P ^ n}

theorem Ideal.ramificationIdx_eq_find {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} [DecidablePred fun (n : ℕ) => ∀ (k : ℕ), map (algebraMap R S) p ≤ P ^ k → k ≤ n] (h : ∃ (n : ℕ), ∀ (k : ℕ), map (algebraMap R S) p ≤ P ^ k → k ≤ n) : p.ramificationIdx P = Nat.find h

theorem Ideal.ramificationIdx_eq_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} (h : ∀ (n : ℕ), ∃ (k : ℕ), map (algebraMap R S) p ≤ P ^ k ∧ n < k) : p.ramificationIdx P = 0

theorem Ideal.ramificationIdx_spec {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} {n : ℕ} (hle : map (algebraMap R S) p ≤ P ^ n) (hgt : ¬map (algebraMap R S) p ≤ P ^ (n + 1)) : p.ramificationIdx P = n

theorem Ideal.ramificationIdx_lt {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} {n : ℕ} (hgt : ¬map (algebraMap R S) p ≤ P ^ n) : p.ramificationIdx P < n

@[simp]

theorem Ideal.ramificationIdx_bot {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {P : Ideal S} : ⊥.ramificationIdx P = 0

@[simp]

theorem Ideal.ramificationIdx_of_not_le {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} (h : ¬map (algebraMap R S) p ≤ P) : p.ramificationIdx P = 0

theorem Ideal.ramificationIdx_bot' {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} (hp : p ≠ ⊥) (hf : Function.Injective ⇑(algebraMap R S)) : p.ramificationIdx ⊥ = 0

theorem Ideal.ramificationIdx_ne_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} {e : ℕ} (he : e ≠ 0) (hle : map (algebraMap R S) p ≤ P ^ e) (hnle : ¬map (algebraMap R S) p ≤ P ^ (e + 1)) : p.ramificationIdx P ≠ 0

theorem Ideal.le_pow_of_le_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} {n : ℕ} (hn : n ≤ p.ramificationIdx P) : map (algebraMap R S) p ≤ P ^ n

theorem Ideal.le_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} : map (algebraMap R S) p ≤ P ^ p.ramificationIdx P

theorem Ideal.le_comap_pow_ramificationIdx {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} : p ≤ comap (algebraMap R S) (P ^ p.ramificationIdx P)

theorem Ideal.le_comap_of_ramificationIdx_ne_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} (h : p.ramificationIdx P ≠ 0) : p ≤ comap (algebraMap R S) P

theorem Ideal.ramificationIdx_comap_eq {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) {S₁ : Type u_1} [CommRing S₁] [Algebra R S₁] (e : S ≃ₐ[R] S₁) (P : Ideal S₁) : p.ramificationIdx (comap e P) = p.ramificationIdx P

theorem Ideal.ramificationIdx_map_eq {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) {S₁ : Type u_1} [CommRing S₁] [Algebra R S₁] {E : Type u_2} [EquivLike E S S₁] [AlgEquivClass E R S S₁] (P : Ideal S) (e : E) : p.ramificationIdx (map e P) = p.ramificationIdx P

theorem Ideal.ramificationIdx_ne_one_iff {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} (hp : map (algebraMap R S) p ≤ P) : p.ramificationIdx P ≠ 1 ↔ map (algebraMap R S) p ≤ P ^ 2

theorem Ideal.ramificationIdx_eq_one_of_map_localization {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} [P.IsPrime] [IsNoetherianRing S] (hpP : map (algebraMap R S) p ≤ P) (hp : P ≠ ⊥) (hp' : P.primeCompl ≤ nonZeroDivisors S) (H : map (algebraMap R (Localization.AtPrime P)) p = IsLocalRing.maximalIdeal (Localization.AtPrime P)) : p.ramificationIdx P = 1

The converse is true when S is a Dedekind domain. See Ideal.ramificationIdx_eq_one_iff_of_isDedekindDomain.

theorem Ideal.ramificationIdx_map_self_eq_one {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} [IsDedekindDomain S] (h₁ : map (algebraMap R S) p ≠ ⊤) (h₂ : map (algebraMap R S) p ≠ ⊥) : p.ramificationIdx (map (algebraMap R S) p) = 1

theorem Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} [IsDedekindDomain S] (hp0 : map (algebraMap R S) p ≠ ⊥) (hP : P.IsPrime) (hP0 : P ≠ ⊥) : p.ramificationIdx P = Multiset.count P (UniqueFactorizationMonoid.normalizedFactors (map (algebraMap R S) p))

theorem Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} [IsDedekindDomain S] (hp : map (algebraMap R S) p ≠ ⊥) (hP : P.IsPrime) : p.ramificationIdx P = multiplicity P (map (algebraMap R S) p)

theorem Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} [IsDedekindDomain S] (hp0 : map (algebraMap R S) p ≠ ⊥) (hP : P.IsPrime) (hP0 : P ≠ ⊥) : p.ramificationIdx P = Multiset.count P (UniqueFactorizationMonoid.factors (map (algebraMap R S) p))

theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] {p : Ideal R} {P : Ideal S} [IsDedekindDomain S] (hp0 : map (algebraMap R S) p ≠ ⊥) (hP : P.IsPrime) (le : map (algebraMap R S) p ≤ P) : p.ramificationIdx P ≠ 0

theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero_of_liesOver {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [IsDedekindDomain S] [IsDomain R] [Module.IsTorsionFree R S] (P : Ideal S) [hP : P.IsPrime] {p : Ideal R} (hp : p ≠ ⊥) [hPp : P.LiesOver p] : p.ramificationIdx P ≠ 0

theorem Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [IsDedekindDomain S] {p : Ideal R} {P : Ideal S} [P.IsPrime] (hp : P ≠ ⊥) (hpP : map (algebraMap R S) p ≤ P) : p.ramificationIdx P = 1 ↔ map (algebraMap R (Localization.AtPrime P)) p = IsLocalRing.maximalIdeal (Localization.AtPrime P)

theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_ne {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [IsDedekindDomain S] [IsDedekindDomain R] {v : Ideal R} {w : Ideal S} {p : Ideal R} (hv : Irreducible v) (hp : Prime p) (hvp : v ≠ p) [w.LiesOver v] : emultiplicity w (map (algebraMap R S) p) = 0

theorem Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [IsDedekindDomain S] [IsDedekindDomain R] [FaithfulSMul R S] {v : Ideal R} {w : Ideal S} {I : Ideal R} (h : I ≠ ⊥) (hv : Irreducible v) (hw : Irreducible w) (hw_bot : w ≠ ⊥) [w.LiesOver v] : emultiplicity w (map (algebraMap R S) I) = ↑(v.ramificationIdx w) * emultiplicity v I

If v is an irreducible ideal of R, w is an irreducible ideal of S lying over v, and I is an ideal of R, then the multiplicity of w in I.map (algebraMap R S) is given by the multiplicity of v in I multiplied by the ramification index of w over v.

theorem Ideal.ramificationIdx_algebra_tower {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [IsDedekindDomain S] [IsDedekindDomain T] {p : Ideal R} {P : Ideal S} {Q : Ideal T} [hpm : P.IsPrime] [hqm : Q.IsPrime] (hg0 : map (algebraMap S T) P ≠ ⊥) (hfg : map (algebraMap R T) p ≠ ⊥) (hg : map (algebraMap S T) P ≤ Q) : p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q

Let T / S / R be a tower of algebras, p, P, Q be ideals in R, S, T respectively, and P and Q are prime. If P = Q ∩ S, then e (Q | p) = e (P | p) * e (Q | P).

@[deprecated Ideal.ramificationIdx_algebra_tower (since := "2026-03-25")]

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 S T] [Algebra R T] [IsScalarTower R S T] [IsDedekindDomain S] [IsDedekindDomain T] {p : Ideal R} {P : Ideal S} {Q : Ideal T} [hpm : P.IsPrime] [hqm : Q.IsPrime] (hg0 : map (algebraMap S T) P ≠ ⊥) (hfg : map (algebraMap R T) p ≠ ⊥) (hg : map (algebraMap S T) P ≤ Q) : p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q

Alias of Ideal.ramificationIdx_algebra_tower.

---

Let T / S / R be a tower of algebras, p, P, Q be ideals in R, S, T respectively, and P and Q are prime. If P = Q ∩ S, then e (Q | p) = e (P | p) * e (Q | P).

theorem Ideal.ramificationIdx_algebra_tower' {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [IsDedekindDomain S] [IsDedekindDomain T] [IsDomain R] [Module.IsTorsionFree R S] [Module.IsTorsionFree S T] (p : Ideal R) (P : Ideal S) (Q : Ideal T) [Q.IsPrime] [Q.LiesOver P] [P.LiesOver p] : p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q