PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

A faithfully flat orbit map represents the coset quotient sheaf

Statement

Assume the Axiom of Choice for the represented-sheaf and geometric suppliers used on this page. Let $k$ be a field, let $G$ be a group scheme of finite type over $k$ acting on a separated finite-type $k$ -scheme $X$ (Algebraic group actions, orbit maps, orbit subschemes and scheme-theoretic stabilizers), let $x \in X (k)$ , and let $H$ be a closed subgroup scheme of $G$ (Morphisms and closed subgroup schemes of group schemes) with $H = G_{x}$ (Fibres of the orbit map and the scheme-theoretic stabilizer as a closed subgroup scheme). Assume the orbit map $ϱ_{x} : G \to O_{x}$ is faithfully flat and locally of finite presentation, where $O_{x}$ is the orbit subscheme. Then $O_{x}$ represents the fppf quotient sheaf $G / H$ (Quotient sheaves and representable quotients for pre-relations and group actions), the quotient morphism is $ϱ_{x}$ , and the kernel-pair morphism $G \times_{k} H \to G \times_{O_{x}} G$ , $(g, h) \mapsto (g, g h)$ , is an isomorphism.

Facts & Assumptions

Given: AC, the action of the finite-type $k$ -group scheme $G$ on the separated finite-type $k$ -scheme $X$ , the point $x \in X (k)$ , the closed subgroup scheme $H = G_{x}$ , and the orbit subscheme $O_{x}$ with $ϱ_{x}$ faithfully flat and locally of finite presentation.

[F1]

Representability criterion: for a pre-relation $s, t : R \to U$ with fppf quotient sheaf $U / R$ and a morphism $q : U \to M$ , if $q \circ s = q \circ t$ , if $h_{U} \to h_{M}$ is a surjection of fppf sheaves, and if $(t, s) : R \to U \times_{M} U$ induced by $h_{R} \to h_{U \times_{M} U}$ is a surjection of fppf sheaves, then $M$ represents $U / R$ ; a faithfully flat morphism locally of finite presentation satisfies either surjectivity instance (Criterion for a scheme to represent an fppf quotient sheaf).

[F2]

The stabilizer satisfies $H (R) = {g \in G (R) : g x_{R} = x_{R}}$ for every $k$ -algebra $R$ , and if the orbit map factors through the locally closed orbit subscheme $O_{x}$ , the morphism $G \times_{k} H \to G \times_{O_{x}} G$ , $(g, h) \mapsto (g, g h)$ , is an isomorphism (Fibres of the orbit map and the scheme-theoretic stabilizer as a closed subgroup scheme).

[F3]

For the pre-relation $R = G \times_{k} H ⇉ U = G$ with $s (g, h) = g$ and $t (g, h) = g h$ , the associated fppf quotient sheaf is $G / H$ (Quotient sheaves and representable quotients for pre-relations and group actions).

Proof

Given: AC, the action of $G$ on $X$ , the point $x \in X (k)$ , the closed subgroup scheme $H = G_{x}$ , and $ϱ_{x} : G \to O_{x}$ faithfully flat and locally of finite presentation.

1.1F3givenconstruct

Set $U = G$ and $R = G \times_{k} H$ , with $s (g, h) = g$ and $t (g, h) = g h$ ; by [F3] the fppf quotient sheaf $U / R$ is exactly $G / H$ .

1.2F2givenalgebra

Condition (1) of the criterion holds: for every $k$ -algebra $R$ and every $(g, h) \in G (R) \times H (R)$ one has $ϱ_{x} (s (g, h)) = ϱ_{x} (g) = g x$ and $ϱ_{x} (t (g, h)) = ϱ_{x} (g h) = g (h x) = g x$ , because $h$ lies in $H (R)$ and $H (R) = {u : u x_{R} = x_{R}}$ by [F2].

1.3F1given

Condition (2) of the criterion holds: $ϱ_{x}$ is faithfully flat and locally of finite presentation, so as a singleton family it is an fppf covering and $h_{G} \to h_{O_{x}}$ is a surjection of fppf sheaves by the instance recorded in [F1].

1.4F2givenconstruct

Condition (3) of the criterion holds: by [F2] the morphism $G \times_{k} H \to G \times_{O_{x}} G$ , $(g, h) \mapsto (g, g h)$ , is an isomorphism; the morphism $(t, s)$ of the criterion is $(g, h) \mapsto (g h, g)$ , which is the composite of that isomorphism with the factor swap on the target, so it is also an isomorphism, in particular a surjection of fppf sheaves.

2.1F1step 1.1step 1.2step 1.3step 1.4given∎

Applying the criterion [F1] to $U = G$ , $R = G \times_{k} H$ , $q = ϱ_{x}$ and $M = O_{x}$ using steps 1.2, 1.3 and 1.4 shows that $O_{x}$ represents the fppf quotient sheaf $G / H$ , with quotient morphism $ϱ_{x}$ ; the kernel-pair statement is step 1.4. This is exactly the assertion.

Depends on

Used by

Dependency tree · two levels

38 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

J. S. Milne, Algebraic Groups (corrected 2022 printing, Cambridge University Press) (standard reference, not scraped)
The Stacks Project, Groupoid Schemes, Sections 39.20 and 39.23 (tags 02VG, 03BD, 03C5, 03BM, 03BE) (standard reference, not scraped)