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.
Analytic topology and finite smooth algebraic stratifications of complex varieties
Definition
Let be a classical algebraic variety over in the sense of Classical algebraic prevarieties, regular maps, and varieties: a separated quasi-compact locally ringed space over with a finite cover by affine models , the morphisms being the regular maps, i.e. the morphisms of locally ringed spaces over (Morphisms of locally ringed spaces).
(a) Analytic topology. An affine model carries the subspace topology of the Euclidean topology of ( as the set of functions , and , , are metrics on it, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Complex -space and its real coordinate dictionary, The complex numbers as , with the real embedding and imaginary unit ). For , is the singleton of empty tuples with its unique topology. On an overlap of two affine charts, the transition isomorphism and its inverse are given locally by polynomial quotient functions (Classical algebraic prevarieties, regular maps, and varieties) and are therefore continuous for the Euclidean topologies: polynomial functions are continuous, and a quotient is continuous wherever its denominator does not vanish (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined, A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions). Hence the topologies transported from the two affine models agree on the overlap, so the affine-model topologies glue to a unique topology on the underlying set of (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace): the analytic topology of . Every regular map of complex classical varieties is continuous for the analytic topologies, by the same local description (Continuity of a map of topological spaces at a point and globally), and the analytic topology refines the Zariski topology because polynomial zero sets are Euclidean closed. Whenever a complex algebraic variety is used as a topological space below it carries the analytic topology, and each subvariety carries the subspace topology.
(b) Smooth points. Let be a classical variety over and let . The point is a smooth point of if its algebraic local ring is a regular local ring: a nonzero Noetherian local ring whose maximal ideal satisfies (embedding dimension and regular local ring). The residue field at a classical complex point is . The variety is smooth if every point is smooth. This intrinsic algebraic condition does not require a Zariski neighbourhood to be algebraically isomorphic to an open subset of affine space.
(c) Finite smooth algebraic stratifications. A finite smooth algebraic stratification with the frontier condition of is a finite decomposition into pairwise disjoint nonempty connected locally closed subsets — the strata — where locally closed means for a Zariski-open and a Zariski-closed , such that each , with its reduced induced algebraic structure, is a smooth algebraic subvariety of ; and such that for every the closure of in is a union of strata. The latter is the frontier condition: the frontier of every stratum is a union of strata (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets, Interior, closure, boundary, exterior, derived set and isolated point in a topological space).
The induced structure is the polynomial-quotient function sheaf, not a restriction of . A locally closed is, locally inside an affine model , the set of points with and for polynomials on (Classical algebraic prevarieties, regular maps, and varieties); the map identifies it with the affine model , and its reduced induced structure sheaf is the one transported along this identification: locally functions of the form with nonvanishing on the set. The ambient restriction is not used, since already at the origin of the affine line the ambient stalk is the local ring of the line while the stalk of the reduced point is . An open subset of an affine model is a union of finitely many principal open subsets: finite generation of the ideal of its closed complement supplies finitely many defining polynomials, whose nonvanishing loci cover the open subset. Each principal open subset is again an affine model, so every locally closed subvariety of is a classical variety for the induced structure sheaf. No existence theorem for stratifications, no common-refinement theorem is asserted. The given chart data and elementary locally closed condition above require no choice principle.
Depends on
Classical algebraic prevarieties, regular maps, and varieties
Morphisms of locally ringed spaces
Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace
The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
as the set of functions , and , , are metrics on it
The complex numbers as , with the real embedding and imaginary unit
Complex -space and its real coordinate dictionary
embedding dimension and regular local ring
Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined
A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions
Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets
Interior, closure, boundary, exterior, derived set and isolated point in a topological space
Continuity of a map of topological spaces at a point and globally