Module

RingHilbertRamificationComparison.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingHilbertRamificationComparison

1 declaration indexed from sourceView source ↗

Module documentation

The ring-character wild predicate is actual Hilbert ramification

This consumer uses the native decomposition action on the actual valuation subring. Both individual ring maps in the sparse comparison are supplied by that action; their coefficient compatibility is definitional.

Imports2

Imported by2

theorem

mem_ramificationGroup_iff_principalUnitMultipliers

L26 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroup_iff_principalUnitMultipliers

Documentation

Actual Hilbert ramification is exactly the principal-unit multiplier predicate used by the ring-only DVR character kernel.

Source context 3 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v

Lean source · statement

theorem mem_ramificationGroup_iff_principalUnitMultipliers
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) (σ : inertiaGroup K V) :
    σ ∈ ramificationGroup K V ↔
      ∀ x : V, ∃ a : Vˣ,
        (σ : decompositionGroup K V) • x = x * (a : V) ∧
          (a : V) - 1 ∈ IsLocalRing.maximalIdeal V

Module documentation

The ring-character wild predicate is actual Hilbert ramification

Declarations

mem_ramificationGroup_iff_principalUnitMultipliers