ClassFieldTower.Martinet.Shafarevich.mixedChar_fixingSubgroup_residualAbelianization_faithful
The actual prime-degree Galois quotient acts faithfully on the abelianization of the fixing subgroup's canonical 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_fixingSubgroup_residualAbelianization_faithful
{F Ω : Type*} [Field F] [Field Ω] [Algebra F Ω] [IsAlgClosure F Ω] [CharZero F]
(S : IntermediateField F Ω) [IsGalois F S]
(vF : _root_.Valuation F (WithZero (Multiplicative ℤ)))
[ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete vF]
(p : ℕ) [Fact p.Prime]
[CharP (IsLocalRing.ResidueField vF.valuationSubring) p]
{r : ℕ} [Fact r.Prime] (hdegree : Module.finrank F S = r) :
Function.Injective
(residualAbelianizationQuotientConjugation
(FiniteGroupClass.pGroup_fullFormation p) S.fixingSubgroup
(InfiniteGalois.fixingSubgroup_isClosed S))