EtaleFundamentalGroups.Inertia.normalizationRootsGroup
The full roots of a fixed degree in the original normalization residue field, retained as its native group object before the field tower appears.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u vLean source · statement
def normalizationRootsGroup
(A : Type u) (L : Type v) [CommRing A] [CommRing L] [Algebra A L]
(Q : Ideal (SchemeTheory.normalizationCommAlgCat A L)) [Q.IsPrime]
(n : ℕ) : GrpCat.{v}