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.
Generator differences form a basis of the free-group augmentation ideal
Statement
If F is free on an arbitrary set X, then is a free resolution of the trivial left module; this exactness assertion requires no choice axiom. Assume additionally the Axiom of Dependent Choice (DC) and supplied projective-resolution data for derived group homology. Then for and .
Facts & Assumptions
Given: F is the reduced-word free group on an arbitrary set X; epsilon sums the coefficients. For the homology conclusions, assume DC and fix the supplied projective resolution of the trivial left module.
Reduced words give the free group with no nonempty reduced word equal to 1 (Reduced words form the free group on an alphabet).
Group homology is the homology obtained by tensoring the supplied projective resolution with the right trivial module (Group homology as a derived functor).
A projective object lifts every morphism through an epimorphism (Projective object).
DC is the explicitly assumed axiom in the derived-homology convention (The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain).
Proof
For a word , telescoping gives . A positive letter contributes a multiple of , and does too. Every element of augmentation zero is , so . Empty words contribute zero; epsilon is onto since epsilon(1)=1.
Interpret as the oriented edge from w to wx. Its boundary is wx-w. The underlying graph is connected by reduced words and has no simple cycle: a simple cycle would give a nonempty reduced word equal to 1, impossible by F1. A finite nonzero edge chain has support in a finite forest. A nonempty finite forest with an edge has a terminal vertex (take an endpoint of a longest simple path); at that vertex its boundary coefficient is plus or minus the nonzero coefficient of its unique incident supported edge. Thus a nonzero finite edge chain cannot have zero boundary, proving injectivity.
Write and denote the displayed free left resolution by . Turn it into a right resolution by . This preserves the underlying exact sequence. Each left regular summand becomes a right regular summand by the coordinate map ; thus , , and the right differential sends the basis vector indexed by x to . Tensoring with a free module preserves exactness: the tensor product is a direct sum of copies of the original sequence, and lifting an element requires preimages only for its finitely many nonzero coordinates. For each fixed q, projectivity of lifts its identity through the canonical surjection from the free left module on its underlying set, making a retract of that free module. Consequently tensoring with also preserves exactness, as a retract of an exact tensor functor. This uses no choice of lifts for an arbitrary basis and no simultaneous choice of splittings for all q.
Form for , with and . These differentials anticommute, so defines the direct-sum total complex. The two augmentations give degreewise surjective chain maps and , zero off q=0 and p=0 respectively. By step 3.1, all augmented columns and all augmented rows are exact. Hence , viewed columnwise with its degree-zero column term replaced by the augmentation kernel, has exact columns; similarly has exact rows.
Both kernel total complexes are acyclic by the following finite argument. For a total n-cycle in , take the largest p with a nonzero component. Its vertical differential is zero, since the component at p+1 is zero. Exactness in that column supplies a vertical primitive. Subtract its total boundary: the p-component vanishes and only a component at p-1 can be introduced. Repeating ends at p=0, where h is zero. There are at most n+1 columns to remove, so the cycle is a boundary. For , use the largest q and horizontal primitives, decreasing q until q=0, where v is zero. Signs are absorbed into the primitives. These arguments use only finitely many existential choices for each cycle.
A degreewise surjective chain map with acyclic kernel induces a homology isomorphism: lift a target cycle; its differential is a kernel cycle, so subtract a kernel primitive to make the lift a cycle. If a source cycle maps to a boundary, lift that boundary's primitive and subtract its differential; the result is a kernel cycle and hence a boundary. This proves surjectivity and injectivity on homology, including degree zero. Applying this to a and b yields under the assumed DC and supplied-resolution convention.
The differential of sends every to zero. Its only nonzero terms are in degree one and in degree zero, proving the asserted homology groups. If X is empty, F=1 and the degree-one term is zero.
Depends on
Used by
Dependency tree · two levels
19 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
- Loh, Group Cohomology, Definitions 1.7.12–13 and Theorem 1.7.15 pp.63–64; Theorem 4.1.18 pp.129–132 (standard reference, not scraped)
- Weibel, An Introduction to Homological Algebra, Definition 6.1.2 and Proposition 6.2.6–Corollary 6.2.7, pp.161,169 (standard reference, not scraped)
- Sharifi, Homological Algebra, Lemma 3.5.8, Proposition 3.5.9 and Remark 3.5.11, pp.66–68 (standard reference, not scraped)