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, 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).

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.