ModuleAbsoluteTameRootsSystem.lean
Nyll.EtaleFundamentalGroups.Inertia.AbsoluteTameRootsSystem
2 declarations indexed from sourceView source ↗ Module documentation
The actual finite-order roots system at the original absolute prime
The index subset is the literal range of the constructed finite-stage tame indices. The coefficients are the original maximal quotient of the absolute normalization. Thus both the index set and the restricted roots system are computed from the original DVR, separable closure and chosen maximal prime.
No cofinality or character comparison is part of the definition; those must be proved from the actual uniformizer-radical stages.
Declarations
EtaleFundamentalGroups.Inertia.actualFiniteTameDegreeSet
DocumentationThe actual finite tame orders, with their constructed invertibility proofs in the original residue field.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory ProCGroups.InverseSystems
universe u v w
attribute [local instance] Ideal.Quotient.field
variable (A : Type u) (K : Type v) (Ω : Type w)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
[Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsGalois K Ω]
(Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]
EtaleFundamentalGroups.Inertia.actualFiniteTameRootsSystem
DocumentationThe actual roots system over finite tame orders at the original absolute normalization prime.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory ProCGroups.InverseSystems
universe u v w
attribute [local instance] Ideal.Quotient.field
variable (A : Type u) (K : Type v) (Ω : Type w)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Field Ω] [Algebra A K] [IsFractionRing A K]
[Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] [IsGalois K Ω]
(Q : Ideal (normalizationCommAlgCat A Ω)) [Q.IsMaximal]