Canonical kernels of ambient commutative group schemes

The kernel of an arbitrary commutative group-scheme morphism exists before imposing any finiteness property: take its pullback against the identity section in internal groups. This file constructs that commutative group scheme, identifies its underlying scheme with the ordinary scheme-theoretic pullback, and proves its universal property on points of every test scheme. Consequently the represented point functors are exact at the source.

This ambient construction is required for Mazur's integral pre-admissible groups, which are quasi-finite rather than finite at primes dividing the level. The final theorems are concrete compatibility consumers: the construction recovers the existing canonical finite-flat kernel when that kernel is flat, and every quasi-finite morphism consumes the ambient point-exactness theorem. No claim is made that the kernel of an arbitrary quasi-finite flat morphism is itself flat; the later four-factor exact sequences must supply that arithmetic input.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.CommGroupScheme.underlyingHom {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) : G.X.left ⟶ H.X.left

Underlying scheme morphism of an ambient commutative group-scheme morphism.

Equations

• AlgebraicGeometry.CommGroupScheme.underlyingHom f = CategoryTheory.Over.Hom.left f.hom.hom.hom

@[reducible, inline]

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

Underlying scheme of the canonical kernel pullback.

Equations

• AlgebraicGeometry.CommGroupScheme.kernelScheme f = CategoryTheory.Limits.pullback (AlgebraicGeometry.CommGroupScheme.underlyingHom f) (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.CommGroupScheme.kernelι {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) : kernelScheme f ⟶ G.X.left

Projection from the canonical kernel scheme to its source.

Equations

• AlgebraicGeometry.CommGroupScheme.kernelι f = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.CommGroupScheme.underlyingHom f) (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

@[reducible, inline]

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

Structure morphism of the canonical kernel scheme.

Equations

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

Zero map from the trivial internal group to the target.

Equations

• H.kernelZero = default

@[reducible, inline]

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

Kernel inherited in internal groups.

Equations

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

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.CommGroupScheme.kernel {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) : CommGroupScheme S

Canonical ambient commutative group-scheme kernel.

Equations

• AlgebraicGeometry.CommGroupScheme.kernel f = { X := (AlgebraicGeometry.CommGroupScheme.kernelGrp f).X, grp := (AlgebraicGeometry.CommGroupScheme.kernelGrp f).grp, comm := ⋯ }

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

Canonical kernel inclusion.

Equations

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

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

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

Canonical identification of the internal-group kernel with the scheme pullback.

Equations

• AlgebraicGeometry.CommGroupScheme.kernelSchemeIso f = ⋯.isoPullback

theorem AlgebraicGeometry.CommGroupScheme.kernelSchemeIso_hom_structureMap {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (kernelSchemeIso f).hom (kernelStructureMap f) = (kernelGrp f).X.hom

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

theorem AlgebraicGeometry.CommGroupScheme.kernelSchemeIso_hom_kernelι {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (kernelSchemeIso f).hom (kernelι f) = underlyingHom (kernelInclusion f)

theorem AlgebraicGeometry.CommGroupScheme.kernelSchemeIso_hom_kernelι_assoc {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : G.X.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (kernelSchemeIso f).hom (CategoryTheory.CategoryStruct.comp (kernelι f) h) = CategoryTheory.CategoryStruct.comp (underlyingHom (kernelInclusion f)) h

theorem AlgebraicGeometry.CommGroupScheme.kernelInclusion_condition {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) : CategoryTheory.CategoryStruct.comp (underlyingHom (kernelInclusion f)) (underlyingHom f) = CategoryTheory.CategoryStruct.comp (kernel f).X.hom (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one)

theorem AlgebraicGeometry.CommGroupScheme.kernelInclusion_condition_assoc {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) {Z : Scheme} (h : H.X.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (underlyingHom (kernelInclusion f)) (CategoryTheory.CategoryStruct.comp (underlyingHom f) h) = CategoryTheory.CategoryStruct.comp (kernelGrp f).X.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one) h)

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.mapPoint_kernelInclusion_eq_one {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) (T : CategoryTheory.Over S) (y : (kernel f).Point T) : (mapPoint f T) ((mapPoint (kernelInclusion f) T) y) = 1

theorem AlgebraicGeometry.CommGroupScheme.existsUnique_kernelPoint_lift {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) (T : CategoryTheory.Over S) (x : G.Point T) (hx : (mapPoint f T) x = 1) : ∃! y : (kernel f).Point T, (mapPoint (kernelInclusion f) T) y = x

Every test-scheme point killed by a group-scheme morphism lifts uniquely to the canonical ambient group-scheme kernel.

theorem AlgebraicGeometry.CommGroupScheme.kernelInclusion_point_injective {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) (T : CategoryTheory.Over S) : Function.Injective ⇑(mapPoint (kernelInclusion f) T)

The canonical kernel inclusion is injective on points of every test scheme.

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

The canonical kernel inclusion as a homomorphism into the pointwise kernel.

Equations

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

noncomputable def AlgebraicGeometry.CommGroupScheme.pointKernelMulEquiv {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) (T : CategoryTheory.Over S) : (kernel f).Point T ≃* ↥(mapPoint f T).ker

The scheme-theoretic ambient kernel represents the pointwise kernel functor on every test scheme, as a multiplicative equivalence rather than only a bijection of sets.

Equations

• AlgebraicGeometry.CommGroupScheme.pointKernelMulEquiv f T = MulEquiv.ofBijective (AlgebraicGeometry.CommGroupScheme.pointKernelHom f T) ⋯

theorem AlgebraicGeometry.CommGroupScheme.kernel_point_mulExact {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) (T : CategoryTheory.Over S) : Function.MulExact ⇑(mapPoint (kernelInclusion f) T) ⇑(mapPoint f T)

The canonical ambient kernel is exact on represented points of every test scheme.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.commGroupScheme_kernel_eq {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CommGroupScheme.kernel f.hom = kernelCommGroupScheme f

Forgetting the finite-flat structure on the existing internal-group kernel gives the canonical ambient kernel definitionally.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.commGroupScheme_kernelInclusion_eq {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CommGroupScheme.kernelInclusion f.hom = kernelCommGroupSchemeInclusion f

The ambient and finite-flat canonical kernel inclusions agree definitionally.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.canonicalKernel_point_mulExact {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) [IsFinite (kernelStructureMap f)] [Flat (kernelStructureMap f)] (T : CategoryTheory.Over S) : Function.MulExact ⇑(mapPoint (kernelInclusion f) T) ⇑(mapPoint f T)

The ambient canonical-kernel exactness specializes to the canonical finite-flat kernel whenever the latter carries the required finite-flat structure.

theorem AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.canonicalAmbientKernel_point_mulExact {S : Scheme} {G H : QuasiFiniteFlatCommGroupScheme S} (f : G ⟶ H) (T : CategoryTheory.Over S) : Function.MulExact ⇑(CommGroupScheme.mapPoint (CommGroupScheme.kernelInclusion f.hom) T) ⇑(mapPoint f T)

Every quasi-finite group-scheme morphism is exact at its canonical ambient kernel on all represented test-scheme points; no finite-flat hypothesis is used.

noncomputable def AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.canonicalAmbientKernel_pointMulEquiv {S : Scheme} {G H : QuasiFiniteFlatCommGroupScheme S} (f : G ⟶ H) (T : CategoryTheory.Over S) : (CommGroupScheme.kernel f.hom).Point T ≃* ↥(mapPoint f T).ker

The canonical ambient kernel of a quasi-finite group-scheme morphism represents its pointwise kernel on every test scheme. The target is ambient because flatness of this kernel is an additional arithmetic theorem, not a formal consequence of the endpoint wrappers.

Equations

• AlgebraicGeometry.QuasiFiniteFlatCommGroupScheme.canonicalAmbientKernel_pointMulEquiv f T = AlgebraicGeometry.CommGroupScheme.pointKernelMulEquiv f.hom T