Documentation

TauCeti.AlgebraicGeometry.GroupScheme.ClosedSubgroup.Criterion

The closed-subgroup criterion #

A closed subscheme of a group scheme is a subgroup scheme exactly when the identity, multiplication of its two copies, and inversion factor through it. Scheme-theoretic factorization is expressed by inclusion of ideal sheaves in the kernels of these maps. Thus the criterion detects the equations on nonreduced bases, not merely stability of geometric points.

grpObjOfClosedImmersion constructs the group law from these three conditions, and exists_grpObj_isMonHom_iff_ker_le proves the converse. The compatible group structure is unique, and is commutative if the ambient group scheme is commutative. The resulting inclusion can be used with ClosedSubgroupScheme.mk. A subgroup scheme is stable under translation by its own points (ker_comap_leftTranslation_le).

The criterion applies to arbitrary closed subschemes, in particular to the finite locally free divisors used to define Drinfeld structures. No Cartier, flatness, finiteness, or smoothness assumption is needed for the group axioms themselves.

References #

source
@[instance_reducible]
noncomputable def TauCeti.GroupScheme.grpObjOfClosedImmersion {S : AlgebraicGeometry.Scheme} {H G : CategoryTheory.Over S} [CategoryTheory.GrpObj G] (i : H ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (he : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)) (hm : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul))) (hj : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv))) :
CategoryTheory.GrpObj H

Construct the group structure on a closed subscheme whose ideal vanishes on the identity, multiplication and inversion maps.

Instances For
    source
    @[simp]
    theorem TauCeti.GroupScheme.grpObjOfClosedImmersion_one {S : AlgebraicGeometry.Scheme} {H G : CategoryTheory.Over S} [CategoryTheory.GrpObj G] (i : H ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (he : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)) (hm : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul))) (hj : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv))) :
    CategoryTheory.MonObj.one = closedImmersionOverLift i CategoryTheory.MonObj.one he

    The identity of the induced group scheme is the lift of the ambient identity.

    source
    @[simp]
    theorem TauCeti.GroupScheme.grpObjOfClosedImmersion_mul {S : AlgebraicGeometry.Scheme} {H G : CategoryTheory.Over S} [CategoryTheory.GrpObj G] (i : H ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (he : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)) (hm : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul))) (hj : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv))) :
    CategoryTheory.MonObj.mul = closedImmersionOverLift i (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul) hm

    The multiplication of the induced group scheme is the lift of the ambient multiplication.

    source
    @[simp]
    theorem TauCeti.GroupScheme.grpObjOfClosedImmersion_inv {S : AlgebraicGeometry.Scheme} {H G : CategoryTheory.Over S} [CategoryTheory.GrpObj G] (i : H ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (he : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)) (hm : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul))) (hj : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv))) :
    CategoryTheory.GrpObj.inv = closedImmersionOverLift i (CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv) hj

    The inversion of the induced group scheme is the lift of the ambient inversion.

    source
    theorem TauCeti.GroupScheme.isMonHom_grpObjOfClosedImmersion {S : AlgebraicGeometry.Scheme} {H G : CategoryTheory.Over S} [CategoryTheory.GrpObj G] (i : H ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (he : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)) (hm : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul))) (hj : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv))) :
    CategoryTheory.IsMonHom i

    The inclusion of the group scheme constructed by the closed-subgroup criterion is a homomorphism.

    source
    theorem TauCeti.GroupScheme.exists_grpObj_isMonHom_iff_ker_le {S : AlgebraicGeometry.Scheme} {H G : CategoryTheory.Over S} [CategoryTheory.GrpObj G] (i : H ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] :
    (∃ (h : CategoryTheory.GrpObj H), CategoryTheory.IsMonHom i) ↔ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one) ∧ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul)) ∧ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv))

    The closed-subgroup criterion. A closed subscheme carries a compatible group structure if and only if its defining ideal vanishes on identity, multiplication and inversion.

    source
    theorem TauCeti.GroupScheme.eq_grpObjOfClosedImmersion {S : AlgebraicGeometry.Scheme} {H G : CategoryTheory.Over S} [CategoryTheory.GrpObj G] (i : H ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (he : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)) (hm : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul))) (hj : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv))) (h : CategoryTheory.GrpObj H) (hi : CategoryTheory.IsMonHom i) :
    h = grpObjOfClosedImmersion i he hm hj

    The compatible group structure supplied by the closed-subgroup criterion is unique.

    source
    theorem TauCeti.GroupScheme.isCommMonObj_grpObjOfClosedImmersion {S : AlgebraicGeometry.Scheme} {H G : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.IsCommMonObj G] (i : H ⟶ G) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (he : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)) (hm : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul))) (hj : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv))) :
    CategoryTheory.IsCommMonObj H

    The subgroup of a commutative group scheme constructed by the criterion is commutative.

    source
    theorem TauCeti.GroupScheme.ker_comap_leftTranslation_le {S : AlgebraicGeometry.Scheme} {H G : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (i : H ⟶ G) [CategoryTheory.IsMonHom i] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ H) :
    (AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i)).comap (CategoryTheory.Over.Hom.left (leftTranslation (CategoryTheory.CategoryStruct.comp x i)).hom) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i)

    A subgroup scheme is stable under translation by its points. Let i : H ⟶ G be a homomorphism of group schemes over S and x an S-point of H. Then left translation by x ≫ i on G carries the closed subscheme cut out by the ideal sheaf of i into itself: the inverse image of that ideal sheaf under the translation is contained in it.

    source
    theorem CategoryTheory.Over.Hom.le_ker_mul {S : AlgebraicGeometry.Scheme} {X Y Z : Over S} [MonObj X] [MonObj Y] (i : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion (left i)] [IsMonHom i] (x y : Z ⟶ Y) (hx : AlgebraicGeometry.Scheme.Hom.ker (left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (left x)) (hy : AlgebraicGeometry.Scheme.Hom.ker (left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (left y)) :
    AlgebraicGeometry.Scheme.Hom.ker (left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (left (x * y))

    Points factoring through a closed immersion that is a monoid homomorphism remain in its closed subscheme after multiplication.