Module

AbsoluteTameCofinality.lean

Nyll.EtaleFundamentalGroups.Inertia.AbsoluteTameCofinality

3 declarations indexed from sourceView source ↗

Module documentation

Cofinality of the actual finite tame orders in every invertible exponent

The chosen finite Galois normalization contains an actual root of a base uniformizer. The finite-ring divisibility theorem supplies its actual tame order as a multiple of the prescribed exponent. Thus the literal finite degree image set is cofinal in the full divisibility order.

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

Imports6

Imported by2

theorem

finiteAbsoluteNormalization_radical_exponent_dvd_tameOrder

L35 ↗

EtaleFundamentalGroups.Inertia.finiteAbsoluteNormalization_radical_exponent_dvd_tameOrder

Documentation

The native finite-field owner supplies radical divisibility before the original upper normalization prime is introduced.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w

Lean source · full declaration

theorem finiteAbsoluteNormalization_radical_exponent_dvd_tameOrder
    (A : Type u) (K : Type v) (Ω : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
    [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsGalois K Ω]
    (E : FiniteGaloisIntermediateField K Ω) :
    let : IsDedekindDomain (finiteAbsoluteNormalizationAlgebra A K Ω E) :=
      finiteAbsoluteNormalizationAlgebra_isDedekindDomain A K Ω E
    ∀ (q : Ideal (finiteAbsoluteNormalizationAlgebra A K Ω E)) [q.IsPrime]
      (hq : q ≠ ⊥) (n : ℕ), IsUnit (n : A) → ∀ (π : A), Irreducible π →
      ∀ (γ : finiteAbsoluteNormalizationAlgebra A K Ω E),
      γ ^ n = (commAlgCoefficientMap (finiteAbsoluteNormalizationAlgebra A K Ω E)).toFun π →
      n ∣ commAlgIdealTameOrder A (finiteAbsoluteNormalizationAlgebra A K Ω E) q hq := by
  dsimp only
  intro q qPrime hq n hn π hπ γ hγ
  let q' : Ideal (normalizationCommAlgCat A (finiteLevelFieldAlgebra A K Ω E)) := q
  have : q'.IsPrime := qPrime
  exact finiteNormalization_radical_exponent_dvd_tameOrder A K
    (finiteLevelFieldAlgebra A K Ω E) q' hq n hn π hπ γ hγ

theorem

exists_actualFiniteStageTameOrder_multiple

L63 ↗

EtaleFundamentalGroups.Inertia.exists_actualFiniteStageTameOrder_multiple

Documentation

Every exponent invertible in the original DVR divides the actual tame order at the chosen original prime of some finite Galois subextension.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]

Lean source · statement

theorem exists_actualFiniteStageTameOrder_multiple
    (n : ℕ) (hn : IsUnit (n : A)) :
    ∃ E : FiniteGaloisIntermediateField K Ω, n ∣ actualFiniteStageTameOrder A K Ω Q E

theorem

actualFiniteTameDegreeSet_cofinal

L77 ↗

EtaleFundamentalGroups.Inertia.actualFiniteTameDegreeSet_cofinal

Documentation

The actual image of finite tame degrees is cofinal among all positive exponents invertible in the base residue field. In characteristic zero this includes every positive integer.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (Ω : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
  [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsSepClosure K Ω]
  (Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]

Lean source · statement

theorem actualFiniteTameDegreeSet_cofinal :
    ∀ n : InvertibleExponent (IsLocalRing.ResidueField A),
      ∃ t : actualFiniteTameDegreeSet A K Ω Q, n ≤ t.val

Module documentation

Cofinality of the actual finite tame orders in every invertible exponent

Declarations

finiteAbsoluteNormalization_radical_exponent_dvd_tameOrder

exists_actualFiniteStageTameOrder_multiple

actualFiniteTameDegreeSet_cofinal