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

Kummer covers of the multiplicative group

Example

Assume AC. Let k be an algebraically closed field, let n≥1 be invertible in k, and put Gm,k=Spec⁡k[u,u−1]. The power map Spec⁡k[t,t−1]⟶Spec⁡k[u,u−1],u⟼tn is a connected finite étale cover of degree n. Its deck group is μn(k), acting by t↦ζt. With geometric basepoint u=1 and a chosen lift t=1, it yields a continuous surjective quotient of π1et(Gm,k,1) of order n. These examples exhibit finite covers; no assertion that they exhaust all covers in positive characteristic is made.

If char⁡k=p>0 and p∣n, the same finite power map is not étale. Its fibre over u=1 is nonreduced, so its degree cannot be interpreted as the number of geometric fibre points of a finite étale cover.

Facts & Assumptions

Given: AC, k, n, the two Laurent polynomial rings and the indicated power map.

[F1]

Finite free algebras with zero differentials are finite étale, and their module rank counts geometric fibre points (Finite étale algebras have finite locally free underlying modules).

[F2]

A connected finite étale cover whose automorphisms act simply transitively on the fibre is Galois. Its finite deck group, with the opposite-action convention if necessary, is a quotient of the profinite fibre-functor group (Finite étale covers admit connected Galois trivializations and subgroup quotients, Finite étale covers are equivalent to finite continuous étale fundamental group sets). The basepoint conventions are Geometric fibre functor and étale fundamental group. AC is inherited through these suppliers (The Axiom of Choice).

Verification

1.1F1algebra

The upstairs algebra is k[u,u−1][T]/(Tn−u): T is automatically invertible because Tn=u, so this quotient is k[t,t−1]. Division by the monic polynomial shows that 1,T,…,Tn−1 is a free basis over the downstairs ring. The derivative nTn−1 is a unit, so the relative differentials vanish. By [F1] the map is finite étale of rank n. Its source is integral and nonempty, hence connected.

2.1F1F2step 1.1

The fibre at u=1 consists of the n distinct roots of Tn−1 in k. Each ζ∈μn(k) gives an automorphism T↦ζT over the base, and these act simply transitively on that fibre. By [F2] all automorphisms are determined by one fibre point, so these are the entire deck group. The explicit reconstruction in [F2] gives a continuous surjection from the fundamental group to its opposite deck group; this is the same group because μn(k) is abelian.

3.1F1step 1.1algebra∎

If p∣n, write n=pam with a≥1 and p∤m. In characteristic p, Tn−1=(Tm−1)pa. Thus the finite fibre over 1 has nonzero nilpotents and is not geometrically regular of dimension zero. It cannot be a fibre of an étale morphism by [F1]. This verifies the characteristic restriction and the degree interpretation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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