Documentation

TauCeti.Topology.Algebra.Group.Profinite.Free.CrossedHomLinearization

The linearisation of crossed homomorphisms of a free pro-p group in the character #

Let F = freeProP p X be the free pro-p group on a finite type X, and let χ, χ' : F → ℤ_pˣ be two continuous characters. Their values lie in the principal units 1 + pℤ_p, and if they are congruent modulo p ^ k on the generators, then they are congruent modulo p ^ k everywhere (TauCeti.freeProP.pow_dvd_sub_of_forall_of). Let f and f' be continuous crossed homomorphisms F → ℤ_p for χ and χ' with the same values on the generators. Then f' ≡ f modulo p ^ k (TauCeti.IsCrossedHom.pow_dvd_sub_of_forall_of_eq), and the quotient (f' - f) / p ^ k, read modulo p, is a Heisenberg cochain for the two 𝔽_p-characters (χ' - χ) / p ^ k mod p and f mod p. On λ_1(F) a Heisenberg cochain is the degree-one form of the class in gr_1(F), evaluated at the two characters. Hence for n ∈ λ_1(F),

f' n ≡ f n + Σ_{i,j} (χ'(x_i) - χ(x_i)) · f(x_j) · B_n(χ_i, χ_j) mod p^(k+1),

where x_i = of i are the generators, χ_i the coordinate 𝔽_p-characters, and B_n the degree-one form of the class of n (TauCeti.freeProP.degreeOneForm), with its values lifted to ℤ_p (TauCeti.IsCrossedHom.pow_succ_dvd_sub_sub_sum_degreeOneForm). This is a Taylor expansion to first order in the character: the value of a crossed homomorphism on a fixed element of the Frattini subgroup, as a function of the values of the character on the generators, has the degree-one form of that element as its derivative modulo p. It is the linearisation that Newton's method uses to find the canonical character of a Demushkin group.

Main result #

References #

theorem TauCeti.IsCrossedHom.pow_succ_dvd_sub_sub_sum_degreeOneForm {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Fintype X] {χ χ' : freeProP p X →ₜ* ℤ_[p]ˣ} {k : ℕ} (hχ : ∀ (x : X), ↑p ^ k ∣ ↑(χ' (freeProP.of x)) - ↑(χ (freeProP.of x))) {f f' : freeProP p X → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hf' : IsCrossedHom (⇑χ') f') (hfc : Continuous f) (hf'c : Continuous f') (hff' : ∀ (x : X), f (freeProP.of x) = f' (freeProP.of x)) (n : ↥(pLowerCentralSeries p (freeProP p X) 1)) :
↑p ^ (k + 1) ∣ f' ↑n - f ↑n - ∑ i : X, ∑ j : X, (↑(χ' (freeProP.of i)) - ↑(χ (freeProP.of i))) * f (freeProP.of j) * (((freeProP.degreeOneForm (gradedMk p (freeProP p X) 1 n)) ((freeProP.dualBasis p X) i)) ((freeProP.dualBasis p X) j)).cast

The first-order expansion of a crossed homomorphism in the character, on the Frattini subgroup. Let χ, χ' : F → ℤ_pˣ be continuous characters of the free pro-p group on a finite type X, congruent modulo p ^ k on the generators x_i = of i, and let f, f' be continuous crossed homomorphisms for χ, χ' with the same values on the generators. Then for n ∈ λ_1(F),

f' n ≡ f n + Σ_{i,j} (χ'(x_i) - χ(x_i)) · f(x_j) · B_n(χ_i, χ_j) mod p^(k+1),

where B_n is the degree-one form of the class of n in gr_1(F) and χ_i are the coordinate 𝔽_p-characters, the values of B_n being lifted from 𝔽_p to ℤ_p.