NYLL
Module

FixedFieldTower.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.FixedFieldTower
17 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: decomposition and inertia tower

This file contains the group-theoretic fixed-field part of the tower Z_P ⊆ T_P ⊆ L in prime-decomposition theory.

Imports1
Imported by2

Declarations

abbrev

inertiaFieldOverDecompositionField

L33 ↗
HilbertRamification.Dedekind.inertiaFieldOverDecompositionField
Documentation

prime-decomposition theory: the inertia field, viewed as an intermediate field over the decomposition field.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
abbrev inertiaFieldOverDecompositionField
    (P : Ideal B) [MulSemiringAction G B] :
    IntermediateField (decompositionField (K := K) (L := L) G P) L
theorem

mem_inertiaFieldOverDecompositionField_iff

L44 ↗
HilbertRamification.Dedekind.mem_inertiaFieldOverDecompositionField_iff
Documentation

Elementwise membership in the inertia field viewed over the decomposition field.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
Lean source · statement
theorem mem_inertiaFieldOverDecompositionField_iff
    {P : Ideal B} [MulSemiringAction G B] {x : L} :
    x ∈ inertiaFieldOverDecompositionField (K := K) (L := L) G P ↔
      ∀ σ ∈ inertiaGroup P G, σ • x = x
theorem

inertiaFieldOverDecompositionField_restrictScalars

L56 ↗
HilbertRamification.Dedekind.inertiaFieldOverDecompositionField_restrictScalars
Documentation

Restricting the inertia field over the decomposition field back to K recovers the inertia field over K.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
Lean source · statement
theorem inertiaFieldOverDecompositionField_restrictScalars
    (P : Ideal B) [MulSemiringAction G B] :
    (inertiaFieldOverDecompositionField (K := K) (L := L) G P).restrictScalars K =
      inertiaField (K := K) (L := L) G P
def

dedekindTower_decompositionGroupEquivGalDecompositionField

L64 ↗
HilbertRamification.Dedekind.dedekindTower_decompositionGroupEquivGalDecompositionField
Documentation

The prime-decomposition tower identity: identify the decomposition group with Gal(L/Z_P).

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
Lean source · statement
def dedekindTower_decompositionGroupEquivGalDecompositionField
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    decompositionGroup P G ≃*
      (L ≃ₐ[decompositionField (K := K) (L := L) G P] L)
theorem

dedekindTower_decompositionGroupEquivGalDecompositionField_apply

L77 ↗
HilbertRamification.Dedekind.dedekindTower_decompositionGroupEquivGalDecompositionField_apply
Documentation

The equivalence G_P ≃ Gal(L/Z_P) acts by the original group action on elements of L.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
Lean source · statement
theorem dedekindTower_decompositionGroupEquivGalDecompositionField_apply
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L]
    (σ : decompositionGroup P G) (x : L) :
    dedekindTower_decompositionGroupEquivGalDecompositionField
        (K := K) (L := L) G P σ x =
      (σ : G) • x
theorem

dedekindTower_decompositionField_finiteDimensional

L88 ↗
HilbertRamification.Dedekind.dedekindTower_decompositionField_finiteDimensional
Documentation

Source fact for the tower Z_P ⊆ L: L is finite-dimensional over the decomposition field.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
Lean source · statement
theorem dedekindTower_decompositionField_finiteDimensional
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    FiniteDimensional (decompositionField (K := K) (L := L) G P) L
theorem

dedekindTower_decompositionField_isGalois

L99 ↗
HilbertRamification.Dedekind.dedekindTower_decompositionField_isGalois
Documentation

Source fact for the tower Z_P ⊆ L: L/Z_P is Galois.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
Lean source · statement
theorem dedekindTower_decompositionField_isGalois
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    IsGalois (decompositionField (K := K) (L := L) G P) L
abbrev

inertiaGroupOverDecompositionField

L111 ↗
HilbertRamification.Dedekind.inertiaGroupOverDecompositionField
Documentation

prime-decomposition theory: the inertia subgroup transported to Gal(L/Z_P).

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
Lean source · statement
abbrev inertiaGroupOverDecompositionField
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    Subgroup (L ≃ₐ[decompositionField (K := K) (L := L) G P] L)
theorem

mem_inertiaGroupOverDecompositionField_iff

L124 ↗
HilbertRamification.Dedekind.mem_inertiaGroupOverDecompositionField_iff
Documentation

Membership in the transported inertia subgroup over the decomposition field.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
Lean source · statement
theorem mem_inertiaGroupOverDecompositionField_iff
    {P : Ideal B} [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L]
    {σ : L ≃ₐ[decompositionField (K := K) (L := L) G P] L} :
    σ ∈ inertiaGroupOverDecompositionField (K := K) (L := L) G P ↔
      ∃ τ : (inertiaGroup P G).subgroupOf (decompositionGroup P G),
        dedekindTower_decompositionGroupEquivGalDecompositionField
          (K := K) (L := L) G P (τ : decompositionGroup P G) = σ
instance

inertiaGroupOverDecompositionField_normal

L141 ↗
HilbertRamification.Dedekind.inertiaGroupOverDecompositionField_normal
Documentation

The transported inertia subgroup is normal in Gal(L/Z_P).

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
instance inertiaGroupOverDecompositionField_normal
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    (inertiaGroupOverDecompositionField (K := K) (L := L) G P).Normal
theorem

dedekindRamification_inertiaFieldOverDecompositionField_fixedField_eq

L155 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldOverDecompositionField_fixedField_eq
Documentation

A prime-decomposition consequence: the fixed field of the transported inertia subgroup over Z_P is T_P.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
theorem dedekindRamification_inertiaFieldOverDecompositionField_fixedField_eq
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    IntermediateField.fixedField
        (inertiaGroupOverDecompositionField (K := K) (L := L) G P) =
      inertiaFieldOverDecompositionField (K := K) (L := L) G P
theorem

dedekindRamification_inertiaFieldOverDecompositionField_fixingSubgroup_eq

L189 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldOverDecompositionField_fixingSubgroup_eq
Documentation

A prime-decomposition consequence: G(L/T_P) over the decomposition field is the transported inertia subgroup.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
theorem dedekindRamification_inertiaFieldOverDecompositionField_fixingSubgroup_eq
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    (inertiaFieldOverDecompositionField (K := K) (L := L) G P).fixingSubgroup =
      inertiaGroupOverDecompositionField (K := K) (L := L) G P
instance

inertiaFieldOverDecompositionField_isGalois

L203 ↗
HilbertRamification.Dedekind.inertiaFieldOverDecompositionField_isGalois
Documentation

The localization and decomposition comparison: T_P/Z_P is normal, at the fixed-field source level.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
instance inertiaFieldOverDecompositionField_isGalois
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    IsGalois (decompositionField (K := K) (L := L) G P)
      (inertiaFieldOverDecompositionField (K := K) (L := L) G P)
def

dedekindRamification_decompositionQuotientInertiaEquivGalInertiaFieldOverDecomposition

L216 ↗
HilbertRamification.Dedekind.dedekindRamification_decompositionQuotientInertiaEquivGalInertiaFieldOverDecomposition
Documentation

The localization and decomposition comparison gives: G_P/I_P ≃ Gal(T_P/Z_P), the fixed-field quotient form.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
def dedekindRamification_decompositionQuotientInertiaEquivGalInertiaFieldOverDecomposition
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    decompositionGroup P G ⧸
        (inertiaGroup P G).subgroupOf (decompositionGroup P G) ≃*
      (inertiaFieldOverDecompositionField (K := K) (L := L) G P ≃ₐ[
        decompositionField (K := K) (L := L) G P]
        inertiaFieldOverDecompositionField (K := K) (L := L) G P)
theorem

dedekindRamification_inertiaFieldOverDecompositionField_finrank_eq_quotient_card

L242 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldOverDecompositionField_finrank_eq_quotient_card
Documentation

A prime-decomposition consequence: [T_P : Z_P] = #(G_P / I_P).

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
theorem dedekindRamification_inertiaFieldOverDecompositionField_finrank_eq_quotient_card
    (P : Ideal B) [MulSemiringAction G B]
    [Finite G] [IsGaloisGroup G K L] :
    Module.finrank (decompositionField (K := K) (L := L) G P)
        (inertiaFieldOverDecompositionField (K := K) (L := L) G P) =
      Nat.card
        (decompositionGroup P G ⧸
          (inertiaGroup P G).subgroupOf (decompositionGroup P G))
def

dedekindRamification_galInertiaFieldOverDecompositionEquivResidueGalois

L271 ↗
HilbertRamification.Dedekind.dedekindRamification_galInertiaFieldOverDecompositionEquivResidueGalois
Documentation

The localization and decomposition comparison: Gal(T_P/Z_P) ≃ Gal(kappa(P)/kappa(p)), obtained by composing the fixed-field quotient identification with the residue exact sequence.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
def dedekindRamification_galInertiaFieldOverDecompositionEquivResidueGalois
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    [MulSemiringAction G B] [SMulCommClass G A B]
    [Finite G] [IsGaloisGroup G K L] [Algebra.IsInvariant A B G] :
    (inertiaFieldOverDecompositionField (K := K) (L := L) G P ≃ₐ[
        decompositionField (K := K) (L := L) G P]
        inertiaFieldOverDecompositionField (K := K) (L := L) G P) ≃*
      (B ⧸ P) ≃ₐ[A ⧸ p] B ⧸ P
theorem

dedekindInertiaField_inertiaField_properties

L287 ↗
HilbertRamification.Dedekind.dedekindInertiaField_inertiaField_properties
Documentation

The localization and decomposition comparison: the inertia field proposition, bundled in the field-theoretic form: T_P/Z_P is normal, Gal(T_P/Z_P) is the residue Galois group, and G(L/T_P)=I_P.

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra Module
variable {A B K L : Type*}
variable [CommRing A] [CommRing B] [Algebra A B]
variable [Field K] [Field L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
variable {G}
variable (G)
variable {G}
variable (G)
Lean source · statement
theorem dedekindInertiaField_inertiaField_properties
    (p : Ideal A) (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    [MulSemiringAction G B] [SMulCommClass G A B]
    [Finite G] [IsGaloisGroup G K L] [Algebra.IsInvariant A B G] :
    IsGalois (decompositionField (K := K) (L := L) G P)
        (inertiaFieldOverDecompositionField (K := K) (L := L) G P) ∧
      Nonempty
        ((inertiaFieldOverDecompositionField (K := K) (L := L) G P ≃ₐ[
            decompositionField (K := K) (L := L) G P]
            inertiaFieldOverDecompositionField (K := K) (L := L) G P) ≃*
          (B ⧸ P) ≃ₐ[A ⧸ p] B ⧸ P) ∧
      fixingSubgroup G
          ((inertiaField (K := K) (L := L) G P : IntermediateField K L) :
            Set L) =
        inertiaGroup P G

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.