Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-09
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 0xXZFexZFϵZ0,(ex)=x1, 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 Hq(F;Z)=0 for q>1 and H1(F;Z)XZ.

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 QZ of the trivial left module.

[F1]

Reduced words give the free group with no nonempty reduced word equal to 1 (Reduced words form the free group on an alphabet).

[F2]

Group homology is the homology obtained by tensoring the supplied projective resolution with the right trivial module (Group homology as a derived functor).

[F3]

A projective object lifts every morphism through an epimorphism (Projective object).

[F4]

Proof

1.1

For a word w=l1ls, telescoping gives w1=j=1sl1lj1(lj1). A positive letter contributes a multiple of x1, and x11=x1(x1) does too. Every element waww of augmentation zero is waw(w1), so im=kerϵ. Empty words contribute zero; epsilon is onto since epsilon(1)=1.

F1givenalgebra
2.1

Interpret wex 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.

F1step 1.1algebra
3.1

Write R=ZF and denote the displayed free left resolution by P. Turn it into a right resolution T by tg=g1t. This preserves the underlying exact sequence. Each left regular summand becomes a right regular summand by the coordinate map gg1; thus T0R, T1XR, and the right differential sends the basis vector indexed by x to x11. 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 Qq lifts its identity through the canonical surjection from the free left module on its underlying set, making Qq a retract of that free module. Consequently tensoring with Qq 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.

F3step 1.1step 2.1algebra
4.1

Form Dpq=TpRQq for p,q0, with h=dT1 and v=(1)p1dQ. These differentials anticommute, so d=h+v defines the direct-sum total complex. The two augmentations give degreewise surjective chain maps a:TotDTRZ and b:TotDZRQ, zero off q=0 and p=0 respectively. By step 3.1, all augmented columns and all augmented rows are exact. Hence kera, viewed columnwise with its degree-zero column term replaced by the augmentation kernel, has exact columns; similarly kerb has exact rows.

step 3.1givenalgebra
5.1

Both kernel total complexes are acyclic by the following finite argument. For a total n-cycle in kera, 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 kerb, 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.

step 4.1algebra
6.1

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 H(TRZ)H(ZRQ)=H(F;Z) under the assumed DC and supplied-resolution convention.

F2F4step 4.1step 5.1algebra
7.1

The differential of TRZ sends every x11 to zero. Its only nonzero terms are XZ in degree one and Z in degree zero, proving the asserted homology groups. If X is empty, F=1 and the degree-one term is zero.

step 3.1step 6.1algebra

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