The graded deviation of an endomorphism congruent to the identity

Let G be a topological group with lower p-series λ_k = TauCeti.pLowerCentralSeries p G k, and let θ : G →* G be a continuous endomorphism that is congruent to the identity modulo λ_m: g⁻¹ * θ g ∈ λ_m for every g. Then g⁻¹ * θ g ∈ λ_{m+k} for g ∈ λ_k, and the assignment g ↦ g⁻¹ * θ g induces additive maps

D_k : gr_k(G) →+ gr_{m+k}(G)

on the graded pieces gr_k(G) = λ_k ⧸ λ_{k+1}, the graded deviation of θ. The map g ↦ g⁻¹ * θ g is a crossed homomorphism, (g * h)⁻¹ * θ (g * h) = (h⁻¹ * (g⁻¹ * θ g) * h) * (h⁻¹ * θ h), and the conjugation acts trivially on the relevant graded piece; this is what makes D_k well defined and additive.

For m ≥ 1 the deviation is a derivation of the graded structure: it satisfies the Leibniz rule D [x, y] = [D x, y] + [x, D y] against the bracket, and it commutes with the p-power operator π in every degree k ≥ 1. In degree zero the exact relation is D (π x) = π (D x) + (p choose 2) • [D x, x], the binomial formula of nilpotency class two, so D commutes with π in degree zero for odd p, while for p = 2 the defect is the bracket [D x, x]. This dyadic defect is not a degree-zero accident of the operator π alone: the deviation carries it into the degree m + 1 for every m, and it is the reason the basis-modification maps of the theory of Demushkin groups acquire an extra bracket term at p = 2.

At m = 0 the congruence hypothesis is empty, so every continuous endomorphism θ has a graded deviation, which is then the difference θ_* - id between the induced graded map and the identity. It is still additive, but it is no longer a derivation: in degree zero the Leibniz rule picks up the quadratic correction D [x, y] = [D x, y] - [D y, x] + [D x, D y], because [x + D x, y + D y] expands bilinearly. This is the level at which the basis modifications of a free pro-p group are arbitrary endomorphisms, and the correction is what makes the basis-modification map in degree one quadratic rather than linear.

The motivating case is a free pro-p group F on generators x_i and the endomorphism x_i ↦ x_i * w_i with w_i ∈ λ_m(F), which moves a relator r ∈ λ_1(F) inside its coset by an element of λ_{m+1}(F) whose class is D_1 ρ, for ρ ∈ gr_1(F) the class of r. That case is developed in TauCeti.Topology.Algebra.Group.Profinite.Free.BasisModification.

Main definitions

• TauCeti.gradedDeviation: the additive map D_k : gr_k(G) →+ gr_{m+k}(G) induced by g ↦ g⁻¹ * θ g.

Main results

• TauCeti.inv_mul_apply_mem_pLowerCentralSeries: g⁻¹ * θ g ∈ λ_{m+k} for g ∈ λ_k.
• TauCeti.gradedMap_eq_id_of_one_le: for m ≥ 1, θ induces the identity on every graded piece.
• TauCeti.gradedDeviation_gradedBracket, TauCeti.gradedDeviation_gradedBracket_zero: the Leibniz rule, for m ≥ 1.
• TauCeti.gradedDeviation_gradedPow_of_one_le, TauCeti.gradedDeviation_gradedPow_zero, TauCeti.gradedDeviation_gradedPow_zero_of_odd, TauCeti.gradedDeviation_gradedPow_zero_of_two: compatibility with π, exact in every degree.
• TauCeti.gradedCast_gradedDeviation_eq_gradedMap_sub, TauCeti.gradedDeviation_gradedBracket_zero_zero: at m = 0, where θ is an arbitrary continuous endomorphism, D_k = θ_* - id, and the Leibniz rule in degree zero acquires the quadratic correction [D x, D y].

References

• J. Labute, Classification of Demushkin groups, Canadian J. Math. 19 (1967), §1 and Proposition 5.

The deviation of an endomorphism congruent to the identity

theorem TauCeti.inv_mul_apply_mem_pLowerCentralSeries {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) {k : ℕ} {g : G} (hg : g ∈ pLowerCentralSeries p G k) : g⁻¹ * θ g ∈ pLowerCentralSeries p G (m + k)

An endomorphism congruent to the identity modulo λ_m is congruent to the identity modulo λ_{m+k} on λ_k.

def TauCeti.gradedDeviation {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) (k : ℕ) : gradedPiece p G k →+ gradedPiece p G (m + k)

The graded deviation D_k : gr_k(G) →+ gr_{m+k}(G) of an endomorphism θ congruent to the identity modulo λ_m: the map induced by g ↦ g⁻¹ * θ g. Its defining equation is TauCeti.gradedDeviation_gradedMk. For m ≥ 1 it is a derivation of the graded structure (TauCeti.gradedDeviation_gradedBracket), compatible with π away from degree zero (TauCeti.gradedDeviation_gradedPow_of_one_le) and with the binomial defect (p choose 2) • [D x, x] in degree zero (TauCeti.gradedDeviation_gradedPow_zero).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.gradedDeviation_gradedMk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) {k : ℕ} (x : ↥(pLowerCentralSeries p G k)) : (gradedDeviation θ hθc hθ k) (gradedMk p G k x) = gradedMk p G (m + k) ⟨(↑x)⁻¹ * θ ↑x, ⋯⟩

The graded deviation on classes: the defining equation of TauCeti.gradedDeviation.

@[simp]

theorem TauCeti.gradedDeviation_gradedMkZero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) (g : G) : (gradedDeviation θ hθc hθ 0) (gradedMkZero p G g) = gradedMk p G m ⟨g⁻¹ * θ g, ⋯⟩

The graded deviation in degree zero: the class of g goes to the class of g⁻¹ * θ g in gr_m(G).

theorem TauCeti.gradedMap_eq_id_of_one_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) (hm : 1 ≤ m) (k : ℕ) : gradedMap p θ hθc k = AddMonoidHom.id (gradedPiece p G k)

An endomorphism congruent to the identity modulo λ_m with m ≥ 1 induces the identity on every graded piece: its deviation on λ_k lies in λ_{m+k} ≤ λ_{k+1}.

theorem TauCeti.gradedDeviation_gradedBracket {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) (hm : 1 ≤ m) {j k : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G k) : (gradedDeviation θ hθc hθ (j + k + 1)) (((gradedBracket p G j k) x) y) = gradedCast p G ⋯ (((gradedBracket p G (m + j) k) ((gradedDeviation θ hθc hθ j) x)) y) + gradedCast p G ⋯ (((gradedBracket p G j (m + k)) x) ((gradedDeviation θ hθc hθ k) y))

The Leibniz rule. For m ≥ 1 the graded deviation is a derivation of the bracket: D [x, y] = [D x, y] + [x, D y], with the two terms transported to the degree m + (j + k + 1). The cross term ⁅x⁻¹ * θ x, y⁻¹ * θ y⁆ has degree 2m + j + k + 1, which is above m + j + k + 1 exactly when m ≥ 1.

@[simp]

theorem TauCeti.gradedDeviation_gradedBracket_zero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) (hm : 1 ≤ m) (x y : gradedPiece p G 0) : (gradedDeviation θ hθc hθ 1) (((gradedBracket p G 0 0) x) y) = ((gradedBracket p G m 0) ((gradedDeviation θ hθc hθ 0) x)) y - ((gradedBracket p G m 0) ((gradedDeviation θ hθc hθ 0) y)) x

The Leibniz rule in degree zero, in the cast-free form D [x, y] = [D x, y] - [D y, x] for x, y ∈ gr_0(G) and m ≥ 1, using skew-symmetry of the bracket to put both terms in gr_{m+1}(G).

@[simp]

theorem TauCeti.gradedDeviation_gradedPow_of_one_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) {k : ℕ} (hk : 1 ≤ k) (x : gradedPiece p G k) : (gradedDeviation θ hθc hθ (k + 1)) (gradedPow p G k x) = gradedPow p G (m + k) ((gradedDeviation θ hθc hθ k) x)

The graded deviation commutes with π above degree zero, for every m: for k ≥ 1, D (π x) = π (D x), because ⁅x, x⁻¹ * θ x⁆ has degree m + 2k + 1 ≥ m + k + 2.

theorem TauCeti.gradedDeviation_gradedPow_zero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) (x : gradedPiece p G 0) : (gradedDeviation θ hθc hθ 1) (gradedPow p G 0 x) = gradedPow p G m ((gradedDeviation θ hθc hθ 0) x) + p.choose 2 • ((gradedBracket p G m 0) ((gradedDeviation θ hθc hθ 0) x)) x

The graded deviation against π in degree zero: D (π x) = π (D x) + (p choose 2) • [D x, x] in gr_{m+1}(G). This is the binomial formula (x * u) ^ p = x ^ p * u ^ p * ⁅u, x⁆ ^ (p choose 2) of nilpotency class two, read modulo λ_{m+2}, where the class of ⁅u, x⁆ ∈ λ_{m+1} is central.

@[simp]

theorem TauCeti.gradedDeviation_gradedPow_zero_of_odd {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) (hp : Odd p) (x : gradedPiece p G 0) : (gradedDeviation θ hθc hθ 1) (gradedPow p G 0 x) = gradedPow p G m ((gradedDeviation θ hθc hθ 0) x)

The graded deviation commutes with π in degree zero for odd p: the defect (p choose 2) • [D x, x] is a multiple of p • [D x, x] = 0.

@[simp]

theorem TauCeti.gradedDeviation_gradedPow_zero_of_two {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) {m : ℕ} (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G m) (hp : p = 2) (x : gradedPiece p G 0) : (gradedDeviation θ hθc hθ 1) (gradedPow p G 0 x) = gradedPow p G m ((gradedDeviation θ hθc hθ 0) x) + ((gradedBracket p G m 0) ((gradedDeviation θ hθc hθ 0) x)) x

The dyadic defect of the graded deviation against π in degree zero. For p = 2, D (π x) = π (D x) + [D x, x] in gr_{m+1}(G): the square of x * u is x ^ 2 * u ^ 2 * ⁅u, x⁆ up to λ_{m+2}, and the commutator does not vanish in gr_{m+1}(G) in general.

The deviation of an arbitrary continuous endomorphism

theorem TauCeti.gradedCast_gradedDeviation_eq_gradedMap_sub {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G 0) (k : ℕ) (x : gradedPiece p G k) : gradedCast p G ⋯ ((gradedDeviation θ hθc hθ k) x) = (gradedMap p θ hθc k) x - x

The graded deviation of an arbitrary endomorphism is the graded map minus the identity. Every continuous endomorphism θ is congruent to the identity modulo λ_0 = G, and its deviation in degree k is D_k x = θ_* x - x, with the degrees 0 + k and k identified.

theorem TauCeti.gradedDeviation_zero_eq_gradedMap_sub {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G 0) (x : gradedPiece p G 0) : (gradedDeviation θ hθc hθ 0) x = (gradedMap p θ hθc 0) x - x

The graded deviation of an arbitrary endomorphism in degree zero: D_0 x = θ_* x - x.

theorem TauCeti.gradedDeviation_one_eq_gradedMap_sub {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G 0) (x : gradedPiece p G 1) : (gradedDeviation θ hθc hθ 1) x = (gradedMap p θ hθc 1) x - x

The graded deviation of an arbitrary endomorphism in degree one: D_1 x = θ_* x - x.

theorem TauCeti.gradedDeviation_gradedBracket_zero_zero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (θ : G →* G) (hθc : Continuous ⇑θ) (hθ : ∀ (g : G), g⁻¹ * θ g ∈ pLowerCentralSeries p G 0) (x y : gradedPiece p G 0) : (gradedDeviation θ hθc hθ 1) (((gradedBracket p G 0 0) x) y) = ((gradedBracket p G 0 0) ((gradedDeviation θ hθc hθ 0) x)) y - ((gradedBracket p G 0 0) ((gradedDeviation θ hθc hθ 0) y)) x + ((gradedBracket p G 0 0) ((gradedDeviation θ hθc hθ 0) x)) ((gradedDeviation θ hθc hθ 0) y)

The Leibniz rule in degree zero for an arbitrary endomorphism, with its quadratic correction: D [x, y] = [D x, y] - [D y, x] + [D x, D y] for x, y ∈ gr_0(G). The correction [D x, D y] is the bilinear expansion of [x + D x, y + D y] - [x, y]; for an endomorphism congruent to the identity modulo λ_1 it vanishes, and the rule is TauCeti.gradedDeviation_gradedBracket_zero.