Documentation

TauCeti.Topology.Algebra.Group.Profinite.Free.Graded

The degree-one graded piece of a free pro-p group #

Let F = freeProP p X be the free pro-p group on a finite linearly ordered type X, with canonical generators x_i = freeProP.of i. The degree-one graded piece gr_1(F) = λ_1(F) ⧸ λ_2(F) of the lower p-series is an 𝔽_p-vector space with basis

π x'_i for i ∈ X, and [x'_i, x'_j] for i < j,

the p-power classes and the brackets of the generator classes x'_i ∈ gr_0(F). So gr_1(F) ≅ 𝔽_p^X ⊕ Λ²(𝔽_p^X) has dimension #X + (#X choose 2).

The basis is the degree-one family TauCeti.degreeOneFamily of the canonical generators, indexed by X ⊕ {(i, j) : i < j}, so its coordinates split a class in gr_1(F) into its p-power part, with one coefficient per generator, and its commutator part, with one coefficient per unordered pair of generators. These coordinates are what reading off the class of a relator of a pro-p group presented on the generators x_i requires. The results hold for any universe of X; the two finite p-groups of p-class two used as detecting groups for this degree-one basis are ℤ/p² and the Heisenberg group over 𝔽_p.

In every degree j, the iterated p-power classes π^j x'_i ∈ gr_j(F) of the generators are linearly independent, detected in the cyclic groups ℤ/pʲ⁺¹ of p-class j + 1 through the exponent sums modulo p ^ (j + 1) (TauCeti.freeProP.exponentSumZModPow): the graded map induced by the i-th of these characters reads off the coefficient of π^j x'_i, and on the class of an element of λ_j(F) it detects whether p ^ (j + 1) divides the i-th exponent sum. For j = 1 the classes π x'_i are the p-power part of the basis above. They span the tails of the successive approximation of relators in normal form.

At p = 2 the bracket [x'_0, x'_1] in gr_1(freeProP 2 (Fin 2)) is therefore nonzero, and the degree-zero power-defect formula shows that the 2-power operator on this free pro-2 group is not additive.

Main definitions #

Main results #

References #

The detecting groups #

The lower p-series of a finite discrete group is its abstract lower p-central series, so the computations below are transported from TauCeti.HeisenbergGroup.pLowerCentralSeries_top_two_eq_bot along a group isomorphism, which lets the detecting groups live in any universe. The cyclic detecting groups ℤ/pⁿ are handled in the same way by MulEquiv.pLowerCentralSeries_eq_bot_multiplicative_zmod_pow and MulEquiv.gradedPowIter_gradedMkZero_ne_zero_multiplicative_zmod_pow.

source
theorem MulEquiv.pLowerCentralSeries_two_eq_bot_heisenbergGroup {p : ℕ} {H : Type u} [Group H] [TopologicalSpace H] [DiscreteTopology H] (e : H ≃* TauCeti.HeisenbergGroup (ZMod p)) :
TauCeti.pLowerCentralSeries p H 2 = ⊥

A discrete group isomorphic to the Heisenberg group over ZMod p has p-class at most two.

source
theorem MulEquiv.gradedPow_gradedMkZero_eq_zero_heisenbergGroup {p : ℕ} {H : Type u} [Group H] [TopologicalSpace H] [DiscreteTopology H] (e : H ≃* TauCeti.HeisenbergGroup (ZMod p)) {a : TauCeti.HeisenbergGroup (ZMod p)} (ha : a.z = 0) (ha' : a.x * a.y = 0) :
TauCeti.gradedPow p H 0 (TauCeti.gradedMkZero p H (e.symm a)) = 0

In a discrete group isomorphic to the Heisenberg group over ZMod p, the p-power classes of the two standard generators (1, 0, 0) and (0, 1, 0) vanish: their p-th powers are trivial.

source
theorem MulEquiv.gradedBracket_gradedMkZero_ne_zero_heisenbergGroup {p : ℕ} {H : Type u} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Fact (Nat.Prime p)] (e : H ≃* TauCeti.HeisenbergGroup (ZMod p)) :
((TauCeti.gradedBracket p H 0 0) (TauCeti.gradedMkZero p H (e.symm { x := 1, y := 0, z := 0 }))) (TauCeti.gradedMkZero p H (e.symm { x := 0, y := 1, z := 0 })) ≠ 0

In a discrete group isomorphic to the Heisenberg group over 𝔽_p, the bracket of the classes of the two standard generators (1, 0, 0) and (0, 1, 0) is nonzero.

Exponent sums along the lower p-series #

The character TauCeti.freeProP.exponentSumZModPow (k + 1) i of the i-th exponent sum modulo p ^ (k + 1) takes values in the discrete cyclic group ℤ/pᵏ⁺¹, whose lower p-series stops at λ_{k+1} = 1. So the graded map it induces on gr_k(F) detects the divisibility of the i-th exponent sum by p ^ (k + 1), and it reads off the coefficient of π^k x'_i.

source
theorem TauCeti.freeProP.dvd_exponentSum_of_mem_pLowerCentralSeries {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {k : ℕ} {y : freeProP p X} (hy : y ∈ pLowerCentralSeries p (freeProP p X) k) (i : X) :
↑p ^ k ∣ Multiplicative.toAdd ((exponentSum p X) y) i

Exponent sums along the lower p-series: the exponent sums of an element of λ_k(F) are divisible by p ^ k.

source
@[simp]
theorem TauCeti.freeProP.padicPow_mem_pLowerCentralSeries_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (i : X) (a : ℤ_[p]) (k : ℕ) :
⋯.padicPow (of i) a ∈ pLowerCentralSeries p (freeProP p X) k ↔ ↑p ^ k ∣ a

A p-adic power of a free generator lies in the k-th lower p-series subgroup exactly when its exponent is divisible by p ^ k in ℤ_p.

source
theorem TauCeti.freeProP.mem_topologicalClosure_closure_singleton_inf_pLowerCentralSeries_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (i : X) (y : freeProP p X) (k : ℕ) :
y ∈ (Subgroup.closure {of i}).topologicalClosure ⊓ pLowerCentralSeries p (freeProP p X) k ↔ ∃ (a : ℤ_[p]), ↑p ^ k ∣ a ∧ ⋯.padicPow (of i) a = y

The intersection of the closed procyclic subgroup generated by x_i with λ_k(F) consists exactly of the p-adic powers x_i ^ a whose exponent is divisible by p ^ k.

source
theorem TauCeti.freeProP.gradedMap_exponentSumZModPow_gradedMk_eq_zero_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {k : ℕ} (i : X) (y : ↥(pLowerCentralSeries p (freeProP p X) k)) :
(gradedMap p (exponentSumZModPow p X (k + 1) i).toMonoidHom ⋯ k) (gradedMk p (freeProP p X) k y) = 0 ↔ ↑p ^ (k + 1) ∣ Multiplicative.toAdd ((exponentSum p X) ↑y) i

Detecting divisibility on a graded piece: the graded map induced on gr_k(F) by the i-th exponent sum modulo p ^ (k + 1) kills the class of y ∈ λ_k(F) exactly when p ^ (k + 1) divides the i-th exponent sum of y.

source
theorem TauCeti.freeProP.gradedMap_exponentSumZModPow_gradedPowIter_gradedMkZero_of_self {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (k : ℕ) (i : X) :
(gradedMap p (exponentSumZModPow p X (k + 1) i).toMonoidHom ⋯ k) (gradedPowIter p (freeProP p X) k (gradedMkZero p (freeProP p X) (of i))) = gradedPowIter p (ULift.{u, 0} (Multiplicative (ZMod (p ^ (k + 1))))) k (gradedMkZero p (ULift.{u, 0} (Multiplicative (ZMod (p ^ (k + 1))))) (MulEquiv.ulift.symm (Multiplicative.ofAdd 1)))

The graded map induced by the i-th exponent sum modulo p ^ (k + 1) sends π^k x'_i to the class π^k of the standard generator of ℤ/pᵏ⁺¹.

source
theorem TauCeti.freeProP.gradedMap_exponentSumZModPow_gradedPowIter_gradedMkZero_of_self_ne_zero {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (k : ℕ) (i : X) :
(gradedMap p (exponentSumZModPow p X (k + 1) i).toMonoidHom ⋯ k) (gradedPowIter p (freeProP p X) k (gradedMkZero p (freeProP p X) (of i))) ≠ 0

The graded map induced by the i-th exponent sum modulo p ^ (k + 1) does not kill π^k x'_i: the class π^k of the standard generator of ℤ/pᵏ⁺¹ is nonzero.

source
theorem TauCeti.freeProP.gradedMap_exponentSumZModPow_gradedPowIter_gradedMkZero_of_of_ne {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (k : ℕ) {i j : X} (hij : j ≠ i) :
(gradedMap p (exponentSumZModPow p X (k + 1) i).toMonoidHom ⋯ k) (gradedPowIter p (freeProP p X) k (gradedMkZero p (freeProP p X) (of j))) = 0

The graded map induced by the i-th exponent sum modulo p ^ (k + 1) kills π^k x'_j for j ≠ i.

The basis of gr_1 of a free pro-p group #

source
theorem TauCeti.freeProP.span_range_degreeOneFamily_of_eq_top (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] [LinearOrder X] :
Submodule.span (ZMod p) (Set.range (degreeOneFamily p of)) = ⊤

Spanning: the p-power classes and the brackets of the generator classes span gr_1(freeProP p X).

source
theorem TauCeti.freeProP.linearIndependent_degreeOneFamily_of (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] [LinearOrder X] :
LinearIndependent (ZMod p) (degreeOneFamily p of)

Linear independence: the p-power classes π x'_i and the brackets [x'_i, x'_j] for i < j of the generator classes are linearly independent in gr_1(freeProP p X). The coefficient of π x'_i is read off in ℤ/p², and the coefficient of [x'_i, x'_j] in the Heisenberg group over 𝔽_p.

source
theorem TauCeti.freeProP.linearIndependent_gradedPowIter_gradedMkZero_of (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) (j : ℕ) :
LinearIndependent (ZMod p) fun (i : X) => gradedPowIter p (freeProP p X) j (gradedMkZero p (freeProP p X) (of i))

The iterated p-powers of the generator classes are linearly independent: for every j, the classes π^j x'_i ∈ gr_j(freeProP p X) of the p ^ j-th powers of the generators are linearly independent. The coefficient of π^j x'_i is read off in ℤ/pʲ⁺¹, by sending x_i to the generator and the other generators to 1.

source
noncomputable def TauCeti.freeProP.degreeOneBasis (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] [LinearOrder X] :
Module.Basis (X ⊕ { ij : X × X // ij.1 < ij.2 }) (ZMod p) (gradedPiece p (freeProP p X) 1)

The standard basis of gr_1 of a free pro-p group of finite rank: the p-power classes π x'_i for i ∈ X and the brackets [x'_i, x'_j] for i < j of the generator classes, indexed by X ⊕ {ij : X × X // ij.1 < ij.2}.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.freeProP.degreeOneBasis_apply (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] [LinearOrder X] (k : X ⊕ { ij : X × X // ij.1 < ij.2 }) :
    (degreeOneBasis p X) k = degreeOneFamily p of k
    source
    theorem TauCeti.freeProP.span_gradedMkZero_image_range_of_eq_top (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] :
    Submodule.span (ZMod p) (gradedMkZero p (freeProP p X) '' Set.range of) = ⊤

    The generator classes span gr_0 of a free pro-p group of finite rank.

    source
    noncomputable def TauCeti.freeProP.degreeZeroBasis (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] :
    Module.Basis X (ZMod p) (gradedPiece p (freeProP p X) 0)

    The basis of gr_0 of a free pro-p group of finite rank formed by the classes x'_i = ⟦x_i⟧ of the generators: the basis TauCeti.freeProP.frattiniQuotientBasis of the Frattini quotient F ⧸ Φ(F), transported along gr_0(F) ≅ F ⧸ λ_1(F) = F ⧸ Φ(F).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.freeProP.degreeZeroBasis_apply (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] (i : X) :
      (degreeZeroBasis p X) i = gradedMkZero p (freeProP p X) (of i)
      source
      theorem TauCeti.freeProP.finrank_gradedPiece_one (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [LinearOrder X] [Fintype X] :
      Module.finrank (ZMod p) (gradedPiece p (freeProP p X) 1) = Fintype.card X + (Fintype.card X).choose 2

      The dimension of gr_1 of a free pro-p group of finite rank is #X + (#X choose 2): gr_1(F) ≅ 𝔽_p^X ⊕ Λ²(𝔽_p^X).

      source
      @[simp]
      theorem TauCeti.freeProP.natCard_gradedPiece_one (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Finite X] :
      Nat.card (gradedPiece p (freeProP p X) 1) = p ^ (Nat.card X + (Nat.card X).choose 2)

      The degree-one graded piece of the free pro-p group on a finite type X has p ^ (#X + (#X choose 2)) elements.

      The spans of the iterated p-power classes #

      source
      noncomputable def TauCeti.freeProP.gradedPowIterSpan (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) (S : Set X) (j : ℕ) :
      Submodule (ZMod p) (gradedPiece p (freeProP p X) j)

      The span of the p-power classes of a set of generators: for S : Set X, the subspace of gr_j(F) spanned by the iterated p-powers π^j x'_i of the generator classes x'_i ∈ gr_0(F) with i ∈ S. The vectors π^j x'_i are linearly independent, so when S is finite it has dimension #S (TauCeti.freeProP.finrank_gradedPowIterSpan), and above degree zero π carries it onto the span in the next degree (TauCeti.freeProP.gradedPowIterSpan_succ). The tails of the successive-approximation arguments of the classification of Demushkin groups are its instances at the index sets those arguments leave free.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem TauCeti.freeProP.gradedPowIterSpan_def {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (S : Set X) (j : ℕ) :
        gradedPowIterSpan p X S j = Submodule.span (ZMod p) ((fun (i : X) => gradedPowIter p (freeProP p X) j (gradedMkZero p (freeProP p X) (of i))) '' S)

        The span of the p-power classes over S is the span of the image of S under i ↦ π^j x'_i.

        source
        @[simp]
        theorem TauCeti.freeProP.gradedPowIter_mem_gradedPowIterSpan_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {S : Set X} {i : X} {j : ℕ} :
        gradedPowIter p (freeProP p X) j (gradedMkZero p (freeProP p X) (of i)) ∈ gradedPowIterSpan p X S j ↔ i ∈ S

        Generator membership in the span of the p-power classes: an iterated power π^j x'_i belongs to the span over S if and only if i ∈ S, because the π^j x'_i are linearly independent (TauCeti.freeProP.linearIndependent_gradedPowIter_gradedMkZero_of).

        source
        @[simp]
        theorem TauCeti.freeProP.gradedPowIterSpan_le_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {S : Set X} {j : ℕ} {W : Submodule (ZMod p) (gradedPiece p (freeProP p X) j)} :
        gradedPowIterSpan p X S j ≤ W ↔ ∀ i ∈ S, gradedPowIter p (freeProP p X) j (gradedMkZero p (freeProP p X) (of i)) ∈ W

        A submodule contains the span of the p-power classes over S if and only if it contains every generator π^j x'_i with i ∈ S.

        source
        theorem TauCeti.freeProP.gradedPowIterSpan_mono {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {S T : Set X} (h : S ⊆ T) (j : ℕ) :
        gradedPowIterSpan p X S j ≤ gradedPowIterSpan p X T j

        The span of the p-power classes is monotone in the index set.

        source
        theorem TauCeti.freeProP.gradedPowIterSpan_succ {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (S : Set X) {j : ℕ} (hj : 1 ≤ j) :
        gradedPowIterSpan p X S (j + 1) = Submodule.map (AddMonoidHom.toZModLinearMap p (gradedPowAddMonoidHom p (freeProP p X) hj)) (gradedPowIterSpan p X S j)

        π carries the span of the p-power classes onto the span in the next degree above degree zero: for j ≥ 1, the span over S in degree j + 1 is the image under π of the span over S in degree j, since π is additive on gr_j(F) and π (π^j x'_i) = π^{j+1} x'_i.

        source
        theorem TauCeti.freeProP.finrank_gradedPowIterSpan {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (S : Set X) [Finite ↑S] (j : ℕ) :
        Module.finrank (ZMod p) ↥(gradedPowIterSpan p X S j) = Nat.card ↑S

        The dimension of the span of the p-power classes over S is the cardinality of S, because the π^j x'_i are linearly independent (TauCeti.freeProP.linearIndependent_gradedPowIter_gradedMkZero_of).

        source
        theorem TauCeti.freeProP.mem_gradedPowIterSpan_iff_exists_finsupp {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {S : Set X} {j : ℕ} {v : gradedPiece p (freeProP p X) j} :
        v ∈ gradedPowIterSpan p X S j ↔ ∃ (c : ↑S →₀ ZMod p), (c.sum fun (i : ↑S) (a : ZMod p) => a • gradedPowIter p (freeProP p X) j (gradedMkZero p (freeProP p X) (of ↑i))) = v

        Membership in the span of the p-power classes: the elements of the span over S are the finitely supported linear combinations of the π^j x'_i over the indices i ∈ S. For a finite index set, TauCeti.freeProP.mem_gradedPowIterSpan_iff states this with a plain coefficient function.

        source
        theorem TauCeti.freeProP.mem_gradedPowIterSpan_iff {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {S : Set X} [Fintype ↑S] {j : ℕ} {v : gradedPiece p (freeProP p X) j} :
        v ∈ gradedPowIterSpan p X S j ↔ ∃ (c : ↑S → ZMod p), ∑ i : ↑S, c i • gradedPowIter p (freeProP p X) j (gradedMkZero p (freeProP p X) (of ↑i)) = v

        Membership in the span of the p-power classes over a finite index set: the elements of the span over a finite S are the linear combinations of the π^j x'_i over the indices i ∈ S. This is the finite-sum form of TauCeti.freeProP.mem_gradedPowIterSpan_iff_exists_finsupp.

        The dyadic failure of additivity #

        source
        theorem TauCeti.gradedBracket_freeProP_two_ne_zero (x y : gradedPiece 2 (freeProP 2 (Fin 2)) 0) (hx : x = gradedMk 2 (freeProP 2 (Fin 2)) 0 ⟨freeProP.of 0, gradedBracket_freeProP_two_ne_zero._proof_1⟩) (hy : y = gradedMk 2 (freeProP 2 (Fin 2)) 0 ⟨freeProP.of 1, gradedBracket_freeProP_two_ne_zero._proof_2⟩) :
        ((gradedBracket 2 (freeProP 2 (Fin 2)) 0 0) x) y ≠ 0

        In the free pro-2 group of rank two, the bracket of the two canonical generator classes is nonzero in degree one.

        source
        theorem TauCeti.gradedPow_add_freeProP_two_ne (x y : gradedPiece 2 (freeProP 2 (Fin 2)) 0) (hx : x = gradedMk 2 (freeProP 2 (Fin 2)) 0 ⟨freeProP.of 0, gradedBracket_freeProP_two_ne_zero._proof_1⟩) (hy : y = gradedMk 2 (freeProP 2 (Fin 2)) 0 ⟨freeProP.of 1, gradedBracket_freeProP_two_ne_zero._proof_2⟩) :
        gradedPow 2 (freeProP 2 (Fin 2)) 0 (x + y) ≠ gradedPow 2 (freeProP 2 (Fin 2)) 0 x + gradedPow 2 (freeProP 2 (Fin 2)) 0 y

        The 2-power operator fails additivity on the two canonical generator classes of the free pro-2 group of rank two.

        source
        theorem TauCeti.gradedPow_freeProP_two_not_additive :
        ¬∀ (x y : gradedPiece 2 (freeProP 2 (Fin 2)) 0), gradedPow 2 (freeProP 2 (Fin 2)) 0 (x + y) = gradedPow 2 (freeProP 2 (Fin 2)) 0 x + gradedPow 2 (freeProP 2 (Fin 2)) 0 y

        The degree-zero 2-power operator of the free pro-2 group of rank two is not additive.