Yamaguchi26AbfaithfulGalois.residueZero_openNormal_prime_index_faithful
The prime-index quotient action is faithful over a residue-zero Henselian DVF whenever the residue group is ab-faithful and its finite extensions have finite primary root groups.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ValuationTheory.DiscreteValuationField
open ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
open RamificationTheory.HilbertRamification.ValuationSubring
attribute [local instance] KummerTheory.fixingSubgroup_normal
universe u vLean source · statement
theorem residueZero_openNormal_prime_index_faithful
{K Ω : Type u} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω] [CharZero K]
(D : HenselianDVF.{u, v} K) [CharZero D.residueField]
(hres : IsAbFaithful Gal(AlgebraicClosure D.residueField/D.residueField))
(hroots : ∀ (E : Type u) [Field E] [Algebra D.residueField E]
[FiniteDimensional D.residueField E] (p : ℕ), p.Prime →
Finite (CommGroup.primaryComponent Eˣ p))
(N : OpenNormalSubgroup Gal(Ω/K))
(hprime : (N : Subgroup Gal(Ω/K)).index.Prime) :
Function.Injective (quotientConjugationTopologicalAbelianizationMap
(N : Subgroup Gal(Ω/K)))