The pro-p class module of an open normal subgroup

For a normal subgroup V of a topological group G, this file defines the maximal pro-p quotient V^ab(p) of the topological abelianization of V. Conjugation induces a continuous action of G ⧸ V on this quotient. If V is open, the defect

q.out * r.out * (q * r).out⁻¹

of the representatives chosen by Quotient.out defines a continuous 2-cocycle with values in V^ab(p), and hence a canonical class u_{G/V}(p) ∈ H²(G ⧸ V, V^ab(p)).

The openness assumption is used only for continuity of the factor set: the quotient G ⧸ V is discrete. The cocycle identity itself is the associativity identity for the chosen representatives, after passing to the abelianization.

Main definitions

• TauCeti.abelianizationProP: the maximal pro-p quotient V^ab(p).
• TauCeti.abelianizationProPMk: the canonical map V → V^ab(p).
• TauCeti.abelianizationProPFactorSet: the factor set defined by Quotient.out.
• TauCeti.abelianizationProPClass: its class in continuous H².

Main results

• TauCeti.abelianizationProPMk_apply: the canonical map is the composite of the two quotient maps.
• TauCeti.continuous_abelianizationProPMk: the canonical map is continuous.
• TauCeti.abelianizationProPMk_conj: the canonical map is equivariant for conjugation.
• TauCeti.abelianizationProPFactorSet_mem_Z2: the factor set is a continuous 2-cocycle when V is open.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., Proposition (3.6.2).

@[reducible, inline]

abbrev TauCeti.abelianizationProP (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) : Type u

The maximal pro-p quotient V^ab(p) of the topological abelianization of V.

noncomputable def TauCeti.abelianizationProPMk (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) : ↥V →* abelianizationProP p G V

The quotient map V → V^ab(p), through the topological abelianization of V.

theorem TauCeti.abelianizationProPMk_apply (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) (v : ↥V) : (abelianizationProPMk p G V) v = (maximalProPQuotient.mk p (TopologicalAbelianization ↥V)) ↑v

The quotient map V → V^ab(p) sends v to the class in the maximal pro-p quotient of its class in the topological abelianization.

theorem TauCeti.abelianizationProPMk_surjective (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) : Function.Surjective ⇑(abelianizationProPMk p G V)

Every element of V^ab(p) is represented by an element of V.

theorem TauCeti.continuous_abelianizationProPMk (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) : Continuous ⇑(abelianizationProPMk p G V)

The quotient map V → V^ab(p) is continuous.

instance TauCeti.abelianizationProPQuotientAction (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] : MulAction.QuotientAction (G ⧸ V) (proPKernel p (TopologicalAbelianization ↥V))

The pro-p kernel of V^ab is stable under conjugation by G ⧸ V.

@[instance_reducible]

noncomputable instance TauCeti.abelianizationProPAction (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] : MulDistribMulAction (G ⧸ V) (abelianizationProP p G V)

Conjugation by G ⧸ V on V^ab descends to V^ab(p).

@[simp]

theorem TauCeti.abelianizationProPMk_conj (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (g : G) (v : ↥V) : ↑g • (abelianizationProPMk p G V) v = (abelianizationProPMk p G V) ((MulAut.conjNormal g) v)

The quotient map V → V^ab(p) intertwines conjugation by g : G with the action of the class of g in G ⧸ V.

instance TauCeti.abelianizationProP_continuousSMul (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] : ContinuousSMul (G ⧸ V) (abelianizationProP p G V)

The action of G ⧸ V on V^ab(p) is jointly continuous.

noncomputable def TauCeti.abelianizationProPFactorSet (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] : (G ⧸ V) × G ⧸ V → Additive (abelianizationProP p G V)

The factor set of the extension of G ⧸ V by V^ab(p), written additively. It sends (q, r) to the class of q.out * r.out * (q * r).out⁻¹.

@[simp]

theorem TauCeti.abelianizationProPFactorSet_apply (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (q r : G ⧸ V) : abelianizationProPFactorSet p G V (q, r) = Additive.ofMul ((abelianizationProPMk p G V) ⟨Quotient.out q * Quotient.out r * (Quotient.out (q * r))⁻¹, ⋯⟩)

The factor set evaluates to the class of the defect of the chosen representatives.

theorem TauCeti.abelianizationProPFactorSet_mem_Z2 (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (hV : IsOpen ↑V) : abelianizationProPFactorSet p G V ∈ ContCohomology.Z2 (G ⧸ V) (Additive (abelianizationProP p G V))

For open normal V, the factor set is a continuous 2-cocycle of G ⧸ V with values in V^ab(p).

noncomputable def TauCeti.abelianizationProPClass (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (hV : IsOpen ↑V) : ContCohomology.H2 (G ⧸ V) (Additive (abelianizationProP p G V))

The canonical class u_{G/V}(p) ∈ H²(G ⧸ V, V^ab(p)) of an open normal subgroup.

theorem TauCeti.abelianizationProPClass_def (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] (hV : IsOpen ↑V) : abelianizationProPClass p G V hV = (ContCohomology.H2pi (G ⧸ V) (Additive (abelianizationProP p G V))) ⟨abelianizationProPFactorSet p G V, ⋯⟩

The class u_{G/V}(p) is the image of the factor-set cocycle under the class map.