NYLL
Module

FiniteIdealRadicalTameDivisibility.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealRadicalTameDivisibility
2 declarations indexed from sourceView source ↗

Module documentation

Actual uniformizer radicals divide the actual finite tame order

The principal-unit kernel at the original prime has the power order proved by its actual localized automorphisms. An invertible radical exponent is coprime to that same residue characteristic, so it survives the genuine inertia cardinality factorization, including inseparable residue extensions.

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

Imports6
Imported by2

Declarations

theorem

natCast_isUnit_coprime_idealResidue

L31 ↗
EtaleFundamentalGroups.Inertia.natCast_isUnit_coprime_idealResidue
Documentation

Base invertibility implies coprimality to the characteristic of the actual prime residue field through the literal coefficient RingHom.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
theorem natCast_isUnit_coprime_idealResidue
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
    (Q : Ideal B) [Q.IsPrime] (n : ℕ) (hn : IsUnit (n : A)) :
    Nat.Coprime n (ringExpChar Q.ResidueField)
theorem

radical_exponent_dvd_finiteIdealTameOrder

L45 ↗
EtaleFundamentalGroups.Inertia.radical_exponent_dvd_finiteIdealTameOrder
Documentation

An actual root of a base uniformizer forces its invertible exponent to divide the actual tame order for the intrinsic coefficient automorphisms. The wild power and inertia cardinality are supplied by their proved owners.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
theorem radical_exponent_dvd_finiteIdealTameOrder
    (A : Type u) (B : Type v)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [CommRing B] [IsDedekindDomain B] [Algebra A B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    [IsGaloisGroup (B ≃ₐ[A] B) A B]
    (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver (IsLocalRing.maximalIdeal A)]
    (hQ : Q ≠ ⊥) (n : ℕ) (hn : IsUnit (n : A))
    (π : A) (hπ : Irreducible π) (γ : B)
    (hγ : γ ^ n = algebraMap A B π) :
    n ∣ finiteIdealTameOrder B (B ≃ₐ[A] B) Q hQ

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