Documentation

TauCeti.Topology.Algebra.Group.Profinite.ProP.H1Dual

The H¹ interpretation for a pro-p group: H¹(G, 𝔽_p) is the continuous 𝔽_p-dual of the #

Frattini quotient #

For a group G with a topology, a prime p, and the trivial G-module 𝔽_p = ZMod p, a class of H¹(G, 𝔽_p) is represented by a continuous 1-cocycle, and with trivial coefficients a continuous 1-cocycle is a continuous character, so TauCeti.ContCohomology.H1EquivOfSmulEqSelf identifies H¹(G, 𝔽_p) with the group of continuous 𝔽_p-valued characters of G. The characteristic fact of this degree is that the 1-coboundaries vanish in it — the character group is what is left over, not a quotient of a larger group of homomorphisms. The ZMod p-module structure that makes this identification an isomorphism of 𝔽_p-vector spaces (TauCeti.instModuleH1, TauCeti.h1EquivContinuousZModDual) needs neither profiniteness nor a pro-p hypothesis, and holds for every modulus n, not only for a prime.

Every continuous 𝔽_p-valued character of G also kills the pro-p Frattini subgroup, so composing the above with precomposition along the projection to the Frattini quotient gives the further identification with the continuous 𝔽_p-dual of G ⧸ Φ(G) (TauCeti.h1EquivFrattiniQuotientDual), whose application lemmas TauCeti.h1EquivFrattiniQuotientDual_apply_mk and TauCeti.h1EquivFrattiniQuotientDual_symm_apply compute it in both directions. This step, too, needs neither profiniteness nor a pro-p hypothesis; what is specific to a pro-p group is the numerical transfer that follows, for which compactness and total disconnectedness are needed.

Here H¹ is the explicit inhomogeneous group TauCeti.ContCohomology.H1 G (ZMod p) = Z¹/B¹, which depends on the action of G on the coefficients, so a statement about it names the action it is made under. The canonical carrier of that same cohomology is TauCeti.cohomFp p G 1, whose coefficients carry the trivial action of G by themselves, so a statement about it names no action of G at all. The identification of the two models of degree one is the existing TauCeti.cohomFpAddEquivH1 of TauCeti.RepresentationTheory.Homological.ContCohomology.TrivialFp.Explicit, which this file does not restate; on the canonical carrier it reads as TauCeti.cohomFpLinearEquivContinuousZModDual, the continuous 𝔽_p-dual of G, and TauCeti.cohomFpEquivFrattiniQuotientDual here is that equivalence followed by the precomposition along the projection to the Frattini quotient. The dimension and finiteness of that carrier are TauCeti.IsProP.rank_cohomFp_one, TauCeti.IsProP.finrank_cohomFp_one and TauCeti.IsProP.finite_cohomFp_one_iff of TauCeti.Topology.Algebra.Group.Profinite.ProP.CohomFp; this file does not restate them.

For a profinite pro-p group, Burnside's basis theorem in cardinal form (TauCeti.IsProP.topologicalGeneratorRank_eq_rank_continuousZModDual) transfers from the continuous dual to H¹, and this is the content of the transfer: the dimension of H¹(G, 𝔽_p) over 𝔽_p is the topological generator rank of G, with no finiteness hypothesis. In particular H¹(G, 𝔽_p) is finite-dimensional exactly when the pro-p group G is topologically finitely generated, which is the finite-dimensionality the two-term Euler formula for an open subgroup U ≤ G needs for the four spaces H⁰ and H¹ of U and G. The count of elements, p ^ d(G) for a topologically finitely generated G and generator rank d, is the existing TauCeti.IsProP.natCard_H1_of_natCard_eq of TauCeti.Topology.Algebra.Group.Profinite.ProP.EulerCharacteristic.Basic, which this file does not restate; on the canonical carrier TauCeti.cohomFp p G 1 it is that theorem read through the existing TauCeti.cohomFpAddEquivH1, so it is not restated on that carrier either.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.h1EquivFrattiniQuotientDual {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) :
ContCohomology.H1 G (ZMod p) ≃ₗ[ZMod p] continuousZModDual p (G ⧸ proPFrattini p G)

H¹(G, 𝔽_p) is the continuous 𝔽_p-dual of the pro-p Frattini quotient. Every continuous 𝔽_p-valued character of G kills the pro-p Frattini subgroup, so the continuous characters of G and those of G ⧸ Φ(G) are the same, and with them their 𝔽_p-module structures.

Instances For
    source
    @[simp]
    theorem TauCeti.h1EquivFrattiniQuotientDual_apply_mk {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (f : ↥(ContCohomology.Z1 G (ZMod p))) (g : G) :
    (Additive.toMul ((h1EquivFrattiniQuotientDual htriv) ↑f)) ↑g = Multiplicative.ofAdd (↑f g)

    The image of a class of H¹(G, 𝔽_p) is the character its cocycle defines on the Frattini quotient: evaluated on the class of g it is the cocycle's value at g.

    source
    @[simp]
    theorem TauCeti.h1EquivFrattiniQuotientDual_symm_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (x : continuousZModDual p (G ⧸ proPFrattini p G)) :
    (h1EquivFrattiniQuotientDual htriv).symm x = ↑((ContCohomology.Z1EquivOfSmulEqSelf htriv).symm (frattiniQuotientDualEquiv x))

    The inverse image of a continuous 𝔽_p-valued character of the Frattini quotient is the class in H¹(G, 𝔽_p) of the continuous 1-cocycle that lifts it to G.

    source
    noncomputable def TauCeti.cohomFpEquivFrattiniQuotientDual {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    ↑(cohomFp p G 1).toModuleCat ≃ₗ[ZMod p] continuousZModDual p (G ⧸ proPFrattini p G)

    TauCeti.cohomFp p G 1 is the continuous 𝔽_p-dual of the pro-p Frattini quotient. This is TauCeti.cohomFpLinearEquivContinuousZModDual of TauCeti.RepresentationTheory.Homological.ContCohomology.TrivialFp.Explicit followed by the precomposition along the projection to the Frattini quotient, and it needs no hypothesis on an action of G: the coefficient object of TauCeti.cohomFp carries the trivial action by construction. It is not a second form of TauCeti.h1EquivFrattiniQuotientDual; the identification of the two models of degree one is the existing TauCeti.cohomFpAddEquivH1, which this file does not restate.

    Instances For
      source
      @[simp]
      theorem TauCeti.cohomFpEquivFrattiniQuotientDual_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : ↑(cohomFp p G 1).toModuleCat) :
      cohomFpEquivFrattiniQuotientDual x = frattiniQuotientDualEquiv.symm ((cohomFpLinearEquivContinuousZModDual p G) x)

      A class of TauCeti.cohomFp p G 1 maps to the character of the Frattini quotient obtained by reading the class, through TauCeti.cohomFpLinearEquivContinuousZModDual, on that quotient.

      source
      @[simp]
      theorem TauCeti.cohomFpEquivFrattiniQuotientDual_symm_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : continuousZModDual p (G ⧸ proPFrattini p G)) :
      cohomFpEquivFrattiniQuotientDual.symm x = (cohomFpLinearEquivContinuousZModDual p G).symm (frattiniQuotientDualEquiv x)

      A continuous 𝔽_p-valued character of the Frattini quotient is read, through TauCeti.frattiniQuotientDualEquiv, as a character of G and then lifted by TauCeti.cohomFpLinearEquivContinuousZModDual to a class of TauCeti.cohomFp p G 1.

      source
      theorem TauCeti.IsProP.rank_H1_eq_topologicalGeneratorRank {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hG : IsProP p G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) :
      Module.rank (ZMod p) (ContCohomology.H1 G (ZMod p)) = topologicalGeneratorRank G

      Burnside's basis theorem for H¹, cardinal form. The dimension of H¹(G, 𝔽_p) over 𝔽_p is the topological generator rank of a profinite pro-p group G, as an identity of cardinals and with no finiteness hypothesis.

      source
      theorem TauCeti.IsProP.finrank_H1_eq_topologicalGeneratorRankNat {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hG : IsProP p G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (hfg : IsTopologicallyFinitelyGenerated G) :
      Module.finrank (ZMod p) (ContCohomology.H1 G (ZMod p)) = topologicalGeneratorRankNat G hfg

      Burnside's basis theorem for H¹, numerical form. The dimension of H¹(G, 𝔽_p) over 𝔽_p is the natural-number topological generator rank of a topologically finitely generated profinite pro-p group.

      source
      theorem TauCeti.IsProP.finite_H1_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hG : IsProP p G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) :
      Module.Finite (ZMod p) (ContCohomology.H1 G (ZMod p)) ↔ IsTopologicallyFinitelyGenerated G

      Finiteness of H¹(G, 𝔽_p). For a profinite pro-p group, H¹(G, 𝔽_p) is finite-dimensional over 𝔽_p exactly when G is topologically finitely generated.