Module

FiniteInertiaRestriction.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteInertiaRestriction

5 declarations indexed from sourceView source ↗

Module documentation

Restriction maps between finite inertia groups

Define finite inertia restriction and transition maps, compare them with Galois restriction, and prove compatibility and surjectivity over a Henselian base.

Imports3

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.BaseChange
Mathlib.FieldTheory.Galois.Profinite
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.HenselianInertiaRestriction

Imported by3

def

finiteInertiaRestriction

L25 ↗

RamificationTheory.HilbertRamification.ValuationSubring.finiteInertiaRestriction

Documentation

Actual restriction of inertia to a finite Galois intermediate field.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

def finiteInertiaRestriction
    (A : _root_.ValuationSubring L) (E : FiniteGaloisIntermediateField K L) :
    inertiaGroup K A →*
      inertiaGroup K (A.comap E.toIntermediateField.val.toRingHom)

theorem

finiteInertiaRestriction_coe

L37 ↗

RamificationTheory.HilbertRamification.ValuationSubring.finiteInertiaRestriction_coe

Documentation

Inertia restriction agrees with the standard Galois restriction homomorphism.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem finiteInertiaRestriction_coe
    (A : _root_.ValuationSubring L) (E : FiniteGaloisIntermediateField K L)
    (σ : inertiaGroup K A) :
    inertiaGroupToAut (K := K) (A.comap E.toIntermediateField.val.toRingHom)
        (finiteInertiaRestriction A E σ) =
      AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E
        (inertiaGroupToAut (K := K) A σ)

def

finiteInertiaTransition

L62 ↗

RamificationTheory.HilbertRamification.ValuationSubring.finiteInertiaTransition

Documentation

Inertia restriction along an inclusion of finite Galois fields.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

def finiteInertiaTransition
    (A : _root_.ValuationSubring L)
    (E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F) :
    inertiaGroup K (A.comap F.toIntermediateField.val.toRingHom) →*
      inertiaGroup K (A.comap E.toIntermediateField.val.toRingHom)

theorem

finiteInertiaTransition_comp

L76 ↗

RamificationTheory.HilbertRamification.ValuationSubring.finiteInertiaTransition_comp

Documentation

Actual finite inertia restriction commutes with transition to a lower field.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem finiteInertiaTransition_comp
    (A : _root_.ValuationSubring L)
    (E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F)
    (σ : inertiaGroup K A) :
    finiteInertiaTransition A E F hEF (finiteInertiaRestriction A F σ) =
      finiteInertiaRestriction A E σ

theorem

finiteInertiaTransition_surjective_of_henselianRing

L111 ↗

RamificationTheory.HilbertRamification.ValuationSubring.finiteInertiaTransition_surjective_of_henselianRing

Documentation

The finite inertia transition is onto over a Henselian base.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem finiteInertiaTransition_surjective_of_henselianRing [IsGalois K L]
    (V : _root_.ValuationSubring K)
    [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (A : _root_.ValuationSubring L) [V.valuation.HasExtension A.valuation]
    (E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F) :
    Function.Surjective (finiteInertiaTransition A E F hEF)

Module documentation

Restriction maps between finite inertia groups

Declarations

finiteInertiaRestriction

finiteInertiaRestriction_coe

finiteInertiaTransition

finiteInertiaTransition_comp

finiteInertiaTransition_surjective_of_henselianRing