Fppf homogeneous quotients #
For an affine group G and a closed subgroup N, the fppf homogeneous quotient G/N
is the sheafification of the presheaf of left cosets A ↦ G(A)/N(A). No normality is
required. Maps from this sheaf to an fppf sheaf are exactly natural maps from G
that are invariant under right multiplication by N.
The construction admits nonreduced groups and value algebras, over any commutative base
ring. It supplies the quotient sheaf whose representability as a homogeneous space can
subsequently be proved. Sheafification is essential: a section of G/N need only lift
to G locally in the fppf topology.
We use Mathlib's left-coset setoid and sheafification adjunction. Values are lifted by one universe so that type-valued sheafification is available on the affine site.
References #
- J. S. Milne, Algebraic Groups (2017), §5, homogeneous spaces and quotient sheaves.
- W. C. Waterhouse, Introduction to Affine Group Schemes, §14.
The presheaf of left cosets by a closed subgroup, without a normality assumption.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The left coset represented by a group point.
Equations
- H.homogeneousQuotientPresheafMk I A g = { down := ↑g }
Instances For
To prove a property of a coset section, it suffices to prove it for representatives.
Mapping a left coset maps its representative by the functor of points.
The natural projection from affine-group points to left cosets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The projection sends a point to its left coset.
Every section of the coset presheaf is represented by an ambient group point.
Two points have the same coset exactly when their difference lies in the closed subgroup.
A natural map from group points which is invariant under the subgroup descends to cosets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The descended map has its prescribed value on every representative.
A map from the coset presheaf is determined by its values on group points.
Maps out of the coset presheaf are precisely natural subgroup-invariant maps out of G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The presheaf universal property restricts a map along the coset projection.
The fppf homogeneous quotient by the closed subgroup cut out by I.
Normality and representability are not required for this construction.
Equations
- H.fppfHomogeneousQuotient I = (CategoryTheory.presheafToSheaf (TauCeti.CommAlgCat.fppfTopology R) (Type (?u.1 + 1))).obj (H.homogeneousQuotientPresheaf I)
Instances For
The homogeneous quotient is obtained by applying the fppf sheafification functor to the coset presheaf.
The quotient's underlying presheaf is the sheafification of the coset presheaf.
The canonical map from affine-group points to the fppf homogeneous quotient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The projection to the homogeneous quotient is the coset projection followed by the unit of fppf sheafification.
The quotient projection sends a point to the sheafification of its left coset.
Every section of the homogeneous quotient lifts fppf locally to a group point.
Maps from G/N to any fppf sheaf are exactly natural maps from G invariant under
right multiplication by the closed subgroup N, over all value algebras.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The universal property sends a sheaf morphism to its composite with the quotient projection.
Descending a subgroup-invariant natural map and then restricting along the quotient projection recovers that map.