Documentation

TauCeti.Data.ZMod.Torsion

Torsion in residue rings with power modulus #

For every nonzero p, the subgroup of ZMod (p ^ (k + 1)) killed by p is additively equivalent to ZMod p. This counts the elements killed by p in prime-power cyclic factors, as required by the rank-two finite-abelian criterion.

In the first nontrivial case k = 1, an element of ZMod (p ^ 2) killed by p is a multiple of p, so it reduces to 0 modulo p (ZMod.cast_eq_zero_of_natCast_mul_eq_zero); this is what prevents a character of order p from lifting modulo p ^ 2. More generally, an element of ZMod (p ^ (n + 1)) killed by p is the reduction of a multiple of p ^ n (ZMod.exists_eq_pow_mul_of_zsmul_eq_zero).

source
theorem ZMod.cast_eq_zero_of_natCast_mul_eq_zero {p : ℕ} [NeZero p] {u : ZMod (p ^ 2)} (hu : ↑p * u = 0) :
u.cast = 0

An element of ZMod (p ^ 2) killed by p reduces to 0 modulo p: its representative is divisible by p.

source
theorem ZMod.exists_eq_pow_mul_of_zsmul_eq_zero {p n : ℕ} [NeZero p] {x : ZMod (p ^ (n + 1))} (hx : ↑p • x = 0) :
∃ (t : ℤ), x = ↑(↑p ^ n * t)

An element of ZMod (p ^ (n + 1)) killed by p is the reduction of a multiple of p ^ n.

source
noncomputable def TauCeti.zmodTorsionByEquiv (p k : ℕ) [NeZero p] :
ZMod p ≃+ ↥(AddSubgroup.torsionBy (ZMod (p ^ (k + 1))) ↑p)

The subgroup of ZMod (p ^ (k + 1)) killed by p is additively equivalent to ZMod p.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.zmodTorsionByEquiv_apply_coe (p k : ℕ) [NeZero p] (x : ZMod p) :
    ↑((zmodTorsionByEquiv p k) x) = ↑(x.val * p ^ k)

    zmodTorsionByEquiv sends a residue to its multiple by p ^ k in the ambient residue ring.

    source
    @[simp]
    theorem TauCeti.zmodTorsionByEquiv_symm_apply (p k : ℕ) [NeZero p] (y : ↥(AddSubgroup.torsionBy (ZMod (p ^ (k + 1))) ↑p)) :
    (zmodTorsionByEquiv p k).symm y = ↑((↑y).val / p ^ k)

    The inverse of zmodTorsionByEquiv divides the representative by p ^ k.

    source
    theorem TauCeti.zmodTorsionByEquiv_apply_eq_iff (p k : ℕ) [NeZero p] (x : ZMod p) (y : ↥(AddSubgroup.torsionBy (ZMod (p ^ (k + 1))) ↑p)) :
    (zmodTorsionByEquiv p k) x = y ↔ ↑(x.val * p ^ k) = ↑y

    Equality with the image of a chosen residue under zmodTorsionByEquiv is characterized in the ambient residue ring.

    source
    theorem TauCeti.zmodTorsionByEquiv_symm_apply_eq_iff (p k : ℕ) [NeZero p] (y : ↥(AddSubgroup.torsionBy (ZMod (p ^ (k + 1))) ↑p)) (x : ZMod p) :
    (zmodTorsionByEquiv p k).symm y = x ↔ ↑(x.val * p ^ k) = ↑y

    The inverse picks the unique residue whose multiple by p ^ k is the given torsion point.