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 inertia degree Ideal.inertiaDeg p P is the degree of the field extension (S / P) : (R / 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, f stands for the inertia degree of P over p, leaving p and P implicit.

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

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

• p.inertiaDeg P = if hPp : Ideal.comap (algebraMap R S) P = p then Module.finrank (R ⧸ p) (S ⧸ P) else 0

@[simp]

theorem Ideal.inertiaDeg_of_subsingleton {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [hp : p.IsMaximal] [hQ : Subsingleton (S ⧸ P)] : p.inertiaDeg P = 0

@[simp]

theorem Ideal.inertiaDeg_algebraMap {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [P.LiesOver p] : p.inertiaDeg P = Module.finrank (R ⧸ p) (S ⧸ P)

theorem Ideal.inertiaDeg_pos {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [p.IsMaximal] [Module.Finite R S] [P.LiesOver p] : 0 < p.inertiaDeg P

theorem Ideal.inertiaDeg_ne_zero {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (p : Ideal R) (P : Ideal S) [p.IsMaximal] [Module.Finite R S] [P.LiesOver p] : p.inertiaDeg P ≠ 0

theorem Ideal.inertiaDeg_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.inertiaDeg (comap e P) = p.inertiaDeg P

theorem Ideal.inertiaDeg_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₁] (P : Ideal S) {E : Type u_2} [EquivLike E S S₁] [AlgEquivClass E R S S₁] (e : E) : p.inertiaDeg (map e P) = p.inertiaDeg P

theorem Ideal.inertiaDeg_bot {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (P : Ideal S) [Nontrivial R] [IsDomain S] [Algebra.IsIntegral R S] [hP : P.LiesOver ⊥] : ⊥.inertiaDeg P = Module.finrank R S

theorem Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] [IsDedekindDomain S] [Module.Free ℤ S] [IsDedekindDomain R] [Module.Free ℤ R] [Algebra S R] [Module.Finite S R] (P : Ideal R) (p : Ideal S) [P.LiesOver p] (hp : p.IsPrime) (hp_ne_bot : p ≠ ⊥) : absNorm P = absNorm p ^ p.inertiaDeg P

theorem Ideal.absNorm_eq_pow_inertiaDeg {R : Type u} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {p : ℤ} (P : Ideal R) [P.LiesOver (span {p})] (hp : Prime p) : absNorm P = p.natAbs ^ (span {p}).inertiaDeg P

The absolute norm of an ideal P above a rational prime p is |p| ^ ((span {p}).inertiaDeg P). See absNorm_eq_pow_inertiaDeg' for a version with p of type ℕ.

theorem Ideal.absNorm_eq_pow_inertiaDeg' {R : Type u} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {p : ℕ} (P : Ideal R) [P.LiesOver (span {↑p})] (hp : Nat.Prime p) : absNorm P = p ^ (span {↑p}).inertiaDeg P

The absolute norm of an ideal P above a rational (positive) prime p is p ^ ((span {p}).inertiaDeg P). See absNorm_eq_pow_inertiaDeg for a version with p of type ℤ.

theorem Ideal.inertiaDeg_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] (p : Ideal R) (P : Ideal S) (I : Ideal T) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p] [I.LiesOver P] : p.inertiaDeg I = p.inertiaDeg P * P.inertiaDeg I

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