Independent cyclic subgroups generated by elements of infinite order give linearly independent generators over the integers
ProvedModuleRank.linearIndependent_of_iSupIndep_zpowers_of_infinite_orderLet be an abelian group and a finite family of its elements such that the cyclic subgroups they generate are independent in the lattice of subgroups -- each meets the supremum of the others trivially -- and such that every has infinite order, in the sense that forces for every integer . Then the family, read additively, is linearly independent over .
Together with the bound in the other direction this pins the rank of such an to the number of members of infinite order, rather than merely bounding it.
The infinite-order hypothesis is not decoration: independence of the cyclic subgroups alone does not give linear independence, since a single element of finite order generates a subgroup independent of the empty family while being additively dependent. Independence here is the lattice condition -- each cyclic subgroup meets the join of all the others trivially -- which is strictly stronger than pairwise triviality. The family is not assumed injective, but the two hypotheses together forbid repetitions, since equal members would force them to be trivial. The finiteness of the index type is a deliberate restriction of scope rather than a requirement for the statement to make sense.
import Mathlib
namespace ModuleRank
theorem linearIndependent_of_iSupIndep_zpowers_of_infinite_order {A : Type*} [CommGroup A] {ι : Type*} [Fintype ι]
(a : ι → A) (hind : iSupIndep fun i => Subgroup.zpowers (a i))
(hinf : ∀ (i : ι) (n : ℤ), a i ^ n = 1 → n = 0) :
LinearIndependent ℤ fun i => Additive.ofMul (a i) := by
sorry
end ModuleRank