Documentation

TauCeti.Topology.Algebra.Group.Profinite.ProP.CrossedHom

Crossed homomorphisms of pro-p groups into ℤ_p along the lower p-series #

Let G be a topological group, χ : G →ₜ* ℤ_pˣ a continuous character with values in the principal units 1 + pℤ_p (as every continuous character of a pro-p group has, TauCeti.IsProP.mem_unitsPrincipal_one), and f : G → ℤ_p a continuous crossed homomorphism for χ, that is f (g * h) = χ g * f h + f g. Along the lower p-series λ_k = λ_k(G) both the character and the crossed homomorphism gain one power of p per step:

The quotient f g / p ^ k, read modulo p, is therefore defined on λ_k; it is additive, because χ ≡ 1 mod p, and it kills λ_{k+1}. It descends to the graded functional Δ_k(f) : gr_k(G) → 𝔽_p on the graded piece gr_k(G) = λ_k ⧸ λ_{k+1} (TauCeti.IsCrossedHom.gradedFunctional), an 𝔽_p-linear functional characterized by Δ_k(f) (class of g) = (f g / p ^ k) mod p (TauCeti.IsCrossedHom.gradedFunctional_gradedMk). On the iterated p-power π^k ξ of the class ξ ∈ gr_0(G) of an element g on which the character is trivial, Δ_k(f) (π^k ξ) = f g mod p (TauCeti.IsCrossedHom.gradedFunctional_gradedPowIter_gradedMkZero), because f (g ^ (p ^ k)) = p ^ k f g when χ g = 1. In degree zero, Δ_0(f) is the reduction of f modulo p, the 𝔽_p-character of G that f induces on the Frattini quotient.

These functionals are the linear maps Δ of Labute's Lemma 4. For the crossed homomorphisms D_i of a free pro-p group F taking the value 1 at the generator x_i and 0 at the others, Δ_k(D_i) takes the value δ_{ij} on the p-power π^k ξ_j of the class of a generator x_j on which the character is trivial, and it vanishes on the image of the basis-modification map δ for the orientation of a Demushkin group in normal form. So when a class of a graded piece of the kernel of the orientation is written as an element of that image plus a combination Σ_j c_j π^k ξ_j of these p-powers, as the constrained span statement of the normal form allows, the Δ_k(D_i) read off the coefficients c_j. That is what cuts the image of δ out of the graded pieces of the kernel of the orientation in the classification of the dyadic Demushkin groups of even rank.

Main definitions #

Main results #

References #

Divisibility of a crossed homomorphism along the lower p-series #

source
theorem TauCeti.IsCrossedHom.pow_dvd_apply_of_mem_pLowerCentralSeries {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hχ : ∀ (g : G), χ g ∈ unitsPrincipal p 1) (hfc : Continuous f) {k : ℕ} {g : G} (hg : g ∈ pLowerCentralSeries p G k) :
↑p ^ k ∣ f g

A continuous crossed homomorphism is divisible by p ^ k on λ_k(G). For a continuous character χ with values in 1 + pℤ_p and a continuous crossed homomorphism f for χ, the elements g with p ^ k ∣ f g form a closed subgroup; it contains the p-th powers of the elements of λ_{k-1}(G), because the geometric sum 1 + χ x + ⋯ + χ x ^ (p - 1) is divisible by p, and their commutators with G, because χ x - 1 ∈ p ^ k ℤ_p for x ∈ λ_{k-1}(G).

The graded functional #

source
noncomputable def TauCeti.IsCrossedHom.gradedFunctional {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hχ : ∀ (g : G), χ g ∈ unitsPrincipal p 1) (hfc : Continuous f) (k : ℕ) :
gradedPiece p G k →ₗ[ZMod p] ZMod p

The graded functional of a crossed homomorphism. For a continuous character χ of G with values in 1 + pℤ_p and a continuous crossed homomorphism f : G → ℤ_p for χ, the 𝔽_p-linear functional Δ_k(f) : gr_k(G) → 𝔽_p on the graded piece gr_k(G) = λ_k ⧸ λ_{k+1} sending the class of g ∈ λ_k(G) to (f g / p ^ k) mod p (TauCeti.IsCrossedHom.gradedFunctional_gradedMk); it is well defined because f is divisible by p ^ k on λ_k(G) and by p ^ (k + 1) on λ_{k+1}(G), and additive because χ ≡ 1 mod p.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.IsCrossedHom.gradedFunctional_gradedMk {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hχ : ∀ (g : G), χ g ∈ unitsPrincipal p 1) (hfc : Continuous f) (k : ℕ) (g : ↥(pLowerCentralSeries p G k)) {c : ℤ_[p]} (hc : f ↑g = ↑p ^ k * c) :
    (hf.gradedFunctional hχ hfc k) (gradedMk p G k g) = PadicInt.toZMod c

    The graded functional on classes: if f g = p ^ k * c for g ∈ λ_k(G), then Δ_k(f) (class of g) = c mod p. This is the defining equation of TauCeti.IsCrossedHom.gradedFunctional, since c is determined by f g.

    source
    @[simp]
    theorem TauCeti.IsCrossedHom.gradedFunctional_gradedMk_eq_zero_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hχ : ∀ (g : G), χ g ∈ unitsPrincipal p 1) (hfc : Continuous f) (k : ℕ) (g : ↥(pLowerCentralSeries p G k)) :
    (hf.gradedFunctional hχ hfc k) (gradedMk p G k g) = 0 ↔ ↑p ^ (k + 1) ∣ f ↑g

    The kernel of the graded functional on classes: Δ_k(f) kills the class of g ∈ λ_k(G) exactly when p ^ (k + 1) ∣ f g.

    source
    @[simp]
    theorem TauCeti.IsCrossedHom.gradedFunctional_gradedMkZero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hχ : ∀ (g : G), χ g ∈ unitsPrincipal p 1) (hfc : Continuous f) (g : G) :
    (hf.gradedFunctional hχ hfc 0) (gradedMkZero p G g) = PadicInt.toZMod (f g)

    In degree zero the graded functional is the reduction modulo p: Δ_0(f) (class of g) = f g mod p.

    source
    theorem TauCeti.IsCrossedHom.gradedFunctional_gradedPowIter_gradedMkZero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hχ : ∀ (g : G), χ g ∈ unitsPrincipal p 1) (hfc : Continuous f) (k : ℕ) {g : G} (hg : χ g = 1) :
    (hf.gradedFunctional hχ hfc k) (gradedPowIter p G k (gradedMkZero p G g)) = PadicInt.toZMod (f g)

    The graded functional on an iterated p-power. For g ∈ G with χ g = 1, the value of Δ_k(f) on π^k ξ, where ξ ∈ gr_0(G) is the class of g, is f g mod p: indeed f (g ^ (p ^ k)) = p ^ k * f g when χ g = 1.

    source
    theorem TauCeti.IsCrossedHom.gradedFunctional_gradedPowIter_gradedMkZero_of_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hχ : ∀ (g : G), χ g ∈ unitsPrincipal p 1) (hfc : Continuous f) (k : ℕ) {g : G} (hg : f g = 0) :
    (hf.gradedFunctional hχ hfc k) (gradedPowIter p G k (gradedMkZero p G g)) = 0

    The graded functional on an iterated p-power of an element killed by the crossed homomorphism: if f g = 0, then Δ_k(f) (π^k ξ) = 0 for the class ξ of g, since f (g ^ (p ^ k)) is a multiple of f g.

    source
    theorem TauCeti.IsCrossedHom.gradedFunctional_gradedPowIterBracket {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hχ : ∀ (g : G), χ g ∈ unitsPrincipal p 1) (hfc : Continuous f) (m : ℕ) (g h : G) :
    (hf.gradedFunctional hχ hfc (m + 1)) (gradedPowIterBracket p G m g h) = (hf.gradedFunctional hχ hfc 1) (((gradedBracket p G 0 0) (gradedMkZero p G g)) (gradedMkZero p G h))

    The graded functional on an iterated p-power of a bracket: Δ_{m+1}(f) (π^m [ξ_g, ξ_h]) = Δ_1(f) ([ξ_g, ξ_h]), because f (⁅g, h⁆ ^ (p ^ m)) = p ^ m * f ⁅g, h⁆, the character being trivial on commutators.

    source
    theorem TauCeti.IsCrossedHom.dvd_apply_of_mem_pLowerCentralSeries_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} (hG : IsProP p G) {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hfc : Continuous f) {g : G} (hg : g ∈ pLowerCentralSeries p G 1) :
    ↑p ∣ f g

    A continuous crossed homomorphism of a pro-p group vanishes modulo p on the Frattini subgroup. For a continuous character χ : G → ℤ_pˣ of a pro-p group G and a continuous crossed homomorphism f for χ, p ∣ f g for g ∈ λ_1(G) = Φ(G): the case k = 1 of TauCeti.IsCrossedHom.pow_dvd_apply_of_mem_pLowerCentralSeries, since χ ≡ 1 mod p.

    Crossed homomorphisms on p-adic powers #

    source
    theorem TauCeti.IsCrossedHom.map_padicPow_eq_zero_of_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} [CompactSpace G] [TotallyDisconnectedSpace G] {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hfc : Continuous f) (hG : IsProP p G) {x : G} (hx : f x = 0) (l : ℤ_[p]) :
    f (hG.padicPow x l) = 0

    A continuous crossed homomorphism vanishing at x vanishes on the p-adic powers of x.

    source
    theorem TauCeti.IsCrossedHom.map_padicPow_of_eq_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} [CompactSpace G] [TotallyDisconnectedSpace G] {f : G → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hfc : Continuous f) (hG : IsProP p G) {x : G} (hx : χ x = 1) (l : ℤ_[p]) :
    f (hG.padicPow x l) = l * f x

    On an element where the character is trivial, a continuous crossed homomorphism is ℤ_p-linear along p-adic powers: f (x ^ l) = l * f x for l ∈ ℤ_p.