Module

DVRUniformizerFactorization.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.DVRUniformizerFactorization

2 declarations indexed from sourceView source ↗

Module documentation

Factorization of mapped uniformizers

Factors a mapped uniformizer into a target uniformizer power and a unit, with exponent given by its additive valuation. For a local DVR algebra, the exponent is the ramification index.

Imports2

Mathlib.RingTheory.DiscreteValuationRing.Basic
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.DVRRamificationOrder

Imported by4

theorem

mappedUniformizer_factorization_addVal

L30 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.mappedUniformizer_factorization_addVal

Documentation

The mapped source uniformizer has its native DVR order as exponent. The unit factor is constructed from the target DVR, with no supplied factorization.

Source context 7 commands

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

namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
variable (A : Type u) (B : Type v)
variable [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
variable [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
omit [IsDomain A] [IsDiscreteValuationRing A] in

Lean source · statement

theorem mappedUniformizer_factorization_addVal
    (f : A →+* B) (hinj : Function.Injective f)
    (π : A) (hπ : Irreducible π) (ρ : B) (hρ : Irreducible ρ) :
    ∃ u : Bˣ,
      f π = ρ ^ (IsDiscreteValuationRing.addVal B (f π)).toNat * (u : B)

theorem

mappedUniformizer_factorization_ramificationIdx

L46 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.mappedUniformizer_factorization_ramificationIdx