Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Finite elementary abelian -groups have bases, basis extension, and a well-defined dimension
Statement
Every finite elementary abelian -group has a basis; every independent subset extends to a basis, every spanning subset contains a basis, and all bases have the same finite size.
Facts & Assumptions
Given: A finite elementary abelian -group , an independent subset , and a spanning subset .
A basis of an elementary abelian -group is an independent spanning subset for its canonical -linear structure (-spanning sets, independence, and bases in an elementary abelian -group).
The cardinality of a finite Cartesian product is the product of the cardinalities of its factors (The product rule: , and ).
If a positive integer is written as a finite product of powers of distinct primes, every exponent equals the corresponding canonical valuation (For and any injective list of primes containing every prime divisor of , one has ; the exponents are determined by , and for every prime outside the list).
Every nonempty subset of has a least element (The well-ordering principle).
Proof
The set of cardinalities of spanning subsets of is nonempty because spans itself, so [L3] gives its least member; choose a spanning subset of that size. It is inclusion-minimal, and if a nontrivial linear relation existed in , one member with nonzero coefficient could be solved for using its inverse scalar, contradicting minimality. Thus is a basis by [F1].
Starting from , adjoin an element outside its span while one exists; adjoining such an element preserves independence, and finiteness makes the process terminate at a spanning independent set. This extends to a basis. Applying the deletion argument of step 1.1 inside extracts a basis from every spanning set.
If is a basis, uniqueness of coordinates gives a bijection , so [L1] gives . For two bases , the equality and uniqueness of the exponent of the prime in [L2] give .
Depends on
- $\mathbb F_p$-spanning sets, independence, and bases in an elementary abelian $p$-group
- The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$, and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$
- For $n \ge 1$ and any injective list $p : r \to \mathbb{Z}$ of primes containing every prime divisor of $n$, one has $n = \prod_{i<r} p_i^{\,v_{p_i}(n)}$; the exponents are determined by $n$, and $v_q(n) = 0$ for every prime $q$ outside the list
- The well-ordering principle
Used by
- Every element outside Φ(P) belongs to a minimal generating set of P Corollary
- Maximal subgroups of a finite p-group are the inverse images of Frattini hyperplanes Corollary
- Minimal generating sets of a finite p-group have size d(P) Corollary
- The generator rank d(P) of a finite p-group Definition
- Burnside Basis Theorem Theorem
- The Frattini quotient is the largest elementary abelian quotient of a finite p-group Theorem
Dependency tree · two levels
44 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- K. Conrad, Generating Sets, consequences of Theorem 6.12 (standard reference, not scraped)
- M. van Beek, Topics in Finite p-Groups, Theorem 3.7 (standard reference, not scraped)