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.
Finite decomposition around isolated fibre points after an elementary étale change
Statement
Assume the Axiom of Choice. Let be separated and locally of finite type, let , and let be distinct isolated points of the fibre , where . There is an elementary étale neighbourhood with and an open-and-closed decomposition such that every is finite, consists of one point mapping to with , and has no point mapping to any .
The induction below uses the locally proved single-point construction Finite neighbourhood of an isolated fibre point after elementary etale change.
Facts & Assumptions
Given: The data and hypotheses in the Statement.
An isolated point of a fibre of a locally finite type morphism admits, after an elementary étale base change, an open neighbourhood finite over the new base with singleton chosen fibre and unchanged residue field. The recorded proof constructs the finite selected component from published algebraic Zariski Main and the coprime lifting lemma (Finite neighbourhood of an isolated fibre point after elementary etale change).
Étale morphisms are stable under composition and base change, and an elementary étale neighbourhood has the chosen residue field unchanged (Étale stability, Etale neighbourhoods and elementary etale neighbourhoods of a point).
If is finite then it is proper (Finite morphisms are proper); if is separated, a -morphism from the proper to is proper (Morphisms from a proper scheme to a separated one are proper) and hence closed (Proper morphisms are closed). Separatedness is stable under base change (Separatedness survives base change).
Fibre products commute with restriction to open subschemes (Restricting fibre products to open subschemes). When has the same residue field as , a point has a unique point over the pair in , because , and that point has residue field (Points of a fibre product via residue-field tensors).
A finite morphism has affine finite module charts (Finite morphisms of schemes). AC is the choice-function axiom (The Axiom of Choice).
Proof
For take , , the identity étale morphism, and ; the empty list of finite pieces satisfies every condition. Suppose inductively that the assertion holds for , over an elementary étale neighbourhood with decomposition . By [F4] the point has a unique lift with residue field ; distinctness of the original points and the fibre conditions put it in . It remains isolated in , because is open in and base change by the residue-field isomorphism identifies this fibre with .
Apply [F1] to the separated, locally finite type morphism at . It gives an elementary étale neighbourhood and an open containing the selected point, finite over , with singleton fibre over and the same residue field. The composite is elementary étale by [F2] and . Base change all prior pieces to ; they remain disjoint open-and-closed pieces, finite over , with their singleton chosen fibres and residue fields by [F4] and finite-module base change.
The new open immersion is also closed. Indeed is finite and hence proper by [F3], and is separated as an open-and-closed subscheme of the separated base change ; [F3] makes proper and therefore closed. Thus is open and closed in and in . Let , an open-and-closed complement. It has no point over mapping to any with : the earlier points lie in their preserved and the new point lies in . This completes the induction step.
Finite induction through gives the displayed decomposition and all fibre conditions. The case of an empty fibre is covered by . No quasi-compactness of or is used, and nonreduced singleton fibres are allowed. AC is spent only through [F1] and the finite/proper suppliers; the single-point étale neighbourhood is supplied by [F1].
Depends on
- The Axiom of Choice
- Etale neighbourhoods and elementary etale neighbourhoods of a point
- Finite morphisms of schemes
- Finite neighbourhood of an isolated fibre point after elementary etale change
- Étale stability
- Restricting fibre products to open subschemes
- Points of a fibre product via residue-field tensors
- Morphisms from a proper scheme to a separated one are proper
- Finite morphisms are proper
- Proper morphisms are closed
- Separatedness survives base change
Used by
Dependency tree · two levels
64 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
- The Stacks Project, More on Morphisms, Section 37.41 (étale neighbourhoods) (standard reference, not scraped)