Characters of a free pro-p group into ℤ_pˣ

A continuous character χ : freeProP p X →ₜ* ℤ_pˣ of a free pro-p group takes its values in the principal units 1 + pℤ_p (TauCeti.IsProP.mem_unitsPrincipal_one) and is determined by its values on the generators; more precisely, two characters congruent modulo p ^ k on the generators are congruent modulo p ^ k everywhere (TauCeti.freeProP.pow_dvd_sub_of_forall_of). Conversely, every family u : X → 1 + pℤ_p is the family of generator values of a continuous character: the universal property of freeProP p X applied to the pro-p group 1 + pℤ_p, lifted to the universe of X. So the continuous characters of freeProP p X into ℤ_pˣ correspond exactly to the families X → 1 + pℤ_p.

Main definitions

• TauCeti.freeProP.characterOfUnits: the continuous character of freeProP p X with prescribed principal-unit values on the generators.

Main results

• TauCeti.freeProP.characterOfUnits_of: the character takes the prescribed values on the generators.
• TauCeti.freeProP.eq_characterOfUnits: every continuous character of a free pro-p group into ℤ_pˣ is the character of its values on the generators.
• TauCeti.freeProP.pow_dvd_sub_of_forall_of: two continuous characters congruent modulo p ^ k on the generators are congruent modulo p ^ k everywhere.

noncomputable def TauCeti.freeProP.characterOfUnits (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) (u : X → ↥(unitsPrincipal p 1)) : freeProP p X →ₜ* ℤ_[p]ˣ

The continuous character of a free pro-p group with prescribed principal-unit values on the generators: for u : X → 1 + pℤ_p, the character freeProP p X → ℤ_pˣ with x ↦ u x on the generators, the universal property applied to the pro-p group 1 + pℤ_p, lifted to the universe of X.

Equations

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

@[simp]

theorem TauCeti.freeProP.characterOfUnits_of (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) (u : X → ↥(unitsPrincipal p 1)) (x : X) : (characterOfUnits p X u) (of x) = ↑(u x)

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

theorem TauCeti.freeProP.eq_characterOfUnits (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) (χ : freeProP p X →ₜ* ℤ_[p]ˣ) : χ = characterOfUnits p X fun (x : X) => ⟨χ (of x), ⋯⟩

Every continuous character of a free pro-p group is the character of its values on the generators, which are principal units.

theorem TauCeti.freeProP.pow_dvd_sub_of_forall_of {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {χ χ' : freeProP p X →ₜ* ℤ_[p]ˣ} {k : ℕ} (hχ : ∀ (x : X), ↑p ^ k ∣ ↑(χ' (of x)) - ↑(χ (of x))) (g : freeProP p X) : ↑p ^ k ∣ ↑(χ' g) - ↑(χ g)

Two continuous characters congruent modulo p ^ k on the generators are congruent modulo p ^ k everywhere: their truncations modulo p ^ k are continuous homomorphisms to a finite group agreeing on the generators.