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.
Defect decrease and finite smoothening
Statement
Assume AC and DC as inherited from the supplied algebra and scheme results. Let be a discrete valuation ring with fraction field and residue field , and let be a strict henselization.
(a) If is a centre whose -points that lift to -sections of are schematically dense in , and is a smooth open subscheme on which is locally free, then the -dilatation of along lowers the positive defect by at least one for every section specializing in .
(b) For separated, flat and of finite type over an arbitrary discrete valuation ring with smooth generic fibre, there is a finite sequence of blowups in special-fibre centres, proper and generically isomorphisms, whose smooth locus contains the image of every -section of .
Facts & Assumptions
Given: AC and DC, a DVR with uniformizer , fraction field , residue field , a strict henselization , a separated flat finite-type -scheme with smooth generic fibre, and a closed centre with schematically dense liftable -points.
Dilatation charts and the defect computation are Dilatations and defect computation: the -chart is flat with its universal property, and the defect is the torsion length of , computed by Jacobian-minor valuations and bounded uniformly on .
A finitely generated algebra over a field which is injective into a product of copies of the separable closure after evaluation is geometrically reduced, and the smooth locus of a reduced finite-type scheme over a perfect field is dense; separatedness and differential rank control the descent of smoothness through field extensions (Finitely generated extensions of a perfect field are separably generated, Differentials of a separably generated field extension, Field tests for geometric regularity).
A coherent sheaf on a reduced finite-type scheme is free on a dense open of every component (Generic freeness over a Noetherian domain).
Proof
Let have schematically dense -points. On an affine chart with coordinate ring , evaluation at the -points embeds into a product of copies of ; tensoring with any field extension , every relation involves finitely many coefficients, so the embedding remains injective, and is reduced because is separable algebraic over . Hence is reduced and is geometrically reduced. Extending to a perfect closure, the function field of each component is separably generated and the differential rank equals the transcendence degree, so the relative Jacobian criterion produces a smooth neighbourhood of every generic point; smoothness descends through field extensions by [F2]. Therefore the smooth locus of is dense and open, and the restriction of to it is free on a dense open by [F3].
Shrink around a specialization in , so is smooth of dimension and is free of rank . Choose lifts whose differentials give its basis, with vanishing on and the mapping to a basis of . Embed into affine space with these as initial coordinates. Independent rows of the remaining relation differentials cut out a smooth ambient of dimension containing , with these differentials as a basis. Locally has ideal : its displayed equations define a smooth subscheme of dimension containing , hence agree with locally. Put and . For write . Since the map identifies the chosen bases, , so every . Thus with . On every liftable section through , and ; hence . Schematic density of those specializations gives . Therefore .
In the dilatation of write . Since , each relation becomes with in the saturated ideal of the dilatation of . Along a lifted section, the Jacobian rows for have -entries and -entries . Choose a maximal-rank minor realizing the old defect in [F1], of size , where is the generic relative dimension at the section. The corresponding minor of the divided equations is multiplied by , with according to its selected coordinate columns. The new defining ideal may have additional generators, so its minimum minor valuation is at most this value: . If , the generic closed immersion agrees near the generic section by smoothness and equal dimension; the ideal vanishes locally at the specialization by flatness and schematic density, so the original section is already smooth. Thus positive defect implies , proving (a).
For a set of nonsmooth -sections, let be the reduced closure of their specializations. It satisfies the liftable density condition by construction. Let be its dense smooth open where is locally free, and let be the sections specializing there. Repeat with , obtaining , and continue. The dimensions of the nonempty centres strictly decrease, so this gives a finite partition with the specialization closure of . In particular is permissible for the whole current : every section of meeting it belongs to and specializes in . Blowing up uniquely lifts sections by properness; those through the centre lie in its -chart, since the pulled-back ideal contains and is contained in . Their positive defects decrease by step 3.1, while all sections outside the centre are unaffected.
Use induction first on the uniform maximal defect from [F1], and within a fixed on the partition length . The case is smooth. Blow up as in step 4.1 and apply the induction to its lifted subset . All resulting centres stay over in the nonsmooth locus, so the other are unaffected. Once is smooth, the remaining sections have defect at most and their canonical partition has length , since the modification is an isomorphism away from ; apply the second induction. This terminates with finitely many permissible special-fibre blowups, proper and generically isomorphisms, smoothing every section of . Initially take to be all nonsmooth sections of . Centres always avoid the smooth locus, so initially smooth sections remain smooth. This proves (b) over every DVR, using no completeness, excellence or perfect-residue hypothesis.
Depends on
- The Axiom of Choice
- The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain
- Dilatations and defect computation
- Generic freeness over a Noetherian domain
- Finitely generated extensions of a perfect field are separably generated
- Differentials of a separably generated field extension
- Field tests for geometric regularity
Used by
Dependency tree · two levels
78 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
- Bosch, Lutkebohmert, Raynaud, Neron Models (1990), 3.3/5 and 3.4/1-2 (finite permissible smoothening) (standard reference, not scraped)