Decomposition and inertia rings

We develop Hilbert's theory of the splitting of a prime ideal in a Galois extension, working throughout at the level of rings.

Let A ⊆ B be commutative rings with B Galois over A with group G, let p be a prime of A and P a prime of B lying over p. The decomposition ring R and the inertia ring R' of P are the intermediate rings fixed by the decomposition and inertia subgroups of P; since the inertia group is contained in the decomposition group, they fit into a tower A ⊆ R ⊆ R' ⊆ B.

Ring predicates

For an intermediate ring R of B, we introduce two characteristic predicates:

• Ideal.IsDecompositionRing G P R: B is Galois over R with Galois group the decomposition group of P, that is the stabilizer of P in G;
• Ideal.IsInertiaRing G P R: B is Galois over R with Galois group the inertia group of P, that is the subgroup of G acting trivially modulo P.

Relation to the classical field setting

In the classical setting L/K is a Galois extension of fields with G = Gal(L/K), and A, B are subrings of K, L with K the fraction field of A, L that of B, and B the integral closure of A in L. The decomposition (resp. inertia) field is the subfield of L fixed by the decomposition (resp. inertia) group of P, and the associated ring is the integral closure of A in this field. Decomposition and inertia rings arising this way are provided by Ideal.IsDecompositionRing.of_isFractionRing and Ideal.IsInertiaRing.of_isFractionRing.

The field-level predicates IsDecompositionField and IsInertiaField defined below will be deprecated in favor of the ring-level predicates Ideal.IsDecompositionRing and Ideal.IsInertiaRing.

class Ideal.IsDecompositionRing {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (P : Ideal B) (R : Type u_3) [CommRing R] [Algebra R B] extends IsGaloisGroup (↥(MulAction.stabilizer G P)) R B : Prop

P.IsDecompositionRing G R states that the intermediate ring R of B is a decomposition ring of the prime P: the ring B is Galois over R with Galois group the decomposition group of P, that is the stabilizer of P under the action of G.

This is the ring-level characteristic predicate; the classical decomposition field is recovered by passing to fraction fields.

• faithful : FaithfulSMul (↥(MulAction.stabilizer G P)) B
• commutes : SMulCommClass (↥(MulAction.stabilizer G P)) R B
• isInvariant : Algebra.IsInvariant R B ↥(MulAction.stabilizer G P)

theorem Ideal.isDecompositionRing_iff {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (P : Ideal B) (R : Type u_3) [CommRing R] [Algebra R B] : IsDecompositionRing G P R ↔ IsGaloisGroup (↥(MulAction.stabilizer G P)) R B

instance Ideal.instIsDecompositionRingOfIsGaloisGroupSubtypeMemSubgroupStabilizer {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (P : Ideal B) (R : Type u_3) [CommRing R] [Algebra R B] [IsGaloisGroup (↥(MulAction.stabilizer G P)) R B] : IsDecompositionRing G P R

class Ideal.IsInertiaRing {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (P : Ideal B) (R : Type u_3) [CommRing R] [Algebra R B] extends IsGaloisGroup (↥(Ideal.inertia G P)) R B : Prop

P.IsInertiaRing G R states that the intermediate ring R of B is an inertia ring of the prime P: the ring B is Galois over R with Galois group the inertia group of P, that is the elements of G acting trivially modulo P (a subgroup of the decomposition group).

This is the ring-level characteristic predicate; the classical inertia field is recovered by passing to fraction fields.

• faithful : FaithfulSMul (↥(Ideal.inertia G P)) B
• commutes : SMulCommClass (↥(Ideal.inertia G P)) R B
• isInvariant : Algebra.IsInvariant R B ↥(Ideal.inertia G P)

theorem Ideal.isInertiaRing_iff {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (P : Ideal B) (R : Type u_3) [CommRing R] [Algebra R B] : IsInertiaRing G P R ↔ IsGaloisGroup (↥(inertia G P)) R B

instance Ideal.instIsInertiaRingOfIsGaloisGroupSubtypeMemSubgroupInertia {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (P : Ideal B) (R : Type u_3) [CommRing R] [Algebra R B] [IsGaloisGroup (↥(inertia G P)) R B] : IsInertiaRing G P R

theorem Ideal.IsDecompositionRing.of_isFractionRing {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (P : Ideal B) (R : Type u_3) [CommRing R] [Algebra R B] (L : Type u_4) [Field L] [Algebra B L] [IsFractionRing B L] [MulSemiringAction G L] [SMulDistribClass G B L] (D : Type u_5) [Field D] [Algebra R D] [Algebra R L] [Algebra D L] [IsScalarTower R D L] [IsScalarTower R B L] [IsFractionRing R D] [IsIntegrallyClosed R] [Algebra.IsIntegral R B] [IsGaloisGroup (↥(MulAction.stabilizer G P)) D L] : IsDecompositionRing G P R

If L is Galois over the field D with the decomposition group of P as a Galois group (so D is the decomposition field of P), and R is an integrally closed subring of D with fraction field D such that B is integral over R, then R is a decomposition ring of P.

theorem Ideal.IsInertiaRing.of_isFractionRing {B : Type u_1} [CommRing B] (G : Type u_2) [Group G] [MulSemiringAction G B] (P : Ideal B) (R : Type u_3) [CommRing R] [Algebra R B] (L : Type u_4) [Field L] [Algebra B L] [IsFractionRing B L] [MulSemiringAction G L] [SMulDistribClass G B L] (E : Type u_5) [Field E] [Algebra R E] [Algebra R L] [Algebra E L] [IsScalarTower R E L] [IsScalarTower R B L] [IsFractionRing R E] [IsIntegrallyClosed R] [Algebra.IsIntegral R B] [IsGaloisGroup (↥(inertia G P)) E L] : IsInertiaRing G P R

If L is Galois over the field E with the inertia group of P as a Galois group (so E is the inertia field of P), and R is an integrally closed subring of E with fraction field E such that B is integral over R, then R is an inertia ring of P.

class IsDecompositionField (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (D : Type u_5) [Field D] [Algebra D L] [MulSemiringAction Gal(L/K) B] extends IsGaloisGroup (↥(MulAction.stabilizer Gal(L/K) P)) D L : Prop

Let L/K be a Galois extension of fields and let P be a prime ideal of B. The predicate that says that D is the decomposition field of P in L/K, that is the subfield fixed by the decomposition subgroup of P, that is the stabilizer of P in Gal(L/K).

• faithful : FaithfulSMul (↥(MulAction.stabilizer Gal(L/K) P)) L
• commutes : SMulCommClass (↥(MulAction.stabilizer Gal(L/K) P)) D L
• isInvariant : Algebra.IsInvariant D L ↥(MulAction.stabilizer Gal(L/K) P)

theorem isDecompositionField_iff (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (D : Type u_5) [Field D] [Algebra D L] [MulSemiringAction Gal(L/K) B] : IsDecompositionField K L P D ↔ IsGaloisGroup (↥(MulAction.stabilizer Gal(L/K) P)) D L

instance instIsDecompositionFieldOfIsGaloisGroupSubtypeAlgEquivMemSubgroupStabilizerIdeal (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (D : Type u_5) [Field D] [Algebra D L] [MulSemiringAction Gal(L/K) B] [h : IsGaloisGroup (↥(MulAction.stabilizer Gal(L/K) P)) D L] : IsDecompositionField K L P D

class IsInertiaField (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (E : Type u_6) [Field E] [Algebra E L] [MulSemiringAction Gal(L/K) B] extends IsGaloisGroup (↥(Ideal.inertia Gal(L/K) P)) E L : Prop

Let L/K be a Galois extension of fields and let P be a prime ideal of B. The predicate that says that E is the inertia field of P in L/K, that is the subfield fixed by the inertia subgroup of P in Gal(L/K).

• faithful : FaithfulSMul (↥(Ideal.inertia Gal(L/K) P)) L
• commutes : SMulCommClass (↥(Ideal.inertia Gal(L/K) P)) E L
• isInvariant : Algebra.IsInvariant E L ↥(Ideal.inertia Gal(L/K) P)

theorem isInertiaField_iff (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (E : Type u_6) [Field E] [Algebra E L] [MulSemiringAction Gal(L/K) B] : IsInertiaField K L P E ↔ IsGaloisGroup (↥(Ideal.inertia Gal(L/K) P)) E L

instance instIsInertiaFieldOfIsGaloisGroupSubtypeAlgEquivMemSubgroupInertia (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (E : Type u_6) [Field E] [Algebra E L] [MulSemiringAction Gal(L/K) B] [h : IsGaloisGroup (↥(Ideal.inertia Gal(L/K) P)) E L] : IsInertiaField K L P E

instance instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) [MulSemiringAction Gal(L/K) B] [IsGalois K L] : IsDecompositionField K L P ↥(FixedPoints.intermediateField ↥(MulAction.stabilizer Gal(L/K) P))

instance instIsInertiaFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupInertiaOfIsGalois (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) [MulSemiringAction Gal(L/K) B] [IsGalois K L] : IsInertiaField K L P ↥(FixedPoints.intermediateField ↥(Ideal.inertia Gal(L/K) P))

theorem IsDecompositionField.of_isGaloisGroup (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (D : Type u_5) [Field D] [Algebra D L] [MulSemiringAction Gal(L/K) B] (G : Type u_7) [Group G] [Finite G] [MulSemiringAction G L] [IsGaloisGroup G K L] [MulSemiringAction G B] [Algebra B L] [IsFractionRing B L] [SMulDistribClass Gal(L/K) B L] [SMulDistribClass G B L] [h : IsGaloisGroup (↥(MulAction.stabilizer G P)) D L] : IsDecompositionField K L P D

If G is a Galois group for L/K and the stabilizer of P in G is a Galois group for L/D, then D is a decomposition field for P.

theorem IsInertiaField.of_isGaloisGroup (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (E : Type u_6) [Field E] [Algebra E L] [MulSemiringAction Gal(L/K) B] (G : Type u_7) [Group G] [Finite G] [MulSemiringAction G L] [IsGaloisGroup G K L] [MulSemiringAction G B] [Algebra B L] [IsFractionRing B L] [SMulDistribClass Gal(L/K) B L] [SMulDistribClass G B L] [h : IsGaloisGroup (↥(Ideal.inertia G P)) E L] : IsInertiaField K L P E

If G is a Galois group for L/K and the inertia group of P in G is a Galois group for L/E, then E is an inertia field for P.

noncomputable def IsDecompositionField.ringEquiv (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (D : Type u_5) [Field D] [Algebra D L] [MulSemiringAction Gal(L/K) B] (D' : Type u_8) [Field D'] [Algebra D' L] [IsDecompositionField K L P D] [IsDecompositionField K L P D'] : D ≃+* D'

Two decomposition fields are isomorphic.

Equations

• IsDecompositionField.ringEquiv K L P D D' = IsGaloisGroup.ringEquiv (↥(MulAction.stabilizer Gal(L/K) P)) D D' L

@[simp]

theorem IsDecompositionField.algebraMap_ringEquiv_apply (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (D : Type u_5) [Field D] [Algebra D L] [MulSemiringAction Gal(L/K) B] (D' : Type u_8) [Field D'] [Algebra D' L] [IsDecompositionField K L P D] [IsDecompositionField K L P D'] (x : D) : (algebraMap D' L) ((ringEquiv K L P D D') x) = (algebraMap D L) x

@[simp]

theorem IsDecompositionField.algebraMap_ringEquiv_symm_apply (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (D : Type u_5) [Field D] [Algebra D L] [MulSemiringAction Gal(L/K) B] (D' : Type u_8) [Field D'] [Algebra D' L] [IsDecompositionField K L P D] [IsDecompositionField K L P D'] (x : D') : (algebraMap D L) ((ringEquiv K L P D D').symm x) = (algebraMap D' L) x

noncomputable def IsInertiaField.ringEquiv (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (E : Type u_6) [Field E] [Algebra E L] [MulSemiringAction Gal(L/K) B] (E' : Type u_9) [Field E'] [Algebra E' L] [IsInertiaField K L P E] [IsInertiaField K L P E'] : E ≃+* E'

Two inertia fields are isomorphic.

Equations

• IsInertiaField.ringEquiv K L P E E' = IsGaloisGroup.ringEquiv (↥(Ideal.inertia Gal(L/K) P)) E E' L

@[simp]

theorem IsInertiaField.algebraMap_ringEquiv_apply (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (E : Type u_6) [Field E] [Algebra E L] [MulSemiringAction Gal(L/K) B] (E' : Type u_9) [Field E'] [Algebra E' L] [IsInertiaField K L P E] [IsInertiaField K L P E'] (x : E) : (algebraMap E' L) ((ringEquiv K L P E E') x) = (algebraMap E L) x

@[simp]

theorem IsInertiaField.algebraMap_ringEquiv_symm_apply (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) (E : Type u_6) [Field E] [Algebra E L] [MulSemiringAction Gal(L/K) B] (E' : Type u_9) [Field E'] [Algebra E' L] [IsInertiaField K L P E] [IsInertiaField K L P E'] (x : E') : (algebraMap E L) ((ringEquiv K L P E E').symm x) = (algebraMap E' L) x

theorem IsDecompositionField.rank_left (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [FiniteDimensional K L] [MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [p.IsPrime] [Algebra.HasSeparableResidueFieldsAt A B p] [P.IsPrime] (D : Type u_5) [Field D] [Algebra D L] [IsDecompositionField K L P D] : Module.finrank D L = p.ramificationIdxIn B * p.inertiaDegIn B

The degree [L : D] of L over the decomposition field D equals the product of the ramification index and the inertia degree of p in B.

theorem IsDecompositionField.rank_right (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [FiniteDimensional K L] [MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [p.IsPrime] [Algebra.HasSeparableResidueFieldsAt A B p] [P.IsPrime] (D : Type u_5) [Field D] [Algebra D L] [IsDecompositionField K L P D] [IsGalois K L] [Algebra K D] [IsScalarTower K D L] : Module.finrank K D = (p.primesOver B).ncard

The degree [D : K] of the decomposition field D over K equals the number of prime ideals of B lying over p.

theorem IsInertiaField.rank_left (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [FiniteDimensional K L] [MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [p.IsPrime] [Algebra.HasSeparableResidueFieldsAt A B p] [P.IsPrime] (E : Type u_6) [Field E] [Algebra E L] [IsInertiaField K L P E] : Module.finrank E L = p.ramificationIdxIn B

The degree [L : E] of L over the inertia field E equals the ramification index of p in B.

theorem IsInertiaField.rank_right (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [FiniteDimensional K L] [MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [p.IsPrime] [Algebra.HasSeparableResidueFieldsAt A B p] [P.IsPrime] (E : Type u_6) [Field E] [Algebra E L] [IsInertiaField K L P E] [IsGalois K L] [Algebra K E] [IsScalarTower K E L] : Module.finrank K E = (p.primesOver B).ncard * p.inertiaDegIn B

The degree [E : K] of the inertia field E over K equals the product of the number of prime ideals of B lying over p and the inertia degree of p in B.

theorem IsInertiaField.rank_decompositionField (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [FiniteDimensional K L] [MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [p.IsPrime] [Algebra.HasSeparableResidueFieldsAt A B p] [P.IsPrime] (D : Type u_5) [Field D] [Algebra D L] [IsDecompositionField K L P D] (E : Type u_6) [Field E] [Algebra E L] [IsInertiaField K L P E] [IsGalois K L] [Algebra K D] [Algebra K E] [Algebra D E] [IsScalarTower K D E] [IsScalarTower K E L] [IsScalarTower K D L] : Module.finrank D E = p.inertiaDegIn B

The degree [E : D] of the inertia field E over the decomposition field D equals the inertia degree of p in B.

theorem IsDecompositionField.primesOver_eq_singleton (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing B] (P : Ideal B) [Algebra B L] [IsFractionRing B L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] (D : Type u_5) (𝓞D : Type u_6) [Field D] [Algebra D L] [IsDecompositionField K L P D] [CommRing 𝓞D] [Algebra 𝓞D D] [IsFractionRing 𝓞D D] [Algebra 𝓞D B] [Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D] [hP : P.IsPrime] [Finite ↥(MulAction.stabilizer Gal(L/K) P)] [IsIntegrallyClosed 𝓞D] [Algebra.IsIntegral 𝓞D B] : 𝓟D.primesOver B = {P}

Let D be the decomposition field of P in L/K. Let 𝓟D be a prime ideal of D below P, then P is the only prime of L above 𝓟D.

theorem IsDecompositionField.ramificationIdxIn_eq (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] (D : Type u_5) (𝓞D : Type u_6) [Field D] [Algebra D L] [IsDecompositionField K L P D] [CommRing 𝓞D] [Algebra 𝓞D D] [IsFractionRing 𝓞D D] [Algebra 𝓞D B] [Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D] [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B] [IsDedekindDomain 𝓞D] [FiniteDimensional K L] [p.IsPrime] [Algebra.HasSeparableResidueFieldsAt A B p] [𝓟D.IsMaximal] [P.IsMaximal] : 𝓟D.ramificationIdxIn B = p.ramificationIdxIn B

Let D be the decomposition field of P in L/K. Let 𝓟D be a prime ideal of D below P, then the ramification index of 𝓟D in L is equal to the ramification index of p in L.

theorem IsDecompositionField.inertiaDegIn_eq (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] (D : Type u_5) (𝓞D : Type u_6) [Field D] [Algebra D L] [IsDecompositionField K L P D] [CommRing 𝓞D] [Algebra 𝓞D D] [IsFractionRing 𝓞D D] [Algebra 𝓞D B] [Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D] [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B] [IsDedekindDomain 𝓞D] [FiniteDimensional K L] [p.IsPrime] [Algebra.HasSeparableResidueFieldsAt A B p] [𝓟D.IsMaximal] [P.IsMaximal] : 𝓟D.inertiaDegIn B = p.inertiaDegIn B

Let D be the decomposition field of P in L/K. Let 𝓟D be a prime ideal of D below P, then the inertia degree of 𝓟D in L is equal to the inertia degree of p in L.

theorem IsDecompositionField.ramificationIdx_eq (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] (D : Type u_5) (𝓞D : Type u_6) [Field D] [Algebra D L] [IsDecompositionField K L P D] [CommRing 𝓞D] [Algebra 𝓞D D] [IsFractionRing 𝓞D D] [Algebra 𝓞D B] [Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D] [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B] [IsDedekindDomain 𝓞D] [FiniteDimensional K L] [p.IsPrime] [Algebra.HasSeparableResidueFieldsAt A B p] [𝓟D.IsMaximal] [P.IsMaximal] : 𝓟D.ramificationIdx A = 1

Let D be the decomposition field of P in L/K. Let 𝓟D be a prime ideal of D below P, then 𝓟D is unramified over K.

theorem IsDecompositionField.inertiaDeg_eq (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [Field K] [Field L] [Algebra K L] [CommRing A] [CommRing B] [Algebra A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [Algebra A K] [IsFractionRing A K] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsFractionRing B L] [MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] (D : Type u_5) (𝓞D : Type u_6) [Field D] [Algebra D L] [IsDecompositionField K L P D] [CommRing 𝓞D] [Algebra 𝓞D D] [IsFractionRing 𝓞D D] [Algebra 𝓞D B] [Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D] [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B] [IsDedekindDomain 𝓞D] [FiniteDimensional K L] [p.IsPrime] [Algebra.HasSeparableResidueFieldsAt A B p] [𝓟D.IsMaximal] [P.IsMaximal] : 𝓟D.inertiaDeg A = 1

Let D be the decomposition field of P in L/K. Let 𝓟D be a prime ideal of D below P, then the inertia degree of 𝓟D over K is equal to 1.