Finite flat commutative group schemes

This file defines finite locally free commutative group schemes over a base scheme S: schemes finite, flat and locally of finite presentation over S, with a commutative group-object structure in Over S, together with their homomorphisms, isomorphisms and base change. Over an affine base, see TauCeti.FiniteLocallyFreeCommAffineGroupSchemeCat.

Main definitions

• TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme S: finite locally free commutative group schemes over S.
• TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.toOver: the underlying object of Over S, with its commutative group-object instances grpObj and isCommMonObj.
• TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.Section: sections of the structure morphism.
• TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.Hom and TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.Iso: homomorphisms and isomorphisms, as morphisms and isomorphisms of the underlying group objects in Grp (Over S).
• TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange: base change along a morphism of schemes, with grpMk_baseChange identifying its group object with the image of that of G under (Over.pullback f).mapGrp, and Hom.baseChange: base change of homomorphisms, with Hom.baseChange_eq, Hom.baseChange_id and Hom.baseChange_comp.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §1.12.
• The Stacks Project, Tag 02KB, for finite locally free morphisms as the finite, flat morphisms locally of finite presentation.

structure TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme (S : AlgebraicGeometry.Scheme) : Type (u + 1)

A finite locally free commutative group scheme over S: a scheme over S whose structure morphism is finite, flat, and locally of finite presentation, with a commutative group-object structure in Over S.

• carrier : AlgebraicGeometry.Scheme

  The underlying scheme.

• structureMap : self.carrier ⟶ S

  The structure morphism to the base.

• grp : CategoryTheory.GrpObj (CategoryTheory.Over.mk self.structureMap)

  The group law, as a group object in the category of schemes over S.

• comm : CategoryTheory.IsCommMonObj (CategoryTheory.Over.mk self.structureMap)

  The group law is commutative.

• finite : AlgebraicGeometry.IsFinite self.structureMap

  The structure morphism is finite.

• flat : AlgebraicGeometry.Flat self.structureMap

  The structure morphism is flat.

• locallyOfFinitePresentation : AlgebraicGeometry.LocallyOfFinitePresentation self.structureMap

  The structure morphism is locally of finite presentation.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.toOver {S : AlgebraicGeometry.Scheme} (G : FiniteFlatCommGroupScheme S) : CategoryTheory.Over S

The underlying object of Over S.

Equations

• G.toOver = CategoryTheory.Over.mk G.structureMap

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.grpObj {S : AlgebraicGeometry.Scheme} (G : FiniteFlatCommGroupScheme S) : CategoryTheory.GrpObj G.toOver

The group law of a finite flat commutative group scheme, as a group object over S.

Equations

• G.grpObj = G.grp

instance TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.isCommMonObj {S : AlgebraicGeometry.Scheme} (G : FiniteFlatCommGroupScheme S) : CategoryTheory.IsCommMonObj G.toOver

The group law of a finite flat commutative group scheme is commutative.

def TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.Section {S : AlgebraicGeometry.Scheme} (G : FiniteFlatCommGroupScheme S) : Type u

Sections of the structure morphism of a finite flat group scheme: morphisms s : S ⟶ G.carrier with s ≫ G.structureMap = 𝟙 S.

Equations

• G.Section = { s : S ⟶ G.carrier // CategoryTheory.CategoryStruct.comp s G.structureMap = CategoryTheory.CategoryStruct.id S }

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.Hom {S : AlgebraicGeometry.Scheme} (G H : FiniteFlatCommGroupScheme S) : Type u

A homomorphism of finite flat commutative group schemes over S: a morphism of the underlying group objects in Grp (Over S), that is, a morphism of schemes over S compatible with the group laws.

Equations

• G.Hom H = ({ X := G.toOver, grp := G.grpObj } ⟶ { X := H.toOver, grp := H.grpObj })

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.Iso {S : AlgebraicGeometry.Scheme} (G H : FiniteFlatCommGroupScheme S) : Type u

An isomorphism of finite flat commutative group schemes over S: an isomorphism of the underlying group objects in Grp (Over S).

Equations

• G.Iso H = ({ X := G.toOver, grp := G.grpObj } ≅ { X := H.toOver, grp := H.grpObj })

noncomputable def TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange {S T : AlgebraicGeometry.Scheme} (G : FiniteFlatCommGroupScheme S) (f : T ⟶ S) : FiniteFlatCommGroupScheme T

The base change of a finite flat commutative group scheme G over S along f : T ⟶ S: the fibre product of G.structureMap and f, with the second projection as structure morphism and the group law obtained by applying the pullback functor Over.pullback f.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_carrier {S T : AlgebraicGeometry.Scheme} (G : FiniteFlatCommGroupScheme S) (f : T ⟶ S) : (G.baseChange f).carrier = CategoryTheory.Limits.pullback G.structureMap f

The underlying scheme of the base change of G along f is the fibre product of G.structureMap and f.

theorem TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.grpMk_baseChange {S T : AlgebraicGeometry.Scheme} (G : FiniteFlatCommGroupScheme S) (f : T ⟶ S) : { X := (G.baseChange f).toOver, grp := (G.baseChange f).grpObj } = (CategoryTheory.Over.pullback f).mapGrp.obj { X := G.toOver, grp := G.grpObj }

The group object underlying the base change of G along f is the image of the group object underlying G under the pullback functor Over.pullback f.

noncomputable def TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.Hom.baseChange {S T : AlgebraicGeometry.Scheme} {G H : FiniteFlatCommGroupScheme S} (φ : G.Hom H) (f : T ⟶ S) : (G.baseChange f).Hom (H.baseChange f)

The base change along f : T ⟶ S of a homomorphism of finite flat commutative group schemes over S: the image of the homomorphism under (Over.pullback f).mapGrp, read through grpMk_baseChange.

Equations

• φ.baseChange f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback f).mapGrp.map φ) (CategoryTheory.eqToHom ⋯))

theorem TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.Hom.baseChange_eq {S T : AlgebraicGeometry.Scheme} {G H : FiniteFlatCommGroupScheme S} (φ : G.Hom H) (f : T ⟶ S) : φ.baseChange f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback f).mapGrp.map φ) (CategoryTheory.eqToHom ⋯))

The base change of a homomorphism is the image of the homomorphism under (Over.pullback f).mapGrp, read through grpMk_baseChange.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.Hom.baseChange_id {S T : AlgebraicGeometry.Scheme} (G : FiniteFlatCommGroupScheme S) (f : T ⟶ S) : baseChange (CategoryTheory.CategoryStruct.id { X := G.toOver, grp := G.grpObj }) f = CategoryTheory.CategoryStruct.id { X := (G.baseChange f).toOver, grp := (G.baseChange f).grpObj }

Base change of homomorphisms preserves identities.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.Hom.baseChange_comp {S T : AlgebraicGeometry.Scheme} {G H K : FiniteFlatCommGroupScheme S} (φ : G.Hom H) (ψ : H.Hom K) (f : T ⟶ S) : baseChange (CategoryTheory.CategoryStruct.comp φ ψ) f = CategoryTheory.CategoryStruct.comp (φ.baseChange f) (ψ.baseChange f)

Base change of homomorphisms preserves composition.