Module

CommAlgIdealTamePrimitiveRoots.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgIdealTamePrimitiveRoots

2 declarations indexed from sourceView source ↗

Module documentation

Primitive roots of native finite tame orders

The actual local inertia-character image supplies a primitive root of the intrinsic tame order. Consequently its full root group is preserved by every residue-field embedding.

Imports5

Imported by3

theorem

commAlgIdealTameOrder_exists_primitiveRoot

L35 ↗

EtaleFundamentalGroups.Inertia.commAlgIdealTameOrder_exists_primitiveRoot

Documentation

The SAME intrinsic finite tame order occurs as a primitive root in the literal residue field of its normalization prime.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
open RamificationTheory.HilbertRamification
universe u v w
variable (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
  [IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
  (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)

Lean source · statement

theorem commAlgIdealTameOrder_exists_primitiveRoot :
    ∃ ζ : Q.ResidueField, IsPrimitiveRoot ζ (commAlgIdealTameOrder A B Q hQ)

theorem

commAlgIdealTameRoots_bijective

L44 ↗

EtaleFundamentalGroups.Inertia.commAlgIdealTameRoots_bijective