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.
Quotients of schemes by etale equivalence relations are algebraic spaces
Statement
Assume the Axiom of Choice inherited from the quotient and descent suppliers (The Axiom of Choice). Let be a scheme, let be a scheme over and let be an etale equivalence relation on over (Groupoids in schemes, relations and etale equivalence relations). Then the fppf quotient sheaf (The fppf quotient sheaf of a pre-relation) is an algebraic space over (Algebraic spaces over a scheme, defined as fppf sheaves), and is etale and surjective; equivalently is a presentation of (Presentations of algebraic spaces).
Facts & Assumptions
Given: A scheme over , an etale equivalence relation , the quotient sheaf , and AC.
Restriction of an etale equivalence relation along an etale morphism is again an etale equivalence relation (Restriction of an etale equivalence relation).
If is flat and locally of finite presentation, then is representable and an open immersion whose image is the saturated open ; it is an isomorphism when that open is all of , in particular when is surjective (Flat locally finitely presented restrictions give open subquotients).
For affine , the quotient is an algebraic space and is representable, etale and surjective (The quotient of an affine etale equivalence relation is an algebraic space).
Disjoint unions of algebraic spaces with a scheme cover, and gluing of an algebraic space from open subfunctors that are algebraic spaces with surjective union, are algebraic spaces (Gluing algebraic spaces along open subfunctors).
If is an algebraic space, then is representable, etale and surjective (Quotient maps of etale equivalence relations are etale surjective).
Proof
Reduction to a disjoint union of affines. Let be the disjoint union of the members of an affine open covering of . The family is a surjective étale morphism, hence flat and locally of finite presentation; by [F1] the restriction of to is an étale equivalence relation, and by [F2] applied to the jointly surjective morphism the induced map is an isomorphism. Hence we may replace by the disjoint union of affine schemes .
The affine pieces. Let be the restriction of to ; by [F1] it is an etale equivalence relation, and by [F3] the quotient is an algebraic space with representable, etale and surjective. The canonical morphisms are representable open immersions by [F2], and the induced map is surjective as a morphism of sheaves because the cover and is the quotient sheaf of : every section of lifts fppf-locally to , hence to some .
The coproduct is an algebraic space. The morphism is a disjoint union of the representable etale surjective covers , hence representable, etale and surjective, and its source is a scheme; by clause (1) of [F4] the coproduct is an algebraic space.
Gluing. The hypotheses of clause (2) of [F4] are satisfied: is an fppf sheaf, each is representable and an open immersion, the map is surjective, and is an algebraic space by step 1.3. Hence is an algebraic space over , and is representable, etale and surjective by [F5], so is a presentation. The Axiom of Choice is inherited from the quotient and descent suppliers used in [F2]-[F3].
Depends on
- The fppf quotient sheaf of a pre-relation
- Groupoids in schemes, relations and etale equivalence relations
- Algebraic spaces over a scheme, defined as fppf sheaves
- Presentations of algebraic spaces
- Restriction of an etale equivalence relation
- Flat locally finitely presented restrictions give open subquotients
- Quotient maps of etale equivalence relations are etale surjective
- The quotient of an affine etale equivalence relation is an algebraic space
- Gluing algebraic spaces along open subfunctors
- The Axiom of Choice
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
44 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, Chapter 65 (Algebraic Spaces), Theorem 65.10.5 (standard reference, not scraped)