Inflation from the maximal pro-p quotient

For a profinite group G and a prime p, pullback along the quotient map G → G(p) onto the maximal pro-p quotient identifies degree-one continuous cohomology with trivial 𝔽_p coefficients, and is injective in degree two. These are the low-degree comparison results between a profinite group and its maximal pro-p quotient.

Together these let the low-degree 𝔽_p-cohomology of G(p) be studied through G: classes in H¹(G, 𝔽_p) are exactly the inflations of classes in H¹(G(p), 𝔽_p), and a class in H²(G(p), 𝔽_p) vanishes as soon as its inflation to G does. In particular H²(G(p), 𝔽_p) embeds in H²(G, 𝔽_p), so bounds on the latter bound the former.

Main results

• TauCeti.explicitInfl2_proPKernel_injective: explicit degree-two inflation from G ⧸ R to G, for R the pro-p kernel, is injective for trivial coefficients killed by p.
• TauCeti.inflH1MaximalProP: degree-one inflation from G(p) to G is a linear equivalence.
• TauCeti.inflH2MaximalProP_injective: degree-two inflation from G(p) to G is injective.
• TauCeti.inflH2MaximalProP_surjective_of_map₂_cupFp_eq_top: degree-two inflation from G(p) to G is surjective when H²(G, 𝔽_p) is spanned by cup products of degree-one classes.

References

• J.-P. Serre, Galois Cohomology, Chapter I, §2.6 and §4.3.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, I §1.6.

theorem TauCeti.explicitInfl2_proPKernel_injective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (htriv : ∀ (g : G) (m : M), g • m = m) (hpM : ∀ (m : M), p • m = 0) : Function.Injective ⇑(ContCohomology.explicitInfl2 G M (proPKernel p G))

Explicit degree-two inflation from the maximal pro-p quotient is injective. For the pro-p kernel R and trivial discrete coefficients M killed by p, the explicit inflation H²(G ⧸ R, M ^ R) → H²(G, M) is injective.

noncomputable def TauCeti.inflH1MaximalProP (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ↑(cohomFp p (maximalProPQuotient p G) 1).toModuleCat ≃ₗ[ZMod p] ↑(cohomFp p G 1).toModuleCat

Degree-one inflation from the maximal pro-p quotient. Pullback along G → G(p) identifies H¹(G(p), 𝔽_p) with H¹(G, 𝔽_p).

Equations

• TauCeti.inflH1MaximalProP p G = LinearEquiv.ofBijective ↑(TopModuleCat.Hom.hom (TauCeti.cohomFpMap p (TauCeti.ContinuousMonoidHom.quotientMk (TauCeti.proPKernel p G)) 1)) ⋯

@[simp]

theorem TauCeti.inflH1MaximalProP_apply (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : ↑(cohomFp p (maximalProPQuotient p G) 1).toModuleCat) : (inflH1MaximalProP p G) x = (CategoryTheory.ConcreteCategory.hom (cohomFpMap p (ContinuousMonoidHom.quotientMk (proPKernel p G)) 1)) x

The degree-one equivalence is the usual contravariant cohomology map along G → G(p).

theorem TauCeti.inflH1MaximalProP_apply_eq_infl (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : ↑(cohomFp p (maximalProPQuotient p G) 1).toModuleCat) : (inflH1MaximalProP p G) x = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.infl (proPKernel p G) (trivialFp p G) 1)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (trivialFpQuotientToInvariantsIso p G (proPKernel p G)).hom 1)) x)

After identifying the quotient-invariants coefficient representation with trivial 𝔽_p, the degree-one equivalence is canonical inflation.

theorem TauCeti.inflH2MaximalProP_injective (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (cohomFpMap p (ContinuousMonoidHom.quotientMk (proPKernel p G)) 2))

Degree-two inflation from the maximal pro-p quotient is injective. The inflation map H²(G(p), 𝔽_p) → H²(G, 𝔽_p) is injective.

theorem TauCeti.inflH2MaximalProP_surjective_of_map₂_cupFp_eq_top (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : Submodule.map₂ (cupFp p G) ⊤ ⊤ = ⊤) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (cohomFpMap p (ContinuousMonoidHom.quotientMk (proPKernel p G)) 2))

Degree-two inflation from the maximal pro-p quotient is surjective when H²(G, 𝔽_p) is spanned by cup products. Every class a ⌣ b with a, b ∈ H¹(G, 𝔽_p) is inflated from G(p), since degree-one inflation is bijective and inflation commutes with the cup product.