Finite flat commutative group schemes

This file packages commutative group objects over a scheme whose structure morphism is finite and flat. The ambient group-scheme category is mathlib's category of internal commutative group objects in Over S; the finite-flat category is its full subcategory. Consequently morphisms carry all compatibility with multiplication, identity, and inverse without repeating those laws.

The rank is deliberately a function on the base. A finite flat morphism need not have a single global rank on a disconnected base. HasConstantOrder G n records the additional assertion needed to speak of one order n.

The scheme-theoretic kernel is the pullback of a homomorphism along the identity section. It is constructed first as a pullback of internal groups, and commutativity follows from its monic map to the commutative source. Packaging it back into the finite-flat category still takes explicit finiteness and flatness hypotheses on its structure map. In particular, flatness of kernels is an arithmetic-base theorem rather than a formal consequence of the source and target being finite flat.

@[reducible, inline]

abbrev AlgebraicGeometry.CommGroupScheme (S : Scheme) : Type (u + 1)

A commutative group scheme over S, expressed as an internal commutative group object in the slice category of schemes over S.

Equations

• AlgebraicGeometry.CommGroupScheme S = CategoryTheory.CommGrp (CategoryTheory.Over S)

def AlgebraicGeometry.finiteFlatCommGroupSchemeProperty (S : Scheme) : CategoryTheory.ObjectProperty (CommGroupScheme S)

The object property saying that the structure morphism of a commutative group scheme is finite and flat.

Equations

• AlgebraicGeometry.finiteFlatCommGroupSchemeProperty S G = (AlgebraicGeometry.IsFinite G.X.hom ∧ AlgebraicGeometry.Flat G.X.hom)

@[reducible, inline]

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

Finite flat commutative group schemes over S form the full subcategory of commutative group schemes whose structure morphism is finite and flat.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme S = (AlgebraicGeometry.finiteFlatCommGroupSchemeProperty S).FullSubcategory

@[reducible, inline]

abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.toCommGroupScheme {S : Scheme} (G : FiniteFlatCommGroupScheme S) : CommGroupScheme S

The underlying commutative group scheme.

Equations

• G.toCommGroupScheme = G.obj

@[reducible, inline]

abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.scheme {S : Scheme} (G : FiniteFlatCommGroupScheme S) : Scheme

The underlying scheme.

Equations

• G.scheme = G.obj.X.left

@[reducible, inline]

abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.structureMap {S : Scheme} (G : FiniteFlatCommGroupScheme S) : G.scheme ⟶ S

The finite flat structure morphism.

Equations

• G.structureMap = G.obj.X.hom

instance AlgebraicGeometry.FiniteFlatCommGroupScheme.instIsFiniteStructureMap {S : Scheme} (G : FiniteFlatCommGroupScheme S) : IsFinite G.structureMap

instance AlgebraicGeometry.FiniteFlatCommGroupScheme.instFlatStructureMap {S : Scheme} (G : FiniteFlatCommGroupScheme S) : Flat G.structureMap

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.hom {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : G.scheme ⟶ H.scheme

The underlying morphism of schemes of a morphism of finite flat commutative group schemes.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.hom f = CategoryTheory.Over.Hom.left f.hom.hom.hom.hom

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.hom_id {S : Scheme} (G : FiniteFlatCommGroupScheme S) : hom (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id G.scheme

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.hom_comp {S : Scheme} {G H K : FiniteFlatCommGroupScheme S} (f : G ⟶ H) (g : H ⟶ K) : hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (hom g)

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.hom_comp_structureMap {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (hom f) H.structureMap = G.structureMap

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.hom_comp_structureMap_assoc {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp H.structureMap h) = CategoryTheory.CategoryStruct.comp G.structureMap h

@[reducible, inline]

abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.Point {S : Scheme} (G : FiniteFlatCommGroupScheme S) (X : CategoryTheory.Over S) : Type u

The group of X-valued points of G, where X is any scheme over the same base.

Because G is an internal commutative group object, this hom-set carries its canonical commutative group structure.

Equations

• G.Point X = (X ⟶ G.obj.X)

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.mapPoint {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) (X : CategoryTheory.Over S) : G.Point X →* H.Point X

A homomorphism of finite-flat commutative group schemes acts on points by postcomposition.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.mapPoint f X = CategoryTheory.IsMonHom.monoidHom f.hom.hom.hom.hom X

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.mapPoint_apply {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) (X : CategoryTheory.Over S) (x : G.Point X) : (mapPoint f X) x = CategoryTheory.CategoryStruct.comp x f.hom.hom.hom.hom

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.mapPoint_id {S : Scheme} (G : FiniteFlatCommGroupScheme S) (X : CategoryTheory.Over S) : mapPoint (CategoryTheory.CategoryStruct.id G) X = MonoidHom.id (G.Point X)

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.mapPoint_comp {S : Scheme} {G H K : FiniteFlatCommGroupScheme S} (f : G ⟶ H) (g : H ⟶ K) (X : CategoryTheory.Over S) : mapPoint (CategoryTheory.CategoryStruct.comp f g) X = (mapPoint g X).comp (mapPoint f X)

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.pointMulEquivOfIso {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (e : G ≅ H) (X : CategoryTheory.Over S) : G.Point X ≃* H.Point X

An isomorphism of finite-flat commutative group schemes induces a multiplicative equivalence on points of every test scheme.

Equations

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

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

Base change of finite flat commutative group schemes. This is a functor because pullback is a finite-product-preserving functor on slice categories, hence maps internal commutative groups.

Equations

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

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_scheme {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) : ((baseChange f).obj G).scheme = CategoryTheory.Limits.pullback G.structureMap f

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_structureMap {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) : ((baseChange f).obj G).structureMap = CategoryTheory.Limits.pullback.snd G.structureMap f

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

Projection from a base-changed finite-flat group scheme to its original scheme.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeProjection f G = CategoryTheory.Limits.pullback.fst G.structureMap f

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeProjection_condition {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) : CategoryTheory.CategoryStruct.comp (baseChangeProjection f G) G.structureMap = CategoryTheory.CategoryStruct.comp ((baseChange f).obj G).structureMap f

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeProjection_condition_assoc {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeProjection f G) (CategoryTheory.CategoryStruct.comp G.structureMap h) = CategoryTheory.CategoryStruct.comp ((baseChange f).obj G).structureMap (CategoryTheory.CategoryStruct.comp f h)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeScheme_hom_ext {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) {X : Scheme} {a b : X ⟶ ((baseChange f).obj G).scheme} (hprojection : CategoryTheory.CategoryStruct.comp a (baseChangeProjection f G) = CategoryTheory.CategoryStruct.comp b (baseChangeProjection f G)) (hbase : CategoryTheory.CategoryStruct.comp a ((baseChange f).obj G).structureMap = CategoryTheory.CategoryStruct.comp b ((baseChange f).obj G).structureMap) : a = b

Two maps into a base-changed scheme agree when they agree after both projections.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeLift {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) {X : Scheme} (a : X ⟶ G.scheme) (b : X ⟶ T) (h : CategoryTheory.CategoryStruct.comp a G.structureMap = CategoryTheory.CategoryStruct.comp b f) : X ⟶ ((baseChange f).obj G).scheme

The universal lift into a base-changed scheme, with its source type kept opaque.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeLift f G a b h = CategoryTheory.Limits.pullback.lift a b h

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeLift_projection {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) {X : Scheme} (a : X ⟶ G.scheme) (b : X ⟶ T) (h : CategoryTheory.CategoryStruct.comp a G.structureMap = CategoryTheory.CategoryStruct.comp b f) : CategoryTheory.CategoryStruct.comp (baseChangeLift f G a b h) (baseChangeProjection f G) = a

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeLift_projection_assoc {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) {X : Scheme} (a : X ⟶ G.scheme) (b : X ⟶ T) (h : CategoryTheory.CategoryStruct.comp a G.structureMap = CategoryTheory.CategoryStruct.comp b f) {Z : Scheme} (h✝ : G.scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeLift f G a b h) (CategoryTheory.CategoryStruct.comp (baseChangeProjection f G) h✝) = CategoryTheory.CategoryStruct.comp a h✝

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeLift_structureMap {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) {X : Scheme} (a : X ⟶ G.scheme) (b : X ⟶ T) (h : CategoryTheory.CategoryStruct.comp a G.structureMap = CategoryTheory.CategoryStruct.comp b f) : CategoryTheory.CategoryStruct.comp (baseChangeLift f G a b h) ((baseChange f).obj G).structureMap = b

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChangeLift_structureMap_assoc {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) {X : Scheme} (a : X ⟶ G.scheme) (b : X ⟶ T) (h : CategoryTheory.CategoryStruct.comp a G.structureMap = CategoryTheory.CategoryStruct.comp b f) {Z : Scheme} (h✝ : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeLift f G a b h) (CategoryTheory.CategoryStruct.comp ((baseChange f).obj G).structureMap h✝) = CategoryTheory.CategoryStruct.comp b h✝

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_hom_projection {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (hom ((baseChange t).map f)) (baseChangeProjection t H) = CategoryTheory.CategoryStruct.comp (baseChangeProjection t G) (hom f)

Base change of a group-scheme homomorphism commutes with the projection to the original source and target.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_hom_projection_assoc {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : H.scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (hom ((baseChange t).map f)) (CategoryTheory.CategoryStruct.comp (baseChangeProjection t H) h) = CategoryTheory.CategoryStruct.comp (baseChangeProjection t G) (CategoryTheory.CategoryStruct.comp (hom f) h)

Base change of a group-scheme homomorphism commutes with the projection to the original source and target.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_hom_structureMap {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (hom ((baseChange t).map f)) ((baseChange t).obj H).structureMap = ((baseChange t).obj G).structureMap

Base change of a group-scheme homomorphism remains a morphism over the new base.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_hom_structureMap_assoc {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (hom ((baseChange t).map f)) (CategoryTheory.CategoryStruct.comp ((baseChange t).obj H).structureMap h) = CategoryTheory.CategoryStruct.comp ((baseChange t).obj G).structureMap h

Base change of a group-scheme homomorphism remains a morphism over the new base.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_one_projection {S T : Scheme} (t : T ⟶ S) (H : FiniteFlatCommGroupScheme S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one) (baseChangeProjection t H) = CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

The identity section of a base-changed group scheme projects to the original identity section.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_one_projection_assoc {S T : Scheme} (t : T ⟶ S) (H : FiniteFlatCommGroupScheme S) {Z : Scheme} (h : H.scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one) (CategoryTheory.CategoryStruct.comp (baseChangeProjection t H) h) = CategoryTheory.CategoryStruct.comp t (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one) h)

The identity section of a base-changed group scheme projects to the original identity section.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_one_structureMap {S T : Scheme} (t : T ⟶ S) (H : FiniteFlatCommGroupScheme S) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one) ((baseChange t).obj H).structureMap = CategoryTheory.CategoryStruct.id T

The identity section of a base-changed group scheme is a section over the new base.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_one_structureMap_assoc {S T : Scheme} (t : T ⟶ S) (H : FiniteFlatCommGroupScheme S) {Z : Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one) (CategoryTheory.CategoryStruct.comp ((baseChange t).obj H).structureMap h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id T) h

The identity section of a base-changed group scheme is a section over the new base.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.baseChange_hom_isPullback {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.IsPullback (baseChangeProjection t G) (hom ((baseChange t).map f)) (hom f) (baseChangeProjection t H)

The square underlying a base-changed group-scheme homomorphism is cartesian.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.directKernelToBaseChangeSource {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.Limits.pullback (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)) ⟶ ((baseChange t).obj G).scheme

The direct pullback kernel over a new base maps canonically to the base-changed source.

Equations

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

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.directKernel_isPullback {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.IsPullback (directKernelToBaseChangeSource t f) (CategoryTheory.Limits.pullback.snd (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))) (hom ((baseChange t).map f)) (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

The direct kernel square remains a pullback after changing the base.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.directKernelToBaseChangeSource_projection {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (directKernelToBaseChangeSource t f) (baseChangeProjection t G) = CategoryTheory.Limits.pullback.fst (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.directKernelToBaseChangeSource_projection_assoc {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : G.scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (directKernelToBaseChangeSource t f) (CategoryTheory.CategoryStruct.comp (baseChangeProjection t G) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))) h

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.directKernelToBaseChangeSource_project {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (directKernelToBaseChangeSource t f) (hom ((baseChange t).map f)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))) (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.directKernelToBaseChangeSource_project_assoc {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : ((baseChange t).obj H).scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (directKernelToBaseChangeSource t f) (CategoryTheory.CategoryStruct.comp (hom ((baseChange t).map f)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one) h)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.directKernelToBaseChangeSource_structureMap {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (directKernelToBaseChangeSource t f) ((baseChange t).obj G).structureMap = CategoryTheory.Limits.pullback.snd (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.directKernelToBaseChangeSource_structureMap_assoc {S T : Scheme} (t : T ⟶ S) {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (directKernelToBaseChangeSource t f) (CategoryTheory.CategoryStruct.comp ((baseChange t).obj G).structureMap h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))) h

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.orderAt {S : Scheme} (G : FiniteFlatCommGroupScheme S) : ↥S → ℕ

The rank of a finite flat commutative group scheme at a point of its base.

Equations

• G.orderAt = AlgebraicGeometry.Scheme.Hom.finrank G.structureMap

def AlgebraicGeometry.FiniteFlatCommGroupScheme.HasConstantOrder {S : Scheme} (G : FiniteFlatCommGroupScheme S) (n : ℕ) : Prop

The assertion that a finite flat commutative group scheme has one constant order on its possibly disconnected base.

Equations

• G.HasConstantOrder n = (G.orderAt = Function.const (↥S) n)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.orderAt_eq_of_iso {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (e : G ≅ H) : G.orderAt = H.orderAt

Isomorphic finite-flat commutative group schemes have the same geometric rank function.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.orderAt_baseChange {S T : Scheme} (f : T ⟶ S) (G : FiniteFlatCommGroupScheme S) (t : ↥T) : ((baseChange f).obj G).orderAt t = G.orderAt (f t)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.hasConstantOrder_baseChange {S T : Scheme} {G : FiniteFlatCommGroupScheme S} {n : ℕ} (hG : G.HasConstantOrder n) (f : T ⟶ S) : ((baseChange f).obj G).HasConstantOrder n

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelScheme {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : Scheme

The underlying scheme of the scheme-theoretic kernel of f, obtained by pulling G back along the identity section of H.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelι {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : kernelScheme f ⟶ G.scheme

The canonical map from the scheme-theoretic kernel to the source group scheme.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelStructureMap {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : kernelScheme f ⟶ S

The structure morphism of the underlying scheme-theoretic kernel.

Equations

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

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.kernel_condition {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (kernelι f) (hom f) = CategoryTheory.CategoryStruct.comp (kernelStructureMap f) (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.kernel_condition_assoc {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : H.scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (kernelι f) (CategoryTheory.CategoryStruct.comp (hom f) h) = CategoryTheory.CategoryStruct.comp (kernelStructureMap f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one) h)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelZero {S : Scheme} (H : FiniteFlatCommGroupScheme S) : CategoryTheory.Grp.trivial (CategoryTheory.Over S) ⟶ CategoryTheory.CommGrp.toGrp H.obj

The zero morphism from the trivial internal group to the target. Its underlying map of schemes is the identity section of the target group scheme.

Equations

• H.kernelZero = default

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelGrp {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.Grp (CategoryTheory.Over S)

The kernel constructed first in internal (not necessarily commutative) groups. Limits of internal groups are created by the forgetful functor, so this pullback inherits its group law without choosing formulas for multiplication and inverse on the underlying scheme.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelGrp f = CategoryTheory.Limits.pullback f.hom.hom H.kernelZero

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelGrp_isComm {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.IsCommMonObj (kernelGrp f).X

The internal group kernel is commutative. The identity section is split mono, hence the first pullback projection is mono. Its underlying map remains mono because the forgetful functor from internal groups preserves pullbacks, and commutativity can therefore be checked after mapping to the commutative source.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelCommGroupScheme {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CommGroupScheme S

The commutative group scheme underlying the scheme-theoretic kernel.

Equations

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

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelCommGroupSchemeInclusion {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : kernelCommGroupScheme f ⟶ G.obj

The kernel inclusion before imposing the finite-flat object property.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelCommGroupSchemeInclusion f = CategoryTheory.InducedCategory.homMk (CategoryTheory.Limits.pullback.fst f.hom.hom H.kernelZero)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelGrp_isPullback {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.IsPullback (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.pullback.fst f.hom.hom H.kernelZero).hom.hom) (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.pullback.snd f.hom.hom H.kernelZero).hom.hom) (hom f) (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

After forgetting first the group structure and then the map to the base, the internal-group kernel square is the scheme-theoretic pullback square.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelGrpSchemeIso {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : (kernelGrp f).X.left ≅ kernelScheme f

The canonical identification of the inherited internal-group kernel with the explicit scheme-theoretic pullback used by kernelScheme.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelGrpSchemeIso f = ⋯.isoPullback

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelGrpSchemeIso_hom_structureMap {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (kernelGrpSchemeIso f).hom (kernelStructureMap f) = (kernelGrp f).X.hom

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelGrpSchemeIso_hom_structureMap_assoc {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (kernelGrpSchemeIso f).hom (CategoryTheory.CategoryStruct.comp (kernelStructureMap f) h) = CategoryTheory.CategoryStruct.comp (kernelGrp f).X.hom h

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelGrpSchemeIso_hom_kernelι {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (kernelGrpSchemeIso f).hom (kernelι f) = CategoryTheory.Over.Hom.left (kernelCommGroupSchemeInclusion f).hom.hom.hom

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelGrpSchemeIso_hom_kernelι_assoc {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : G.scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (kernelGrpSchemeIso f).hom (CategoryTheory.CategoryStruct.comp (kernelι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (kernelCommGroupSchemeInclusion f).hom.hom.hom) h

structure AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : Type (u + 1)

Data certifying that the scheme-theoretic kernel carries the expected finite-flat commutative group-scheme structure. The isomorphism fixes its underlying scheme and structure map, while the universal pullback above fixes its geometric meaning.

• kernel : FiniteFlatCommGroupScheme S

  The kernel as a finite flat commutative group scheme.

• inclusion : self.kernel ⟶ G

  The kernel inclusion as a homomorphism of group schemes.

• schemeIso : self.kernel.scheme ≅ kernelScheme f

  Identification with the scheme-theoretic pullback kernel.

• schemeIso_hom_structureMap : CategoryTheory.CategoryStruct.comp self.schemeIso.hom (kernelStructureMap f) = self.kernel.structureMap

  Compatibility of the identification with the maps to the base.

• schemeIso_hom_kernelι : CategoryTheory.CategoryStruct.comp self.schemeIso.hom (kernelι f) = hom self.inclusion

  Compatibility of the group-scheme inclusion with the pullback projection.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelFiniteFlat {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) [IsFinite (kernelStructureMap f)] [Flat (kernelStructureMap f)] : FiniteFlatCommGroupScheme S

The inherited kernel group scheme, packaged as finite flat when its structure morphism is known to be finite and flat. These hypotheses are intentionally attached to the explicit scheme-theoretic structure map rather than inferred from G and H.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelFiniteFlat f = { obj := AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelCommGroupScheme f, property := ⋯ }

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.kernel {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) [IsFinite (kernelStructureMap f)] [Flat (kernelStructureMap f)] : FiniteFlatCommGroupScheme S

The finite-flat kernel of f, under the exact geometric hypotheses needed over the base.

Flatness of kernels is not automatic over an arbitrary scheme, so the hypotheses deliberately remain visible at this public entry point.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.kernel f = AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelFiniteFlat f

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelFiniteFlatInclusion {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) [IsFinite (kernelStructureMap f)] [Flat (kernelStructureMap f)] : kernelFiniteFlat f ⟶ G

The inclusion of the finite-flat kernel into its source.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelFiniteFlatInclusion f = CategoryTheory.ObjectProperty.homMk (AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelCommGroupSchemeInclusion f)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelInclusion {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) [IsFinite (kernelStructureMap f)] [Flat (kernelStructureMap f)] : kernel f ⟶ G

The canonical inclusion of the finite-flat kernel.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelInclusion f = AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelFiniteFlatInclusion f

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelPresentationOfFiniteFlat {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) [IsFinite (kernelStructureMap f)] [Flat (kernelStructureMap f)] : KernelPresentation f

The canonical finite-flat kernel presentation under the precise hypotheses needed to put the inherited group scheme in FiniteFlatCommGroupScheme S.

Equations

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

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.kernelPresentation_exists_of_finite_flat {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) [IsFinite (kernelStructureMap f)] [Flat (kernelStructureMap f)] : Nonempty (KernelPresentation f)

A scheme-theoretic kernel known finite and flat has the canonical certified presentation. This permanent theorem is the destination of the checked Challenge bridge.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeKernelMap {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : CategoryTheory.Limits.pullback P.kernel.structureMap t ⟶ CategoryTheory.Limits.pullback (kernelStructureMap f) t

The first comparison map in the geometric pullback of a certified kernel.

Equations

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

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeKernelIso {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : CategoryTheory.Limits.pullback P.kernel.structureMap t ≅ CategoryTheory.Limits.pullback (kernelStructureMap f) t

Pulling back the chosen kernel scheme or its canonical scheme-theoretic model gives isomorphic schemes over the new base.

Equations

• P.baseChangeKernelIso t = CategoryTheory.asIso (P.baseChangeKernelMap t)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeKernelIso_hom_fst {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : CategoryTheory.CategoryStruct.comp (P.baseChangeKernelIso t).hom (CategoryTheory.Limits.pullback.fst (kernelStructureMap f) t) = CategoryTheory.CategoryStruct.comp (baseChangeProjection t P.kernel) P.schemeIso.hom

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeKernelIso_hom_fst_assoc {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) {Z : Scheme} (h : kernelScheme f ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.baseChangeKernelIso t).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (kernelStructureMap f) t) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (baseChangeProjection t P.kernel) P.schemeIso.hom) h

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeKernelIso_hom_snd {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : CategoryTheory.CategoryStruct.comp (P.baseChangeKernelIso t).hom (CategoryTheory.Limits.pullback.snd (kernelStructureMap f) t) = ((FiniteFlatCommGroupScheme.baseChange t).obj P.kernel).structureMap

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeKernelIso_hom_snd_assoc {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) {Z : Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.baseChangeKernelIso t).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (kernelStructureMap f) t) h) = CategoryTheory.CategoryStruct.comp ((FiniteFlatCommGroupScheme.baseChange t).obj P.kernel).structureMap h

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeDirectIso {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : ((FiniteFlatCommGroupScheme.baseChange t).obj P.kernel).scheme ≅ CategoryTheory.Limits.pullback (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))

The pullback of a certified kernel is the direct kernel of the original morphism against the base-changed identity section.

Equations

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

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeDirectIso_hom_fst {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : CategoryTheory.CategoryStruct.comp (P.baseChangeDirectIso t).hom (CategoryTheory.Limits.pullback.fst (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))) = CategoryTheory.CategoryStruct.comp (baseChangeProjection t P.kernel) (hom P.inclusion)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeDirectIso_hom_fst_assoc {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) {Z : Scheme} (h : G.scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.baseChangeDirectIso t).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))) h) = CategoryTheory.CategoryStruct.comp (baseChangeProjection t P.kernel) (CategoryTheory.CategoryStruct.comp (hom P.inclusion) h)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeDirectIso_hom_snd {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : CategoryTheory.CategoryStruct.comp (P.baseChangeDirectIso t).hom (CategoryTheory.Limits.pullback.snd (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))) = ((FiniteFlatCommGroupScheme.baseChange t).obj P.kernel).structureMap

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeDirectIso_hom_snd_assoc {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) {Z : Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.baseChangeDirectIso t).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (hom f) (CategoryTheory.CategoryStruct.comp t (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one))) h) = CategoryTheory.CategoryStruct.comp ((FiniteFlatCommGroupScheme.baseChange t).obj P.kernel).structureMap h

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeDirectIso_hom_toSource {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : CategoryTheory.CategoryStruct.comp (P.baseChangeDirectIso t).hom (directKernelToBaseChangeSource t f) = hom ((FiniteFlatCommGroupScheme.baseChange t).map P.inclusion)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeDirectIso_hom_toSource_assoc {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) {Z : Scheme} (h : ((FiniteFlatCommGroupScheme.baseChange t).obj G).scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.baseChangeDirectIso t).hom (CategoryTheory.CategoryStruct.comp (directKernelToBaseChangeSource t f) h) = CategoryTheory.CategoryStruct.comp (hom ((FiniteFlatCommGroupScheme.baseChange t).map P.inclusion)) h

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeSchemeIso {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : ((FiniteFlatCommGroupScheme.baseChange t).obj P.kernel).scheme ≅ kernelScheme ((FiniteFlatCommGroupScheme.baseChange t).map f)

The canonical identification of a pulled-back certified kernel with the scheme-theoretic kernel of the pulled-back homomorphism.

Equations

• P.baseChangeSchemeIso t = P.baseChangeDirectIso t ≪≫ ⋯.isoPullback

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeSchemeIso_hom_structureMap {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : CategoryTheory.CategoryStruct.comp (P.baseChangeSchemeIso t).hom (kernelStructureMap ((FiniteFlatCommGroupScheme.baseChange t).map f)) = ((FiniteFlatCommGroupScheme.baseChange t).obj P.kernel).structureMap

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeSchemeIso_hom_structureMap_assoc {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) {Z : Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.baseChangeSchemeIso t).hom (CategoryTheory.CategoryStruct.comp (kernelStructureMap ((FiniteFlatCommGroupScheme.baseChange t).map f)) h) = CategoryTheory.CategoryStruct.comp ((FiniteFlatCommGroupScheme.baseChange t).obj P.kernel).structureMap h

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeSchemeIso_hom_kernelι {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : CategoryTheory.CategoryStruct.comp (P.baseChangeSchemeIso t).hom (kernelι ((FiniteFlatCommGroupScheme.baseChange t).map f)) = hom ((FiniteFlatCommGroupScheme.baseChange t).map P.inclusion)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChangeSchemeIso_hom_kernelι_assoc {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) {Z : Scheme} (h : ((FiniteFlatCommGroupScheme.baseChange t).obj G).scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.baseChangeSchemeIso t).hom (CategoryTheory.CategoryStruct.comp (kernelι ((FiniteFlatCommGroupScheme.baseChange t).map f)) h) = CategoryTheory.CategoryStruct.comp (hom ((FiniteFlatCommGroupScheme.baseChange t).map P.inclusion)) h

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChange {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : KernelPresentation ((FiniteFlatCommGroupScheme.baseChange t).map f)

Certified scheme-theoretic kernels commute with arbitrary base change.

Equations

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

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChange_kernel {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : (P.baseChange t).kernel = (FiniteFlatCommGroupScheme.baseChange t).obj P.kernel

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChange_inclusion {S T : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (t : T ⟶ S) : (P.baseChange t).inclusion = (FiniteFlatCommGroupScheme.baseChange t).map P.inclusion

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.inclusion_condition {S : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) : CategoryTheory.CategoryStruct.comp (hom P.inclusion) (hom f) = CategoryTheory.CategoryStruct.comp P.kernel.structureMap (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

The certified kernel inclusion maps trivially to the target group scheme.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.inclusion_condition_assoc {S : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) {Z : Scheme} (h : H.scheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (hom P.inclusion) (CategoryTheory.CategoryStruct.comp (hom f) h) = CategoryTheory.CategoryStruct.comp P.kernel.structureMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one) h)

The certified kernel inclusion maps trivially to the target group scheme.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.mapPoint_inclusion_eq_one {S : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (X : CategoryTheory.Over S) (y : P.kernel.Point X) : (mapPoint f X) ((mapPoint P.inclusion X) y) = 1

A point of a certified scheme-theoretic kernel maps to the identity in the target.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.point_condition_scheme {S : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (X : CategoryTheory.Over S) (x : G.Point X) (hx : (mapPoint f X) x = 1) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left x) (hom f) = CategoryTheory.CategoryStruct.comp X.hom (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

Pointwise kernel membership is the scheme-theoretic pullback condition.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.existsUnique_point_lift {S : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (X : CategoryTheory.Over S) (x : G.Point X) (hx : (mapPoint f X) x = 1) : ∃! y : P.kernel.Point X, (mapPoint P.inclusion X) y = x

Every point killed by f lifts uniquely to the certified scheme-theoretic kernel.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.pointKernelHom {S : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (X : CategoryTheory.Over S) : P.kernel.Point X →* ↥(mapPoint f X).ker

The inclusion identifies geometric kernel points with the actual kernel of the induced homomorphism on points.

Equations

• P.pointKernelHom X = (AlgebraicGeometry.FiniteFlatCommGroupScheme.mapPoint P.inclusion X).codRestrict (AlgebraicGeometry.FiniteFlatCommGroupScheme.mapPoint f X).ker ⋯

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.pointMulEquiv {S : Scheme} {G H : FiniteFlatCommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (X : CategoryTheory.Over S) : P.kernel.Point X ≃* ↥(mapPoint f X).ker

Scheme-theoretic kernels represent the pointwise kernel functor, multiplicatively and on every test scheme over the base.

Equations

• P.pointMulEquiv X = MulEquiv.ofBijective (P.pointKernelHom X) ⋯