ModuleFiniteIdealTameOrder.lean
Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealTameOrder
5 declarations indexed from sourceView source ↗ Module documentation
Tame and wild orders at an original prime
Defines the finite tame and principal-unit kernel orders and factors the inertia cardinality. Establishes positivity and residue-field invertibility of the tame order.
Declarations
EtaleFundamentalGroups.Inertia.finiteIdealTameOrder
DocumentationThe actual finite tame degree at the original normalization prime. Its local DVR and stabilizer action are constructed from that original prime.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
variable (B : Type u) [CommRing B] [IsDedekindDomain B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
EtaleFundamentalGroups.Inertia.finiteIdealWildOrder
DocumentationThe actual principal-unit kernel order at that same original prime.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
variable (B : Type u) [CommRing B] [IsDedekindDomain B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
EtaleFundamentalGroups.Inertia.finiteIdealInertia_card_eq_tame_mul_wild
DocumentationThe original ideal-inertia order is the product of the actual tame order and actual principal-unit kernel order. No residue field is opened here.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
variable (B : Type u) [CommRing B] [IsDedekindDomain B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
EtaleFundamentalGroups.Inertia.finiteIdealTameOrder_pos
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
variable (B : Type u) [CommRing B] [IsDedekindDomain B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
EtaleFundamentalGroups.Inertia.finiteIdealTameOrder_isUnit
DocumentationThe actual degree at the original prime is invertible in its actual local residue field.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
variable (B : Type u) [CommRing B] [IsDedekindDomain B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)