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 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 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) (D : Type u_5) [Field D] [Algebra D L] [MulSemiringAction Gal(L/K) B] [h : IsGaloisGroup (↥(Ideal.inertia Gal(L/K) P)) D L] :
      IsInertiaField K L P D
      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] [Algebra B L] [IsFractionRing B L] [SMulDistribClass Gal(L/K) B L] (G : Type u_7) [Group G] [Finite G] [MulSemiringAction G L] [IsGaloisGroup G K L] [MulSemiringAction G B] [SMulDistribClass G B L] [h : IsGaloisGroup (↥(MulAction.stabilizer G P)) D L] :
      IsDecompositionField K L P D
      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) (D : Type u_5) [Field D] [Algebra D L] [MulSemiringAction Gal(L/K) B] [Algebra B L] [IsFractionRing B L] [SMulDistribClass Gal(L/K) B L] (G : Type u_7) [Group G] [Finite G] [MulSemiringAction G L] [IsGaloisGroup G K L] [MulSemiringAction G B] [SMulDistribClass G B L] [h : IsGaloisGroup (↥(Ideal.inertia G P)) D L] :
      IsInertiaField K L P D