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:
Ris the ring of integers of a number fieldK,Lis a finite separable extension ofK,Sis the integral closure ofRinL,pandPare maximal ideals,Pis an ideal lying overp. 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.
Instances For
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
@[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)
:
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)
:
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