Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-14
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.

Mod-two cohomology rings of complex projective spaces

Statement

Assume AC. For every integer n≥0, H∗(CPn;F2)≅F2[cn]/(cnn+1),∣cn∣=2, where cn is reduction modulo two of the normalized integral generator. Also H∗(CP∞;F2)≅F2[c],∣c∣=2. All odd cohomology groups vanish. Standard skeletal restrictions preserve the named generators and are isomorphisms in every degree at most twice the complex dimension of the finite target.

Facts & Assumptions

Given: The standard finite skeleta CP0⊂CP1⊂⋯⊂CP∞ and coefficients F2.

[F1]

A CW complex with no cells in adjacent dimensions has zero cellular boundary computes a cellular complex with no adjacent cells, while Cellular homology computes singular homology, Oriented cellular chain group, and Cellular maps induce cellular chain maps compare its oriented cell generators and skeletal maps with singular homology.

[F2]

Under AC, Topological universal coefficient short exact sequence for cohomology gives natural evaluation exact sequences for integral and mod-two cohomology, natural also in coefficient homomorphisms.

[F4]

Homotopic maps induce equal maps in singular cohomology applies to the coordinate retractions below, and Excision for singular cohomology removes closed coordinate hyperplanes lying inside the open relative subspaces.

[F5]

Under AC, Local coordinate cup products generate top relative cohomology says that the two coefficient-one local generators on Ci×Cj≅R2i×R2j have nonzero top mod-two relative cup product when i,j≥1.

[F6]

Relative cup products are natural and connector-compatible transports open relative products. Pullback is a unital ring homomorphism by Cup product is natural, unital and associative.

[F7]

Singular cochain complex with coefficients, Singular cup product on cochains, and Singular cohomology is contravariantly functorial make coefficient reduction valuewise on cochains and make it commute with coboundary, pullback, and the front/back cup formula.

[A1]

The Axiom of Choice is assumed exactly through [F2] and [F5].

Proof

technique · build the standard even-cell filtration explicitly, compute its additive groups, prove finite products by local relative coordinates, and detect infinite powers on finite skeleta
1.1givenconstruct

The standard filtration gives one oriented cell in each even dimension and no odd cells. Write Pr=CPr as nonzero vectors in Cr+1 modulo nonzero complex scaling. Attach a real 2r-disk to Pr−1 by w⟼[w0:⋯:wr−1:1−∥w∥2]. The boundary lands in Pr−1, while each line outside Pr−1 has a unique unit representative whose last coordinate is positive real, so the open disk maps homeomorphically to the complement. The attachment quotient is compact. Projective space is Hausdorff because a unit vector z maps to the rank-one matrix zz∗, whose fibres are precisely scalar-phase orbits; the induced continuous bijection from the compact phase quotient to its matrix image is a homeomorphism. Hence the attachment map from its compact quotient to Pr is a homeomorphism. Starting from P0=∗ gives compatible cells in dimensions 0,2,…,2r. Orient the 2r-cell by the ordered real and imaginary coordinates of Cr.

2.1F1step 1.1

Integral homology is one copy of Z in each occupied even degree, naturally under skeletal inclusions. There are no cells in adjacent dimensions, so [F1] makes every cellular differential zero and compares the resulting groups with singular homology. The positive 2k-cell in the standard Pk gives the generator of H2k(Pn;Z) for k≤n. A standard inclusion is the identity on each cell it contains, so [F1] makes its homology map the identity on these generators. The union P∞ has the same calculation in every fixed degree: one copy of Z in nonnegative even degrees and zero in odd degrees.

3.1F2A1step 2.1

Integral and mod-two cohomology are additively determined, with natural skeletal restrictions. In [F2], all Ext terms vanish because the preceding integral homology group in each even degree is zero and the preceding group in each odd degree is free. Evaluation therefore gives H2k(Pn;Z)=Z and H2k(Pn;F2)=F2 for 0≤k≤n, with all odd groups zero; the same holds in every degree for P∞. Naturality and step 2.1 make restriction to Pn an isomorphism through degree 2n. Let un∈H2(Pn;Z) be the class evaluating as +1 on the positive P1 cell when n≥1, and put u0=0. Restrictions preserve these normalized classes.

4.1F2F7step 3.1

Reduction modulo two of the normalized integral class is the unique finite degree-two generator. For n≥1, choose an integral cocycle representing un and reduce its values modulo two. By [F7], this commutes with coboundary and is independent of the cocycle representative; it defines cn. Coefficient naturality of evaluation in [F2] makes cn evaluate as 1 on the mod-two reduction of the positive P1 cell, so it is nonzero and hence is the unique class in degree two. The front/back formula in [F7] shows that reduction commutes with cup products. Put c0=0. Restriction preserves every cn because it preserves un and commutes with coefficient reduction.

5.1F4step 4.1

Complementary coordinate projective subspaces admit the required explicit retractions. Fix i,j≥1 with i+j=n. Let E=Pi use coordinates z0,…,zi, let F=Pj use zi,…,zn, and let p=E∩F=[ei]. Put V=Pn∖F and W=Pn∖E. Scaling zi,…,zn to zero retracts V and E∖{p} onto the same coordinate Pi−1; the first i coordinates cannot all vanish on either domain. Symmetrically, W and F∖{p} retract onto Pj−1. Scaling only zi to zero retracts Pn∖{p} onto a coordinate Pn−1. Each formula commutes with complex scaling, never produces the zero vector on its stated domain, fixes the target, and is continuous in affine coordinates, so [F4] applies.

6.1F3F4step 3.1step 5.1

The complementary classes lift uniquely to relative generators and the top local-to-global map is an isomorphism. Step 5.1 and step 3.1 give H2i−1(V;F2)=H2i(V;F2)=0. Exactness in [F3] therefore makes H2i(Pn,V)→H2i(Pn) an isomorphism. The analogous map for (E,E∖{p}) is an isomorphism, and the natural pair square together with the absolute restriction isomorphism of step 3.1 identifies these two relative groups. The same holds for F,W in degree 2j. Finally the punctured-space retraction gives vanishing in degrees 2n−1 and 2n, so H2n(Pn,Pn∖{p})→H2n(Pn) is an isomorphism.

7.1F3F4F5F6A1step 6.1

The product of the unique classes in complementary positive even degrees is the nonzero top class. In the affine chart zi≠0, ordered ratios identify a neighborhood of p with Ci×Cj. They identify E,F with the two coordinate planes, V with (Ci∖0)×Cj, and W with Ci×(Cj∖0). Excision in [F4], followed by contraction of the unused coordinate, identifies the nonzero relative classes from step 6.1 with the coefficient-one local generators. Their relative product is nonzero by [F5]. The open complements satisfy V∪W=Pn∖{p}, so [F6] transports the product to the top relative group and then through step 6.1 to a nonzero absolute product. Since that top group is one-dimensional by step 3.1, this is its unique nonzero class.

8.1F6step 3.1step 4.1step 7.1

Every finite projective space has the asserted truncated polynomial ring. For n=0, only the unit remains and c0=0. For n=1, c1 is nonzero and c12=0 above dimension two. Inductively suppose the claim holds for Pn−1. Step 4.1 and [F6] make cnk restrict to the nonzero cn−1k for k<n. Step 7.1 with i=n−1,j=1 then makes cnn=cnn−1cn the nonzero top class. All higher powers vanish above dimension 2n. With the additive calculation of step 3.1, polynomial evaluation is onto and its kernel is exactly (cnn+1).

9.1F2F6A1step 2.1step 3.1step 8.1

Finite-skeleton detection gives the infinite polynomial ring. Let c be the unique nonzero element of H2(P∞;F2). Restriction to every Pn with n≥1 is an isomorphism in degree two, so it sends c to cn. By [F6], ck restricts to cnk, which is nonzero when n≥k by step 8.1. Hence ck is the unique nonzero class in degree 2k from step 3.1. Polynomial evaluation is onto degreewise and injective because a polynomial has finitely many homogeneous terms of distinct degrees.

10.1F1F2F3F4F5F6F7A1step 1.1step 2.1step 3.1step 4.1step 5.1step 6.1step 7.1step 8.1step 9.1∎

Every boundary, degeneracy, and choice case is explicit. The cases n=0,1, the unit power k=0, the top power k=n, and the first vanishing power k=n+1 were separated. There is no top degree for P∞, but every fixed power is detected on a finite skeleton. The spaces are nonempty; zero classes and all odd groups are zero. The local product uses i,j≥1, so no zero-dimensional factor is smuggled into [F5]. The homotopies in step 5.1 specify both endpoints and their nonzero domains. The singular cochain definitions in [F7] retain degenerate simplices. Coefficient reduction is a specified map and introduces no choice. AC is used exactly through UCT [F2] and the local product [F5]; the finite coordinate constructions add none. No biconditional or converse is asserted.

Depends on

Dependency tree · 2 levels

Sources