Module

ActualFiniteWildOrder.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteWildOrder

1 declaration indexed from sourceView source ↗

Module documentation

Primary wild order over the original residue characteristic

Literal prime contraction identifies the finite prime residue characteristic with the original base residue characteristic. No subgroup or inertia group is introduced during this arithmetic step.

Imports8

Imported by2

theorem

actualFiniteStageWildOrder_exists_baseResidue_expChar_pow

L34 ↗

EtaleFundamentalGroups.Inertia.actualFiniteStageWildOrder_exists_baseResidue_expChar_pow

Documentation

The existing actual finite wild order is a power of the base residue exponential characteristic, supplied from the same actual normalization.

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 · statement

theorem actualFiniteStageWildOrder_exists_baseResidue_expChar_pow
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal]
    (E : FiniteGaloisIntermediateField K L) :
    ∃ n : ℕ, actualFiniteStageWildOrder A K L Q E =
      (ringExpChar (IsLocalRing.ResidueField A)) ^ n

Module documentation

Primary wild order over the original residue characteristic

Declarations

actualFiniteStageWildOrder_exists_baseResidue_expChar_pow