Geometric kernel presentations for ambient commutative group schemes

The canonical kernel of an arbitrary morphism of commutative group schemes exists, but it need not inherit a finiteness or flatness property from the source and target. A KernelPresentation records an actual supplied group scheme, its chosen inclusion, and its geometric identification with that canonical kernel. Compatibility with the inclusion rules out unrelated pointwise models.

This interface is deliberately independent of finite-flat and quasi-finite wrappers. Its point-kernel equivalence, unique lift, and represented-point exactness API therefore applies to both settings without duplicating the later fppf connecting construction. No claim is made that an arbitrary canonical kernel is flat, quasi-finite, finite, or finitely presented.

@[simp]

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

Ambient group-scheme point maps preserve identity morphisms.

@[simp]

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

Ambient group-scheme point maps turn composition into composition of homomorphisms.

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

An isomorphism of ambient 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.

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

A supplied commutative group scheme identified geometrically with the canonical kernel of f. The explicit inclusion preserves a caller's chosen exact-sequence morphism, while the compatibility field certifies that it is the inclusion induced by the geometric kernel.

• kernel : CommGroupScheme S

  The supplied geometric kernel object.

• inclusion : self.kernel ⟶ G

  The chosen inclusion into the source.

• kernelIso : self.kernel ≅ CommGroupScheme.kernel f

  Identification with the canonical ambient group-scheme kernel.

• kernelIso_hom_kernelInclusion : CategoryTheory.CategoryStruct.comp self.kernelIso.hom (kernelInclusion f) = self.inclusion

  The chosen inclusion is the canonical one under the geometric identification.

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

Points of a supplied geometric kernel are the pointwise kernel of the original morphism.

Equations

• P.pointKernelMulEquiv T = (AlgebraicGeometry.CommGroupScheme.pointMulEquivOfIso P.kernelIso T).trans (AlgebraicGeometry.CommGroupScheme.pointKernelMulEquiv f T)

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.pointKernelMulEquiv_apply {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (T : CategoryTheory.Over S) (x : P.kernel.Point T) : ↑((P.pointKernelMulEquiv T) x) = (mapPoint P.inclusion T) x

@[simp]

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

Every supplied-kernel point maps to the identity in the target.

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.liftPoint {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) {T : CategoryTheory.Over S} (x : G.Point T) (hx : (mapPoint f T) x = 1) : P.kernel.Point T

The canonical chosen lift of a point killed by the original morphism.

Equations

• P.liftPoint x hx = (P.pointKernelMulEquiv T).symm ⟨x, hx⟩

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.mapPoint_liftPoint {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) {T : CategoryTheory.Over S} (x : G.Point T) (hx : (mapPoint f T) x = 1) : (mapPoint P.inclusion T) (P.liftPoint x hx) = x

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.inclusion_point_injective {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (T : CategoryTheory.Over S) : Function.Injective ⇑(mapPoint P.inclusion T)

A supplied geometric kernel inclusion is injective on every test scheme.

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

Every killed point lifts uniquely through the supplied geometric kernel.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.point_mulExact {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (T : CategoryTheory.Over S) : Function.MulExact ⇑(mapPoint P.inclusion T) ⇑(mapPoint f T)

A geometric kernel presentation is exact on represented points of every test scheme.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.mapPoint_eq_one_iff_exists_kernelPoint {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (T : CategoryTheory.Over S) (x : G.Point T) : (mapPoint f T) x = 1 ↔ ∃ (y : P.kernel.Point T), (mapPoint P.inclusion T) y = x

Concrete represented-point consumer of the ambient presentation: a source point is killed exactly when it comes from the supplied geometric kernel.

Arbitrary base change

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.baseChange {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) {T : Scheme} (t : T ⟶ S) : KernelPresentation ((CategoryTheory.Over.pullback t).mapCommGrp.map f)

Certified geometric kernels of ambient commutative group-scheme homomorphisms commute with arbitrary base change.

Equations

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

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.baseChange_kernel {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) {T : Scheme} (t : T ⟶ S) : (P.baseChange t).kernel = (CategoryTheory.Over.pullback t).mapCommGrp.obj P.kernel

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.baseChange_inclusion {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) {T : Scheme} (t : T ⟶ S) : (P.baseChange t).inclusion = (CategoryTheory.Over.pullback t).mapCommGrp.map P.inclusion