Documentation

TauCeti.Topology.Algebra.Group.Profinite.Free.Rank

The generator rank of a free pro-p group #

The canonical generators of freeProP p X generate it topologically (freeProP.topologicalClosure_closure_range_of_eq_top), so for finite X the free pro-p group is topologically finitely generated (isTopologicallyFinitelyGenerated_freeProP). In the Frattini quotient freeProP p X β§Έ proPFrattini p (freeProP p X), an 𝔽_p-vector space, the classes of the generators are linearly independent: any assignment of exponents modulo p to the generators is realised by a continuous character of the free pro-p group, through its universal property. For finite X the classes also span, by Burnside's basis theorem, so they form a basis indexed by X. The Frattini quotient is therefore 𝔽_p^X, and the topological generator rank of freeProP p X is the cardinality of X, in natural-number and in cardinal form.

For X of any cardinality the universal property identifies the continuous 𝔽_p-valued characters of freeProP p X with the arbitrary functions X β†’ 𝔽_p (freeProP.continuousZModDualEquiv), so by Burnside's basis theorem in cardinal form the topological generator rank is the 𝔽_p-dimension of 𝔽_p^X. For finite X this is #X again; for infinite X the ErdΕ‘s–Kaplansky theorem gives the dimension p ^ #X, which is strictly larger than #X (Ribes–Zalesskii, Section 3.3). This is why the free objects of infinite rank, whose bases converge to 1, are indexed by a profinite space rather than by a discrete type.

For finite X the continuous 𝔽_p-dual has the basis dual to the generators (freeProP.dualBasis), and the automorphisms of freeProP p X act on it through their transposes. A family of elements whose classes span the Frattini quotient is the image of the generators under a continuous automorphism (Burnside's basis theorem and the Hopf property of topologically finitely generated profinite groups), and every linear automorphism of the continuous dual is the transpose of a continuous automorphism of freeProP p X.

Main definitions #

Main results #

References #

source
theorem TauCeti.freeProP.linearIndependent_frattiniQuotient_of (p : β„•) (X : Type u) [Fact (Nat.Prime p)] :
LinearIndependent (ZMod p) fun (x : X) => Additive.ofMul ((QuotientGroup.mk' (proPFrattini p (freeProP p X))) (of x))

The classes of the generators in the Frattini quotient are linearly independent over 𝔽_p, for a generating type X of any cardinality.

Continuous characters of a free pro-p group #

source
noncomputable def TauCeti.freeProP.characterOfFun (p : β„•) (X : Type u) [Fact (Nat.Prime p)] (f : X β†’ ZMod p) :
freeProP p X β†’β‚œ* Multiplicative (ZMod p)

The continuous 𝔽_p-valued character of the free pro-p group on X taking the value f x at the generator x, for an arbitrary function f : X β†’ ZMod p: the universal property applied to the finite p-group β„€/p, lifted to the universe of X.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.freeProP.characterOfFun_of (p : β„•) (X : Type u) [Fact (Nat.Prime p)] (f : X β†’ ZMod p) (x : X) :
    (characterOfFun p X f) (of x) = Multiplicative.ofAdd (f x)

    The character attached to f takes the value f x at the generator x.

    source
    noncomputable def TauCeti.freeProP.continuousZModDualEquiv (p : β„•) (X : Type u) [Fact (Nat.Prime p)] :
    continuousZModDual p (freeProP p X) ≃ₗ[ZMod p] X β†’ ZMod p

    The continuous 𝔽_p-dual of a free pro-p group is 𝔽_p^X. Evaluation at the generators identifies the continuous characters of freeProP p X with the arbitrary functions X β†’ 𝔽_p, as 𝔽_p-vector spaces; the inverse is TauCeti.freeProP.characterOfFun. No finiteness of X is needed.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.freeProP.continuousZModDualEquiv_apply (p : β„•) (X : Type u) [Fact (Nat.Prime p)] (Ο† : continuousZModDual p (freeProP p X)) (x : X) :
      (continuousZModDualEquiv p X) Ο† x = Multiplicative.toAdd ((Additive.toMul Ο†) (of x))
      source
      @[simp]
      theorem TauCeti.freeProP.continuousZModDualEquiv_symm_apply (p : β„•) (X : Type u) [Fact (Nat.Prime p)] (f : X β†’ ZMod p) :
      (continuousZModDualEquiv p X).symm f = Additive.ofMul (characterOfFun p X f)

      Finite rank #

      source
      noncomputable def TauCeti.freeProP.frattiniQuotientBasis (p : β„•) (X : Type u) [Fact (Nat.Prime p)] [Finite X] :
      Module.Basis X (ZMod p) (Additive (freeProP p X β§Έ proPFrattini p (freeProP p X)))

      The Frattini quotient of a free pro-p group of finite rank is 𝔽_p^X. For finite X the classes of the generators form a basis of the Frattini quotient of freeProP p X, indexed by X.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.freeProP.frattiniQuotientBasis_apply (p : β„•) (X : Type u) [Fact (Nat.Prime p)] [Finite X] (x : X) :
        (frattiniQuotientBasis p X) x = Additive.ofMul ((QuotientGroup.mk' (proPFrattini p (freeProP p X))) (of x))

        The basis vector of the Frattini quotient at x is the class of the generator at x.

        source
        @[simp]
        theorem TauCeti.freeProP.finrank_quotient_proPFrattini (p : β„•) (X : Type u) [Fact (Nat.Prime p)] [Finite X] :
        Module.finrank (ZMod p) (Additive (freeProP p X β§Έ proPFrattini p (freeProP p X))) = Nat.card X

        The Frattini quotient of the free pro-p group on a finite type X has dimension Nat.card X over 𝔽_p.

        The dual basis of the generators #

        source
        noncomputable def TauCeti.freeProP.dualBasis (p : β„•) (X : Type u) [Fact (Nat.Prime p)] [Finite X] :
        Module.Basis X (ZMod p) (continuousZModDual p (freeProP p X))

        The dual basis of the generators: the basis of the continuous 𝔽_p-dual of freeProP p X whose i-th vector is the coordinate character x_j ↦ Ξ΄_{ij}.

        Equations
        Instances For
          source
          instance TauCeti.freeProP.instFiniteZModContinuousZModDual (p : β„•) (X : Type u) [Fact (Nat.Prime p)] [Finite X] :
          Module.Finite (ZMod p) (continuousZModDual p (freeProP p X))

          The continuous 𝔽_p-dual of a free pro-p group of finite rank is finite-dimensional.

          source
          theorem TauCeti.freeProP.dualBasis_apply (p : β„•) (X : Type u) [Fact (Nat.Prime p)] [Finite X] [DecidableEq X] (i : X) :
          (dualBasis p X) i = Additive.ofMul (characterOfFun p X (Pi.single i 1))

          The i-th vector of the dual basis is the character reading off the exponent of x_i.

          source
          @[simp]
          theorem TauCeti.freeProP.toMul_dualBasis_of (p : β„•) (X : Type u) [Fact (Nat.Prime p)] [Finite X] [DecidableEq X] (i j : X) :
          (Additive.toMul ((dualBasis p X) i)) (of j) = Multiplicative.ofAdd (Pi.single i 1 j)

          The i-th coordinate character takes the value Ξ΄_{ij} at the generator x_j.

          source
          @[simp]
          theorem TauCeti.freeProP.dualBasis_repr (p : β„•) (X : Type u) [Fact (Nat.Prime p)] [Finite X] (Ο‡ : continuousZModDual p (freeProP p X)) (i : X) :
          ((dualBasis p X).repr Ο‡) i = Multiplicative.toAdd ((Additive.toMul Ο‡) (of i))

          The i-th coordinate of a character in the dual basis is its value at the generator x_i.

          source
          theorem TauCeti.freeProP.toMul_dualBasis_freeProPGen (p : β„•) [Fact (Nat.Prime p)] {n : β„•} (k : Fin n) (a : β„•) :
          Multiplicative.toAdd ((Additive.toMul ((dualBasis p (Fin n)) k)) (freeProPGen p n a)) = if ↑k = a then 1 else 0

          The k-th coordinate character of freeProP p (Fin n) takes the value Ξ΄_{k a} at the β„•-indexed generator x_a, including out of range, where x_a = 1.

          Automorphisms of a free pro-p group of finite rank #

          source
          noncomputable def TauCeti.freeProP.continuousMulEquivOfTopologicallyGenerates {p : β„•} {X : Type u} [Finite X] (y : X β†’ freeProP p X) (hy : (Subgroup.closure (Set.range y)).topologicalClosure = ⊀) :
          freeProP p X β‰ƒβ‚œ* freeProP p X

          The automorphism of a free pro-p group of finite rank sending the generators to a topological generating family. The endomorphism x_i ↦ y_i is surjective because the y_i generate topologically, hence bijective by the Hopf property of topologically finitely generated profinite groups.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.freeProP.continuousMulEquivOfTopologicallyGenerates_of {p : β„•} {X : Type u} [Finite X] (y : X β†’ freeProP p X) (hy : (Subgroup.closure (Set.range y)).topologicalClosure = ⊀) (i : X) :
            (continuousMulEquivOfTopologicallyGenerates y hy) (of i) = y i

            The automorphism attached to a topological generating family sends the generators to it.

            source
            theorem TauCeti.freeProP.exists_continuousMulEquiv_continuousZModDualMap_eq {p : β„•} {X : Type u} [Fact (Nat.Prime p)] [Finite X] (S : continuousZModDual p (freeProP p X) ≃ₗ[ZMod p] continuousZModDual p (freeProP p X)) :
            βˆƒ (e : freeProP p X β‰ƒβ‚œ* freeProP p X), βˆ€ (Ο‡ : continuousZModDual p (freeProP p X)), (↑e).continuousZModDualMap Ο‡ = S Ο‡

            Every linear automorphism of the continuous 𝔽_p-dual of a free pro-p group of finite rank is the transpose of a continuous automorphism. Given S, a dual family y of the basis S⁻¹ Ο‡_i, where Ο‡_i is the dual basis of the generators, satisfies Ο‡ (y_j) = (S Ο‡)(x_j) for every character Ο‡; it generates topologically, by Burnside's basis theorem, and the automorphism x_j ↦ y_j has transpose S.

            source
            theorem TauCeti.freeProP.exists_continuousMulEquiv_continuousZModDualMap_eq_and_apply_of_eq_of_forall_toMul_of_eq {p : β„•} {X : Type u} [Fact (Nat.Prime p)] [Finite X] (S : continuousZModDual p (freeProP p X) ≃ₗ[ZMod p] continuousZModDual p (freeProP p X)) {T : Set X} (hT : βˆ€ j ∈ T, βˆ€ (Ο‡ : continuousZModDual p (freeProP p X)), (Additive.toMul (S Ο‡)) (of j) = (Additive.toMul Ο‡) (of j)) :
            βˆƒ (e : freeProP p X β‰ƒβ‚œ* freeProP p X), (βˆ€ (Ο‡ : continuousZModDual p (freeProP p X)), (↑e).continuousZModDualMap Ο‡ = S Ο‡) ∧ βˆ€ j ∈ T, e (of j) = of j

            A linear automorphism of the dual is the transpose of an automorphism fixing prescribed generators. If S acts trivially on the values at the generators x_j, j ∈ T, in the sense that (S Ο‡) (x_j) = Ο‡ (x_j) for every character Ο‡, then S is the transpose of a continuous automorphism e with e (x_j) = x_j for every j ∈ T.

            source
            theorem TauCeti.topologicalGeneratorRank_freeProP_eq_rank (p : β„•) {X : Type u} [Fact (Nat.Prime p)] :
            topologicalGeneratorRank (freeProP p X) = Module.rank (ZMod p) (X β†’ ZMod p)

            The rank of a free pro-p group is the dimension of 𝔽_p^X, for a generating type X of any cardinality: Burnside's basis theorem in cardinal form, read through the continuous dual TauCeti.freeProP.continuousZModDualEquiv.

            source
            theorem TauCeti.topologicalGeneratorRank_freeProP_of_infinite (p : β„•) {X : Type u} [Fact (Nat.Prime p)] [Infinite X] :
            topologicalGeneratorRank (freeProP p X) = ↑p ^ Cardinal.mk X

            The free pro-p group on an infinite type X has rank p ^ #X. The continuous dual is 𝔽_p^X, whose dimension over 𝔽_p is its cardinality by the ErdΕ‘s–Kaplansky theorem.

            source
            theorem TauCeti.mk_lt_topologicalGeneratorRank_freeProP (p : β„•) {X : Type u} [Fact (Nat.Prime p)] [Infinite X] :
            Cardinal.mk X < topologicalGeneratorRank (freeProP p X)

            An infinite type is strictly smaller than the rank of the free pro-p group on it: the rank is p ^ #X, not #X.

            source
            @[simp]
            theorem TauCeti.topologicalGeneratorRankNat_freeProP (p : β„•) {X : Type u} [Fact (Nat.Prime p)] [Finite X] (h : IsTopologicallyFinitelyGenerated (freeProP p X)) :
            topologicalGeneratorRankNat (freeProP p X) h = Nat.card X

            The free pro-p group on a finite type X has topological generator rank Nat.card X, in natural-number form.

            source
            @[simp]
            theorem TauCeti.topologicalGeneratorRank_freeProP (p : β„•) {X : Type u} [Fact (Nat.Prime p)] [Finite X] :
            topologicalGeneratorRank (freeProP p X) = Cardinal.mk X

            The free pro-p group on a finite type X has topological generator rank #X, in cardinal form.