The abelianization structure… to Structure theorem for…

DefinitionThe abelianization structure theorem for one-relator pro-p groups#

Let G = presentedProP p X {r} be the pro-p group on a finite type X with the single relator r, and write the exponent vector of r as exponentSum r = q • w with w x₀ = 1. Then

G^{ab} ≃ₜ* ℤ_p^{X ∖ {x₀}} × ℤ_p ⧸ q ℤ_p

as topological groups, the isomorphism sending the class of the generator at x ≠ x₀ to the coordinate vector at x and the class of the generator at x₀ to (-w, 1). When q ≠ 0 the factor ℤ_p ⧸ q ℤ_p is finite cyclic and is the torsion subgroup of G^{ab}; when q = 0 it is ℤ_p and G^{ab} ≅ ℤ_p^X is torsion-free.

TauCeti.presentedProP.oneRelatorAbelianizationEquiv.{u} {p : ℕ} [Fact (Nat.Prime p)] {X : Type u}
  (r : TauCeti.freeProP p X) (x₀ : X) (w : X → ℤ_[p]) (hw : w x₀ = 1) (q : ℤ_[p])
  (hr : Multiplicative.toAdd ((TauCeti.freeProP.exponentSum p X) r) = q • w) [Finite X] :
  TopologicalAbelianization (TauCeti.presentedProP p X {r}) ≃ₜ*
    Multiplicative (({ x // x ≠ x₀ } → ℤ_[p]) × ℤ_[p] ⧸ Ideal.span {q})
Lean

Formalized in Tau Ceti as TauCeti.presentedProP.oneRelatorAbelianizationEquiv.

Other forms

The abelianization structure theorem for Demushkin groups (Labute, p. 106). Formalized in Tau Ceti as TauCeti.IsDemushkin.nonempty_continuousMulEquiv_topologicalAbelianization.

TauCeti.IsDemushkin.nonempty_continuousMulEquiv_topologicalAbelianization.{u} {p : ℕ}
  [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  (hG : TauCeti.IsDemushkin p G) [CompactSpace G] [TotallyDisconnectedSpace G] :
  Nonempty
    (TopologicalAbelianization G ≃ₜ*
      Multiplicative
        ((Fin (TauCeti.demushkinRank hG - 1) → ℤ_[p]) ×
          ℤ_[p] ⧸ Ideal.span {↑(TauCeti.demushkinQ hG)}))
Sources
LeanTauCeti.presentedProP.oneRelatorAbelianizationEquiv · TauCeti.IsDemushkin.nonempty_continuousMulEquiv_topologicalAbelianization
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) · Labute's Theorem 2 at the even-rank dyadic endpoint · Labute's Theorem 2 · Labute's Theorem 2 for odd rank · Labute's Theorem 2 for q ≠ 2 · The existence theorem of the classification for q ≠ 2, as an equivalence (Labute, Theorem 1 and Remark 2; Demushkin and Serre) · 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)

TheoremBurnside's basis theorem, cardinal form#

The topological generator rank of a profinite pro-p group is the dimension of its continuous 𝔽_p-dual over 𝔽_p. No finiteness hypothesis is needed, and the statement is an identity of cardinals.

TauCeti.IsProP.topologicalGeneratorRank_eq_rank_continuousZModDual.{u} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G) :
  TauCeti.topologicalGeneratorRank G = Module.rank (ZMod p) (TauCeti.continuousZModDual p G)
Lean

Formalized in Tau Ceti as TauCeti.IsProP.topologicalGeneratorRank_eq_rank_continuousZModDual.

Other forms

Burnside's basis theorem for H¹, cardinal form. Formalized in Tau Ceti as TauCeti.IsProP.rank_H1_eq_topologicalGeneratorRank.

TauCeti.IsProP.rank_H1_eq_topologicalGeneratorRank.{u} {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 : TauCeti.IsProP p G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) :
  Module.rank (ZMod p) (TauCeti.ContCohomology.H1 G (ZMod p)) = TauCeti.topologicalGeneratorRank G

Burnside's basis theorem for H¹, numerical form. Formalized in Tau Ceti as TauCeti.IsProP.finrank_H1_eq_topologicalGeneratorRankNat.

TauCeti.IsProP.finrank_H1_eq_topologicalGeneratorRankNat.{u} {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 : TauCeti.IsProP p G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G) :
  Module.finrank (ZMod p) (TauCeti.ContCohomology.H1 G (ZMod p)) =
    TauCeti.topologicalGeneratorRankNat G hfg

Burnside's basis theorem for normal generation. Formalized in Tau Ceti as TauCeti.IsProP.topologicalClosure_normalClosure_eq_iff_quotient_pLowerCentralStep.

TauCeti.IsProP.topologicalClosure_normalClosure_eq_iff_quotient_pLowerCentralStep.{u} {p : ℕ}
  {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
  [TotallyDisconnectedSpace F] (hF : TauCeti.IsProP p F) (hp : Nat.Prime p) {R : Subgroup F}
  [R.Normal] (hR : IsClosed ↑R) (s : Set ↥R) :
  (Subgroup.normalClosure (Subtype.val '' s)).topologicalClosure = R ↔
    (Subgroup.closure
          (⇑(QuotientGroup.mk' ((TauCeti.pLowerCentralStep p R).subgroupOf R)) ''
            s)).topologicalClosure =
      ⊤

Burnside's basis theorem, cardinal form: the lower bound. Formalized in Tau Ceti as TauCeti.topologicalGeneratorRank_le_rank_continuousZModDual.

TauCeti.topologicalGeneratorRank_le_rank_continuousZModDual.{u} {p : ℕ} [hp : Fact (Nat.Prime p)]
  {W : Type u} [CommGroup W] [TopologicalSpace W] [IsTopologicalGroup W] [CompactSpace W]
  [TotallyDisconnectedSpace W] [hW : _root_.Module (ZMod p) (Additive W)] :
  TauCeti.topologicalGeneratorRank W ≤ Module.rank (ZMod p) (TauCeti.continuousZModDual p W)

Burnside's basis theorem, dense spanning form. Formalized in Tau Ceti as TauCeti.topologicallyGenerates_iff_frattiniQuotient_span_topologicalClosure_eq_top.

TauCeti.topologicallyGenerates_iff_frattiniQuotient_span_topologicalClosure_eq_top.{u_1} {p : ℕ}
  [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G) (s : Set G) :
  (Subgroup.closure s).topologicalClosure = ⊤ ↔
    (Submodule.span (ZMod p)
            ((fun g => Additive.ofMul ((QuotientGroup.mk' (TauCeti.proPFrattini p G)) g)) ''
              s)).toAddSubgroup.topologicalClosure =
      ⊤

Burnside's basis theorem, generation form. Formalized in Tau Ceti as TauCeti.topologicallyGenerates_iff_frattiniQuotient.

TauCeti.topologicallyGenerates_iff_frattiniQuotient.{u} {p : ℕ} [hp : Fact (Nat.Prime p)]
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G) (s : Set G) :
  (Subgroup.closure s).topologicalClosure = ⊤ ↔
    (Subgroup.closure (⇑(QuotientGroup.mk' (TauCeti.proPFrattini p G)) '' s)).topologicalClosure = ⊤

Burnside's basis theorem, numerical form against the dual. Formalized in Tau Ceti as TauCeti.IsProP.finrank_continuousZModDual_eq_topologicalGeneratorRankNat.

TauCeti.IsProP.finrank_continuousZModDual_eq_topologicalGeneratorRankNat.{u} {p : ℕ}
  [hp : 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) :
  Module.finrank (ZMod p) (TauCeti.continuousZModDual p G) =
    TauCeti.topologicalGeneratorRankNat G hfg

Burnside's basis theorem, spanning form. Formalized in Tau Ceti as TauCeti.topologicallyGenerates_iff_frattiniQuotient_span_eq_top.

TauCeti.topologicallyGenerates_iff_frattiniQuotient_span_eq_top.{u_1} {p : ℕ} [Fact (Nat.Prime p)]
  {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] [Finite (G ⧸ TauCeti.proPFrattini p G)] (hG : TauCeti.IsProP p G)
  (s : Set G) :
  (Subgroup.closure s).topologicalClosure = ⊤ ↔
    Submodule.span (ZMod p)
        ((fun g => Additive.ofMul ((QuotientGroup.mk' (TauCeti.proPFrattini p G)) g)) '' s) =
      ⊤
Sources
LeanTauCeti.IsProP.topologicalGeneratorRank_eq_rank_continuousZModDual · TauCeti.IsProP.rank_H1_eq_topologicalGeneratorRank · TauCeti.IsProP.finrank_H1_eq_topologicalGeneratorRankNat · TauCeti.IsProP.topologicalClosure_normalClosure_eq_iff_quotient_pLowerCentralStep · TauCeti.topologicalGeneratorRank_le_rank_continuousZModDual · TauCeti.topologicallyGenerates_iff_frattiniQuotient_span_topologicalClosure_eq_top · TauCeti.topologicallyGenerates_iff_frattiniQuotient · TauCeti.IsProP.finrank_continuousZModDual_eq_topologicalGeneratorRankNat · TauCeti.topologicallyGenerates_iff_frattiniQuotient_span_eq_top
Uses 1 · Used by 30
Proof usesNakayama's lemma for pro-p groups
Used byShafarevich's theorem · The generator rank of a local absolute Galois group (NSW (7.4.1)) · 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) · The open Frattini criterion · The three-term Euler formula · The three-term Euler identity under cd_p G ≤ 2 · The two-term Euler formula · The data are not determined in rank one · The peripheral-power theorem · 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 · Serre's theorem at arbitrary rank, as an equivalence · 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 Golod–Shafarevich inequality · 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) · Every invertible matrix over 𝔽_p comes from a continuous automorphism of the free pro-p group of finite rank · The Schreier index formula for open subgroups

TheoremBurnside's criterion modulo λ_1#

A continuous endomorphism of a pro-p group congruent to the identity modulo λ_1 = Φ is surjective.

TauCeti.IsProP.surjective_of_forall_inv_mul_mem_pLowerCentralSeries_one.{u_1} {p : ℕ} {G : Type u_1}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)] (hG : TauCeti.IsProP p G) {φ : G →* G}
  (hφ : Continuous ⇑φ) (h : ∀ (g : G), g⁻¹ * φ g ∈ TauCeti.pLowerCentralSeries p G 1) :
  Function.Surjective ⇑φ
Lean

Formalized in Tau Ceti as TauCeti.IsProP.surjective_of_forall_inv_mul_mem_pLowerCentralSeries_one.

Sources
LeanTauCeti.IsProP.surjective_of_forall_inv_mul_mem_pLowerCentralSeries_one
Used by 3
Used byThe marked presentation of G_{ℚ₂(√-2)}(2) · Labute's Theorem 2 · The constrained successive-approximation theorem

TheoremBurnside's surjectivity criterion#

A continuous homomorphism from a compact group to a profinite pro-p group is surjective exactly when its composites with all index-p quotient maps are surjective.

TauCeti.IsProP.surjective_iff_surjective_quotient_index_eq.{u_1, u_2} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] {H : Type u_2} [Group H] [TopologicalSpace H]
  [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] [TopologicalSpace G]
  [CompactSpace G] (hH : TauCeti.IsProP p H) (f : G →* H) (hf : Continuous ⇑f) :
  Function.Surjective ⇑f ↔
    ∀ (U : OpenNormalSubgroup H),
      (↑U.toOpenSubgroup).index = p →
        Function.Surjective ⇑((QuotientGroup.mk' ↑U.toOpenSubgroup).comp f)
Lean

Formalized in Tau Ceti as TauCeti.IsProP.surjective_iff_surjective_quotient_index_eq.

Sources
LeanTauCeti.IsProP.surjective_iff_surjective_quotient_index_eq

TheoremThe existence theorem of the classification for odd rank, as an equivalence (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2)#

Let n be odd and let A ≤ ℤ₂ˣ be a subgroup. Then (n, A) is the pair of invariants of a Demushkin group, presented on n generators by one relator, exactly when A = {±1}, or n ≥ 3 and A = {±1} × U^(f) for some f ≥ 2. At n = 1 the only admissible image is {±1}, the image of the canonical character of ℤ/2. Every such A is closed and pro-2, so no hypothesis on A is needed.

TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff_of_odd {n : ℕ} (hn : Odd n)
  {A : Subgroup ℤ_[2]ˣ} :
  (∃ r,
      ∃ (hG : TauCeti.IsDemushkin 2 (TauCeti.presentedProP 2 (Fin n) {r})),
        TauCeti.demushkinRank hG = n ∧ (TauCeti.demushkinCharacter hG).range = A) ↔
    A = Subgroup.zpowers (-1) ∨ 3 ≤ n ∧ ∃ f, 2 ≤ f ∧ A = TauCeti.unitsPlusMinus f
Lean

Formalized in Tau Ceti as TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff_of_odd.

Sources
LeanTauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff_of_odd
Uses 5
Statement usesThe Demushkin predicate
Proof usesBurnside's basis theorem, cardinal form · The existence theorem of the classification of Demushkin groups, rank one (Labute, Remark 2 (iii); NSW (3.9.10)) · 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 for even rank, as an equivalence (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2)#

Let n be even and let A ≤ ℤ_pˣ be a closed pro-p subgroup. Then (n, A) is the pair of invariants (rank, Im χ) of a Demushkin group, presented on n generators by one relator, exactly when (A : A^p) < p ^ n as supernatural numbers. At p = 2 the condition excludes exactly n = 0 and the non-procyclic images {±1} × U^(f) in rank two; at an odd prime it excludes exactly n = 0. Together with TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff_of_odd, this is the full list of the pairs of invariants of Demushkin groups.

TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff_of_even {p : ℕ} [hp : Fact (Nat.Prime p)]
  {n : ℕ} (hn : Even n) {A : Subgroup ℤ_[p]ˣ} (hA : IsClosed ↑A) (hAp : TauCeti.IsProP p ↥A) :
  (∃ r,
      ∃ (hG : TauCeti.IsDemushkin p (TauCeti.presentedProP p (Fin n) {r})),
        TauCeti.demushkinRank hG = n ∧ (TauCeti.demushkinCharacter hG).range = A) ↔
    ((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_of_even.

Sources
LeanTauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff_of_even
Uses 5
Statement usesThe Demushkin predicate
Proof usesBurnside's basis theorem, cardinal form · The existence theorem of the classification of Demushkin groups, rank one (Labute, Remark 2 (iii); NSW (3.9.10)) · 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)

DefinitionThe first isomorphism theorem for a surjective strict homomorphism of topological groups#

G ⧸ f.ker ≃ₜ* H.

ContinuousMulEquiv.quotientKerEquivOfSurjective.{u_1, u_2} {G : Type u_1} {H : Type u_2} [Group G]
  [Group H] [TopologicalSpace G] [TopologicalSpace H] (f : G →* H) (hf : Topology.IsStrictMap ⇑f)
  (hs : Function.Surjective ⇑f) : G ⧸ f.ker ≃ₜ* H
Lean

Formalized in Tau Ceti as ContinuousMulEquiv.quotientKerEquivOfSurjective.

Other forms

The first isomorphism theorem for a surjective strict homomorphism of topological additive groups. Formalized in Tau Ceti as ContinuousAddEquiv.quotientKerEquivOfSurjective.

ContinuousAddEquiv.quotientKerEquivOfSurjective.{u_1, u_2} {G : Type u_1} {H : Type u_2}
  [AddGroup G] [AddGroup H] [TopologicalSpace G] [TopologicalSpace H] (f : G →+ H)
  (hf : Topology.IsStrictMap ⇑f) (hs : Function.Surjective ⇑f) : G ⧸ f.ker ≃ₜ+ H
Sources
LeanContinuousMulEquiv.quotientKerEquivOfSurjective · ContinuousAddEquiv.quotientKerEquivOfSurjective
Used by 21
Used byThe adic spectrum of a classical affinoid algebra is an affinoid adic space · The marked presentation of G_{ℚ₂}(2) · The marked presentation of G_{ℚ₂(√-2)}(2) · The finite level of the generator theorem (NSW, proof of (7.4.1)) · The p-cohomological dimension of the profinite integers is one, for every prime p · 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 · Labute's criterion · Labute's Theorem 2 · Labute's Theorem 2 for odd rank · Labute's Theorem 2 for q ≠ 2 · Serre's theorem at arbitrary rank, as an equivalence · 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 Golod–Shafarevich inequality · 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) · The pro-p Nielsen–Schreier theorem · The Schreier index formula for open subgroups

TheoremThe Frattini criterion for a kernel#

If every continuous 𝔽_p-valued character of G factors through a continuous homomorphism φ : G → H, then the kernel of φ lies in the pro-p Frattini subgroup of G.

ContinuousMonoidHom.ker_le_proPFrattini_of_forall_exists_comp_eq.{u, u_1} {p : ℕ}
  [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {H : Type u_1}
  [Group H] [TopologicalSpace H] (φ : G →ₜ* H)
  (h : ∀ (ψ : G →ₜ* Multiplicative (ZMod p)), ∃ χ, χ.comp φ = ψ) : φ.ker ≤ TauCeti.proPFrattini p G
Lean

Formalized in Tau Ceti as ContinuousMonoidHom.ker_le_proPFrattini_of_forall_exists_comp_eq.

Sources
LeanContinuousMonoidHom.ker_le_proPFrattini_of_forall_exists_comp_eq
Used by 1
Used bySerre's theorem at arbitrary rank, as an equivalence

TheoremGaschütz's lifting lemma for profinite groups#

Along a continuous surjection f : G →* H from a profinite group onto a Hausdorff group, an ι-tuple that topologically generates H lifts to an ι-tuple that topologically generates G, provided G is topologically generated by some ι-tuple, with ι finite.

TauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top.{u_1, u_2, u_3} {G : Type u_1}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
  [T2Space H] {ι : Type u_3} [Finite ι] {f : G →* H} (hf : Continuous ⇑f)
  (hsurj : Function.Surjective ⇑f) {g : ι → G}
  (hg : (Subgroup.closure (Set.range g)).topologicalClosure = ⊤) {h : ι → H}
  (hh : (Subgroup.closure (Set.range h)).topologicalClosure = ⊤) :
  ∃ g', ⇑f ∘ g' = h ∧ (Subgroup.closure (Set.range g')).topologicalClosure = ⊤
Lean

Formalized in Tau Ceti as TauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top.

Other forms

Gaschütz's lifting lemma, generator-rank form. Formalized in Tau Ceti as TauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top_of_topologicalGeneratorRankNat_le.

TauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top_of_topologicalGeneratorRankNat_le.{u_1,
    u_2}
  {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
  [T2Space H] (hG : TauCeti.IsTopologicallyFinitelyGenerated G) {n : ℕ}
  (hn : TauCeti.topologicalGeneratorRankNat G hG ≤ n) {f : G →* H} (hf : Continuous ⇑f)
  (hsurj : Function.Surjective ⇑f) {h : Fin n → H}
  (hh : (Subgroup.closure (Set.range h)).topologicalClosure = ⊤) :
  ∃ g', ⇑f ∘ g' = h ∧ (Subgroup.closure (Set.range g')).topologicalClosure = ⊤
Sources
LeanTauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top · TauCeti.exists_comp_eq_and_topologicalClosure_closure_range_eq_top_of_topologicalGeneratorRankNat_le
Uses 1
Proof usesGaschütz's lemma

TheoremHenkel's open mapping theorem#

A surjective A-equivariant additive map from a complete first-countable nonarchimedean group to a Baire space is open, when A has a zero sequence of units.

Only continuity at zero is asked of f, and only continuity in the scalar at zero is asked of the action, in the form hc that the Baire step already uses.

TauCeti.HasZeroSequenceOfUnits.isOpenMap.{u_1, u_2, u_3, u_4} {A : Type u_1} {M : Type u_2}
  {N : Type u_3} [MonoidWithZero A] [TopologicalSpace A] [TauCeti.HasZeroSequenceOfUnits A]
  [AddCommGroup M] [UniformSpace M] [IsUniformAddGroup M] [CompleteSpace M]
  [(nhds 0).IsCountablyGenerated] [NonarchimedeanAddGroup M] [MulActionWithZero A M] [AddGroup N]
  [TopologicalSpace N] [IsTopologicalAddGroup N] [T0Space N] [BaireSpace N] [MulAction A N]
  [ContinuousConstSMul A N] {F : Type u_4} [FunLike F M N] [MulActionHomClass F A M N]
  [AddMonoidHomClass F M N] (f : F) (hf : Function.Surjective ⇑f) (hfc : ContinuousAt (⇑f) 0)
  (hc : ∀ (x : M), ContinuousAt (fun a => a • x) 0) : IsOpenMap ⇑f
Lean

Formalized in Tau Ceti as TauCeti.HasZeroSequenceOfUnits.isOpenMap.

Sources
LeanTauCeti.HasZeroSequenceOfUnits.isOpenMap
Used by 8
Used byTate's acyclicity theorem for the standard Laurent cover of the closed unit disc · Every strongly noetherian Tate ring is sheafy · 𝒪_𝒴 is a sheaf · The adic spectrum of a classical affinoid algebra is an affinoid adic space · The interval ring B^I is stably sheafy for all radii 0 < ρ₁ ≤ ρ₂ < 1 · Open Mapping Theorem for normed modules over a Tate ring · The open mapping theorem over a Tate ring · Henkel's theorem in quotient form

TheoremHenkel's theorem in quotient form#

Under exactly the hypotheses of TauCeti.HasZeroSequenceOfUnits.isOpenMap, the map does not merely carry open sets to open sets: the topology of N is the one coinduced from M, so a map out of N is continuous exactly when its composite with f is.

The quotient conclusion needs f continuous everywhere, but that is not an extra hypothesis: an additive homomorphism out of a topological group is continuous as soon as it is continuous at 0 (continuous_of_continuousAt_zero), so hfc is the same assumption the open-mapping theorem makes. This is the form behind TauCeti.Huber.IsTateRing.isModuleTopology, which pins down the topology of a finite module over a Tate ring.

TauCeti.HasZeroSequenceOfUnits.isQuotientMap.{u_1, u_2, u_3, u_4} {A : Type u_1} {M : Type u_2}
  {N : Type u_3} [MonoidWithZero A] [TopologicalSpace A] [TauCeti.HasZeroSequenceOfUnits A]
  [AddCommGroup M] [UniformSpace M] [IsUniformAddGroup M] [CompleteSpace M]
  [(nhds 0).IsCountablyGenerated] [NonarchimedeanAddGroup M] [MulActionWithZero A M] [AddGroup N]
  [TopologicalSpace N] [IsTopologicalAddGroup N] [T0Space N] [BaireSpace N] [MulAction A N]
  [ContinuousConstSMul A N] {F : Type u_4} [FunLike F M N] [MulActionHomClass F A M N]
  [AddMonoidHomClass F M N] (f : F) (hf : Function.Surjective ⇑f) (hfc : ContinuousAt (⇑f) 0)
  (hc : ∀ (x : M), ContinuousAt (fun a => a • x) 0) : Topology.IsQuotientMap ⇑f
Lean

Formalized in Tau Ceti as TauCeti.HasZeroSequenceOfUnits.isQuotientMap.

Sources
LeanTauCeti.HasZeroSequenceOfUnits.isQuotientMap
Uses 1 · Used by 5
Proof usesHenkel's open mapping theorem
Used byTate's acyclicity theorem for the standard Laurent cover of the closed unit disc · Every strongly noetherian Tate ring is sheafy · 𝒪_𝒴 is a sheaf · The adic spectrum of a classical affinoid algebra is an affinoid adic space · The interval ring B^I is stably sheafy for all radii 0 < ρ₁ ≤ ρ₂ < 1

TheoremLabute's Theorem 2 at the even-rank dyadic endpoint#

Let r, r' ∈ Φ(F) be relators of the free pro-2 group on an even number n of generators presenting Demushkin groups whose canonical characters both have image {±1}. 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_eq_zpowers_neg_one {n : ℕ}
  (hn : Even 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'}))
  (hA : (TauCeti.demushkinCharacter hG).range = Subgroup.zpowers (-1))
  (hA' : (TauCeti.demushkinCharacter hG').range = Subgroup.zpowers (-1)) : ∃ e, e r = r'
Lean

Formalized in Tau Ceti as TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_eq_zpowers_neg_one.

Sources
LeanTauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_eq_zpowers_neg_one
Uses 8 · 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 relative successive-approximation theorem · The successive-approximation theorem with tails
Used byLabute's Theorem 2

TheoremLabute's Theorem 4: a Demushkin group has exactly one continuous character with the prescription property# 

TauCeti.IsDemushkin.existsUnique_hasPrescriptionProperty.{v} {p : ℕ} [Fact (Nat.Prime p)]
  {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] (hG : TauCeti.IsDemushkin p G) :
  ∃! χ, TauCeti.HasPrescriptionProperty χ
Lean

Formalized in Tau Ceti as TauCeti.IsDemushkin.existsUnique_hasPrescriptionProperty.

Sources
LeanTauCeti.IsDemushkin.existsUnique_hasPrescriptionProperty
Uses 3 · Used by 13
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 · 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) · Labute's Theorem 2 · Labute's Theorem 2 for odd rank · 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ⁱ · 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 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)

TheoremLagrange's theorem for profinite groups#

the supernatural order of the ambient group is the order of a closed subgroup times its supernatural index.

Subgroup.profiniteOrder_eq_mul_profiniteIndex.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G)
  (hH : IsClosed ↑H) : TauCeti.profiniteOrder G = TauCeti.profiniteOrder ↥H * H.profiniteIndex
Lean

Formalized in Tau Ceti as Subgroup.profiniteOrder_eq_mul_profiniteIndex.

Sources
LeanSubgroup.profiniteOrder_eq_mul_profiniteIndex
Uses 1
Proof usesThe third isomorphism theorem for coset spaces

DefinitionLyndon's theorem for the relation module (NSW (5.6.6))#

For a finite group G generated by the family g : ι → G, the maximal abelian pro-p quotient R^ab(p) of the kernel R of lift g : F → G is isomorphic to the relation module relationModule ℤ_[p] G g. The isomorphism sends the class of r ∈ R to its Fox derivative (coe_abelianizationProPEquivRelationModule_ofMul), it is ℤ_p-linear (abelianizationProPEquivRelationModule_padicPow), and it is equivariant (abelianizationProPEquivRelationModule_smul).

TauCeti.freeProfiniteGroup.abelianizationProPEquivRelationModule.{u} (p : ℕ) [Fact (Nat.Prime p)]
  {G : Type u} [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] {ι : Type u}
  {g : ι → G} (hg : Subgroup.closure (Set.range g) = ⊤) [DecidableEq ι] [Fintype ι] :
  Additive
      (TauCeti.abelianizationProP p (↑(TauCeti.freeProfiniteGroup ι).toProfinite.toTop)
        (↑(TauCeti.freeProfiniteGroup.lift g)).ker) ≃+
    ↥(TauCeti.MonoidAlgebra.relationModule ℤ_[p] G g)
Lean

Formalized in Tau Ceti as TauCeti.freeProfiniteGroup.abelianizationProPEquivRelationModule.

Sources
LeanTauCeti.freeProfiniteGroup.abelianizationProPEquivRelationModule
Used by 1
Used byThe finite level of the generator theorem (NSW, proof of (7.4.1))

DefinitionMacbeath's theorem#

If the translates of a path-connected open set U cover a simply connected space X, then G is presented by the Macbeath generators and relations of U.

TauCeti.macbeathEquiv.{u_1, u_2} {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X}
  [TopologicalSpace X] [ContinuousConstSMul G X] [SimplyConnectedSpace X] (hUo : IsOpen U)
  (hUc : IsPathConnected U) (hcover : ⋃ g, g • U = Set.univ) :
  PresentedGroup (TauCeti.macbeathRels G U) ≃* G
Lean

Formalized in Tau Ceti as TauCeti.macbeathEquiv.

Other forms

Macbeath's theorem, as a description of the relations. Formalized in Tau Ceti as TauCeti.ker_lift_eq_normalClosure_macbeathRels.

TauCeti.ker_lift_eq_normalClosure_macbeathRels.{u_1, u_2} {G : Type u_1} {X : Type u_2} [Group G]
  [MulAction G X] {U : Set X} [TopologicalSpace X] [ContinuousConstSMul G X]
  [SimplyConnectedSpace X] (hUo : IsOpen U) (hUc : IsPathConnected U)
  (hcover : ⋃ g, g • U = Set.univ) :
  (FreeGroup.lift Subtype.val).ker = Subgroup.normalClosure (TauCeti.macbeathRels G U)

Macbeath's theorem for a tile, as a description of the relations. Formalized in Tau Ceti as TauCeti.ker_lift_eq_normalClosure_macbeathRels_of_locallyFinite.

TauCeti.ker_lift_eq_normalClosure_macbeathRels_of_locallyFinite.{u_1, u_2} {G : Type u_1}
  {X : Type u_2} [Group G] [MulAction G X] [PseudoMetricSpace X] [IsIsometricSMul G X] {P : Set X}
  [LocallyPathConnectedSpace X] [SimplyConnectedSpace X] (hPc : IsClosed P) (hP : IsConnected P)
  (hlf : LocallyFinite fun g => g • P) (hcover : ⋃ g, g • P = Set.univ) :
  (FreeGroup.lift Subtype.val).ker = Subgroup.normalClosure (TauCeti.macbeathRels G P)

Macbeath's theorem for a tile. Formalized in Tau Ceti as TauCeti.macbeathHom_injective_of_locallyFinite.

TauCeti.macbeathHom_injective_of_locallyFinite.{u_1, u_2} {G : Type u_1} {X : Type u_2} [Group G]
  [MulAction G X] [PseudoMetricSpace X] [IsIsometricSMul G X] {P : Set X}
  [LocallyPathConnectedSpace X] [SimplyConnectedSpace X] (hPc : IsClosed P) (hP : IsConnected P)
  (hlf : LocallyFinite fun g => g • P) (hcover : ⋃ g, g • P = Set.univ) :
  Function.Injective ⇑(TauCeti.macbeathHom G P)
Sources
LeanTauCeti.macbeathEquiv · TauCeti.ker_lift_eq_normalClosure_macbeathRels · TauCeti.ker_lift_eq_normalClosure_macbeathRels_of_locallyFinite · TauCeti.macbeathHom_injective_of_locallyFinite
Used by 1
Used byPoincaré's presentation theorem

TheoremNakayama's lemma for pro-p groups#

In a profinite pro-p group a subgroup K with K ≤ closure (Kᵖ ⬝ [K, G]) is trivial: it lies in every term of the lower p-series.

TauCeti.IsProP.eq_bot_of_le_pLowerCentralStep.{u_1} {p : ℕ} {G : Type u_1} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
  (hG : TauCeti.IsProP p G) (hp : Nat.Prime p) {K : Subgroup G}
  (h : K ≤ TauCeti.pLowerCentralStep p K) : K = ⊥
Lean

Formalized in Tau Ceti as TauCeti.IsProP.eq_bot_of_le_pLowerCentralStep.

Other forms

Nakayama's lemma for pro-p groups, relative form. Formalized in Tau Ceti as TauCeti.IsProP.le_of_le_topologicalClosure_sup_pLowerCentralStep.

TauCeti.IsProP.le_of_le_topologicalClosure_sup_pLowerCentralStep.{u_1} {p : ℕ} {G : Type u_1}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G) (hp : Nat.Prime p) {R N : Subgroup G}
  [N.Normal] (hN : IsClosed ↑N) (h : R ≤ (N ⊔ TauCeti.pLowerCentralStep p R).topologicalClosure) :
  R ≤ N
Sources
LeanTauCeti.IsProP.eq_bot_of_le_pLowerCentralStep · TauCeti.IsProP.le_of_le_topologicalClosure_sup_pLowerCentralStep
Used by 1
Used byBurnside's basis theorem, cardinal form

TheoremThe open Frattini criterion#

A profinite pro-p group is topologically finitely generated exactly when its Frattini subgroup is open.

TauCeti.IsProP.isTopologicallyFinitelyGenerated_iff_isOpen_proPFrattini.{u_1} {G : Type u_1}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {p : ℕ}
  [Fact (Nat.Prime p)] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G) :
  TauCeti.IsTopologicallyFinitelyGenerated G ↔ IsOpen ↑(TauCeti.proPFrattini p G)
Lean

Formalized in Tau Ceti as TauCeti.IsProP.isTopologicallyFinitelyGenerated_iff_isOpen_proPFrattini.

Sources
LeanTauCeti.IsProP.isTopologicallyFinitelyGenerated_iff_isOpen_proPFrattini
Uses 1
Proof usesBurnside's basis theorem, cardinal form

TheoremThe Schreier bound#

Let U be an open subgroup of finite index in a topologically finitely generated topological group G. Then U is topologically finitely generated (TauCeti.IsTopologicallyFinitelyGenerated.of_openSubgroup_of_finiteIndex), and d(U) ≤ 1 + [G : U] * (d(G) - 1), with subtraction in ℕ. This is the topological form of Schreier's index formula Subgroup.rank_le_one_add_index_mul_rank_sub_one. The bound is sharp: finite-index subgroups of nontrivial finitely generated discrete free groups attain it, by the Nielsen–Schreier theorem.

TauCeti.topologicalGeneratorRankNat_le_of_openSubgroup_of_finiteIndex.{u} {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] (hG : TauCeti.IsTopologicallyFinitelyGenerated G)
  (U : OpenSubgroup G) [(↑U).FiniteIndex] :
  TauCeti.topologicalGeneratorRankNat ↥↑U ⋯ ≤
    1 + (↑U).index * (TauCeti.topologicalGeneratorRankNat G hG - 1)
Lean

Formalized in Tau Ceti as TauCeti.topologicalGeneratorRankNat_le_of_openSubgroup_of_finiteIndex.

Other forms

The Schreier bound for open subgroups of a compact group. Formalized in Tau Ceti as TauCeti.topologicalGeneratorRankNat_le_of_openSubgroup.

TauCeti.topologicalGeneratorRankNat_le_of_openSubgroup.{u} {G : Type u} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  (hG : TauCeti.IsTopologicallyFinitelyGenerated G) (U : OpenSubgroup G) :
  TauCeti.topologicalGeneratorRankNat ↥↑U ⋯ ≤
    1 + (↑U).index * (TauCeti.topologicalGeneratorRankNat G hG - 1)
Sources
LeanTauCeti.topologicalGeneratorRankNat_le_of_openSubgroup_of_finiteIndex · TauCeti.topologicalGeneratorRankNat_le_of_openSubgroup
Uses 1 · Used by 1
Proof usesSchreier's index formula
Used byThe generator rank of a local absolute Galois group (NSW (7.4.1))

TheoremStructure theorem for topologically finitely generated abelian pro-p groups#

Such a group is topologically isomorphic to ℤ_p ^ r × ∏ i : Fin m, ℤ/p^(e i) with every e i positive, where the finite factor carries the discrete topology.

TauCeti.IsProP.exists_continuousMulEquiv_pi_padicInt_prod_pi_zmod.{u_1} {p : ℕ} [Fact (Nat.Prime p)]
  {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A]
  [TotallyDisconnectedSpace A] (hA : TauCeti.IsProP p A)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated A) :
  ∃ r m e,
    (∀ (i : Fin m), 0 < e i) ∧
      Nonempty (A ≃ₜ* Multiplicative ((Fin r → ℤ_[p]) × ((i : Fin m) → ZMod (p ^ e i))))
Lean

Formalized in Tau Ceti as TauCeti.IsProP.exists_continuousMulEquiv_pi_padicInt_prod_pi_zmod.

Other forms

Structure theorem for topologically finitely generated abelian pro-p groups, as topological ℤ_[p]-modules. Formalized in Tau Ceti as TauCeti.IsProP.exists_continuousLinearEquiv_pi_padicInt_prod_torsion.

TauCeti.IsProP.exists_continuousLinearEquiv_pi_padicInt_prod_torsion.{u_1} {p : ℕ}
  [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]
  [CompactSpace A] [TotallyDisconnectedSpace A] (hA : TauCeti.IsProP p A)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated A) :
  ∃ r, Nonempty (Additive A ≃L[ℤ_[p]] (Fin r → ℤ_[p]) × ↥(Submodule.torsion ℤ_[p] (Additive A)))
Sources
LeanTauCeti.IsProP.exists_continuousMulEquiv_pi_padicInt_prod_pi_zmod · TauCeti.IsProP.exists_continuousLinearEquiv_pi_padicInt_prod_torsion
Uses 1 · Used by 1
Proof usesStructure theorem for finitely generated modules over a discrete valuation ring
Used byStructure theorem for torsion-free topologically finitely generated abelian pro-p groups

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.