Documentation

TauCeti.Topology.Algebra.Group.Profinite.Demushkin.Basic

Demushkin groups #

A Demushkin group is a pro-p group G whose cohomology with trivial 𝔽_p coefficients looks like that of a closed surface: H¹(G, 𝔽_p) is finite-dimensional, H²(G, 𝔽_p) is one-dimensional, and the cup product H¹(G, 𝔽_p) × H¹(G, 𝔽_p) → H²(G, 𝔽_p) is a nondegenerate pairing (Labute, p. 106). The maximal pro-p quotients of the absolute Galois groups of p-adic fields containing the p-th roots of unity are the motivating examples.

The definition is the predicate IsDemushkin p G, stated against the continuous cohomology cohomFp p G n and the cup product cupFp p G on it. Its first consequences are proved here: a Demushkin group is topologically finitely generated, its rank demushkinRank is the dimension of H¹(G, 𝔽_p), and it is a one-relator pro-p group, presented on demushkinRank generators by a single relator lying in the Frattini subgroup of the free pro-p group, and its rank is positive. A free pro-p group is not Demushkin, since its H²(G, 𝔽_p) vanishes.

Main definitions #

Main results #

References #

source
structure TauCeti.IsDemushkin (p : ℕ) [Fact (Nat.Prime p)] (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
Prop

The Demushkin predicate (Labute, p. 106), for a prime p and a profinite group G: a pro-p group whose H¹(G, 𝔽_p) is finite-dimensional, whose H²(G, 𝔽_p) is one-dimensional, and on which the cup product H¹(G, 𝔽_p) × H¹(G, 𝔽_p) → H²(G, 𝔽_p) is nondegenerate on both sides. The primality and profiniteness of the ambient data are hypotheses of the predicate, so that it is only stated on its mathematical domain, and the pro-p hypothesis is a field, so that no theorem about Demushkin groups applies to a group that satisfies only the cohomological clauses. Finite generation is a consequence, IsDemushkin.isTopologicallyFinitelyGenerated, and is not assumed.

Instances For
    source
    theorem TauCeti.IsDemushkin.isTopologicallyFinitelyGenerated {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
    IsTopologicallyFinitelyGenerated G

    A Demushkin group is topologically finitely generated: its H¹(G, 𝔽_p) is finite-dimensional, and the dimension of H¹(G, 𝔽_p) is the topological generator rank.

    source
    noncomputable def TauCeti.demushkinRank {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
    ℕ

    The rank of a Demushkin group: its topological generator rank, as a natural number. Every numerical statement about a Demushkin group is about this accessor.

    Equations
    Instances For
      source
      theorem TauCeti.demushkinRank_def {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
      demushkinRank hG = topologicalGeneratorRankNat G ⋯

      The rank of a Demushkin group is its topological generator rank.

      source
      theorem TauCeti.demushkinRank_presentedProP {p : ℕ} [Fact (Nat.Prime p)] {X : Type v} [Finite X] {rels : Set (freeProP p X)} (hrels : rels ⊆ ↑(proPFrattini p (freeProP p X))) (hG : IsDemushkin p (presentedProP p X rels)) :
      demushkinRank hG = Nat.card X

      The rank of a presented Demushkin group is the number of generators when the relators lie in the Frattini subgroup: such a presentation is minimal.

      source
      theorem TauCeti.demushkinRank_congr {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hG : IsDemushkin p G) (hH : IsDemushkin p H) (e : G ≃ₜ* H) :
      demushkinRank hG = demushkinRank hH

      The rank of a Demushkin group is an isomorphism invariant.

      source
      theorem TauCeti.IsDemushkin.finrank_cohomFp_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
      Module.finrank (ZMod p) ↑(cohomFp p G 1).toModuleCat = demushkinRank hG

      The rank of a Demushkin group is the dimension of H¹(G, 𝔽_p).

      source
      theorem TauCeti.IsDemushkin.finite_cohomFp_two {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin p G) :
      Finite ↑(cohomFp p G 2).toModuleCat

      H²(G, 𝔽_p) of a Demushkin group is finite, being one-dimensional over 𝔽_p.

      source
      theorem TauCeti.IsDemushkin.exists_mem_proPFrattini_continuousMulEquiv_presentedProP {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (X : Type u) [Finite X] (hX : Nat.card X = demushkinRank hG) :
      ∃ r ∈ proPFrattini p (freeProP p X), Nonempty (presentedProP p X {r} ≃ₜ* G)

      A Demushkin group is a one-relator pro-p group. On any finite type X with demushkinRank hG elements, a Demushkin group G is presented by a single relator r of the free pro-p group on X, and r lies in the Frattini subgroup Φ(F) = closure (Fᵖ [F, F]), so the presentation is minimal: the number of relators of a minimal presentation is the dimension of H²(G, 𝔽_p), which is 1.

      source
      theorem TauCeti.IsDemushkin.exists_mem_proPFrattini_continuousMulEquiv_presentedProP_fin {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
      ∃ r ∈ proPFrattini p (freeProP p (Fin (demushkinRank hG))), Nonempty (presentedProP p (Fin (demushkinRank hG)) {r} ≃ₜ* G)

      A Demushkin group is a one-relator pro-p group on Fin n, n = demushkinRank hG: it is presented by a single relator r ∈ Φ(F) of the free pro-p group on Fin (demushkinRank hG), whatever the universe of G.

      source
      theorem TauCeti.IsDemushkin.demushkinRank_pos {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) :
      0 < demushkinRank hG

      A Demushkin group has positive rank: on an empty generating type the presented group is trivial, and a trivial group has vanishing H²(G, 𝔽_p), which is not one-dimensional.

      source
      theorem TauCeti.IsDemushkin.card_pos_presentedProP {p : ℕ} [Fact (Nat.Prime p)] {X : Type v} [Finite X] {rels : Set (freeProP p X)} (hG : IsDemushkin p (presentedProP p X rels)) :
      0 < Nat.card X

      A presentation of a Demushkin group has at least one generator: the rank of the group is positive and at most the number of generators.

      source
      theorem TauCeti.IsDemushkin.mem_proPFrattini_of_presentedProP_singleton {p : ℕ} [Fact (Nat.Prime p)] {X : Type v} [Finite X] {r : freeProP p X} (hG : IsDemushkin p (presentedProP p X {r})) :
      r ∈ proPFrattini p (freeProP p X)

      A relator presenting a Demushkin group lies in the Frattini subgroup: a one-relator presentation ⟨X ∣ r⟩ of a Demushkin group on a finite type X is minimal. In the count #X + dim H²(G, 𝔽_p) = d(G) + d(R ⧸ Rᵖ[R, F]) of the presentation, H²(G, 𝔽_p) is one-dimensional and the single relator normally generates R, so d(G) ≥ #X, and d(G) ≤ #X always.

      source
      theorem TauCeti.not_isDemushkin_freeProP {p : ℕ} [Fact (Nat.Prime p)] (X : Type u) :
      ¬IsDemushkin p (freeProP p X)

      A free pro-p group is not Demushkin: its H²(F, 𝔽_p) vanishes, so it is not one-dimensional. This covers the trivial group and ℤ_p.