Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generated
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.

A proper singular curve with weight-zero cohomology

Example

Assume AC (The Axiom of Choice). Let C be an integral complex projective curve whose normalization ν:P1→C is an isomorphism outside a single ordinary node, with two distinct points above that node. Then H1(C,Q) is one-dimensional of weight 0, illustrating that proper singular cohomology need not be pure of its degree.

Verification

Given: The Axiom of Choice (The Axiom of Choice), an integral complex rational projective curve C with a single singular point, an ordinary node, and its normalization ν:P1→C identifying two distinct points a,b and an isomorphism over the complement of the node.

[F1] Normalization resolves the singularities of a projective curve and Finite morphisms are proper: the normalization of an integral projective curve over a perfect field is a nonsingular projective curve and the normalization map is finite and birational, hence proper and surjective; for the rational nodal curve the normalization is P1 and ν is an isomorphism over the smooth locus.

[F2] Proper hypercovers compute constructible derived cohomology and Proper cohomology and functorial mixed Hodge weights: the Cech nerve of a proper surjection is a proper hypercover, its descent spectral sequence E1p,q=Hq(Cp,Q)⇒Hp+q(C,Q) is strongly convergent with finite diagonals, and for a proper hypercover with smooth projective terms the associated mixed Hodge complex has Gr⁡qWHn(C,Q)≅E2n−q,q with weights at most n.

[F4] The reduction of a scheme, Fibre product of schemes and Morphisms from a proper scheme to a separated one are proper: reduction keeps the underlying points and kills nilpotents; fibre products represent compatible tuples; projective complex schemes are proper by Projective morphisms are proper, and a morphism from a proper complex scheme to a separated complex scheme is proper. The matching and split conventions are those of Split augmented simplicial schemes and matching objects.

[F3] Stereographic projection identifies the Riemann sphere with the unit two-sphere, Homology of spheres and Cohomology over a field is dual to homology over that field: P1(C)≅S2, so H0(P1,Q)=Q and H1(P1,Q)=0, the latter as the dual of H1(S2;Q)=0; also H2(P1,Q)=Q and all higher groups vanish.

1.1F1F2F3F4givenconstructalgebra

Use the reduced Cech nerve Cp=(P1×C⋯×CP1)red, with p+1 factors and maps deleting or repeating entries. Reduction is functorial: a map from a reduced scheme kills nilpotents and hence factors through the target reduction. The underlying points off the node form the diagonal; over the node the tuples are in {a,b}p+1. The diagonal is a closed immersion, and its complement consists of the 2p+1−2 mixed tuples, an open finite set of closed complex points. This set is also closed, so these points and the diagonal are open-and-closed components. The mixed components are reduced points. The reduced diagonal component equals P1: its closed immersion has the whole underlying support, so its ideal lies in the zero nilradical of that reduced component. Thus Cp=Pd1⊔Tp is smooth projective. Every compatible boundary tuple of geometric points has exactly the p+1 compatible vertices of the Cech nerve, so it lifts to Cp; this proves surjectivity of every matching map, even if its target has nilpotents. These maps are proper by [F4], since their sources are projective and the finite matching limits are separated. The augmentation is proper surjective by [F1]. The reduced nerve is also split: repeated adjacent entries are degeneracies, and compressing successive equal entries gives the unique alternating nondegenerate tuple; for p=0 the nondegenerate part is P1. Apply [F2]. Its row E1p,0 has one copy of Q for the diagonal and one per mixed tuple; by [F3] the positive rows vanish except for the single diagonal copy in degree two.

2.1step 1.1algebra

Compute the degree-zero row in low degrees. On C0=P1 one has E10,0=Q, and on C1=Pd1⊔{ab}⊔{ba} one has E11,0=Qd⊕Qab⊕Qba; the alternating sum of the two face pullbacks δ0 sends a constant to the differences of the two diagonal values, hence is zero. On C2 the six nonconstant tuples contribute the coordinates for (aab),(aba),(abb),(baa),(bab),(bba), and evaluating the alternating sum δ1(c) on these components and on the diagonal gives cd on the diagonal and on (aab),(abb),(baa),(bba), and cab+cba−cd on (aba),(bab), where c=(cd,cab,cba). Hence δ1(c)=0 exactly when cd=0 and cba=−cab, so E21,0=ker⁡δ1/im⁡δ0 is one-dimensional, generated by (0,1,−1).

3.1F2F3step 2.1algebra∎

The other total-degree-one entry is E10,1=H1(P1,Q)=0 by [F3], so it contributes nothing; the spectral sequence is first-quadrant with finite diagonals and degenerates at E2 by [F2]. Therefore H1(C,Q)≅E21,0 is one-dimensional, and by the weight identification of [F2] its graded pieces are Gr⁡0WH1=E21,0=Q and Gr⁡1WH1=E20,1=0. The first-quadrant weight identification also makes all graded pieces of negative weight zero; together with the upper bound 1 and finiteness of the weight filtration, this gives W−1H1=0 and W0H1=H1: the whole one-dimensional space is pure of weight 0 and type (0,0) (Rational mixed Hodge structures), as asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

94 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