EtaleFundamentalGroups.Inertia.normalizationQuotientRootsEquiv
The SAME maximal quotient/residue comparison, restricted to roots.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v
attribute [local instance] Ideal.Quotient.fieldLean source · statement
def normalizationQuotientRootsEquiv
(A : Type u) (L : Type v) [CommRing A] [CommRing L] [Algebra A L]
(Q : Ideal (SchemeTheory.normalizationCommAlgCat A L).carrier) [Q.IsMaximal]
(n : ℕ) : (normalizationRootsGroup A L Q n).carrier ≃*
rootsOfUnity n ((SchemeTheory.normalizationCommAlgCat A L).carrier ⧸ Q)