Module

SepClosedResidueDerivedProP.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.SepClosedResidueDerivedProP

1 declaration indexed from sourceView source ↗

Module documentation

Closed derived terms over a separably closed residue field

Finite Galois restrictions of each positive closed derived term land in finite p-group commutators. The Krull neighborhood basis therefore supplies an open-normal p-group basis on the derived term itself.

Imports7

Imported by2

theorem

topDerived_hasOpenNormalBasisInClass_of_separablyClosedResidue

L32 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.topDerived_hasOpenNormalBasisInClass_of_separablyClosedResidue

Documentation

Every closed derived term after the first is pro-p over separably closed residue.

Source context 6 commands

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

open scoped Topology
namespace ValuationTheory.DiscreteValuationField
open ProCGroups.ProC ProCGroups.FiniteStepSolvableQuotients
open RamificationTheory.HilbertRamification.ValuationSubring
noncomputable section
universe u v

Lean source · statement

theorem HenselianDVF.topDerived_hasOpenNormalBasisInClass_of_separablyClosedResidue
    {K : Type u} [Field K] [CharZero K]
    (base : HenselianDVF.{u, v} K) (p : ℕ) [Fact p.Prime]
    [CharP base.residueField p] [IsSepClosed base.residueField]
    (m : ℕ) (hm : 1 ≤ m) :
    HasOpenNormalBasisInClass (ProCGroups.FiniteGroupClass.pGroup p)
      (topDerivedTop Gal(AlgebraicClosure K/K) m)

Module documentation

Closed derived terms over a separably closed residue field

Declarations

topDerived_hasOpenNormalBasisInClass_of_separablyClosedResidue