Two-power ranks of finite abelian groups

DefinitionThe subgroup \(2^kA\)#✓fully proved

For an abelian group \(A\), written additively, and a natural number \(k\), \(2^kA\) is the subgroup \(\{2^k a : a \in A\}\) of \(A\), the image of multiplication by \(2^k\).

def twoPowerImage (A : Type*) [AddCommGroup A] (k : ℕ) : Submodule ℤ A :=
  LinearMap.range (LinearMap.lsmul ℤ A (2 ^ k : ℤ))

Used by 2

Used byThe two-power layer \(2^{j-1}A / 2^jA\) · The \(2^j\)-rank of a finite abelian group

AbbreviationThe two-power layer \(2^{j-1}A / 2^jA\)#✓fully proved

For an abelian group \(A\), written additively, and a natural number \(j\), this is the quotient group \(2^{j-1}A / 2^jA\), where \(2^kA\) denotes the subgroup \(\{2^k a : a \in A\}\) and \(2^jA \subseteq 2^{j-1}A\). For \(j = 0\), where \(j - 1\) is read as \(0\), it is the trivial quotient \(A / A\).

abbrev higherTwoPowerLayer (A : Type*) [AddCommGroup A] (j : ℕ) : Type _ :=
  twoPowerImage A (j - 1) ⧸
    ((twoPowerImage A j).comap (twoPowerImage A (j - 1)).subtype).toAddSubgroup

Uses 1 · Used by 1

Statement usesThe subgroup \(2^kA\)

Used byThe \(2^j\)-rank of a finite abelian group

DefinitionThe \(2^j\)-rank of a finite abelian group#✓fully proved

Let \(A\) be a finite abelian group, written additively, and let \(j \ge 1\) be an integer. Writing \(2^kA\) for the subgroup \(\{2^k a : a \in A\}\), the \(2^j\)-rank of \(A\) is the dimension over \(\mathbb{F}_2\) of the quotient \(2^{j-1}A / 2^jA\), which is an \(\mathbb{F}_2\)-vector space because \(2\) kills it.

noncomputable def higherTwoPowerRank (A : Type*) [AddCommGroup A] [Finite A]
    (j : ℕ) (hj : 0 < j) : ℕ :=
  letI : Fact (0 < j) := ⟨hj⟩
  Module.finrank (ZMod 2) (higherTwoPowerLayer A j)

Uses 2 · Used by 1

Statement usesThe two-power layer \(2^{j-1}A / 2^jA\) · The subgroup \(2^kA\)

Used byThe \(4\)-rank of a finite abelian group

AbbreviationThe \(4\)-rank of a finite abelian group#✓fully proved

For a finite abelian group \(A\), written additively, the \(4\)-rank of \(A\) is the dimension over \(\mathbb{F}_2\) of the quotient \(2A / 4A\), where \(2A = \{2a : a \in A\}\) and \(4A = \{4a : a \in A\}\); it is the \(2^j\)-rank of \(A\) for \(j = 2\).

noncomputable abbrev fourRank (A : Type*) [AddCommGroup A] [Finite A] : ℕ :=
  higherTwoPowerRank A 2 (by norm_num)

Uses 1

Statement usesThe \(2^j\)-rank of a finite abelian group

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.