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 be an algebraically closed field, let be invertible in , and put . The power map is a connected finite étale cover of degree . Its deck group is , acting by . With geometric basepoint and a chosen lift , it yields a continuous surjective quotient of of order . These examples exhibit finite covers; no assertion that they exhaust all covers in positive characteristic is made.
If and , the same finite power map is not étale. Its fibre over is nonreduced, so its degree cannot be interpreted as the number of geometric fibre points of a finite étale cover.
Facts & Assumptions
Given: AC, , , the two Laurent polynomial rings and the indicated power map.
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).
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
The upstairs algebra is : is automatically invertible because , so this quotient is . Division by the monic polynomial shows that is a free basis over the downstairs ring. The derivative is a unit, so the relative differentials vanish. By [F1] the map is finite étale of rank . Its source is integral and nonempty, hence connected.
The fibre at consists of the distinct roots of in . Each gives an automorphism 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 is abelian.
If , write with and . In characteristic , . Thus the finite fibre over 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
- The Axiom of Choice
- Geometric fibre functor and étale fundamental group
- Finite étale algebras have finite locally free underlying modules
- Finite étale covers admit connected Galois trivializations and subgroup quotients
- Finite étale covers are equivalent to finite continuous étale fundamental group sets
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
- Milne, Lectures on Étale Cohomology §3, multiplicative-group coverings and base-field dependence (standard reference, not scraped)
- SGA 1, Exposé V, fibre-functor classification (standard reference, not scraped)