ModuleFiniteIdealTameExactness.lean
Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealTameExactness
4 declarations indexed from sourceView source ↗ Module documentation
Wild kernels of finite ideal tame characters
Transports the principal-unit wild subgroup to original ideal inertia and computes its cardinality. Proves surjectivity and the kernel formula for the finite tame character.
Declarations
EtaleFundamentalGroups.Inertia.finiteIdealWildSubgroup
DocumentationThe actual original finite wild subgroup, transported from the SAME principal-unit kernel along the literal inertia identification.
Source context 6 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
variable (B : Type u) [CommRing B] [IsDedekindDomain B]
(G : Type u) [Group G] [MulSemiringAction G B]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
EtaleFundamentalGroups.Inertia.finiteIdealWildSubgroup_card
DocumentationThe transported wild subgroup has exactly the already computed original wild order.
Source context 6 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
variable (B : Type u) [CommRing B] [IsDedekindDomain B]
(G : Type u) [Group G] [MulSemiringAction G B]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
EtaleFundamentalGroups.Inertia.finiteIdealTameCharacterGroupMap_surjective
DocumentationThe raw actual original finite character is onto its full root group.
Source context 6 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
variable (B : Type u) [CommRing B] [IsDedekindDomain B]
(G : Type u) [Group G] [MulSemiringAction G B]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
EtaleFundamentalGroups.Inertia.finiteIdealTameCharacterGroupMap_ker
DocumentationIts original-domain kernel is precisely that same transported principal-unit subgroup.
Source context 6 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
variable (B : Type u) [CommRing B] [IsDedekindDomain B]
(G : Type u) [Group G] [MulSemiringAction G B]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)