The classification of Demushkin… to The necessity half of the…

TheoremThe classification of Demushkin groups (Labute)#

two Demushkin groups are topologically isomorphic if and only if they have the same rank and their canonical characters have the same image. The forward direction is the invariance of both invariants under isomorphism; the converse is TauCeti.IsDemushkin.nonempty_continuousMulEquiv_of_range_demushkinCharacter_eq.

TauCeti.IsDemushkin.nonempty_continuousMulEquiv_iff.{u, v} {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 : TauCeti.IsDemushkin p G)
  (hH : TauCeti.IsDemushkin p H) :
  Nonempty (G ≃ₜ* H) ↔
    TauCeti.demushkinRank hG = TauCeti.demushkinRank hH ∧
      (TauCeti.demushkinCharacter hG).range = (TauCeti.demushkinCharacter hH).range
Lean

Formalized in Tau Ceti as TauCeti.IsDemushkin.nonempty_continuousMulEquiv_iff.

Sources
LeanTauCeti.IsDemushkin.nonempty_continuousMulEquiv_iff
Uses 6 · Used by 1
Statement usesThe Demushkin predicate
Proof usesBurnside's basis theorem, cardinal form · The first isomorphism theorem for a surjective strict homomorphism of topological groups · Labute's criterion · Labute's Theorem 2 · Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property
Used byThe isomorphism type of an open subgroup of a Demushkin group

TheoremUniqueness of the dyadic Demushkin groups of even rank with image {±1} × U^(f) (Labute, Theorem 6)#

Two Demushkin groups at p = 2 of the same even rank n ≥ 4 whose canonical characters have the same image V^(f) = {±1} × U^(f), f ≥ 2 finite, are topologically isomorphic.

TauCeti.IsDemushkin.nonempty_continuousMulEquiv_of_even_demushkinRank_of_range_eq_unitsPlusMinus.{u,
    v}
  {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 : TauCeti.IsDemushkin 2 G)
  (hH : TauCeti.IsDemushkin 2 H) (hn : TauCeti.demushkinRank hG = TauCeti.demushkinRank hH)
  (heven : Even (TauCeti.demushkinRank hG)) (hn3 : 3 < TauCeti.demushkinRank hG) {f : ℕ}
  (hf : 2 ≤ f) (hA : (TauCeti.demushkinCharacter hG).range = TauCeti.unitsPlusMinus f)
  (hB : (TauCeti.demushkinCharacter hH).range = TauCeti.unitsPlusMinus f) : Nonempty (G ≃ₜ* H)
Lean

Formalized in Tau Ceti as TauCeti.IsDemushkin.nonempty_continuousMulEquiv_of_even_demushkinRank_of_range_eq_unitsPlusMinus.

Sources
LeanTauCeti.IsDemushkin.nonempty_continuousMulEquiv_of_even_demushkinRank_of_range_eq_unitsPlusMinus
Uses 10
Statement usesThe Demushkin predicate
Proof usesThe abelianization structure theorem for one-relator pro-p groups · Burnside's basis theorem, cardinal form · The constrained successive-approximation theorem · Dedekind's modular law · The first isomorphism theorem for a surjective strict homomorphism of topological groups · Labute's criterion · Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property · The relative successive-approximation theorem · The successive-approximation theorem with tails

TheoremTate's theorem: an infinite Demushkin group has p-cohomological dimension exactly 2#

The lower bound is H²(G, 𝔽_p) ≠ 0; the upper bound is the right exactness of H² on the finite 𝔽_p[G]-modules, which Tate's perfect duality provides.

TauCeti.IsDemushkin.cohomologicalDimensionAt_eq_two.{u} {p : ℕ} [Fact (Nat.Prime p)] {G : Type u}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] [Infinite G] (hG : TauCeti.IsDemushkin p G) :
  TauCeti.cohomologicalDimensionAt p G = 2
Lean

Formalized in Tau Ceti as TauCeti.IsDemushkin.cohomologicalDimensionAt_eq_two.

Sources
LeanTauCeti.IsDemushkin.cohomologicalDimensionAt_eq_two
Uses 2 · Used by 2
Statement usesThe Demushkin predicate
Proof usesTate's duality criterion for cd_p G ≤ 2
Used byTate's duality map α₁ of an infinite Demushkin group with coefficients I(χ)/pⁱ is bijective on every finite discrete G-module M killed by pⁱ · The isomorphism type of an open subgroup of a Demushkin group

TheoremTate's duality map α₁ of an infinite Demushkin group with coefficients I(χ)/pⁱ is bijective on every finite discrete G-module M killed by pⁱ#

H¹(G, M) × H¹(G, Hom(M, I(χ)/pⁱ)) → H²(G, I(χ)/pⁱ) is a perfect pairing.

TauCeti.IsDemushkin.dualityMap1_zModTwist_bijective.{u} {p : ℕ} [Fact (Nat.Prime p)] {G : Type u}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] [Infinite G] (hG : TauCeti.IsDemushkin p G) (i : ℕ) (M : Type u)
  [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M]
  [ContinuousSMul G M] [Finite M] (hM : ∀ (x : M), p ^ i • x = 0) :
  Function.Bijective
    ⇑(TauCeti.ContCohomology.dualityMap1 G M (TauCeti.ZModTwist (TauCeti.demushkinCharacter hG) i))
Lean

Formalized in Tau Ceti as TauCeti.IsDemushkin.dualityMap1_zModTwist_bijective.

Sources
LeanTauCeti.IsDemushkin.dualityMap1_zModTwist_bijective
Uses 3
Statement usesThe Demushkin predicate
Proof usesLabute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property · Tate's theorem: an infinite Demushkin group has p-cohomological dimension exactly 2

TheoremAn open subgroup of an infinite Demushkin group is Demushkin (Serre's exposé, §9.2)#

The subgroup is pro-p and topologically finitely generated with G; its H²(U, 𝔽_p) is one-dimensional by TauCeti.IsDemushkin.finrank_cohomFp_two_openSubgroup; and its cup product is nondegenerate because a nonzero class of H¹(U, 𝔽_p) ≅ H¹(G, Coind_U^G 𝔽_p) is paired nontrivially by Tate's duality map α₁ of G, a pairing which is the corestriction of a cup product of U.

TauCeti.IsDemushkin.openSubgroup.{u} {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
  [Infinite G] (hG : TauCeti.IsDemushkin p G) (U : OpenSubgroup G) : TauCeti.IsDemushkin p ↥↑U
Lean

Formalized in Tau Ceti as TauCeti.IsDemushkin.openSubgroup.

Sources
LeanTauCeti.IsDemushkin.openSubgroup
Uses 3 · Used by 1
Statement usesThe Demushkin predicate
Proof usesBurnside's basis theorem, cardinal form · Shapiro's lemma in degree one
Used byThe isomorphism type of an open subgroup of a Demushkin group

TheoremThe isomorphism type of an open subgroup of a Demushkin group#

an open subgroup U of an infinite Demushkin group G is topologically isomorphic to a Demushkin group H if and only if H has rank 2 + [G : U] (n(G) - 2) and the canonical character of H has image χ(U), where χ is the canonical character of G.

TauCeti.IsDemushkin.nonempty_continuousMulEquiv_openSubgroup_iff.{u, v} {p : ℕ} [Fact (Nat.Prime p)]
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] [Infinite G] (hG : TauCeti.IsDemushkin p G) (U : OpenSubgroup G)
  {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H]
  [TotallyDisconnectedSpace H] (hH : TauCeti.IsDemushkin p H) :
  Nonempty (↥↑U ≃ₜ* H) ↔
    TauCeti.demushkinRank hH = 2 + (↑U).index * (TauCeti.demushkinRank hG - 2) ∧
      (TauCeti.demushkinCharacter hH).range =
        Subgroup.map (TauCeti.demushkinCharacter hG).toMonoidHom ↑U
Lean

Formalized in Tau Ceti as TauCeti.IsDemushkin.nonempty_continuousMulEquiv_openSubgroup_iff.

Sources
LeanTauCeti.IsDemushkin.nonempty_continuousMulEquiv_openSubgroup_iff
Uses 11
Statement usesThe Demushkin predicate
Proof usesThe abelianization structure theorem for one-relator pro-p groups · An open subgroup of an infinite Demushkin group is Demushkin (Serre's exposé, §9.2) · Burnside's basis theorem, cardinal form · The classification of Demushkin groups (Labute) · The first isomorphism theorem for a surjective strict homomorphism of topological groups · Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property · Shapiro's lemma in degree one · Tate's duality criterion for cd_p G ≤ 2 · Tate's theorem: an infinite Demushkin group has p-cohomological dimension exactly 2 · The three-term Euler formula

TheoremSerre's theorem at arbitrary rank, as an equivalence#

A pro-p group G has cd_p G ≤ 1 if and only if it is free pro-p on a pointed profinite space: some subset s of G converging to 1 has a presentation F_p(insert 1 s, 1) → G that is a topological isomorphism.

TauCeti.IsProP.cohomologicalDimensionAt_le_one_iff_exists_convergesToOne_continuousMulEquiv_presentation.{u}
  {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G) :
  TauCeti.cohomologicalDimensionAt p G ≤ 1 ↔
    ∃ s, TauCeti.ConvergesToOne s ∧ ∃ e, ⇑e = ⇑(hG.presentation s)
Lean

Formalized in Tau Ceti as TauCeti.IsProP.cohomologicalDimensionAt_le_one_iff_exists_convergesToOne_continuousMulEquiv_presentation.

Other forms

Serre's theorem. Formalized in Tau Ceti as TauCeti.IsProP.nonempty_continuousMulEquiv_freeProP_of_cohomologicalDimensionAt_le_one.

TauCeti.IsProP.nonempty_continuousMulEquiv_freeProP_of_cohomologicalDimensionAt_le_one.{u} {p : ℕ}
  [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G)
  (hcd : TauCeti.cohomologicalDimensionAt p G ≤ 1) (X : Type u) [Finite X]
  (hX : Nat.card X = TauCeti.topologicalGeneratorRankNat G hfg) :
  Nonempty (G ≃ₜ* TauCeti.freeProP p X)

Serre's theorem at arbitrary rank. Formalized in Tau Ceti as TauCeti.IsProP.exists_convergesToOne_continuousMulEquiv_presentation_of_cohomologicalDimensionAt_le_one.

TauCeti.IsProP.exists_convergesToOne_continuousMulEquiv_presentation_of_cohomologicalDimensionAt_le_one.{u}
  {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G)
  (hcd : TauCeti.cohomologicalDimensionAt p G ≤ 1) :
  ∃ s, TauCeti.ConvergesToOne s ∧ ∃ e, ⇑e = ⇑(hG.presentation s)
Sources
LeanTauCeti.IsProP.cohomologicalDimensionAt_le_one_iff_exists_convergesToOne_continuousMulEquiv_presentation · TauCeti.IsProP.nonempty_continuousMulEquiv_freeProP_of_cohomologicalDimensionAt_le_one · TauCeti.IsProP.exists_convergesToOne_continuousMulEquiv_presentation_of_cohomologicalDimensionAt_le_one
Uses 4 · Used by 2
Proof usesBurnside's basis theorem, cardinal form · Dimension shifting in every positive degree · The first isomorphism theorem for a surjective strict homomorphism of topological groups · The Frattini criterion for a kernel
Used byShafarevich's theorem · The pro-p Nielsen–Schreier theorem

TheoremThe Golod–Shafarevich inequality#

A nontrivial finite p-group G, with the discrete topology, satisfies d(G)² < 4 r(G), where d(G) is its generator rank and r(G) = dim_{𝔽_p} H²(G, 𝔽_p) is its relation rank. Finite generation follows from TauCeti.isTopologicallyFinitelyGenerated_of_fg.

IsPGroup.sq_topologicalGeneratorRankNat_lt_four_mul_finrank_cohomFp_two.{u} {p : ℕ}
  [Fact (Nat.Prime p)] {G : Type u} [Group G] [Finite G] [Nontrivial G] [TopologicalSpace G]
  [DiscreteTopology G] (hG : IsPGroup p G) :
  TauCeti.topologicalGeneratorRankNat G ⋯ ^ 2 <
    4 * Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 2).toModuleCat
Lean

Formalized in Tau Ceti as IsPGroup.sq_topologicalGeneratorRankNat_lt_four_mul_finrank_cohomFp_two.

Sources
LeanIsPGroup.sq_topologicalGeneratorRankNat_lt_four_mul_finrank_cohomFp_two
Uses 3
Proof usesBurnside's basis theorem, cardinal form · The first isomorphism theorem for a surjective strict homomorphism of topological groups · The Golod–Shafarevich inequality for finite-dimensional algebras

StructureThe Demushkin predicate#

The Demushkin predicate (Labute, p. 106), for a prime p and a topological 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 of p is a hypothesis of the predicate. Profiniteness is not: no field mentions CompactSpace G or TotallyDisconnectedSpace G, so Lean leaves those section instances out of the structure, and the predicate is also defined for topological groups that are not profinite. The presentation results below assume both; on profinite groups, its intended mathematical domain, this is Labute's notion. 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.

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

Formalized in Tau Ceti as TauCeti.IsDemushkin.

Sources
LeanTauCeti.IsDemushkin
Used by 21
Used byDemushkin's theorem · The marked presentation of G_{ℚ₂}(2) · The marked presentation of G_{ℚ₂(√-2)}(2) · Labute's Theorem 2 at the even-rank dyadic endpoint · Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property · The abelianization structure theorem for one-relator pro-p groups · The existence theorem of the classification for odd rank, as an equivalence (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2) · The existence theorem of the classification of Demushkin groups for even rank, as an equivalence (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2) · An open subgroup of an infinite Demushkin group is Demushkin (Serre's exposé, §9.2) · Labute's criterion · Labute's Theorem 2 · Labute's Theorem 2 for odd rank · Labute's Theorem 2 for q ≠ 2 · Tate's duality map α₁ of an infinite Demushkin group with coefficients I(χ)/pⁱ is bijective on every finite discrete G-module M killed by pⁱ · Tate's theorem: an infinite Demushkin group has p-cohomological dimension exactly 2 · The classification of Demushkin groups (Labute) · The existence theorem of the classification for q ≠ 2, as an equivalence (Labute, Theorem 1 and Remark 2; Demushkin and Serre) · The existence theorem of the classification of Demushkin groups, rank one (Labute, Remark 2 (iii); NSW (3.9.10)) · The isomorphism type of an open subgroup of a Demushkin group · The necessity half of the existence theorem for q ≠ 2 (Labute, Theorem 1) · Uniqueness of the dyadic Demushkin groups of even rank with image {±1} × U^(f) (Labute, Theorem 6)

TheoremThe unconstrained successive-approximation theorem#

Let r, w ∈ λ_1(F) be relators of the free pro-p group F on a finite linearly ordered type with the same class ρ ∈ gr_1(F), and suppose the basis-modification map δ_ρ is onto gr_{m+1}(F) for every m ≥ 1. Then a continuous automorphism of F carries r to w.

TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_basisModificationDelta_eq_top.{u}
  {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] [LinearOrder X]
  (r w : ↥(TauCeti.pLowerCentralSeries p (TauCeti.freeProP p X) 1))
  (h :
    TauCeti.gradedMk p (TauCeti.freeProP p X) 1 r = TauCeti.gradedMk p (TauCeti.freeProP p X) 1 w)
  (hspan :
    ∀ (m : ℕ) (hm : 1 ≤ m),
      ((TauCeti.freeProP.basisModificationDelta p X hm)
            (TauCeti.gradedMk p (TauCeti.freeProP p X) 1 r)).range =
        ⊤) :
  ∃ e, e ↑r = ↑w
Lean

Formalized in Tau Ceti as TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_basisModificationDelta_eq_top.

Sources
LeanTauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_basisModificationDelta_eq_top
Uses 1 · Used by 1
Proof usesThe constrained successive-approximation theorem
Used byLabute's Theorem 2 for q ≠ 2

DefinitionTauCeti.profiniteFrattini#

The Frattini subgroup Φ(G) of a topological group: the intersection of its maximal open subgroups. For a profinite group this is the Frattini subgroup of Ribes–Zalesskii; with the discrete topology it is Mathlib's frattini (TauCeti.profiniteFrattini_eq_frattini).

TauCeti.profiniteFrattini.{u} (G : Type u) [Group G] [TopologicalSpace G] : Subgroup G
Lean

Formalized in Tau Ceti as TauCeti.profiniteFrattini.

Sources
LeanTauCeti.profiniteFrattini
Used by 4
Used byTauCeti.Peripheral.peripheralAut_eq_top_rank_one · Generation modulo the Frattini subgroup · The continuous automorphisms of a pro-p group acting trivially on its Frattini quotient form a pro-p group · The kernel on the Frattini quotient is the inverse limit of the finite kernels

TheoremGeneration modulo the Frattini subgroup#

A set topologically generates a profinite group if and only if its image topologically generates the quotient by the Frattini subgroup.

TauCeti.topologicalClosure_closure_eq_top_iff_quotient_profiniteFrattini.{u} {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
  (s : Set G) :
  (Subgroup.closure s).topologicalClosure = ⊤ ↔
    (Subgroup.closure
          (⇑(QuotientGroup.mk' (TauCeti.profiniteFrattini G)) '' s)).topologicalClosure =
      ⊤
Lean

Formalized in Tau Ceti as TauCeti.topologicalClosure_closure_eq_top_iff_quotient_profiniteFrattini.

Sources
LeanTauCeti.topologicalClosure_closure_eq_top_iff_quotient_profiniteFrattini
Uses 1
Statement usesTauCeti.profiniteFrattini

TheoremThe constrained successive-approximation theorem#

Let r, w ∈ λ_1(F) be relators of the free pro-p group F on a finite linearly ordered type with the same class ρ ∈ gr_1(F), let Z ⊆ F and let C : X → Subgroup F be closed admissible corrections, with every admissible basis modification θ_ω, ω : X → λ_1(F) with ω_i ∈ C i for every i, preserving each C i, and every admissible endomorphism φ of F, one with x_i⁻¹ * φ(x_i) ∈ C i for every i, congruent to the identity modulo λ_1(F) having its deviation (φ r)⁻¹ * w in Z. Suppose that for every m ≥ 1 each element of λ_{m+1}(F) lying in Z has class δ_ρ(⟦ω⟧) for a family ω : X → λ_m(F) with ω_i ∈ C i for every i. Then an admissible continuous automorphism of F carries r to w.

The admissibility of the automorphism is the limit of the admissibility of the finite approximations, which needs the C i closed. The constrained span statement is the hypothesis a normal-form argument has to establish; it is assumed here. Taking Z = F and C i = F recovers the unconstrained theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_basisModificationDelta_eq_top.

TauCeti.freeProP.exists_continuousMulEquiv_apply_eq.{u} {p : ℕ} [Fact (Nat.Prime p)] {X : Type u}
  [Finite X] [LinearOrder X] (Z : Set (TauCeti.freeProP p X))
  (C : X → Subgroup (TauCeti.freeProP p X)) (hclosed : ∀ (i : X), IsClosed ↑(C i))
  (hC :
    ∀ (ω : X → ↥(TauCeti.pLowerCentralSeries p (TauCeti.freeProP p X) 1)),
      (∀ (i : X), ↑(ω i) ∈ C i) →
        ∀ (i : X), ∀ c ∈ C i, (TauCeti.freeProP.basisModification ω) c ∈ C i)
  (r w : ↥(TauCeti.pLowerCentralSeries p (TauCeti.freeProP p X) 1))
  (h :
    TauCeti.gradedMk p (TauCeti.freeProP p X) 1 r = TauCeti.gradedMk p (TauCeti.freeProP p X) 1 w)
  (hZ :
    ∀ (φ : TauCeti.freeProP p X →ₜ* TauCeti.freeProP p X),
      (∀ (g : TauCeti.freeProP p X),
          g⁻¹ * φ g ∈ TauCeti.pLowerCentralSeries p (TauCeti.freeProP p X) 1) →
        (∀ (i : X), (TauCeti.freeProP.of i)⁻¹ * φ (TauCeti.freeProP.of i) ∈ C i) →
          (φ ↑r)⁻¹ * ↑w ∈ Z)
  (hspan :
    ∀ (m : ℕ) (hm : 1 ≤ m) (z : ↥(TauCeti.pLowerCentralSeries p (TauCeti.freeProP p X) (m + 1))),
      ↑z ∈ Z →
        ∃ ω,
          (∀ (i : X), ↑(ω i) ∈ C i) ∧
            (((TauCeti.freeProP.basisModificationDelta p X hm)
                  (TauCeti.gradedMk p (TauCeti.freeProP p X) 1 r))
                fun i => TauCeti.gradedMk p (TauCeti.freeProP p X) m (ω i)) =
              TauCeti.gradedMk p (TauCeti.freeProP p X) (m + 1) z) :
  ∃ e, (∀ (i : X), (TauCeti.freeProP.of i)⁻¹ * e (TauCeti.freeProP.of i) ∈ C i) ∧ e ↑r = ↑w
Lean

Formalized in Tau Ceti as TauCeti.freeProP.exists_continuousMulEquiv_apply_eq.

Sources
LeanTauCeti.freeProP.exists_continuousMulEquiv_apply_eq
Uses 1 · Used by 5
Proof usesBurnside's criterion modulo λ_1
Used byThe marked presentation of G_{ℚ₂(√-2)}(2) · Labute's Theorem 2 · The unconstrained successive-approximation theorem · Uniqueness of the dyadic Demushkin groups of even rank with image {±1} × U^(f) (Labute, Theorem 6) · The relative successive-approximation theorem

TheoremThe existence theorem of the classification for q ≠ 2, as an equivalence (Labute, Theorem 1 and Remark 2; Demushkin and Serre)#

Let A ≤ ℤ_pˣ be a closed pro-p subgroup, contained in 1 + 4ℤ_2 when p = 2; these are the possible images of the canonical characters of the Demushkin groups with q ≠ 2 (TauCeti.demushkinQ_ne_two_iff_range_demushkinCharacter_le). Then (n, A) is the pair of invariants of a Demushkin group, presented on n generators by one relator, exactly when n is even and (A : A^p) < p ^ n. Together with TauCeti.IsDemushkin.nonempty_continuousMulEquiv_of_range_demushkinCharacter_eq, this classifies the Demushkin groups with q ≠ 2 by their rank and the image of their canonical character.

TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ}
  {A : Subgroup ℤ_[p]ˣ} (hA : IsClosed ↑A) (hAp : TauCeti.IsProP p ↥A)
  (hA₂ : p = 2 → A ≤ TauCeti.unitsPrincipal p 2) :
  (∃ r,
      ∃ (hG : TauCeti.IsDemushkin p (TauCeti.presentedProP p (Fin n) {r})),
        TauCeti.demushkinRank hG = n ∧ (TauCeti.demushkinCharacter hG).range = A) ↔
    Even n ∧
      ((Subgroup.map (powMonoidHom p) A).subgroupOf A).profiniteIndex <
        TauCeti.Supernatural.primePower ⟨p, ⋯⟩ ↑n
Lean

Formalized in Tau Ceti as TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff.

Sources
LeanTauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff
Uses 7
Statement usesThe Demushkin predicate
Proof usesThe abelianization structure theorem for one-relator pro-p groups · Burnside's basis theorem, cardinal form · The existence theorem of the classification of Demushkin groups, rank one (Labute, Remark 2 (iii); NSW (3.9.10)) · The first isomorphism theorem for a surjective strict homomorphism of topological groups · Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property · The necessity half of the existence theorem for q ≠ 2 (Labute, Theorem 1)

TheoremThe existence theorem of the classification of Demushkin groups, rank one (Labute, Remark 2 (iii); NSW (3.9.10))#

There is a Demushkin group of rank 1, presented on one generator by the single relator x₁², namely ℤ/2, which has exactly one continuous character with the prescription property, and that character has image {±1}. This is the instance n = 1 of the odd-rank statement at level f = ∞, whose relator word reads x₁² at rank one.

TauCeti.exists_isDemushkin_one_range_eq_zpowers_neg_one :
  ∃ r,
    ∃ (hG : TauCeti.IsDemushkin 2 (TauCeti.presentedProP 2 (Fin 1) {r})),
      TauCeti.demushkinRank hG = 1 ∧
        (∃! χ, TauCeti.HasPrescriptionProperty χ) ∧
          ∀ (χ : TauCeti.presentedProP 2 (Fin 1) {r} →ₜ* ℤ_[2]ˣ),
            TauCeti.HasPrescriptionProperty χ → χ.range = Subgroup.zpowers (-1)
Lean

Formalized in Tau Ceti as TauCeti.exists_isDemushkin_one_range_eq_zpowers_neg_one.

Other forms

The existence theorem of the classification of Demushkin groups, even rank (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2). Formalized in Tau Ceti as TauCeti.exists_isDemushkin_range_eq_of_even_of_lt.

TauCeti.exists_isDemushkin_range_eq_of_even_of_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ}
  {A : Subgroup ℤ_[p]ˣ} (hA : IsClosed ↑A) (hAp : TauCeti.IsProP p ↥A) (hn : Even n)
  (hlt :
    ((Subgroup.map (powMonoidHom p) A).subgroupOf A).profiniteIndex <
      TauCeti.Supernatural.primePower ⟨p, ⋯⟩ ↑n) :
  ∃ r,
    ∃ (hG : TauCeti.IsDemushkin p (TauCeti.presentedProP p (Fin n) {r})),
      TauCeti.demushkinRank hG = n ∧
        (∃! χ, TauCeti.HasPrescriptionProperty χ) ∧
          ∀ (χ : TauCeti.presentedProP p (Fin n) {r} →ₜ* ℤ_[p]ˣ),
            TauCeti.HasPrescriptionProperty χ → χ.range = A

The existence theorem of the classification of Demushkin groups, odd rank n ≥ 3 (Labute, Theorem 1; Serre, Theorem 3.2). Formalized in Tau Ceti as TauCeti.exists_isDemushkin_range_eq_unitsPlusMinus_of_odd.

TauCeti.exists_isDemushkin_range_eq_unitsPlusMinus_of_odd {n : ℕ} (hn : Odd n) (hn₃ : 3 ≤ n) {f : ℕ}
  (hf : 2 ≤ f) :
  ∃ r,
    ∃ (hG : TauCeti.IsDemushkin 2 (TauCeti.presentedProP 2 (Fin n) {r})),
      TauCeti.demushkinRank hG = n ∧
        (∃! χ, TauCeti.HasPrescriptionProperty χ) ∧
          ∀ (χ : TauCeti.presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ),
            TauCeti.HasPrescriptionProperty χ → χ.range = TauCeti.unitsPlusMinus f

The existence theorem of the classification of Demushkin groups, odd rank at level f = ∞ (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2). Formalized in Tau Ceti as TauCeti.exists_isDemushkin_range_eq_zpowers_neg_one_of_odd.

TauCeti.exists_isDemushkin_range_eq_zpowers_neg_one_of_odd {n : ℕ} (hn : Odd n) :
  ∃ r,
    ∃ (hG : TauCeti.IsDemushkin 2 (TauCeti.presentedProP 2 (Fin n) {r})),
      TauCeti.demushkinRank hG = n ∧
        (∃! χ, TauCeti.HasPrescriptionProperty χ) ∧
          ∀ (χ : TauCeti.presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ),
            TauCeti.HasPrescriptionProperty χ → χ.range = Subgroup.zpowers (-1)
Sources
LeanTauCeti.exists_isDemushkin_one_range_eq_zpowers_neg_one · TauCeti.exists_isDemushkin_range_eq_of_even_of_lt · TauCeti.exists_isDemushkin_range_eq_unitsPlusMinus_of_odd · TauCeti.exists_isDemushkin_range_eq_zpowers_neg_one_of_odd
Uses 5 · Used by 3
Statement usesThe Demushkin predicate
Proof usesBurnside's basis theorem, cardinal form · Labute's classification of the closed subgroups of ℤ_2ˣ · Labute's criterion · The third isomorphism theorem for coset spaces
Used byThe existence theorem of the classification for odd rank, as an equivalence (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2) · The existence theorem of the classification of Demushkin groups for even rank, as an equivalence (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2) · The existence theorem of the classification for q ≠ 2, as an equivalence (Labute, Theorem 1 and Remark 2; Demushkin and Serre)

TheoremLabute's criterion#

Let F be the free pro-p group on a finite type X, let r ∈ Φ(F), and let G ≅ ⟨X ∣ r⟩. Then G is a Demushkin group exactly when X is nonempty and the degree-one form of the class of r in gr_1(F) is nondegenerate.

TauCeti.isDemushkin_iff_nondegenerate_degreeOneForm.{u, v} {p : ℕ} [Fact (Nat.Prime p)] {X : Type u}
  [Finite X] {r : TauCeti.freeProP p X} {G : Type v} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
  (hr : r ∈ TauCeti.proPFrattini p (TauCeti.freeProP p X))
  (e : TauCeti.presentedProP p X {r} ≃ₜ* G) :
  TauCeti.IsDemushkin p G ↔
    Nonempty X ∧
      (TauCeti.freeProP.degreeOneForm
          (TauCeti.gradedMk p (TauCeti.freeProP p X) 1 ⟨r, ⋯⟩)).Nondegenerate
Lean

Formalized in Tau Ceti as TauCeti.isDemushkin_iff_nondegenerate_degreeOneForm.

Other forms

Labute's criterion, sufficiency. Formalized in Tau Ceti as TauCeti.isDemushkin_of_nondegenerate_degreeOneForm.

TauCeti.isDemushkin_of_nondegenerate_degreeOneForm.{u, v} {p : ℕ} [Fact (Nat.Prime p)] {X : Type u}
  [Finite X] {r : TauCeti.freeProP p X} {G : Type v} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
  (hr : r ∈ TauCeti.proPFrattini p (TauCeti.freeProP p X)) (e : TauCeti.presentedProP p X {r} ≃ₜ* G)
  [Nonempty X]
  (hnd :
    (TauCeti.freeProP.degreeOneForm
        (TauCeti.gradedMk p (TauCeti.freeProP p X) 1 ⟨r, ⋯⟩)).Nondegenerate) :
  TauCeti.IsDemushkin p G
Sources
LeanTauCeti.isDemushkin_iff_nondegenerate_degreeOneForm · TauCeti.isDemushkin_of_nondegenerate_degreeOneForm
Uses 3 · Used by 9
Statement usesThe Demushkin predicate
Proof usesBurnside's basis theorem, cardinal form · The first isomorphism theorem for a surjective strict homomorphism of topological groups
Used byThe marked presentation of G_{ℚ₂}(2) · The marked presentation of G_{ℚ₂(√-2)}(2) · Labute's Theorem 2 at the even-rank dyadic endpoint · Labute's Theorem 2 · Labute's Theorem 2 for odd rank · The classification of Demushkin groups (Labute) · The existence theorem of the classification of Demushkin groups, rank one (Labute, Remark 2 (iii); NSW (3.9.10)) · The necessity half of the existence theorem for q ≠ 2 (Labute, Theorem 1) · Uniqueness of the dyadic Demushkin groups of even rank with image {±1} × U^(f) (Labute, Theorem 6)

TheoremLabute's Theorem 2#

Let r, r' be relators of the free pro-p group F on n generators whose presented groups are Demushkin groups whose canonical characters have the same image. Then a continuous automorphism of F carries r to r'; in particular the closed normal closures of r and r' are carried to each other, so two Demushkin relators with the same invariants differ by a change of basis of F. The relators lie in Φ(F) and both groups have rank n automatically (TauCeti.IsDemushkin.mem_proPFrattini_of_presentedProP_singleton).

TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_demushkinCharacter_eq {p : ℕ}
  [Fact (Nat.Prime p)] {n : ℕ} {r r' : TauCeti.freeProP p (Fin n)}
  (hG : TauCeti.IsDemushkin p (TauCeti.presentedProP p (Fin n) {r}))
  (hG' : TauCeti.IsDemushkin p (TauCeti.presentedProP p (Fin n) {r'}))
  (h : (TauCeti.demushkinCharacter hG).range = (TauCeti.demushkinCharacter hG').range) :
  ∃ e, e r = r'
Lean

Formalized in Tau Ceti as TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_demushkinCharacter_eq.

Sources
LeanTauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_demushkinCharacter_eq
Uses 15 · Used by 1
Statement usesThe Demushkin predicate
Proof usesThe abelianization structure theorem for one-relator pro-p groups · Burnside's basis theorem, cardinal form · Burnside's criterion modulo λ_1 · The constrained successive-approximation theorem · Dedekind's modular law · The first isomorphism theorem for a surjective strict homomorphism of topological groups · Labute's classification of the closed subgroups of ℤ_2ˣ · Labute's criterion · Labute's Theorem 2 at the even-rank dyadic endpoint · Labute's Theorem 2 for q ≠ 2 · Labute's Theorem 2 for odd rank · Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property · The relative successive-approximation theorem · The successive-approximation theorem with tails
Used byThe classification of Demushkin groups (Labute)

TheoremLabute's Theorem 2 for q ≠ 2#

Let r, r' ∈ Φ(F) be relators of the free pro-p group on n generators whose presented groups are Demushkin groups with the same q-invariant q ≠ 2. Then a continuous automorphism of F carries r to r'; in particular the closed normal closures of r and r' are carried to each other.

TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_demushkinQ_eq {p : ℕ} [Fact (Nat.Prime p)]
  {n : ℕ} {r r' : TauCeti.freeProP p (Fin n)}
  (hr : r ∈ TauCeti.proPFrattini p (TauCeti.freeProP p (Fin n)))
  (hr' : r' ∈ TauCeti.proPFrattini p (TauCeti.freeProP p (Fin n)))
  (hG : TauCeti.IsDemushkin p (TauCeti.presentedProP p (Fin n) {r}))
  (hG' : TauCeti.IsDemushkin p (TauCeti.presentedProP p (Fin n) {r'}))
  (hq : TauCeti.demushkinQ hG = TauCeti.demushkinQ hG') (hq2 : TauCeti.demushkinQ hG ≠ 2) :
  ∃ e, e r = r'
Lean

Formalized in Tau Ceti as TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_demushkinQ_eq.

Sources
LeanTauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_demushkinQ_eq
Uses 6 · Used by 1
Statement usesThe Demushkin predicate
Proof usesThe abelianization structure theorem for one-relator pro-p groups · Burnside's basis theorem, cardinal form · The first isomorphism theorem for a surjective strict homomorphism of topological groups · The relative successive-approximation theorem · The unconstrained successive-approximation theorem
Used byLabute's Theorem 2

TheoremLabute's Theorem 2 for odd rank#

Let r, r' ∈ Φ(F) be relators of the free pro-2 group on an odd number n of generators whose presented groups are Demushkin groups whose canonical characters have the same image. Then a continuous automorphism of F carries r to r'; in particular the closed normal closures of r and r' are carried to each other.

TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_demushkinCharacter_eq_of_odd {n : ℕ}
  (hn : Odd n) {r r' : TauCeti.freeProP 2 (Fin n)}
  (hr : r ∈ TauCeti.proPFrattini 2 (TauCeti.freeProP 2 (Fin n)))
  (hr' : r' ∈ TauCeti.proPFrattini 2 (TauCeti.freeProP 2 (Fin n)))
  (hG : TauCeti.IsDemushkin 2 (TauCeti.presentedProP 2 (Fin n) {r}))
  (hG' : TauCeti.IsDemushkin 2 (TauCeti.presentedProP 2 (Fin n) {r'}))
  (h : (TauCeti.demushkinCharacter hG).range = (TauCeti.demushkinCharacter hG').range) :
  ∃ e, e r = r'
Lean

Formalized in Tau Ceti as TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_demushkinCharacter_eq_of_odd.

Sources
LeanTauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_demushkinCharacter_eq_of_odd
Uses 9 · Used by 1
Statement usesThe Demushkin predicate
Proof usesThe abelianization structure theorem for one-relator pro-p groups · Burnside's basis theorem, cardinal form · The first isomorphism theorem for a surjective strict homomorphism of topological groups · Labute's criterion · Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property · The necessity half of the existence theorem for q ≠ 2 (Labute, Theorem 1) · The relative successive-approximation theorem · The successive-approximation theorem with tails
Used byLabute's Theorem 2

TheoremThe necessity half of the existence theorem for q ≠ 2 (Labute, Theorem 1)#

For a Demushkin group G of rank n with q(G) ≠ 2, the image A of its canonical character has (A : A^p) < p ^ n. Indeed A is trivial, with (A : A^p) = 1, or the principal unit group 1 + qℤ_p, with (A : A^p) = p, while n ≥ 2. Together with the parity of the rank (TauCeti.IsDemushkin.even_demushkinRank_of_demushkinQ_ne_two), this places (n, A) in the first situation of the existence theorem.

TauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_demushkinQ_ne_two.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
  (hG : TauCeti.IsDemushkin p G) (hq2 : TauCeti.demushkinQ hG ≠ 2) :
  ((Subgroup.map (powMonoidHom p) (TauCeti.demushkinCharacter hG).range).subgroupOf
        (TauCeti.demushkinCharacter hG).range).profiniteIndex <
    TauCeti.Supernatural.primePower ⟨p, ⋯⟩ ↑(TauCeti.demushkinRank hG)
Lean

Formalized in Tau Ceti as TauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_demushkinQ_ne_two.

Other forms

The necessity half of the existence theorem for even rank (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2). Formalized in Tau Ceti as TauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_even_demushkinRank.

TauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_even_demushkinRank.{u}
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] {p : ℕ} [hp : Fact (Nat.Prime p)] (hG : TauCeti.IsDemushkin p G)
  (hn : Even (TauCeti.demushkinRank hG)) :
  ((Subgroup.map (powMonoidHom p) (TauCeti.demushkinCharacter hG).range).subgroupOf
        (TauCeti.demushkinCharacter hG).range).profiniteIndex <
    TauCeti.Supernatural.primePower ⟨p, ⋯⟩ ↑(TauCeti.demushkinRank hG)

The necessity half of the existence theorem for odd rank (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2). Formalized in Tau Ceti as TauCeti.IsDemushkin.range_demushkinCharacter_eq_zpowers_neg_one_or_unitsPlusMinus_of_odd_demushkinRank.

TauCeti.IsDemushkin.range_demushkinCharacter_eq_zpowers_neg_one_or_unitsPlusMinus_of_odd_demushkinRank.{u}
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] (hG : TauCeti.IsDemushkin 2 G)
  (hn : Odd (TauCeti.demushkinRank hG)) :
  (TauCeti.demushkinCharacter hG).range = Subgroup.zpowers (-1) ∨
    3 ≤ TauCeti.demushkinRank hG ∧
      ∃ f, 2 ≤ f ∧ (TauCeti.demushkinCharacter hG).range = TauCeti.unitsPlusMinus f

The necessity half of the existence theorem for odd rank, relator form (Labute, Theorem 1 and Remark 2). Formalized in Tau Ceti as TauCeti.freeProP.range_demushkinCharacter_eq_zpowers_neg_one_or_unitsPlusMinus_of_odd.

TauCeti.freeProP.range_demushkinCharacter_eq_zpowers_neg_one_or_unitsPlusMinus_of_odd {n : ℕ}
  (hn : Odd n) {r : TauCeti.freeProP 2 (Fin n)}
  (hr : r ∈ TauCeti.proPFrattini 2 (TauCeti.freeProP 2 (Fin n)))
  (hG : TauCeti.IsDemushkin 2 (TauCeti.presentedProP 2 (Fin n) {r})) :
  (TauCeti.demushkinCharacter hG).range = Subgroup.zpowers (-1) ∨
    3 ≤ n ∧ ∃ f, 2 ≤ f ∧ (TauCeti.demushkinCharacter hG).range = TauCeti.unitsPlusMinus f
Sources
LeanTauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_demushkinQ_ne_two · TauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_even_demushkinRank · TauCeti.IsDemushkin.range_demushkinCharacter_eq_zpowers_neg_one_or_unitsPlusMinus_of_odd_demushkinRank · TauCeti.freeProP.range_demushkinCharacter_eq_zpowers_neg_one_or_unitsPlusMinus_of_odd
Uses 10 · Used by 4
Statement usesThe Demushkin predicate
Proof usesThe abelianization structure theorem for one-relator pro-p groups · Burnside's basis theorem, cardinal form · The first isomorphism theorem for a surjective strict homomorphism of topological groups · Labute's classification of the closed subgroups of ℤ_2ˣ · Labute's criterion · Labute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property · The relative successive-approximation theorem · The successive-approximation theorem with tails · The third isomorphism theorem for coset spaces
Used byThe existence theorem of the classification for odd rank, as an equivalence (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2) · The existence theorem of the classification of Demushkin groups for even rank, as an equivalence (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2) · Labute's Theorem 2 for odd rank · The existence theorem of the classification for q ≠ 2, as an equivalence (Labute, Theorem 1 and Remark 2; Demushkin and Serre)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.