Multiplication by a natural number coprime to an exponent

Let M be an additive group and p a natural number killing every element of M. Multiplication by a natural number n coprime to p is then bijective (TauCeti.nsmul_right_bijective_of_coprime): the Bézout decomposition TauCeti.exists_zsmul_add_zsmul_eq_of_coprime writes every m as i • (n • m) + j • (p • m), the second summand vanishes, and the coefficient i is independent of m, so m ↦ i • m is a two-sided inverse. No finiteness and no commutativity are involved. Two coprime exponents therefore leave nothing (TauCeti.subsingleton_of_forall_nsmul_eq_zero_of_coprime), so a nontrivial group has at most one prime exponent (TauCeti.eq_of_prime_forall_nsmul_eq_zero).

For a commutative M this computes the torsion subgroups and the reductions of M at every natural number at once. Away from the exponent, injectivity makes the torsion subgroup M[n] — Mathlib's AddSubgroup.torsionBy M (n : ℤ) — trivial and surjectivity makes nM = M, so the reduction M / nM — Mathlib's ModN M n — is trivial. At the exponent the two computations are the opposite ones: M[p] = ⊤ (TauCeti.torsionBy_eq_top_of_forall_nsmul_eq_zero) and pM = ⊥, the latter making the reduction M itself (TauCeti.modNEquiv).

Main definitions

• TauCeti.modNEquiv: at the exponent, the reduction M / pM is M again.

Main results

• TauCeti.nsmul_right_bijective_of_coprime: multiplication by a natural number coprime to an exponent is bijective, with TauCeti.subsingleton_of_forall_nsmul_eq_zero_of_coprime and TauCeti.eq_of_prime_forall_nsmul_eq_zero the uniqueness consequences.
• TauCeti.torsionBy_eq_bot_of_coprime, TauCeti.subsingleton_modN_of_coprime: away from the exponent both the torsion subgroup and the reduction vanish.
• TauCeti.torsionBy_eq_top_of_forall_nsmul_eq_zero, TauCeti.range_lsmul_eq_bot_of_forall_nsmul_eq_zero: at the exponent itself everything is torsion and multiplication is zero.

Multiplication by a coprime natural number

theorem TauCeti.nsmul_right_bijective_of_coprime {M : Type u_1} [AddGroup M] {p n : ℕ} (hp : ∀ (m : M), p • m = 0) (h : n.Coprime p) : Function.Bijective fun (m : M) => n • m

Multiplication by a natural number coprime to an exponent is bijective. If p kills every element of M and n is coprime to p, the Bézout decomposition TauCeti.exists_zsmul_add_zsmul_eq_of_coprime exhibits m ↦ i • m as a two-sided inverse of m ↦ n • m, because its p-multiple summand vanishes.

Mathlib's Nat.Coprime.nsmul_right_bijective is the same conclusion from a different hypothesis, coprimality with Nat.card M for a finite M. The hypothesis here asks for no finiteness: an infinite 𝔽_p-vector space is covered.

theorem TauCeti.subsingleton_of_forall_nsmul_eq_zero_of_coprime {M : Type u_1} [AddGroup M] {p q : ℕ} (hp : ∀ (m : M), p • m = 0) (hq : ∀ (m : M), q • m = 0) (h : p.Coprime q) : Subsingleton M

Two coprime exponents leave nothing. If coprime naturals p and q both kill every element of M then M is trivial: multiplication by q is bijective by TauCeti.nsmul_right_bijective_of_coprime and is also the zero map.

theorem TauCeti.eq_of_prime_forall_nsmul_eq_zero {M : Type u_1} [AddGroup M] {p q : ℕ} [Nontrivial M] (hp : Nat.Prime p) (hq : Nat.Prime q) (hp' : ∀ (m : M), p • m = 0) (hq' : ∀ (m : M), q • m = 0) : p = q

A nontrivial group has at most one prime exponent. Two primes both killing a nontrivial group are coprime unless equal, and coprime exponents leave nothing (TauCeti.subsingleton_of_forall_nsmul_eq_zero_of_coprime).

Torsion and reduction

theorem TauCeti.torsionBy_eq_bot_of_coprime {M : Type u_1} [AddCommGroup M] {p n : ℕ} (hp : ∀ (m : M), p • m = 0) (h : n.Coprime p) : AddSubgroup.torsionBy M ↑n = ⊥

Away from the exponent there is no torsion. If p kills M and n is coprime to p, multiplication by n is injective, so the n-torsion subgroup M[n] is trivial.

theorem TauCeti.range_lsmul_eq_top_of_coprime {M : Type u_1} [AddCommGroup M] {p n : ℕ} (hp : ∀ (m : M), p • m = 0) (h : n.Coprime p) : ((LinearMap.lsmul ℤ M) ↑n).range = ⊤

Away from the exponent multiplication is onto. If p kills M and n is coprime to p then n M = M, which is the statement that TauCeti.subsingleton_modN_of_coprime quotients by.

theorem TauCeti.subsingleton_modN_of_coprime {M : Type u_1} [AddCommGroup M] {p n : ℕ} (hp : ∀ (m : M), p • m = 0) (h : n.Coprime p) : Subsingleton (ModN M n)

Away from the exponent the reduction vanishes. If p kills M and n is coprime to p then M / nM — Mathlib's ModN M n — is trivial.

theorem TauCeti.torsionBy_eq_top_of_forall_nsmul_eq_zero {M : Type u_1} [AddCommGroup M] {p : ℕ} (hp : ∀ (m : M), p • m = 0) : AddSubgroup.torsionBy M ↑p = ⊤

At the exponent everything is torsion. If p kills M then the p-torsion subgroup M[p] — Mathlib's AddSubgroup.torsionBy M (p : ℤ) — is everything.

theorem TauCeti.range_lsmul_eq_bot_of_forall_nsmul_eq_zero {M : Type u_1} [AddCommGroup M] {p : ℕ} (hp : ∀ (m : M), p • m = 0) : ((LinearMap.lsmul ℤ M) ↑p).range = ⊥

At the exponent multiplication is zero.

noncomputable def TauCeti.modNEquiv {M : Type u_1} [AddCommGroup M] {p : ℕ} (hp : ∀ (m : M), p • m = 0) : ModN M p ≃ₗ[ℤ] M

At the exponent the reduction is the module itself. Since pM = 0, the quotient ModN M p = M / pM is M, linearly over ℤ.

Equations

• TauCeti.modNEquiv hp = ((LinearMap.lsmul ℤ M) ↑p).range.quotEquivOfEqBot ⋯

@[simp]

theorem TauCeti.modNEquiv_apply_mkQ {M : Type u_1} [AddCommGroup M] {p : ℕ} (hp : ∀ (m : M), p • m = 0) (m : M) : (modNEquiv hp) ((ModN.mkQ p) m) = m

TauCeti.modNEquiv undoes Mathlib's quotient map ModN.mkQ. Mathlib's Submodule.quotEquivOfEqBot_apply_mk is this statement for the Submodule.Quotient.mk spelling, which ModN.mkQ is definitionally but not syntactically, so it never fires here.

@[simp]

theorem TauCeti.modNEquiv_symm_apply {M : Type u_1} [AddCommGroup M] {p : ℕ} (hp : ∀ (m : M), p • m = 0) (m : M) : (modNEquiv hp).symm m = (ModN.mkQ p) m

The inverse of TauCeti.modNEquiv is the quotient map ModN.mkQ, the ModN spelling that Mathlib's Submodule.quotEquivOfEqBot_symm_apply does not match.