# Ramification index and inertia degree #

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 f p P is the multiplicity of P in map f p, and the inertia degree Ideal.inertiaDeg f p P is the degree of the field extension (S / P) : (R / p).

## Main results #

The main theorem Ideal.sum_ramification_inertia states that for all coprime P lying over p, Σ P, ramification_idx f p P * inertia_deg f p P equals the degree of the field extension Frac(S) : Frac(R).

## 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 and f for the inertia degree of P over p, leaving p and P implicit.

noncomputable def Ideal.ramificationIdx {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) :

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
Instances For
theorem Ideal.ramificationIdx_eq_find {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } (h : ∃ (n : ), ∀ (k : ), P ^ kk n) :
=
theorem Ideal.ramificationIdx_eq_zero {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } (h : ∀ (n : ), ∃ (k : ), P ^ k n < k) :
= 0
theorem Ideal.ramificationIdx_spec {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } {n : } (hle : P ^ n) (hgt : ¬ P ^ (n + 1)) :
= n
theorem Ideal.ramificationIdx_lt {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } {n : } (hgt : ¬ P ^ n) :
< n
@[simp]
theorem Ideal.ramificationIdx_bot {R : Type u} [] {S : Type v} [] {f : R →+* S} {P : } :
= 0
@[simp]
theorem Ideal.ramificationIdx_of_not_le {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } (h : ¬ P) :
= 0
theorem Ideal.ramificationIdx_ne_zero {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } {e : } (he : e 0) (hle : P ^ e) (hnle : ¬ P ^ (e + 1)) :
0
theorem Ideal.le_pow_of_le_ramificationIdx {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } {n : } (hn : n ) :
P ^ n
theorem Ideal.le_pow_ramificationIdx {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } :
P ^
theorem Ideal.le_comap_pow_ramificationIdx {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } :
p Ideal.comap f (P ^ )
theorem Ideal.le_comap_of_ramificationIdx_ne_zero {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } (h : 0) :
p
theorem Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } [] (hp0 : ) (hP : P.IsPrime) (hP0 : P ) :
theorem Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } [] (hp0 : ) (hP : P.IsPrime) (hP0 : P ) :
theorem Ideal.IsDedekindDomain.ramificationIdx_ne_zero {R : Type u} [] {S : Type v} [] {f : R →+* S} {p : } {P : } [] (hp0 : ) (hP : P.IsPrime) (le : P) :
0
noncomputable def Ideal.inertiaDeg {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [p.IsMaximal] :

The inertia degree of P : Ideal S lying over p : Ideal R is the degree of the extension (S / P) : (R / p).

We do not assume P lies over p in the definition; we return 0 instead.

See inertiaDeg_algebraMap for the common case where f = algebraMap R S and there is an algebra structure R / p → S / P.

Equations
Instances For
@[simp]
theorem Ideal.inertiaDeg_of_subsingleton {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [hp : p.IsMaximal] [hQ : Subsingleton (S P)] :
= 0
@[simp]
theorem Ideal.inertiaDeg_algebraMap {R : Type u} [] {S : Type v} [] (p : ) (P : ) [Algebra R S] [Algebra (R p) (S P)] [IsScalarTower R (R p) (S P)] [hp : p.IsMaximal] :
theorem Ideal.FinrankQuotientMap.linearIndependent_of_nontrivial {R : Type u} [] {S : Type v} [] [Algebra R S] (K : Type u_1) [] [Algebra R K] [hRK : ] {V : Type u_3} {V' : Type u_4} {V'' : Type u_5} [] [Module R V] [Module K V] [] [] [Module R V'] [Module S V'] [IsScalarTower R S V'] [AddCommGroup V''] [Module R V''] [] (hRS : RingHom.ker () ) (f : V'' →ₗ[R] V) (hf : ) (f' : V'' →ₗ[R] V') {ι : Type u_6} {b : ιV''} (hb' : LinearIndependent S (f' b)) :

Let V be a vector space over K = Frac(R), S / R a ring extension and V' a module over S. If b, in the intersection V'' of V and V', is linear independent over S in V', then it is linear independent over R in V.

The statement we prove is actually slightly more general:

• it suffices that the inclusion algebraMap R S : R → S is nontrivial
• the function f' : V'' → V' doesn't need to be injective
theorem Ideal.FinrankQuotientMap.span_eq_top {R : Type u} [] {S : Type v} [] (p : ) [Algebra R S] {K : Type u_1} [] [Algebra R K] {L : Type u_2} [] [Algebra S L] [] [] [] [Algebra K L] [] [Algebra R L] [] [] [] [] (hp : p ) (b : Set S) (hb' : Submodule.restrictScalars R (Ideal.map () p) = ) :
Submodule.span K (() '' b) =

If b mod p spans S/p as R/p-space, then b itself spans Frac(S) as K-space.

Here,

• p is an ideal of R such that R / p is nontrivial
• K is a field that has an embedding of R (in particular we can take K = Frac(R))
• L is a field extension of K
• S is the integral closure of R in L

More precisely, we avoid quotients in this statement and instead require that b ∪ pS spans S.

theorem Ideal.finrank_quotient_map {R : Type u} [] {S : Type v} [] (p : ) [Algebra R S] (K : Type u_1) [] [Algebra R K] [hRK : ] (L : Type u_2) [] [Algebra S L] [] [] [] [Algebra K L] [Algebra R L] [] [] [] [hp : p.IsMaximal] [] :

If p is a maximal ideal of R, and S is the integral closure of R in L, then the dimension [S/pS : R/p] is equal to [Frac(S) : Frac(R)].

noncomputable instance Ideal.Quotient.algebraQuotientPowRamificationIdx {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) :
Algebra (R p) (S P ^ )

R / p has a canonical map to S / (P ^ e), where e is the ramification index of P over p.

Equations
@[simp]
theorem Ideal.Quotient.algebraMap_quotient_pow_ramificationIdx {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) (x : R) :
(algebraMap (R p) (S P ^ )) ( x) = (Ideal.Quotient.mk (P ^ )) (f x)
def Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [hfp : NeZero ()] :
Algebra (R p) (S P)

If P lies over p, then R / p has a canonical map to S / P.

This can't be an instance since the map f : R → S is generally not inferrable.

Equations
Instances For
@[simp]
theorem Ideal.Quotient.algebraMap_quotient_of_ramificationIdx_neZero {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [hfp : NeZero ()] (x : R) :
(algebraMap (R p) (S P)) ( x) = (f x)
@[simp]
theorem Ideal.powQuotSuccInclusion_apply_coe {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) (i : ) (x : (Ideal.map (Ideal.Quotient.mk (P ^ )) (P ^ (i + 1)))) :
(() x) = x
def Ideal.powQuotSuccInclusion {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) (i : ) :
(Ideal.map (Ideal.Quotient.mk (P ^ )) (P ^ (i + 1))) →ₗ[R p] (Ideal.map (Ideal.Quotient.mk (P ^ )) (P ^ i))

The inclusion (P^(i + 1) / P^e) ⊂ (P^i / P^e).

Equations
Instances For
theorem Ideal.powQuotSuccInclusion_injective {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) (i : ) :
noncomputable def Ideal.quotientToQuotientRangePowQuotSuccAux {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) {i : } {a : S} (a_mem : a P ^ i) :
S P(Ideal.map (Ideal.Quotient.mk (P ^ )) (P ^ i))

S ⧸ P embeds into the quotient by P^(i+1) ⧸ P^e as a subspace of P^i ⧸ P^e. See quotientToQuotientRangePowQuotSucc for this as a linear map, and quotientRangePowQuotSuccInclusionEquiv for this as a linear equivalence.

Equations
Instances For
theorem Ideal.quotientToQuotientRangePowQuotSuccAux_mk {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) {i : } {a : S} (a_mem : a P ^ i) (x : S) :
= Submodule.Quotient.mk (Ideal.Quotient.mk (P ^ )) (a * x),
noncomputable def Ideal.quotientToQuotientRangePowQuotSucc {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [hfp : NeZero ()] {i : } {a : S} (a_mem : a P ^ i) :
S P →ₗ[R p] (Ideal.map (Ideal.Quotient.mk (P ^ )) (P ^ i))

S ⧸ P embeds into the quotient by P^(i+1) ⧸ P^e as a subspace of P^i ⧸ P^e.

Equations
• = { toFun := , map_add' := , map_smul' := }
Instances For
theorem Ideal.quotientToQuotientRangePowQuotSucc_mk {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [hfp : NeZero ()] {i : } {a : S} (a_mem : a P ^ i) (x : S) :
() = Submodule.Quotient.mk (Ideal.Quotient.mk (P ^ )) (a * x),
theorem Ideal.quotientToQuotientRangePowQuotSucc_injective {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [hfp : NeZero ()] [] [P.IsPrime] {i : } (hi : i < ) {a : S} (a_mem : a P ^ i) (a_not_mem : aP ^ (i + 1)) :
theorem Ideal.quotientToQuotientRangePowQuotSucc_surjective {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [hfp : NeZero ()] [] (hP0 : P ) [hP : P.IsPrime] {i : } (hi : i < ) {a : S} (a_mem : a P ^ i) (a_not_mem : aP ^ (i + 1)) :
noncomputable def Ideal.quotientRangePowQuotSuccInclusionEquiv {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [hfp : NeZero ()] [] [P.IsPrime] (hP : P ) {i : } (hi : i < ) :
((Ideal.map (Ideal.Quotient.mk (P ^ )) (P ^ i)) ) ≃ₗ[R p] S P

Quotienting P^i / P^e by its subspace P^(i+1) ⧸ P^e is R ⧸ p-linearly isomorphic to S ⧸ P.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Ideal.rank_pow_quot_aux {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [hfp : NeZero ()] [] [p.IsMaximal] [P.IsPrime] (hP0 : P ) {i : } (hi : i < ) :
Module.rank (R p) (Ideal.map (Ideal.Quotient.mk (P ^ )) (P ^ i)) = Module.rank (R p) (S P) + Module.rank (R p) (Ideal.map (Ideal.Quotient.mk (P ^ )) (P ^ (i + 1)))

Since the inclusion (P^(i + 1) / P^e) ⊂ (P^i / P^e) has a kernel isomorphic to P / S, [P^i / P^e : R / p] = [P^(i+1) / P^e : R / p] + [P / S : R / p]

theorem Ideal.rank_pow_quot {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [hfp : NeZero ()] [] [p.IsMaximal] [P.IsPrime] (hP0 : P ) (i : ) (hi : i ) :
Module.rank (R p) (Ideal.map (Ideal.Quotient.mk (P ^ )) (P ^ i)) = ( - i) Module.rank (R p) (S P)
theorem Ideal.rank_prime_pow_ramificationIdx {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [] [p.IsMaximal] [P.IsPrime] (hP0 : P ) (he : 0) :
Module.rank (R p) (S P ^ ) = Module.rank (R p) (S P)

If p is a maximal ideal of R, S extends R and P^e lies over p, then the dimension [S/(P^e) : R/p] is equal to e * [S/P : R/p].

theorem Ideal.finrank_prime_pow_ramificationIdx {R : Type u} [] {S : Type v} [] (f : R →+* S) (p : ) (P : ) [] (hP0 : P ) [p.IsMaximal] [P.IsPrime] (he : 0) :

If p is a maximal ideal of R, S extends R and P^e lies over p, then the dimension [S/(P^e) : R/p], as a natural number, is equal to e * [S/P : R/p].

## Properties of the factors of p.map (algebraMap R S)#

theorem Ideal.Factors.ne_bot {R : Type u} [] {S : Type v} [] (p : ) [] [Algebra R S] (P : { x : // x ().toFinset }) :
P
instance Ideal.Factors.isPrime {R : Type u} [] {S : Type v} [] (p : ) [] [Algebra R S] (P : { x : // x ().toFinset }) :
(P).IsPrime
Equations
• =
theorem Ideal.Factors.ramificationIdx_ne_zero {R : Type u} [] {S : Type v} [] (p : ) [] [Algebra R S] (P : { x : // x ().toFinset }) :
instance Ideal.Factors.fact_ramificationIdx_neZero {R : Type u} [] {S : Type v} [] (p : ) [] [Algebra R S] (P : { x : // x ().toFinset }) :
Equations
• =
instance Ideal.Factors.isScalarTower {R : Type u} [] {S : Type v} [] (p : ) [] [Algebra R S] (P : { x : // x ().toFinset }) :
IsScalarTower R (R p) (S P)
Equations
• =
theorem Ideal.Factors.finrank_pow_ramificationIdx {R : Type u} [] {S : Type v} [] (p : ) [] [Algebra R S] [p.IsMaximal] (P : { x : // x ().toFinset }) :
instance Ideal.Factors.finiteDimensional_quotient {R : Type u} [] {S : Type v} [] (p : ) [] [Algebra R S] [] [p.IsMaximal] (P : { x : // x ().toFinset }) :
FiniteDimensional (R p) (S P)
Equations
• =
theorem Ideal.Factors.inertiaDeg_ne_zero {R : Type u} [] {S : Type v} [] (p : ) [] [Algebra R S] [] [p.IsMaximal] (P : { x : // x ().toFinset }) :
instance Ideal.Factors.finiteDimensional_quotient_pow {R : Type u} [] {S : Type v} [] (p : ) [] [Algebra R S] [] [p.IsMaximal] (P : { x : // x ().toFinset }) :
Equations
• =
noncomputable def Ideal.Factors.piQuotientEquiv {R : Type u} [] {S : Type v} [] [] [Algebra R S] (p : ) (hp : Ideal.map () p ) :
S Ideal.map () p ≃+* ((P : { x : // x ().toFinset }) → S P ^ Ideal.ramificationIdx () p P)

Chinese remainder theorem for a ring of integers: if the prime ideal p : Ideal R factors in S as ∏ i, P i ^ e i, then S ⧸ I factors as Π i, R ⧸ (P i ^ e i).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Ideal.Factors.piQuotientEquiv_mk {R : Type u} [] {S : Type v} [] [] [Algebra R S] (p : ) (hp : Ideal.map () p ) (x : S) :
((Ideal.Quotient.mk (Ideal.map () p)) x) = fun (x_1 : { x : // x ().toFinset }) => (Ideal.Quotient.mk (x_1 ^ Ideal.ramificationIdx () p x_1)) x
@[simp]
theorem Ideal.Factors.piQuotientEquiv_map {R : Type u} [] {S : Type v} [] [] [Algebra R S] (p : ) (hp : Ideal.map () p ) (x : R) :
((algebraMap R (S Ideal.map () p)) x) = fun (x_1 : { x : // x ().toFinset }) => (Ideal.Quotient.mk (x_1 ^ Ideal.ramificationIdx () p x_1)) (() x)
noncomputable def Ideal.Factors.piQuotientLinearEquiv {R : Type u} [] (S : Type v) [] [] [Algebra R S] (p : ) (hp : Ideal.map () p ) :
(S Ideal.map () p) ≃ₗ[R p] (P : { x : // x ().toFinset }) → S P ^ Ideal.ramificationIdx () p P

Chinese remainder theorem for a ring of integers: if the prime ideal p : Ideal R factors in S as ∏ i, P i ^ e i, then S ⧸ I factors R ⧸ I-linearly as Π i, R ⧸ (P i ^ e i).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Ideal.sum_ramification_inertia {R : Type u} [] {S : Type v} [] (p : ) [] [Algebra R S] (K : Type u_1) (L : Type u_2) [] [] [] [Algebra R K] [] [Algebra S L] [] [Algebra K L] [Algebra R L] [] [] [] [] [p.IsMaximal] (hp0 : p ) :
(().toFinset.sum fun (P : ) => Ideal.ramificationIdx () p P * Ideal.inertiaDeg () p P) =

The fundamental identity of ramification index e and inertia degree f: for P ranging over the primes lying over p, ∑ P, e P * f P = [Frac(S) : Frac(R)]; here S is a finite R-module (and thus Frac(S) : Frac(R) is a finite extension) and p is maximal.