ClassFieldTower.Martinet.Shafarevich.mixedChar_openSubgroup_residualAbelianization_faithful
An open normal subgroup of any prime index has faithful quotient conjugation on its abelianized pro-p residual quotient.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Martinet.Shafarevich
open ProCGroups ProCGroups.ProC
attribute [local instance] KummerTheory.fixingSubgroup_normalLean source · statement
theorem mixedChar_openSubgroup_residualAbelianization_faithful
{F Ω : Type*} [Field F] [Field Ω] [Algebra F Ω] [IsAlgClosure F Ω] [CharZero F]
(vF : _root_.Valuation F (WithZero (Multiplicative ℤ)))
[ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vF]
(p : ℕ) [Fact p.Prime]
[hres : CharP (IsLocalRing.ResidueField vF.valuationSubring) p]
(N : Subgroup Gal(Ω/F)) [N.Normal]
(hN : IsOpen (N : Set Gal(Ω/F))) {r : ℕ} [Fact r.Prime]
(hindex : N.index = r) :
Function.Injective
(residualAbelianizationQuotientConjugation
(FiniteGroupClass.pGroup_fullFormation p) N (N.isClosed_of_isOpen hN))