Cardinality bounds for n-torsion in finite commutative groups

The n-torsion subgroup of a commutative group G is (powMonoidHom n : G →* G).ker.

Main results

• MonoidHom.card_powMonoidHom_ker_le_of_surjective: a surjection does not increase the n-torsion.
• MonoidHom.card_powMonoidHom_ker_le_mul: the n-torsion of G is bounded by the n-torsion of the kernel of φ : G →* H times the n-torsion of H.
• MonoidHom.card_powMonoidHom_ker_le_of_coset_cover: a subgroup covered by finitely many cosets of the image of φ has m-torsion bounded by the m-torsion of the source times the number of cosets.

def MonoidHom.powMonoidHomKerMap {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (φ : G →* H) (n : ℕ) : ↥(powMonoidHom n).ker →* ↥(powMonoidHom n).ker

Power torsion maps functorially under a group homomorphism.

Equations

• φ.powMonoidHomKerMap n = { toFun := fun (x : ↥(powMonoidHom n).ker) => ⟨φ ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem MonoidHom.card_powMonoidHom_ker_le_of_surjective {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (φ : G →* H) (hφ : Function.Surjective ⇑φ) (n : ℕ) : Nat.card ↥(powMonoidHom n).ker ≤ Nat.card ↥(powMonoidHom n).ker

A surjective homomorphism does not increase the number of n-torsion elements.

theorem MonoidHom.card_powMonoidHom_ker_le_mul {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (φ : G →* H) (n : ℕ) : Nat.card ↥(powMonoidHom n).ker ≤ Nat.card ↥(powMonoidHom n).ker * Nat.card ↥(powMonoidHom n).ker

The torsion of the middle group is bounded by the torsion of a homomorphism's kernel and the torsion of its target.

theorem MonoidHom.card_powMonoidHom_ker_le_of_coset_cover {A : Type u_3} {G : Type u_4} {ι : Type u_5} [CommGroup A] [CommGroup G] [Finite A] [Finite G] [Fintype ι] (φ : A →* G) (S : Subgroup G) (c : ι → G) (hcover : ∀ (x : ↥S), ∃ (a : A) (i : ι), ↑x = φ a * c i) (m : ℕ) : Nat.card ↥(powMonoidHom m).ker ≤ Nat.card ↥(powMonoidHom m).ker * Fintype.card ι

A subgroup covered by finitely many cosets of the image of φ has m-torsion bounded by the m-torsion of the source times the number of cosets.