EtaleFundamentalGroups.Inertia.finiteIdealWildOrder_exists_expChar_pow
The order of the same actual principal-unit subgroup of the original normalization-prime action is a power of its own residue exponential characteristic. The intrinsic automorphism order law is constructed before forgetting the coefficient algebra, then applied to the actual subgroup.
Source context 5 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 vLean source · statement
theorem finiteIdealWildOrder_exists_expChar_pow
(A : Type u) (B : Type v)
[rA : CommRing A] [dA : IsDomain A]
[rB : CommRing B] [dB : IsDedekindDomain B]
[aAB : Algebra A B] [finAB : Module.Finite A B] [tfAB : Module.IsTorsionFree A B] :
∀ (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥),
∃ n : ℕ, finiteIdealWildOrder B (B ≃ₐ[A] B) Q hQ =
(ringExpChar Q.ResidueField) ^ n