Module

RingTameOrderRamification.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingTameOrderRamification

3 declarations indexed from sourceView source ↗

Module documentation

Tame orders and ramification indices

Proves that the finite tame order is invertible in the residue field and divides the valuation of every nonzero fixed element. It consequently divides the ramification index of an injective DVR algebra with a compatible action.

Imports4

Imported by3

theorem

tameOrder_isUnit_residue

L34 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.tameOrder_isUnit_residue

Documentation

An actual finite tame degree is invertible in the actual residue field.

Source context 7 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v w
section OneRing
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [Finite G] [MulSemiringAction G R]

Lean source · statement

theorem tameOrder_isUnit_residue : IsUnit (tameOrder R G : ResidueField R)

theorem

tameOrder_dvd_addVal_of_fixed

L40 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.tameOrder_dvd_addVal_of_fixed

Documentation

Every actual nonzero fixed ring element has order divisible by the tame degree.

Source context 7 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v w
section OneRing
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [Finite G] [MulSemiringAction G R]

Lean source · statement

theorem tameOrder_dvd_addVal_of_fixed (x : R) (hx : x ≠ 0)
    (hfixed : ∀ g : G, g • x = x) :
    tameOrder R G ∣ (IsDiscreteValuationRing.addVal R x).toNat

theorem

tameOrder_dvd_ramificationIdx

L61 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.tameOrder_dvd_ramificationIdx

Documentation

The actual tame degree divides the actual ramification index of an injective DVR algebra on which the group acts over the base. The group/residue calculation and the two-ring valuation comparison are closed separate suppliers.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v w

Lean source · statement

theorem tameOrder_dvd_ramificationIdx
    (A : Type u) (R : Type v)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Algebra A R]
    [(maximalIdeal R).LiesOver (maximalIdeal A)]
    (G : Type w) [Group G] [Finite G] [MulSemiringAction G R] [SMulCommClass G A R]
    (hinj : Function.Injective (algebraMap A R)) :
    tameOrder R G ∣ (maximalIdeal R).ramificationIdx A

Module documentation

Tame orders and ramification indices

Declarations

tameOrder_isUnit_residue

tameOrder_dvd_addVal_of_fixed

tameOrder_dvd_ramificationIdx