Module

HenselianNormality.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.HenselianNormality

3 declarations indexed from sourceView source ↗

Module documentation

Ambient normality of inertia and ramification over a Henselian base

The defining principal-unit condition for ramification is preserved by conjugation by every decomposition automorphism. Over a Henselian base, decomposition is the full automorphism group, so both actual inertia and actual ramification are normal subgroups of that group.

Imports2

Imported by1

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.All

theorem

ramificationGroup_map_inertiaSubtype_normal

L28 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup_map_inertiaSubtype_normal

Documentation

Ramification, embedded in decomposition through inertia, is normal in decomposition. No finiteness, algebraicity, or Henselianity is required.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem ramificationGroup_map_inertiaSubtype_normal
    (A : _root_.ValuationSubring L) :
    ((ramificationGroup K A).map (inertiaGroup K A).subtype).Normal

theorem

inertiaGroupInAut_normal_of_henselianRing

L53 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut_normal_of_henselianRing

Documentation

Actual inertia is normal in the full automorphism group of an algebraic extension of a Henselian valued field.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem inertiaGroupInAut_normal_of_henselianRing
    [Algebra.IsAlgebraic K L]
    (V : _root_.ValuationSubring K)
    [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (A : _root_.ValuationSubring L) [V.valuation.HasExtension A.valuation] :
    (inertiaGroupInAut K A).Normal

theorem

ramificationGroupInAut_normal_of_henselianRing

L69 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInAut_normal_of_henselianRing

Documentation

Actual ramification is normal in the full automorphism group of an algebraic extension of a Henselian valued field.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem ramificationGroupInAut_normal_of_henselianRing
    [Algebra.IsAlgebraic K L]
    (V : _root_.ValuationSubring K)
    [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (A : _root_.ValuationSubring L) [V.valuation.HasExtension A.valuation] :
    (ramificationGroupInAut K A).Normal

Module documentation

Ambient normality of inertia and ramification over a Henselian base

Declarations

ramificationGroup_map_inertiaSubtype_normal

inertiaGroupInAut_normal_of_henselianRing

ramificationGroupInAut_normal_of_henselianRing