ModuleActualFiniteTameIndex.lean
Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteTameIndex
3 declarations indexed from sourceView source ↗ Module documentation
Finite tame degrees as roots-system indices
Proves positivity and base-ring invertibility of the finite tame degree, and uses them to construct an index of the canonical roots system.
Declarations
EtaleFundamentalGroups.Inertia.actualFiniteStageTameOrder_pos
DocumentationPositivity of the degree at the original chosen prime.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
(Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal]
EtaleFundamentalGroups.Inertia.actualFiniteStageTameOrder_isUnit
DocumentationInvertibility of that actual degree in the original DVR.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
(Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal]
EtaleFundamentalGroups.Inertia.actualFiniteStageTameIndex
DocumentationThe actual finite tame degree as an index of the canonical base-residue roots system. Its invertibility has been proved from the original data.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[Field K] [Field L] [Algebra A K] [IsFractionRing A K]
[Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
(Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal]