Ramification theory in Galois extensions of Dedekind domains

In this file, we discuss the ramification theory in Galois extensions of Dedekind domains, which is also called Hilbert's Ramification Theory.

Assume B / A is a finite extension of Dedekind domains, K is the fraction ring of A, L is the fraction ring of K, L / K is a Galois extension.

Main definitions

• Ideal.ramificationIdxIn: It can be seen from the theorem Ideal.ramificationIdx_eq_of_IsGalois that all Ideal.ramificationIdx over a fixed maximal ideal p of A are the same, which we define as Ideal.ramificationIdxIn.

• Ideal.inertiaDegIn: It can be seen from the theorem Ideal.inertiaDeg_eq_of_IsGalois that all Ideal.inertiaDeg over a fixed maximal ideal p of A are the same, which we define as Ideal.inertiaDegIn.

Main results

• ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn: Let p be a maximal ideal of A, r be the number of prime ideals lying over p, e be the ramification index of p in B, and f be the inertia degree of p in B. Then r * (e * f) = [L : K]. It is the form of the Ideal.sum_ramification_inertia in the case of Galois extension.

References

• [J Neukirch, Algebraic Number Theory][Neukirch1992]

noncomputable def Ideal.ramificationIdxIn {A : Type u_1} [CommRing A] (p : Ideal A) (B : Type u_2) [CommRing B] [Algebra A B] : ℕ

If L / K is a Galois extension, it can be seen from the theorem Ideal.ramificationIdx_eq_of_IsGalois that all Ideal.ramificationIdx over a fixed maximal ideal p of A are the same, which we define as Ideal.ramificationIdxIn.

Equations

• p.ramificationIdxIn B = if h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p then Ideal.ramificationIdx (algebraMap A B) p h.choose else 0

noncomputable def Ideal.inertiaDegIn {A : Type u_1} [CommRing A] (p : Ideal A) (B : Type u_2) [CommRing B] [Algebra A B] : ℕ

If L / K is a Galois extension, it can be seen from the theorem Ideal.inertiaDeg_eq_of_IsGalois that all Ideal.inertiaDeg over a fixed maximal ideal p of A are the same, which we define as Ideal.inertiaDegIn.

Equations

• p.inertiaDegIn B = if h : ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p then p.inertiaDeg h.choose else 0

instance Ideal.instMulActionAlgEquivElemPrimesOver {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} : MulAction (B ≃ₐ[A] B) ↑(p.primesOver B)

Equations

• Ideal.instMulActionAlgEquivElemPrimesOver = MulAction.mk ⋯ ⋯

@[simp]

theorem Ideal.coe_smul_primesOver {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (σ : B ≃ₐ[A] B) (P : ↑(p.primesOver B)) : ↑(σ • P) = map σ ↑P

@[simp]

theorem Ideal.coe_smul_primesOver_mk {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (σ : B ≃ₐ[A] B) (P : Ideal B) [P.IsPrime] [P.LiesOver p] : ↑(σ • primesOver.mk p P) = map σ P

instance Ideal.instMulActionAlgEquivElemPrimesOver_1 {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] : MulAction (L ≃ₐ[K] L) ↑(p.primesOver B)

Equations

• Ideal.instMulActionAlgEquivElemPrimesOver_1 K L = MulAction.mk ⋯ ⋯

theorem Ideal.coe_smul_primesOver_eq_map_galRestrict {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] (σ : L ≃ₐ[K] L) (P : ↑(p.primesOver B)) : ↑(σ • P) = map ((galRestrict A K L B) σ) ↑P

theorem Ideal.coe_smul_primesOver_mk_eq_map_galRestrict {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] {p : Ideal A} (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] (σ : L ≃ₐ[K] L) (P : Ideal B) [P.IsPrime] [P.LiesOver p] : ↑(σ • primesOver.mk p P) = map ((galRestrict A K L B) σ) P

theorem Ideal.exists_map_eq_of_isGalois {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] (p : Ideal A) (P Q : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] [hQp : Q.IsPrime] [Q.LiesOver p] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [FiniteDimensional K L] [IsGalois K L] : ∃ (σ : B ≃ₐ[A] B), map σ P = Q

If p is a maximal ideal of A, P and Q are prime ideals lying over p, then there exists σ ∈ Aut (B / A) such that σ P = Q. In other words, the Galois group Gal(L / K) acts transitively on the set of all prime ideals lying over p.

theorem Ideal.isPretransitive_of_isGalois {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] (p : Ideal A) (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [FiniteDimensional K L] [IsGalois K L] : MulAction.IsPretransitive (B ≃ₐ[A] B) ↑(p.primesOver B)

instance Ideal.instIsPretransitiveAlgEquivElemPrimesOverOfIsGalois {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] (p : Ideal A) (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [FiniteDimensional K L] [IsGalois K L] : MulAction.IsPretransitive (L ≃ₐ[K] L) ↑(p.primesOver B)

theorem Ideal.ramificationIdx_eq_of_isGalois {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] (p : Ideal A) (P Q : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] [hQp : Q.IsPrime] [Q.LiesOver p] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [FiniteDimensional K L] [IsGalois K L] : ramificationIdx (algebraMap A B) p P = ramificationIdx (algebraMap A B) p Q

All the ramificationIdx over a fixed maximal ideal are the same.

theorem Ideal.inertiaDeg_eq_of_isGalois {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] (p : Ideal A) (P Q : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] [hQp : Q.IsPrime] [Q.LiesOver p] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [FiniteDimensional K L] [p.IsMaximal] [IsGalois K L] : p.inertiaDeg P = p.inertiaDeg Q

All the inertiaDeg over a fixed maximal ideal are the same.

theorem Ideal.ramificationIdxIn_eq_ramificationIdx {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] (p : Ideal A) (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [FiniteDimensional K L] [IsGalois K L] : p.ramificationIdxIn B = ramificationIdx (algebraMap A B) p P

The ramificationIdxIn is equal to any ramification index over the same ideal.

theorem Ideal.inertiaDegIn_eq_inertiaDeg {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [IsDomain B] [IsIntegrallyClosed B] [Algebra A B] [Module.Finite A B] (p : Ideal A) (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [FiniteDimensional K L] [p.IsMaximal] [IsGalois K L] : p.inertiaDegIn B = p.inertiaDeg P

The inertiaDegIn is equal to any ramification index over the same ideal.

theorem Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn {A : Type u_1} [CommRing A] [IsDedekindDomain A] {p : Ideal A} (hpb : p ≠ ⊥) [p.IsMaximal] (B : Type u_2) [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [FiniteDimensional K L] [IsGalois K L] : (p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B) = Module.finrank K L

The form of the fundamental identity in the case of Galois extension.