Module

RamificationGroup.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RamificationGroup

8 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: ramification subgroup source lemmas

This file records the first structural facts about the classical ramification subgroup R_w. The key point for the later character map I_w -> Hom(Delta/Gamma, lambda*) is that R_w is a normal subgroup of I_w, not merely a subgroup.

Imports1

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.ValuationSubring

Imported by5

theorem

decompositionGroup_mapEquiv_mem_principalUnitGroup

L33 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup_mapEquiv_mem_principalUnitGroup

Documentation

A decomposition-group automorphism preserves the principal unit group of the valuation subring it stabilizes.

Source context 6 commands

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

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

Lean source · statement

theorem decompositionGroup_mapEquiv_mem_principalUnitGroup
    (A : _root_.ValuationSubring L) (τ : decompositionGroup K A)
    {u : Lˣ} (hu : u ∈ A.principalUnitGroup) :
    Units.mapEquiv ((τ : L ≃ₐ[K] L).toMulEquiv) u ∈ A.principalUnitGroup

instance

ramificationGroup_normal

L88 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup_normal

Documentation

The normality calculation for the ramification subgroup: the ramification group is normal in inertia.

Source context 6 commands

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

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

Lean source · statement

instance ramificationGroup_normal (A : _root_.ValuationSubring L) :
    (ramificationGroup K A).Normal

def

inertiaGroupEquivInAut

L113 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupEquivInAut

Documentation

The inertia group is canonically equivalent to its image in the ambient K-automorphism group.

Source context 6 commands

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

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

Lean source · statement

def inertiaGroupEquivInAut
    (A : _root_.ValuationSubring L) :
    inertiaGroup K A ≃* inertiaGroupInAut K A

abbrev

ramificationGroupInInertiaAut

L121 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInInertiaAut

Documentation

The ramification subgroup, viewed as a subgroup of ambient inertia.

Source context 6 commands

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

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

Lean source · statement

abbrev ramificationGroupInInertiaAut
    (A : _root_.ValuationSubring L) :
    Subgroup (inertiaGroupInAut K A)

theorem

mem_ramificationGroupInInertiaAut_iff

L128 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroupInInertiaAut_iff

Documentation

States the theorem mem_ramificationGroupInInertiaAut_iff.

Source context 6 commands

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

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

Lean source · statement

theorem mem_ramificationGroupInInertiaAut_iff
    (A : _root_.ValuationSubring L) (σ : inertiaGroupInAut K A) :
    σ ∈ ramificationGroupInInertiaAut K A ↔
      ∃ τ : ramificationGroup K A,
        inertiaGroupEquivInAut (K := K) A τ = σ

instance

ramificationGroupInInertiaAut_normal

L140 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInInertiaAut_normal

Documentation

The ambient copy of R_w is normal inside the ambient copy of I_w.

Source context 6 commands

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

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

Lean source · statement

instance ramificationGroupInInertiaAut_normal
    (A : _root_.ValuationSubring L) :
    (ramificationGroupInInertiaAut K A).Normal

def

inertiaGroupQuotientRamificationEquivInertiaAutQuotient

L151 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupQuotientRamificationEquivInertiaAutQuotient

Documentation

The tame-inertia quotient identification source: transport the quotient I_w/R_w to the corresponding quotient of the ambient automorphism subgroups.

Source context 6 commands

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

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

Lean source · statement

def inertiaGroupQuotientRamificationEquivInertiaAutQuotient
    (A : _root_.ValuationSubring L) :
    inertiaGroup K A ⧸ ramificationGroup K A ≃*
      inertiaGroupInAut K A ⧸ ramificationGroupInInertiaAut K A

theorem

inertiaGroupQuotientRamificationEquivInertiaAutQuotient_mk

L162 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupQuotientRamificationEquivInertiaAutQuotient_mk

Documentation

States the theorem inertiaGroupQuotientRamificationEquivInertiaAutQuotient_mk.

Source context 6 commands

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

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

Lean source · statement

theorem inertiaGroupQuotientRamificationEquivInertiaAutQuotient_mk
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    inertiaGroupQuotientRamificationEquivInertiaAutQuotient
        (K := K) A (QuotientGroup.mk' (ramificationGroup K A) σ) =
      QuotientGroup.mk' (ramificationGroupInInertiaAut K A)
        (inertiaGroupEquivInAut (K := K) A σ)

Module documentation

Hilbert ramification theory: ramification subgroup source lemmas

Declarations