Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-13
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.

Integral homology of a wedge of higher spheres has its cell basis

Statement

Let n≥2 and let W=⋁j∈JSjn be the CW wedge of a set of copies of an oriented sphere, with inclusions ιj, common vertex b, and projections pj collapsing the other summands. The empty wedge means a point. With integral coefficients, H0(W)=Z,Hi(W)=0(0<i≠n), and the map Ψ:⨁j∈JZ⟶Hn(W),(aj)⟼∑jaj(ιj)∗[Sjn] is an isomorphism. Its inverse sends z to the finitely supported vector whose jth coefficient is determined by (pj)∗z=aj[Sjn]. These statements require no choice principle.

Facts & Assumptions

[F1]

The first potentially nonzero homotopy group of a wedge of higher spheres has its cell basis supplies this wedge's CW structure, its continuous collapsing projections and path connectedness. Its proof also constructs the finite-support integer direct sum and its universal property. No homotopy-to-homology comparison theorem is used here.

[F2]

A CW quotient induces relative singular homology isomorphisms identifies the homology of a nonempty CW pair with homology relative to the quotient point by the actual quotient map.

[F3]

Long exact sequence of a pair gives the exact sequence with its inclusion and quotient maps.

[F4]

For a path-connected based space (V,v), the pair exact sequence [F3], vanishing positive homology of the point, and the H0 isomorphism supplied by [F5] show directly that Hi(V)→Hi(V,{v}) is an isomorphism for every i≥1.

[F5]

Homology of spheres gives the oriented integral sphere groups. Zero-th singular homology is free on path components identifies H0 for a path-connected nonempty space with Z.

Proof

Given: The spheres, their supplied orientations, and the CW wedge in the statement. All chain and homology groups in this proof have coefficients Z.

1.1F1F2F3F4given

For a finite set J and j∈J, put U=⋁k∈J∖{j}Skn, retaining b when this set is empty. This is a nonempty CW subcomplex by [F1]. Collapsing the last sphere gives a continuous retraction r:W→U, since its characteristic-disk restrictions are the identity on the remaining disks and constant on the last. The quotient W/U is canonically Sjn: its one remaining characteristic disk has its entire boundary collapsed, and the map-out test is precisely that of this sphere. Under this identification the quotient map is pj. Write k:U↪W, s=ιj, and jS:Hi(Sjn)→Hi(Sjn,{b}). For i>0, [F2] and [F4] make t=jS−1(pj)∗:Hi(W,U)→Hi(Sjn) an isomorphism. If jW:Hi(W)→Hi(W,U) is the pair map, naturality on singular chains gives tjW=(pj)∗, since both sides postcompose with pj.

1.2F1F6given

For any set J, every integral singular chain c in W is supported in a finite subwedge. Indeed [F6] writes c as a finite sum of singular simplices. Their domains are compact by [F6], so each image lies in a finite CW subcomplex. The union of the finitely many resulting cell sets, enlarged by b, is a finite subwedge of this particular CW structure. Only finitely many witnesses are needed for this one chain. Inclusions of subspaces induce injective singular chain maps: distinct maps into the subspace remain distinct after its set-theoretic inclusion, so their finite formal sums stay distinct. Consequently a chain supported in a subwedge is a cycle there exactly when it is a cycle in W, and a displayed boundary equation between supported chains also holds in the subwedge.

2.1F3F4step 1.1

For i>0, k∗ is injective because r∗k∗=1. Also (pj)∗s∗=1. Exactness of [F3] and step 1.1 give ker⁡(pj)∗=im⁡k∗. For any z∈Hi(W), z−s∗(pj)∗z is in that kernel, so is uniquely k∗x. Applying r∗ gives x=r∗z, since rs:Sjn→U is constant and is zero on positive homology: it factors through a point, whose positive homology vanishes as used in [F4]. Therefore z=k∗r∗z+s∗(pj)∗z. Conversely r∗k∗=1, (pj)∗s∗=1, and both cross composites are zero by the same constant-map argument. Thus (k∗,s∗) gives an isomorphism Hi(U)⊕Hi(Sjn)→Hi(W) with inverse (r∗,(pj)∗). This also proves the splitting in degree one without assuming anything about a negative-degree group.

3.1F1F4F5step 2.1

Induction on the finite cardinality of J now proves that the positive homology of a finite wedge is the direct sum of the homology of its sphere summands, with inclusions as the forward map and the collapsing projections as inverse. The initial empty wedge is a point and has zero positive homology. Each induction step is precisely step 2.1. In positive degree i≠n, all summand groups vanish by [F5]; in degree n, each is the copy of Z specified by its supplied orientation. Hence the formulas in the statement hold for finite J, including a singleton. There is no choice of an ordering over all finite subsets: induction proves the unique maps specified by the coordinate formulas.

4.1F1F5F6step 1.2step 3.1

For arbitrary J, every class z∈Hi(W) with i>0 has a finite cycle representative in a finite subwedge by step 1.2. If i≠n, step 3.1 makes it a boundary in that subwedge and hence in W. If i=n, step 3.1 expresses it as a finite sum of the sphere orientation classes, proving surjectivity of Ψ. This map is well defined by finite sums in the abelian homology group and the finite-support group construction [F1]. If a finite vector a maps to zero, represent its finite sum by orientation cycles in those finitely many spheres. Its image is the boundary of one finite chain in W. Step 1.2 puts that chain in a finite subwedge; enlarge it by the finite support of a. The chain boundary equation holds already there, so step 3.1 forces every coefficient of a to be zero. This proves injectivity.

5.1F1F4F5step 1.2step 3.1step 4.1∎

A cycle for z∈Hn(W) is supported in a finite subwedge WJ0 by step 1.2. For j∉J0, pj is constant there, so (pj)∗z=0 in positive degree. For j∈J0, the finite computation of step 3.1 identifies its coefficient with exactly (pj)∗z=aj[Sjn]. This proves the asserted inverse and finite support; the coefficients depend only on z because induced homology maps are well defined. Finally W is nonempty and path connected by [F1], including the stipulated empty wedge, so [F5] gives H0(W)=Z. Thus degree zero is one shared component, not a sum over J. Zero vectors and zero cycles were included in the finite argument, and no first-degree exception is hidden: H1(W)=0 since n≥2. Every arbitrary-index passage used a single finite chain or bounding chain, and orientations were supplied, so no AC was used.

Depends on

Dependency tree · 2 levels

Sources