Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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 cyclic geometric weight-zero monodromy system

Example

Assume AC (The Axiom of Choice). The finite étale morphism f:C×→C×, z↦zr, for r≥1, gives a rank-r geometric pure weight-zero local system R0f∗Q (Geometric polarizable Hodge variations on algebraic bases, Local systems and pullback). Its monodromy cyclically permutes the r sheets and its complexification is a direct sum of one-dimensional root-of-unity characters (The group μn(K) of n-th roots of unity in a field, and primitive n-th roots of unity).

Verification

1.1givenconstructalgebra

Geometric structure and the local system. The graph {(t,[u:v])∈C××P1:ur=tvr} is closed, and z↦(zr,[z:1]) identifies C× with it over C×, so f is projective and proper and its fibres are the r distinct r-th roots of the base point. On coordinate rings f is module-finite, the source ring being generated over the target ring by 1,z,…,zr−1; and it is smooth of relative dimension zero because the derivative rzr−1 is a unit on C×, so the Jacobian criterion Relative Jacobian criterion with its presentation hypothesis applies and the relative dimension is 1−1=0, which is exactly étaleness by the definition Étale morphism of schemes. Thus f is finite étale. Therefore R0f∗Q is a finite-rank local system of rank r in the sense of Local systems and pullback: over each base point the fibre is H0 of r reduced points, with the sheet-indicator functions as a rational basis, and these bases are transported by the deck identifications of the fibres. Every indicator function is locally constant of Hodge type (0,0), so the local system is pure of weight zero. The standard positive definite dot product in the indicator basis is rational, flat because transport permutes the basis vectors and hence preserves the form, and positive on every fibre; it is therefore the polarization required for a geometric polarizable weight-zero variation, whose algebraic realization is f itself on the open U=C×.

2.1step 1.1givenconstructalgebra∎

Monodromy and semisimplicity. The homotopy z↦((1−u)+u∣t0∣/∣z∣)z gives a deformation retraction of C× to the circle of radius ∣t0∣, fixing t0 throughout. Multiplication w↦t0w identifies that circle, based at t0, with the geometric unit circle, based at 1. Hence The trigonometric loops give π1({(x,y):x2+y2=1},(1,0))≅Z makes γ(t)=e2πitt0 a positive generator at t0. Label the roots by za=ζaz0 and their indicator functions by ea, where ζ=e2πi/r has order r by The n-th roots of a complex number and the n distinct roots of unity for every n≥1. The lifted loop t↦e2πit/rza ends at za+1. Covariant cohomology transport is the inverse pullback, so Tγea=ea+1. The left monodromy convention of Local systems and pullback uses ρ(γ)=Tγˉ, hence ρ(γ)ea=ea−1. Therefore vj=∑a=0r−1ζjaea satisfies ρ(γ)vj=ζjvj. These vectors form a basis: the geometric-sum identity ∑a=0r−1ζka=0 for r∤k and r otherwise gives the inverse Fourier matrix r−1(ζ−ja). Thus the complexification is a direct sum of the r distinct one-dimensional characters, including the trivial character when r=1, and is semisimple. Finally Semisimplicity of geometric Gauss-Manin local systems applies to this smooth projective morphism and proves semisimplicity over every characteristic-zero coefficient field, including fields without the r-th roots of unity.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 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