Documentation

TauCeti.Topology.Algebra.Group.LowerCentralSeries.Graded.LieRing

The graded Lie ring of the lower p-series #

For a topological group G and p : ℕ, the graded pieces gr_k(G) = λ_k ⧸ λ_{k+1} of the lower p-series carry the bracket TauCeti.gradedBracket p G j k : gr_j(G) →+ gr_k(G) →+ gr_{j+k+1}(G) induced by the group commutator, alternating and satisfying the Jacobi identity degree by degree. This file assembles these brackets into a Lie ring structure on the direct sum

⨁ k, gr_k(G),

on which the bracket of homogeneous elements of degrees j and k is their graded bracket, of degree j + k + 1 (TauCeti.of_lie_of); the shift by one is because the series is 0-based. Every graded piece is killed by p, so the direct sum is a Lie algebra over ZMod p. For p = 0 this is the graded Lie ring ⨁ n, γ_n(G) ⧸ γ_{n+1}(G) of the closed lower central series, whose pieces are TauCeti.lcsGradedPiece G n = gradedPiece 0 G n, as a Lie algebra over ZMod 0 = ℤ.

A continuous homomorphism G →* H induces a Lie algebra homomorphism of the graded Lie rings (TauCeti.gradedLieHom), functorially.

When G is a pro-ℓ group for a prime ℓ, each graded piece is an abelian pro-ℓ group, hence a ℤ_ℓ-module (TauCeti.IsProP.gradedPieceModule), and the graded bracket is ℤ_ℓ-bilinear. The direct sum of these modules is then a Lie algebra over ℤ_ℓ (TauCeti.IsProP.gradedLieAlgebra).

Main definitions #

Main results #

References #

source
@[simp]
theorem TauCeti.of_gradedCast {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (h : j = k) (x : gradedPiece p G j) :
(DirectSum.of (gradedPiece p G) k) ((gradedCast p G h) x) = (DirectSum.of (gradedPiece p G) j) x

Transport along an equality of degrees does not change an element of the direct sum of the graded pieces.

The bracket on the direct sum #

source
def TauCeti.gradedLieBracket (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
(DirectSum ℕ fun (k : ℕ) => gradedPiece p G k) →+ (DirectSum ℕ fun (k : ℕ) => gradedPiece p G k) →+ DirectSum ℕ fun (k : ℕ) => gradedPiece p G k

The graded bracket on the direct sum ⨁ k, gr_k(G), as a biadditive map: the biadditive extension of the graded brackets, which on homogeneous elements of degrees j and k is TauCeti.gradedBracket p G j k, landing in degree j + k + 1 (TauCeti.of_lie_of). It is the bracket of the graded Lie ring (TauCeti.gradedLieBracket_apply).

Instances For
    source
    @[instance_reducible]
    instance TauCeti.instBracketDirectSumNatGradedPiece {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Bracket (DirectSum ℕ fun (k : ℕ) => gradedPiece p G k) (DirectSum ℕ fun (k : ℕ) => gradedPiece p G k)

    The bracket of the graded Lie ring ⨁ k, gr_k(G), given by TauCeti.gradedLieBracket.

    source
    @[simp]
    theorem TauCeti.gradedLieBracket_apply {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x y : DirectSum ℕ fun (k : ℕ) => gradedPiece p G k) :
    ((gradedLieBracket p G) x) y = ⁅x, y⁆

    The biadditive map TauCeti.gradedLieBracket is the bracket of the graded Lie ring.

    source
    @[simp]
    theorem TauCeti.of_lie_of {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G k) :
    ⁅(DirectSum.of (gradedPiece p G) j) x, (DirectSum.of (gradedPiece p G) k) y⁆ = (DirectSum.of (gradedPiece p G) (j + k + 1)) (((gradedBracket p G j k) x) y)

    The bracket of homogeneous elements of degrees j and k is their graded bracket, of degree j + k + 1.

    source
    theorem TauCeti.gradedLieBracket_flip {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    (gradedLieBracket p G).flip = -gradedLieBracket p G

    Skew-symmetry of the graded bracket on the direct sum: [y, x] = -[x, y].

    source
    @[instance_reducible]
    instance TauCeti.instLieRingDirectSumNatGradedPiece {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    LieRing (DirectSum ℕ fun (k : ℕ) => gradedPiece p G k)

    The graded Lie ring ⨁ k, gr_k(G) of the lower p-series: the graded brackets are alternating and satisfy the Jacobi identity degree by degree, hence so does their biadditive extension to the direct sum.

    source
    @[instance_reducible]
    instance TauCeti.instLieAlgebraZModDirectSumNatGradedPiece {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    LieAlgebra (ZMod p) (DirectSum ℕ fun (k : ℕ) => gradedPiece p G k)

    Every graded piece is a ZMod p-module and the graded bracket is biadditive, so the graded Lie ring is a Lie algebra over ZMod p.

    Functoriality #

    source
    def TauCeti.gradedLieHom (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) :
    (DirectSum ℕ fun (k : ℕ) => gradedPiece p G k) →ₗ⁅ZMod p⁆ DirectSum ℕ fun (k : ℕ) => gradedPiece p H k

    The graded Lie homomorphism of a continuous homomorphism f : G →* H: the graded maps TauCeti.gradedMap p f hf k of all degrees, assembled into a homomorphism of graded Lie algebras ⨁ k, gr_k(G) →ₗ⁅ZMod p⁆ ⨁ k, gr_k(H). Its value on homogeneous elements is TauCeti.gradedLieHom_of.

    Instances For
      source
      @[simp]
      theorem TauCeti.gradedLieHom_of {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (k : ℕ) (x : gradedPiece p G k) :
      (gradedLieHom p f hf) ((DirectSum.of (gradedPiece p G) k) x) = (DirectSum.of (gradedPiece p H) k) ((gradedMap p f hf k) x)

      The graded Lie homomorphism of f is the graded map of f in each degree.

      source
      @[simp]
      theorem TauCeti.gradedLieHom_id {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
      gradedLieHom p (MonoidHom.id G) ⋯ = LieHom.id

      The identity of G induces the identity of the graded Lie ring.

      source
      theorem TauCeti.gradedLieHom_comp {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {K : Type w} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] (g : H →* K) (hg : Continuous ⇑g) (f : G →* H) (hf : Continuous ⇑f) :
      gradedLieHom p (g.comp f) ⋯ = (gradedLieHom p g hg).comp (gradedLieHom p f hf)

      The graded Lie homomorphism of a composite is the composite of the graded Lie homomorphisms: the graded Lie ring is a functor.

      The ℤ_ℓ-Lie algebra of a pro-ℓ group #

      source
      @[instance_reducible]
      noncomputable def TauCeti.IsProP.gradedLieAlgebra (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP ℓ G) :
      LieAlgebra ℤ_[ℓ] (DirectSum ℕ fun (k : ℕ) => gradedPiece p G k)

      The ℤ_ℓ-Lie algebra of a pro-ℓ group. For a pro-ℓ group G, the graded Lie ring ⨁ k, gr_k(G) of the lower p-series is a Lie algebra over ℤ_ℓ, for the ℤ_ℓ-module structure which in each degree is TauCeti.IsProP.gradedPieceModule: the graded bracket is ℤ_ℓ-bilinear. For p = 0 this is the ℤ_ℓ-Lie algebra of the closed lower central series.

      Instances For