Module

UniformizerRadicalRamification.lean

Nyll.EtaleFundamentalGroups.Inertia.UniformizerRadicalRamification

6 declarations indexed from sourceView source ↗

Module documentation

Uniformizer radicals force divisibility of the ramification index

The length definition of the ramification index and additivity of order of vanishing give the divisibility used in Stacks Project, Tag 0BUB. The root need not be a uniformizer, and no residue separability or characteristic-zero hypothesis is used.

Reference: https://stacks.math.columbia.edu/tag/0BUB

Imports3

Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.OrderOfVanishing.Basic
Mathlib.RingTheory.RamificationInertia.Ramification

Imported by4

def

localizedCoefficient

L30 ↗

EtaleFundamentalGroups.Inertia.localizedCoefficient

Documentation

The actual coefficient map to the prime localization, constructed as a ring-homomorphism composite. It does not install another scalar action.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

def localizedCoefficient
    (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (q : Ideal B) [q.IsPrime] : A →+* Localization.AtPrime q

theorem

ramificationIdx_eq_ord_localizedCoefficient

L37 ↗

EtaleFundamentalGroups.Inertia.ramificationIdx_eq_ord_localizedCoefficient

Documentation

The prime generator computes the literal ramification length. All localization scalar structures needed by that length stay in this owner.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem ramificationIdx_eq_ord_localizedCoefficient
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (q : Ideal B) [q.IsPrime] (π : A)
    (hunder : q.under A = Ideal.span (Set.singleton π)) :
    q.ramificationIdx A =
      (Ring.ord (Localization.AtPrime q) (localizedCoefficient A q π)).toNat

theorem

ramificationIdx_eq_ord_localized_uniformizer

L52 ↗

EtaleFundamentalGroups.Inertia.ramificationIdx_eq_ord_localized_uniformizer

Documentation

An original DVR uniformizer computes the actual ramification index through the literal composite coefficient map into the prime localization. The A-action on that localization stays inside the existing length owner.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem ramificationIdx_eq_ord_localized_uniformizer
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsDomain A] [IsDiscreteValuationRing A] [Algebra A B]
    (Q : Ideal B) [Q.IsPrime] [Q.LiesOver (IsLocalRing.maximalIdeal A)]
    (π : A) (hπ : Irreducible π) :
    Q.ramificationIdx A =
      (Ring.ord (Localization.AtPrime Q)
        (algebraMap B (Localization.AtPrime Q) (algebraMap A B π))).toNat

theorem

exponent_dvd_ord_of_pow_eq

L65 ↗

EtaleFundamentalGroups.Inertia.exponent_dvd_ord_of_pow_eq

Documentation

The actual order-of-vanishing calculation is a one-ring statement.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem exponent_dvd_ord_of_pow_eq
    {S : Type u} [CommRing S] (n : ℕ) (α β : S)
    (hα : α ∈ nonZeroDivisors S) (hpow : α ^ n = β) :
    n ∣ (Ring.ord S β).toNat

theorem

exponent_dvd_ramificationIdx_of_pow_eq

L74 ↗

EtaleFundamentalGroups.Inertia.exponent_dvd_ramificationIdx_of_pow_eq

Documentation

An actual radical of a generator of the contracted prime forces its exponent to divide the ramification index.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem exponent_dvd_ramificationIdx_of_pow_eq
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsDomain A] [IsDomain B] [Algebra A B] [FaithfulSMul A B]
    (q : Ideal B) [q.IsPrime] (π : A) (hπ : π ≠ 0)
    (hunder : q.under A = Ideal.span (Set.singleton π))
    (n : ℕ) (hn : n ≠ 0) (α : B)
    (hα : α ^ n = algebraMap A B π) :
    n ∣ q.ramificationIdx A

theorem

exponent_dvd_ramificationIdx_of_uniformizer_pow_eq

L98 ↗

EtaleFundamentalGroups.Inertia.exponent_dvd_ramificationIdx_of_uniformizer_pow_eq

Documentation

The original DVR specialization, for every prime over the maximal ideal, without imposing separability on its residue extension.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem exponent_dvd_ramificationIdx_of_uniformizer_pow_eq
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    [IsDomain A] [IsDomain B] [IsDiscreteValuationRing A]
    [Algebra A B] [FaithfulSMul A B]
    (q : Ideal B) [q.IsPrime] [q.LiesOver (IsLocalRing.maximalIdeal A)]
    (π : A) (hπ : Irreducible π) (n : ℕ) (hn : n ≠ 0)
    (α : B) (hα : α ^ n = algebraMap A B π) :
    n ∣ q.ramificationIdx A

Module documentation

Uniformizer radicals force divisibility of the ramification index

Declarations

localizedCoefficient

ramificationIdx_eq_ord_localizedCoefficient

ramificationIdx_eq_ord_localized_uniformizer

exponent_dvd_ord_of_pow_eq

exponent_dvd_ramificationIdx_of_pow_eq

exponent_dvd_ramificationIdx_of_uniformizer_pow_eq