NYLL
Module

FiniteIdealTameRamification.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealTameRamification
3 declarations indexed from sourceView source ↗

Module documentation

Tame orders and ramification indices

Proves that the finite tame order at the original normalization prime divides its ramification index.

Imports6
Imported by3

Declarations

theorem

localizedCoefficient_ne_zero

L31 ↗
EtaleFundamentalGroups.Inertia.localizedCoefficient_ne_zero
Source context 5 commands

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

noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v w
Lean source · statement
theorem localizedCoefficient_ne_zero
    {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 : A) (ha : a ≠ 0) :
    algebraMap B (Localization.AtPrime Q) (algebraMap A B a) ≠ 0
theorem

localizedCoefficient_fixed

L42 ↗
EtaleFundamentalGroups.Inertia.localizedCoefficient_fixed
Source context 5 commands

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

noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v w
Lean source · statement
theorem localizedCoefficient_fixed
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (G : Type w) [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (Q : Ideal B) [Q.IsPrime] (a : A) (σ : MulAction.stabilizer G Q) :
    σ • algebraMap B (Localization.AtPrime Q) (algebraMap A B a) =
      algebraMap B (Localization.AtPrime Q) (algebraMap A B a)
theorem

finiteIdealTameOrder_dvd_ramificationIdx

L53 ↗
EtaleFundamentalGroups.Inertia.finiteIdealTameOrder_dvd_ramificationIdx
Documentation

The actual finite tame order at the original normalization prime divides its original ramification index. The coefficient nonzero/fixed calculations, length comparison and one-DVR character calculation remain separate scopes.

Source context 5 commands

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

noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v w
Lean source · statement
theorem finiteIdealTameOrder_dvd_ramificationIdx
    (A : Type u) (B : Type v)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [CommRing B] [IsDedekindDomain B] [Algebra A B] [FaithfulSMul A B]
    (G : Type w) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B]
    (Q : Ideal B) [Q.IsPrime] [Q.LiesOver (IsLocalRing.maximalIdeal A)] (hQ : Q ≠ ⊥) :
    finiteIdealTameOrder B G Q hQ ∣ Q.ramificationIdx A

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.