Torsion subgroups, products, and maps

A subgroup of an additive commutative group consists of torsion points as soon as it is finite: its cardinality annihilates each of its elements, so a subgroup H is contained in the Nat.card H-torsion subgroup. For finite H this says that a subgroup with n elements is n-torsion; for infinite H one has Nat.card H = 0 and the statement is the trivial H ≤ A[0].

A linear map f with a left inverse up to multiplication by a nonzerodivisor a, that is g ∘ f = a • id, reflects torsion: if f x is torsion then so is x.

Torsion also commutes with products and additive equivalences. When a ∣ b, the a-torsion inside the b-torsion subgroup is the ambient a-torsion subgroup.

Main definitions

• TauCeti.AddSubgroup.torsionByPiEquiv: torsion of a product is the product of torsions.
• TauCeti.AddSubgroup.torsionByTorsionByEquiv: nested torsion for a ∣ b.
• AddEquiv.torsionByCongr: transport torsion along an additive equivalence.

Main results

• AddSubgroup.le_torsionBy_natCard: a subgroup H is contained in the Nat.card H-torsion subgroup.
• TauCeti.Submodule.comap_torsion_le_of_comp_eq_smul: a linear map with a left inverse up to a nonzerodivisor reflects torsion.

theorem AddSubgroup.le_torsionBy_natCard {A : Type u_1} [AddCommGroup A] {H : AddSubgroup A} : H ≤ torsionBy A ↑(Nat.card ↥H)

A subgroup H consists of Nat.card H-torsion points; for finite H this is the statement that a subgroup with n elements is n-torsion, and for infinite H it is the trivial H ≤ A[0].

def TauCeti.AddSubgroup.torsionByPiEquiv {ι : Type u_1} (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] (n : ℤ) : ↥(AddSubgroup.torsionBy ((i : ι) → A i) n) ≃+ ((i : ι) → ↥(AddSubgroup.torsionBy (A i) n))

Torsion in a product of additive commutative groups is additively equivalent to the product of their torsion subgroups.

Equations

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

@[simp]

theorem TauCeti.AddSubgroup.torsionByPiEquiv_apply_coe {ι : Type u_1} (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] (n : ℤ) (x : ↥(AddSubgroup.torsionBy ((i : ι) → A i) n)) (i : ι) : ↑((torsionByPiEquiv A n) x i) = ↑x i

torsionByPiEquiv sends a torsion element to its pointwise torsion elements.

@[simp]

theorem TauCeti.AddSubgroup.torsionByPiEquiv_symm_apply_coe {ι : Type u_1} (A : ι → Type u_2) [(i : ι) → AddCommGroup (A i)] (n : ℤ) (x : (i : ι) → ↥(AddSubgroup.torsionBy (A i) n)) (i : ι) : ↑((torsionByPiEquiv A n).symm x) i = ↑(x i)

The inverse of torsionByPiEquiv assembles torsion elements pointwise.

def TauCeti.AddSubgroup.torsionByTorsionByEquiv {A : Type u_1} [AddCommGroup A] {a b : ℤ} (hab : a ∣ b) : ↥(AddSubgroup.torsionBy (↥(AddSubgroup.torsionBy A b)) a) ≃+ ↥(AddSubgroup.torsionBy A a)

Torsion by a inside the b-torsion subgroup is the ambient a-torsion when a ∣ b.

Equations

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

@[simp]

theorem TauCeti.AddSubgroup.torsionByTorsionByEquiv_apply_coe {A : Type u_1} [AddCommGroup A] {a b : ℤ} (hab : a ∣ b) (x : ↥(AddSubgroup.torsionBy (↥(AddSubgroup.torsionBy A b)) a)) : ↑((torsionByTorsionByEquiv hab) x) = ↑↑x

torsionByTorsionByEquiv preserves the underlying ambient element.

@[simp]

theorem TauCeti.AddSubgroup.torsionByTorsionByEquiv_symm_apply_coe {A : Type u_1} [AddCommGroup A] {a b : ℤ} (hab : a ∣ b) (x : ↥(AddSubgroup.torsionBy A a)) : ↑↑((torsionByTorsionByEquiv hab).symm x) = ↑x

The inverse of torsionByTorsionByEquiv preserves the underlying ambient element.

def AddEquiv.torsionByCongr {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] (e : A ≃+ B) (n : ℤ) : ↥(AddSubgroup.torsionBy A n) ≃+ ↥(AddSubgroup.torsionBy B n)

An additive equivalence carries the n-torsion subgroup to the n-torsion subgroup.

Equations

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

@[simp]

theorem AddEquiv.torsionByCongr_apply_coe {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] (e : A ≃+ B) (n : ℤ) (x : ↥(AddSubgroup.torsionBy A n)) : ↑((e.torsionByCongr n) x) = e ↑x

torsionByCongr applies its additive equivalence to the underlying element.

@[simp]

theorem AddEquiv.torsionByCongr_symm_apply_coe {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] (e : A ≃+ B) (n : ℤ) (x : ↥(AddSubgroup.torsionBy B n)) : ↑((e.torsionByCongr n).symm x) = e.symm ↑x

The inverse of torsionByCongr applies the inverse additive equivalence.

theorem TauCeti.Submodule.comap_torsion_le_of_comp_eq_smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} {a : R} (ha : a ∈ nonZeroDivisors R) (hgf : ∀ (x : M), g (f x) = a • x) : Submodule.comap f (Submodule.torsion R N) ≤ Submodule.torsion R M

A linear map f for which some g satisfies g ∘ f = a • id with a a nonzerodivisor reflects torsion: an element whose image is torsion is itself torsion.