Lifting characters of ℤ_p^ι × ℤ_p ⧸ (q) from 𝔽_p to ℤ/p²

An additive homomorphism ψ : ℤ_p → 𝔽_p is determined by ψ 1: it kills pℤ_p, so it is x ↦ (x mod p) ψ(1). Consequently a continuous character of the abelian pro-p group A = ℤ_p^ι × ℤ_p ⧸ (q), ι finite and p ∣ q, with values in 𝔽_p is a combination of the reductions modulo p of the coordinates. This decides when such a character lifts to a continuous character with values in ℤ/p²:

• if p² ∣ q, including q = 0, every character A → 𝔽_p lifts, the lift being the same combination of the truncations modulo p² of the coordinates;
• if q = p, the reduction (x, y) ↦ y mod p on the factor ℤ_p ⧸ (p) = 𝔽_p does not lift: a lift would take an element of order p to an element of ℤ/p² killed by p, whose reduction modulo p is 0.

At p = 2 this is the module-theoretic side of the fact that the cup square on H¹(G, 𝔽₂) of a Demushkin group G vanishes identically exactly when its invariant q is not 2: through G^{ab} ≅ ℤ_2^{n-1} × ℤ_2 ⧸ (q), the characters of G with values in 𝔽₂ that lift to ℤ/4 are exactly those with vanishing cup square.

Main declarations

• PadicInt.addMonoidHom_apply_eq_toZMod_mul_apply_one: an additive homomorphism ℤ_p → 𝔽_p is x ↦ (x mod p) ψ(1).
• PadicInt.piProdQuotientSpanToZMod: the character (x, y) ↦ y mod p of ℤ_p^ι × ℤ_p ⧸ (q), for p ∣ q.
• PadicInt.exists_forall_castHom_toAdd_eq_toAdd_of_pow_two_dvd: for p² ∣ q, every continuous character ℤ_p^ι × ℤ_p ⧸ (q) → 𝔽_p lifts to ℤ/p².
• PadicInt.exists_castHom_toAdd_ne_toAdd_piProdQuotientSpanToZMod: the character (x, y) ↦ y mod p of ℤ_p^ι × ℤ_p ⧸ (p) does not lift to ℤ/p².

theorem PadicInt.addMonoidHom_apply_eq_toZMod_mul_apply_one {p : ℕ} [Fact (Nat.Prime p)] (ψ : ℤ_[p] →+ ZMod p) (x : ℤ_[p]) : ψ x = toZMod x * ψ 1

An additive homomorphism ℤ_p → 𝔽_p is determined by its value at 1: it kills pℤ_p, so it is x ↦ (x mod p) ψ(1).

noncomputable def PadicInt.piProdQuotientSpanToZMod {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {q : ℤ_[p]} (hq : ↑p ∣ q) : Multiplicative ((ι → ℤ_[p]) × ℤ_[p] ⧸ Ideal.span {q}) →ₜ* Multiplicative (ZMod p)

The character (x, y) ↦ y mod p of ℤ_p^ι × ℤ_p ⧸ (q), for p ∣ q: the reduction modulo p of the second coordinate, as a continuous character with values in 𝔽_p.

Equations

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

@[simp]

theorem PadicInt.piProdQuotientSpanToZMod_ofAdd {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {q : ℤ_[p]} (hq : ↑p ∣ q) (x : ι → ℤ_[p]) (y : ℤ_[p] ⧸ Ideal.span {q}) : (piProdQuotientSpanToZMod hq) (Multiplicative.ofAdd (x, y)) = Multiplicative.ofAdd ((quotientSpanToZMod hq) y)

The character (x, y) ↦ y mod p takes the value y mod p at (x, y).

Lifting from 𝔽_p to ℤ/p²

theorem PadicInt.exists_forall_castHom_toAdd_eq_toAdd_of_pow_two_dvd {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {q : ℤ_[p]} [Finite ι] (hq : ↑p ^ 2 ∣ q) (χ : Multiplicative ((ι → ℤ_[p]) × ℤ_[p] ⧸ Ideal.span {q}) →ₜ* Multiplicative (ZMod p)) : ∃ (φ : Multiplicative ((ι → ℤ_[p]) × ℤ_[p] ⧸ Ideal.span {q}) →ₜ* Multiplicative (ZMod (p ^ 2))), ∀ (a : Multiplicative ((ι → ℤ_[p]) × ℤ_[p] ⧸ Ideal.span {q})), (ZMod.castHom ⋯ (ZMod p)) (Multiplicative.toAdd (φ a)) = Multiplicative.toAdd (χ a)

For p² ∣ q, every continuous character ℤ_p^ι × ℤ_p ⧸ (q) → 𝔽_p lifts to ℤ/p²: writing the character as (x, y) ↦ ∑ᵢ (xᵢ mod p) cᵢ + (y mod p) c₀, the same combination of the truncations modulo p² of the coordinates is a continuous character with values in ℤ/p² whose reduction modulo p is the given one. This includes q = 0.

theorem PadicInt.exists_castHom_toAdd_ne_toAdd_piProdQuotientSpanToZMod {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} (φ : Multiplicative ((ι → ℤ_[p]) × ℤ_[p] ⧸ Ideal.span {↑p}) →ₜ* Multiplicative (ZMod (p ^ 2))) : ∃ (a : Multiplicative ((ι → ℤ_[p]) × ℤ_[p] ⧸ Ideal.span {↑p})), (ZMod.castHom ⋯ (ZMod p)) (Multiplicative.toAdd (φ a)) ≠ Multiplicative.toAdd ((piProdQuotientSpanToZMod ⋯) a)

The character (x, y) ↦ y mod p of ℤ_p^ι × ℤ_p ⧸ (p) does not lift to ℤ/p²: the element (0, 1) has order p, so a lift would send it to an element of ℤ/p² killed by p, whose reduction modulo p is 0, while the character takes the value 1 there.