Module

SepClosedResidueInertia.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.SepClosedResidueInertia

2 declarations indexed from sourceView source ↗

Module documentation

Inertia over a separably closed residue field

The algebraic residue extension is purely inseparable, so its Galois action is trivial. On each finite Galois layer the inertia character sends the commutator to one, placing it in the actual wild ramification group.

Imports5

Imported by2

def

henselianGalToInertia

L37 ↗

RamificationTheory.HilbertRamification.ValuationSubring.henselianGalToInertia

Documentation

Over a separably closed residue field every Galois automorphism is inertia.

Source context 5 commands

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

open scoped commutatorElement Topology
namespace RamificationTheory.HilbertRamification.ValuationSubring
noncomputable section
universe u v w x
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  {Γ : Type w} {Δ : Type x}
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : Valuation K Γ) (w : Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (IsLocalRing.maximalIdeal v.valuationSubring)]
  [IsSepClosed (IsLocalRing.ResidueField v.valuationSubring)]

Lean source · full declaration

def henselianGalToInertia : Gal(L/K) →* inertiaGroup K w.valuationSubring where
  toFun σ := ⟨henselianGalToDecomposition v w σ, by
    have : Algebra.IsIntegral (IsLocalRing.ResidueField v.valuationSubring)
        (IsLocalRing.ResidueField w.valuationSubring) :=
      henselianResidueExtension_isIntegral v w
    have he := Subsingleton.elim (henselianResidueAction v w σ).toAlgHom
      (AlgHom.id (IsLocalRing.ResidueField v.valuationSubring)
        (IsLocalRing.ResidueField w.valuationSubring))
    apply RingEquiv.ext
    intro a
    exact congrArg (fun f => f a) he⟩
  map_one' := rfl
  map_mul' _ _ := rfl

theorem

commutator_isPGroup_of_henselian_separablyClosedResidue

L53 ↗

RamificationTheory.HilbertRamification.ValuationSubring.commutator_isPGroup_of_henselian_separablyClosedResidue

Documentation

The commutator of finite Galois inertia lies in wild inertia.

Source context 6 commands

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

open scoped commutatorElement Topology
namespace RamificationTheory.HilbertRamification.ValuationSubring
noncomputable section
universe u v w x
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  {Γ : Type w} {Δ : Type x}
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : Valuation K Γ) (w : Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (IsLocalRing.maximalIdeal v.valuationSubring)]
  [IsSepClosed (IsLocalRing.ResidueField v.valuationSubring)]
include v in

Lean source · statement

theorem commutator_isPGroup_of_henselian_separablyClosedResidue
    [FiniteDimensional K L] (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField w.valuationSubring) p] :
    IsPGroup p (commutator Gal(L/K))

Module documentation

Inertia over a separably closed residue field

Declarations

henselianGalToInertia

commutator_isPGroup_of_henselian_separablyClosedResidue