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.
is projective but not free over
Example
Let . The ideal is isomorphic to as an -module. It is projective but not free.
Facts & Assumptions
Given: The ring and its ideal .
Under AC, being a direct summand of a free module is equivalent to projectivity (Equivalent characterizations of projective modules).
A free module with a finite basis is projective using only finite choice, which is provable in ZF (Free modules are projective, with the exact choice boundary).
A free module is a direct sum of copies of the regular module, with one standard vector per basis element (The free module on a set and its standard basis).
Verification
The element is idempotent modulo , and is also idempotent, with and . Hence .
The module has two elements. A free module on the empty set has one element; a free module on a nonempty finite set of size has elements; and a free module on an infinite set has infinitely many distinct standard basis vectors. None has two elements.
Thus is a direct summand of the rank-one free module , which is projective without AC by [L2]. Precomposing a map from with the projection , lifting from , and restricting the lift to proves directly that is projective. The map sending to is an -module isomorphism.
Hence is projective and nonfree over .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 29 results over 8 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- A. Kleshchev, Lectures on Abstract Algebra for Graduate Students, sections 3.6, 3.14, and 3.15 (standard reference, not scraped)
- The Stacks Project, Algebra (standard reference, not scraped)
- P. Hekmati, Homological Algebra, section 3.1 (standard reference, not scraped)