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.
Note: This definition of ramification index will eventually be replaced by Ideal.ramificationIdx.
Instances For
@[deprecated Ideal.ramificationIdx'_eq_find (since := "2026-07-01")]
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)
:
Alias of Ideal.ramificationIdx'_eq_find.
@[deprecated Ideal.ramificationIdx'_eq_zero (since := "2026-07-01")]
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)
:
Alias of Ideal.ramificationIdx'_eq_zero.
@[deprecated Ideal.ramificationIdx'_spec (since := "2026-07-01")]
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))
:
Alias of Ideal.ramificationIdx'_spec.
@[deprecated Ideal.ramificationIdx'_lt (since := "2026-07-01")]
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)
:
Alias of Ideal.ramificationIdx'_lt.
@[deprecated Ideal.ramificationIdx'_bot (since := "2026-07-01")]
theorem
Ideal.ramificationIdx_bot
{R : Type u}
[CommRing R]
{S : Type v}
[CommRing S]
[Algebra R S]
{P : Ideal S}
:
Alias of Ideal.ramificationIdx'_bot.
@[deprecated Ideal.ramificationIdx'_of_not_le (since := "2026-07-01")]
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)
:
Alias of Ideal.ramificationIdx'_of_not_le.
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))
:
@[deprecated Ideal.ramificationIdx'_bot' (since := "2026-07-01")]
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))
:
Alias of Ideal.ramificationIdx'_bot'.
@[deprecated Ideal.ramificationIdx'_ne_zero (since := "2026-07-01")]
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))
:
Alias of Ideal.ramificationIdx'_ne_zero.
@[deprecated Ideal.le_pow_of_le_ramificationIdx' (since := "2026-07-01")]
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)
:
Alias of Ideal.le_pow_of_le_ramificationIdx'.
@[deprecated Ideal.le_pow_ramificationIdx' (since := "2026-07-01")]
theorem
Ideal.le_pow_ramificationIdx
{R : Type u}
[CommRing R]
{S : Type v}
[CommRing S]
[Algebra R S]
{p : Ideal R}
{P : Ideal S}
:
Alias of Ideal.le_pow_ramificationIdx'.
@[deprecated Ideal.le_comap_pow_ramificationIdx' (since := "2026-07-01")]
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}
:
Alias of Ideal.le_comap_pow_ramificationIdx'.
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)
:
@[deprecated Ideal.le_comap_of_ramificationIdx'_ne_zero (since := "2026-07-01")]
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)
:
@[deprecated Ideal.ramificationIdx'_comap_eq (since := "2026-07-01")]
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₁)
:
Alias of Ideal.ramificationIdx'_comap_eq.
@[deprecated Ideal.ramificationIdx'_map_eq (since := "2026-07-01")]
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)
:
Alias of Ideal.ramificationIdx'_map_eq.
@[deprecated Ideal.ramificationIdx'_ne_one_iff (since := "2026-07-01")]
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)
:
Alias of Ideal.ramificationIdx'_ne_one_iff.
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))
:
The converse is true when S is a Dedekind domain.
See Ideal.ramificationIdx'_eq_one_iff_of_isDedekindDomain.
@[deprecated Ideal.ramificationIdx'_eq_one_of_map_localization (since := "2026-07-01")]
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))
:
Alias of Ideal.ramificationIdx'_eq_one_of_map_localization.
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 ≠ ⊥)
:
@[deprecated Ideal.ramificationIdx'_map_self_eq_one (since := "2026-07-01")]
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 ≠ ⊥)
:
Alias of Ideal.ramificationIdx'_map_self_eq_one.
theorem
Ideal.ramificationIdx'_le_ramificationIdx'
{R : Type u}
[CommRing R]
{S : Type v}
[CommRing S]
[Algebra R S]
(p : Ideal R)
(P : Ideal S)
{T : Type u_2}
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
(Q : Ideal T)
(hp : p = comap (algebraMap R S) P)
(h : p.ramificationIdx' Q ≠ 0)
:
@[deprecated Ideal.ramificationIdx'_le_ramificationIdx' (since := "2026-07-01")]
theorem
Ideal.ramificationIdx_le_ramificationIdx
{R : Type u}
[CommRing R]
{S : Type v}
[CommRing S]
[Algebra R S]
(p : Ideal R)
(P : Ideal S)
{T : Type u_2}
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
(Q : Ideal T)
(hp : p = comap (algebraMap R S) P)
(h : p.ramificationIdx' Q ≠ 0)
:
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)
:
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)
:
@[deprecated Ideal.IsDedekindDomain.ramificationIdx'_ne_zero (since := "2026-07-01")]
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)
:
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]
:
@[deprecated Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver (since := "2026-07-01")]
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]
:
Alias of Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver.
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)
@[deprecated Ideal.IsDedekindDomain.ramificationIdx'_eq_one_iff (since := "2026-07-01")]
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)
Alias of Ideal.IsDedekindDomain.ramificationIdx'_eq_one_iff.
theorem
Ideal.IsDedekindDomain.ramificationIdx'_le_ramificationIdx'
{R : Type u}
[CommRing R]
{S : Type v}
[CommRing S]
[Algebra R S]
[IsDedekindDomain S]
[IsDomain R]
[Module.IsTorsionFree R S]
{S₀ : Type u_2}
[CommRing S₀]
[Algebra R S₀]
[Algebra S₀ S]
[IsScalarTower R S₀ S]
(p : Ideal R)
(P : Ideal S₀)
(Q : Ideal S)
[Q.LiesOver p]
[hP : P.LiesOver p]
[Q.IsPrime]
(hp : p ≠ ⊥)
:
@[deprecated Ideal.IsDedekindDomain.ramificationIdx'_le_ramificationIdx' (since := "2026-07-01")]
theorem
Ideal.IsDedekindDomain.ramificationIdx_le_ramificationIdx
{R : Type u}
[CommRing R]
{S : Type v}
[CommRing S]
[Algebra R S]
[IsDedekindDomain S]
[IsDomain R]
[Module.IsTorsionFree R S]
{S₀ : Type u_2}
[CommRing S₀]
[Algebra R S₀]
[Algebra S₀ S]
[IsScalarTower R S₀ S]
(p : Ideal R)
(P : Ideal S₀)
(Q : Ideal S)
[Q.LiesOver p]
[hP : P.LiesOver p]
[Q.IsPrime]
(hp : p ≠ ⊥)
:
Alias of Ideal.IsDedekindDomain.ramificationIdx'_le_ramificationIdx'.
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]
:
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]
:
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.
@[deprecated Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx'_mul (since := "2026-07-01")]
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]
:
Alias of Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx'_mul.
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)
:
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-07-01")]
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)
:
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]
:
@[deprecated Ideal.ramificationIdx'_algebra_tower' (since := "2026-07-01")]
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]
:
Alias of Ideal.ramificationIdx'_algebra_tower'.