ClassFieldTower.Martinet.Shafarevich.mixedChar_fixingSubgroup_residualAbelianization_conjugation_ne_one
An ambient automorphism outside a prime-degree fixing subgroup acts nontrivially on the abelianization of that subgroup's actual pro-p residual quotient over a complete mixed-characteristic discretely valued base.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Abelian
attribute [local instance] KummerTheory.fixingSubgroup_normal KummerTheory.closureOverIntermediate
-- The only new local instance is finite dimensionality, derived from the degree.
-- Normality and closure-over-intermediate are the existing canonical instances.Lean source · statement
theorem mixedChar_fixingSubgroup_residualAbelianization_conjugation_ne_one
{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)
(g : Gal(Ω/F)) (hg : g ∉ S.fixingSubgroup) :
(TopologicalAbelianization.congr
(residualQuotientConjugationContinuousMulEquiv
(FiniteGroupClass.pGroup_fullFormation p) S.fixingSubgroup
(InfiniteGalois.fixingSubgroup_isClosed S) g)).toMulEquiv ≠ 1