Module

RamificationCharacterization.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RamificationCharacterization

3 declarations indexed from sourceView source ↗

Module documentation

Ramification inside the decomposition group

The principal-unit condition forces trivial residue action, so the ramification group inside inertia has a canonical image in the decomposition group.

Imports1

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.ValuationSubring

Imported by2

theorem

ramificationCondition_mem_inertiaGroup

L30 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationCondition_mem_inertiaGroup

Documentation

The intrinsic principal-unit ramification condition already forces an element of the decomposition group to lie in inertia.

Source context 6 commands

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

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

Lean source · statement

theorem ramificationCondition_mem_inertiaGroup
    (A : _root_.ValuationSubring L) (sigma : decompositionGroup K A)
    (hsigma : ∀ x : Lˣ,
      automorphismUnitQuotient K A sigma x ∈ A.principalUnitGroup) :
    sigma ∈ inertiaGroup K A

abbrev

ramificationGroupInDecomposition

L69 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInDecomposition

Documentation

The ramification group transported from inertia into the decomposition group.

Source context 6 commands

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

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

Lean source · statement

abbrev ramificationGroupInDecomposition
    (A : _root_.ValuationSubring L) :
    Subgroup (decompositionGroup K A)

theorem

mem_ramificationGroupInDecomposition_iff

L74 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroupInDecomposition_iff

Documentation

Membership in the transported ramification group is the intrinsic principal-unit condition.

Source context 6 commands

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

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

Lean source · statement

theorem mem_ramificationGroupInDecomposition_iff
    (A : _root_.ValuationSubring L) (sigma : decompositionGroup K A) :
    sigma ∈ ramificationGroupInDecomposition K A ↔
      ∀ x : Lˣ,
        automorphismUnitQuotient K A sigma x ∈ A.principalUnitGroup

Module documentation

Ramification inside the decomposition group

Declarations

ramificationCondition_mem_inertiaGroup

ramificationGroupInDecomposition

mem_ramificationGroupInDecomposition_iff