Documentation

Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Decomposition and Inertia fields #

In this file, we develop Hilbert Theory on the splitting of prime ideals in a Galois extension.

Let L/K be a Galois extension of fields. Let A and B be subrings of K L respectively with K fraction field of A, L fraction field of B and B the integral closure of A in L.

For P a prime ideal of B lying over the prime ideal p of A, the decomposition field D of P in L/K is the subfield of elements of L fixed by the stabilizer of P in Gal(L/K), and the inertia field E of P in L/K is the subfield of elements of L fixed by the inertia group of P in Gal(L/K).

Let e and f the ramification index and inertia degree of P over p and let g be the number of prime ideals above p in L. Denote by 𝓟D, resp. 𝓟E, the prime ideal of D, resp. E, below P. Then we have the following properties

degree            ramif. index   inertia deg.
        L      P
  e     |      |      e               1
        E      𝓟E
  f     |      |      1               f
        D      𝓟D
  g     |      |      1               1
        K      p
source
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).

Instances
    source
    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
    source
    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
    source
    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).

    Instances
      source
      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
      source
      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
      source
      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))
      source
      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))
      source
      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.

      source
      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.

      source
      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
      Instances For
        source
        @[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
        source
        @[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
        source
        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
        Instances For
          source
          @[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
          source
          @[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
          source
          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] [Ring.HasFiniteQuotients A] [P.IsMaximal] (D : Type u_5) [Field D] [Algebra D L] [IsDecompositionField K L P D] (hp : p ≠ ⊥) :
          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.

          source
          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] [Ring.HasFiniteQuotients A] [P.IsMaximal] (D : Type u_5) [Field D] [Algebra D L] [IsDecompositionField K L P D] [IsGalois K L] [Algebra K D] [IsScalarTower K D L] (hp : p ≠ ⊥) :
          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.

          source
          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] [Ring.HasFiniteQuotients A] [P.IsMaximal] (E : Type u_6) [Field E] [Algebra E L] [IsInertiaField K L P E] (hp : p ≠ ⊥) :
          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.

          source
          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] [Ring.HasFiniteQuotients A] [P.IsMaximal] (E : Type u_6) [Field E] [Algebra E L] [IsInertiaField K L P E] [IsGalois K L] [Algebra K E] [IsScalarTower K E L] (hp : p ≠ ⊥) :
          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.

          source
          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] [Ring.HasFiniteQuotients A] [P.IsMaximal] (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] (hp : p ≠ ⊥) :
          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.

          source
          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.

          source
          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] [𝓟D.LiesOver p] [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal] [p.IsMaximal] (hp : p ≠ ⊥) :
          𝓟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.

          source
          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] [𝓟D.LiesOver p] [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal] [p.IsMaximal] (hp : p ≠ ⊥) :
          𝓟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.

          source
          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] [𝓟D.LiesOver p] [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal] [p.IsMaximal] (hp : p ≠ ⊥) :
          p.ramificationIdx 𝓟D = 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.

          source
          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] [𝓟D.LiesOver p] [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal] [p.IsMaximal] (hp : p ≠ ⊥) :
          p.inertiaDeg 𝓟D = 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.