Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
How 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.

Under Choice, a submodule of an arbitrary-rank free module over a PID is free

Statement

Assume the Axiom of Choice. If R is a commutative principal ideal domain, F is a free R-module on an arbitrary set, and N⊆F is a submodule, then N is free.

Facts & Assumptions

Given: Such R,F,N, and AC.

[F1]

In a PID every ideal is principal, and the ring is a domain: Principal ideal domain.

[F2]

A free module has unique finite-support basis expansions, including the empty basis for zero: The free module on a set and its standard basis.

[F3]

AC selects an element of each nonempty set in a set-indexed family: The Axiom of Choice.

[F4]

Under AC every set can be well ordered: The well-ordering theorem.

[F5]

A property on a well-order follows if its truth below any element implies its truth at that element: Transfinite induction.

Proof

1.1F2F4given

Fix a basis (ea)a∈I of F and well-order I. Put F≤a=span⁡{eb:b≤a}, F<a=span⁡{eb:b<a}, and N≤a=N∩F≤a. The coordinate projection pa:F→R is linear by uniqueness of basis expansions.

2.1step 1.1F1F3

Its image Ja=pa(N≤a) is an ideal: pa(x)−pa(y)=pa(x−y) and rpa(x)=pa(rx) for x,y∈N≤a and r∈R. Write Ja=(ρa). For each a with Ja≠0, the set of pairs (ρ,u) with Ja=(ρ), u∈N≤a, and pa(u)=ρ is nonempty. AC selects such a pair (ρa,ua) simultaneously for these indices. In particular ρa≠0. Let S={a:Ja≠0}.

3.1step 1.1step 2.1F2

We verify the hypothesis of transfinite induction for the assertion that N≤a is spanned by the ub with b∈S, b≤a. Suppose the assertion holds at every b<a and take x∈N≤a. If pa(x)=0, put y=x. Otherwise a∈S, and pa(x)=rρa for some r∈R; put y=x−rua. In both situations y∈N∩F<a. If y≠0, its finite support has a greatest element b<a, so the assertion at b expresses y in the required earlier generators. If y=0, its expression is the empty sum. Restoring rua when present proves the assertion at a.

3.2step 1.1step 2.1F1

For a finite relation ∑a∈Eraua=0 with distinct a∈S, suppose some coefficient is nonzero and take the greatest such index a. Every ub with b<a has zero a coordinate. Applying pa gives raρa=0. Since R is a domain and ρa≠0, this forces ra=0, contrary to its selection. Thus all coefficients vanish.

4.1step 3.1F2F5

Transfinite induction now proves the assertion at every a. Each nonzero x∈N has a greatest support index and hence belongs to one N≤a; therefore the ua span N. This also covers a limit initial segment: every one of its finite supports lies in a smaller principal initial segment, so no additional generator is needed at a limit cut.

5.1step 4.1step 3.2F2∎

Spanning and independence make (ua)a∈S a basis. If N=0, every Ja=0 and this is the empty basis; if I=∅, also F=N=0. In rank one the same construction is simply the zero ideal or its single nonzero generator. These possibilities require no choice from an empty fiber.

Depends on

Dependency tree · 2 levels

Sources