Module

AlgebraicRamificationProP.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.AlgebraicRamificationProP

2 declarations indexed from sourceView source ↗

Module documentation

The actual ramification subgroup is pro-p

Restriction to a finite Galois layer lands in that layer's actual ramification group. Its finite image is therefore a p-group in residue characteristic p. The kernels of these continuous restrictions form a Krull neighborhood basis. No surjectivity of restriction on ramification groups is required.

Imports6

Imported by1

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.All

theorem

restrictNormal_ramification_range_isPGroup

L33 ↗

RamificationTheory.HilbertRamification.ValuationSubring.restrictNormal_ramification_range_isPGroup

Source context 5 commands

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

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

Lean source · statement

theorem restrictNormal_ramification_range_isPGroup
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (A : _root_.ValuationSubring L) (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField A) p]
    (E : FiniteGaloisIntermediateField K L) :
    IsPGroup p
      (((AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E).comp
        (ramificationGroupInAut K A).subtype).range)

theorem

ramificationGroupInAut_hasOpenNormalBasisInClass_of_isGalois_residueChar

L92 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInAut_hasOpenNormalBasisInClass_of_isGalois_residueChar

Documentation

For an algebraic Galois extension, the actual ramification subgroup in the ambient automorphism group has an open-normal p-group basis in residue characteristic p. No Henselianity, discreteness, or residue perfectness is needed.