Functoriality of global commutative fppf H¹

A natural transformation of commutative-group-valued presheaves acts pointwise on Čech cochains. This file proves that the action preserves cocycles and cohomology, commutes with genuine cover refinements, and descends to the common-refinement quotient defining global relative fppf H¹. Identity and composition are proved both before and after globalization.

The geometric sections apply the construction first to an arbitrary commutative group-scheme morphism and then to the existing finite-flat wrapper. The two induced maps agree definitionally. Thus quasi-finite coefficients can use the same functorial cohomology without creating a parallel theory, while the finite-flat low-degree sequence retains its existing API.

@[instance_reducible]

def CategoryTheory.PresheafOfCommGroups.coefficientCommGroupA {C : Type u} [Category.{v, u} C] {A : Functor Cᵒᵖ CommGrpCat} (X : Cᵒᵖ) : CommGroup ↑((toGroups A).obj X)

Equations

• CategoryTheory.PresheafOfCommGroups.coefficientCommGroupA X = id inferInstance

@[instance_reducible]

def CategoryTheory.PresheafOfCommGroups.coefficientCommGroupB {C : Type u} [Category.{v, u} C] {B : Functor Cᵒᵖ CommGrpCat} (X : Cᵒᵖ) : CommGroup ↑((toGroups B).obj X)

Equations

• CategoryTheory.PresheafOfCommGroups.coefficientCommGroupB X = id inferInstance

@[instance_reducible]

def CategoryTheory.PresheafOfCommGroups.coefficientCommGroupD {C : Type u} [Category.{v, u} C] {D : Functor Cᵒᵖ CommGrpCat} (X : Cᵒᵖ) : CommGroup ↑((toGroups D).obj X)

Equations

• CategoryTheory.PresheafOfCommGroups.coefficientCommGroupD X = id inferInstance

@[reducible, inline]

abbrev CategoryTheory.PresheafOfCommGroups.NatTrans.appHom {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} (η : A ⟶ B) (X : Cᵒᵖ) : ↑((toGroups A).obj X) →* ↑((toGroups B).obj X)

The component homomorphism, with both coefficient presheaves forgotten to groups.

Equations

• CategoryTheory.PresheafOfCommGroups.NatTrans.appHom η X = CommGrpCat.Hom.hom (η.app X)

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.naturality_apply {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} (η : A ⟶ B) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : ↑((toGroups A).obj X)) : (ConcreteCategory.hom ((toGroups B).map f)) ((appHom η X) x) = (appHom η Y) ((ConcreteCategory.hom ((toGroups A).map f)) x)

Elementwise naturality after forgetting both coefficient presheaves to groups.

def CategoryTheory.PresheafOfCommGroups.NatTrans.mapZeroCochain {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (a : PresheafOfGroups.ZeroCochain (toGroups A) U) : PresheafOfGroups.ZeroCochain (toGroups B) U

Apply a natural transformation to a zero-cochain, component by component.

Equations

• CategoryTheory.PresheafOfCommGroups.NatTrans.mapZeroCochain η a i = (CategoryTheory.PresheafOfCommGroups.NatTrans.appHom η (Opposite.op (U i))) (a i)

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapZeroCochain_apply {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (a : PresheafOfGroups.ZeroCochain (toGroups A) U) (i : I) : mapZeroCochain η a i = (appHom η (Opposite.op (U i))) (a i)

def CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCochain {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (c : PresheafOfGroups.OneCochain (toGroups A) U) : PresheafOfGroups.OneCochain (toGroups B) U

Apply a natural transformation to every overlap value of a one-cochain.

Equations

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

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCochain_ev {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (c : PresheafOfGroups.OneCochain (toGroups A) U) (i j : I) {T : C} (a : T ⟶ U i) (b : T ⟶ U j) : (mapOneCochain η c).ev i j a b = (appHom η (Opposite.op T)) (c.ev i j a b)

def CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCocycle {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (c : PresheafOfGroups.OneCocycle (toGroups A) U) : PresheafOfGroups.OneCocycle (toGroups B) U

A coefficient map sends one-cocycles to one-cocycles.

Equations

• CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCocycle η c = { toOneCochain := CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCochain η c.toOneCochain, ev_trans := ⋯ }

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCocycle_toOneCochain {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (c : PresheafOfGroups.OneCocycle (toGroups A) U) : (mapOneCocycle η c).toOneCochain = mapOneCochain η c.toOneCochain

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCocycle_one {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) : mapOneCocycle η 1 = 1

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.map_oneCohomologyRelation {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) {c d : PresheafOfGroups.OneCochain (toGroups A) U} {a : PresheafOfGroups.ZeroCochain (toGroups A) U} (h : PresheafOfGroups.OneCohomologyRelation c d a) : PresheafOfGroups.OneCohomologyRelation (mapOneCochain η c) (mapOneCochain η d) (mapZeroCochain η a)

Coefficient maps preserve the explicit degree-one cohomology relation.

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.map_isCohomologous {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) {c d : PresheafOfGroups.OneCocycle (toGroups A) U} (h : c.IsCohomologous d) : (mapOneCocycle η c).IsCohomologous (mapOneCocycle η d)

Coefficient maps preserve cohomologous cocycles.

def CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOne {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) : H1 A U → H1 B U

The map on cover-level H¹ induced by a coefficient natural transformation.

Equations

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

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOne_class {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (c : PresheafOfGroups.OneCocycle (toGroups A) U) : mapHOne η c.class = (mapOneCocycle η c).class

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCocycle_mul {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (c d : PresheafOfGroups.OneCocycle (toGroups A) U) : mapOneCocycle η (OneCocycle.mul A c d) = OneCocycle.mul B (mapOneCocycle η c) (mapOneCocycle η d)

Mapping coefficients commutes with pointwise multiplication of commutative cocycles.

def CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOneHom {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) : H1 A U →* H1 B U

Cover-level functoriality is a homomorphism for the canonical H¹ group laws.

Equations

• CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOneHom η = { toFun := CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOne η, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOneHom_apply {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (x : H1 A U) : (mapHOneHom η) x = mapHOne η x

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCocycle_id {C : Type u} [Category.{v, u} C] {A : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (c : PresheafOfGroups.OneCocycle (toGroups A) U) : mapOneCocycle (CategoryStruct.id A) c = c

Mapping a cocycle by the identity natural transformation changes nothing.

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCocycle_comp {C : Type u} [Category.{v, u} C] {A B D : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (θ : B ⟶ D) (c : PresheafOfGroups.OneCocycle (toGroups A) U) : mapOneCocycle (CategoryStruct.comp η θ) c = mapOneCocycle θ (mapOneCocycle η c)

Mapping a cocycle by a composite is successive mapping.

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOneHom_id {C : Type u} [Category.{v, u} C] {A : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} : mapHOneHom (CategoryStruct.id A) = MonoidHom.id (H1 A U)

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOneHom_comp {C : Type u} [Category.{v, u} C] {A B D : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {U : I → C} (η : A ⟶ B) (θ : B ⟶ D) : mapHOneHom (CategoryStruct.comp η θ) = (mapHOneHom θ).comp (mapHOneHom η)

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCocycle_pullback {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (η : A ⟶ B) (r : PresheafOfGroups.FamilyRefinement V U) (c : PresheafOfGroups.OneCocycle (toGroups A) U) : mapOneCocycle η (r.pullbackOneCocycle c) = r.pullbackOneCocycle (mapOneCocycle η c)

Coefficient mapping commutes strictly with pullback of one-cocycles along a refinement.

theorem CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOne_pullback {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ CommGrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (η : A ⟶ B) (r : PresheafOfGroups.FamilyRefinement V U) (x : H1 A U) : (mapHOneHom η) ((pullbackHOneHom A r) x) = (pullbackHOneHom B r) ((mapHOneHom η) x)

Coefficient mapping and cover refinement commute on H¹.

noncomputable def AlgebraicGeometry.Scheme.FppfHOne.map {X : Scheme} {A B : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat} (η : A ⟶ B) : X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A) → X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups B)

Apply a coefficient natural transformation to a global fppf class. On a representative cover this is the pointwise map of its actual Čech cocycle.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.FppfHOne.map_mk {X : Scheme} {A B : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat} (η : A ⟶ B) (𝒰 : Cover fppfPrecoverage X) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) : map η (mk 𝒰 x) = mk 𝒰 ((CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOneHom η) x)

theorem AlgebraicGeometry.Scheme.FppfHOne.map_mul {X : Scheme} {A B : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat} (η : A ⟶ B) (x y : X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A)) : map η (x * y) = map η x * map η y

Coefficient mapping preserves the global common-refinement product.

noncomputable def AlgebraicGeometry.Scheme.FppfHOne.mapHom {X : Scheme} {A B : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat} (η : A ⟶ B) : X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A) →* X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups B)

Global relative fppf H¹ is covariantly functorial in commutative coefficients.

Equations

• AlgebraicGeometry.Scheme.FppfHOne.mapHom η = { toFun := AlgebraicGeometry.Scheme.FppfHOne.map η, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.FppfHOne.mapHom_apply {X : Scheme} {A B : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat} (η : A ⟶ B) (x : X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A)) : (mapHom η) x = map η x

@[simp]

theorem AlgebraicGeometry.Scheme.FppfHOne.map_id {X : Scheme} {A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat} : map (CategoryTheory.CategoryStruct.id A) = id

theorem AlgebraicGeometry.Scheme.FppfHOne.map_comp {X : Scheme} {A B D : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat} (η : A ⟶ B) (θ : B ⟶ D) : map (CategoryTheory.CategoryStruct.comp η θ) = map θ ∘ map η

@[simp]

theorem AlgebraicGeometry.Scheme.FppfHOne.mapHom_id {X : Scheme} {A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat} : mapHom (CategoryTheory.CategoryStruct.id A) = MonoidHom.id (X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A))

theorem AlgebraicGeometry.Scheme.FppfHOne.mapHom_comp {X : Scheme} {A B D : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat} (η : A ⟶ B) (θ : B ⟶ D) : mapHom (CategoryTheory.CategoryStruct.comp η θ) = (mapHom θ).comp (mapHom η)

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

An ambient commutative group scheme acts on its groups of test-scheme points by postcomposition. No finiteness property of the representing scheme is used.

Equations

• AlgebraicGeometry.CommGroupScheme.mapPoint f T = CategoryTheory.IsMonHom.monoidHom f.hom.hom.hom T

@[simp]

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

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

A morphism of ambient commutative group schemes induces the natural transformation of represented point presheaves given by postcomposition.

Equations

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

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.commPointPresheafMap_id {S : Scheme} (G : CommGroupScheme S) : commPointPresheafMap (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id G.commPointPresheaf

theorem AlgebraicGeometry.CommGroupScheme.commPointPresheafMap_comp {S : Scheme} {G H K : CommGroupScheme S} (f : G ⟶ H) (g : H ⟶ K) : commPointPresheafMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (commPointPresheafMap f) (commPointPresheafMap g)

noncomputable def AlgebraicGeometry.CommGroupScheme.fppfHOneMap {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) : G.FppfHOne →* H.FppfHOne

The map on global fppf H¹ induced by a morphism of ambient commutative group schemes.

Equations

• AlgebraicGeometry.CommGroupScheme.fppfHOneMap f = AlgebraicGeometry.Scheme.FppfHOne.mapHom (AlgebraicGeometry.CommGroupScheme.commPointPresheafMap f)

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.fppfHOneMap_class {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) (Ucover : Scheme.Cover Scheme.fppfPrecoverage S) (x : CategoryTheory.PresheafOfCommGroups.H1 G.commPointPresheaf Ucover.overFamily) : (fppfHOneMap f) (Scheme.FppfHOne.mk Ucover x) = Scheme.FppfHOne.mk Ucover ((CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOneHom (commPointPresheafMap f)) x)

On a cover-level class, an ambient group-scheme map acts pointwise on the Cech cocycle.

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.fppfHOneMap_id {S : Scheme} (G : CommGroupScheme S) : fppfHOneMap (CategoryTheory.CategoryStruct.id G) = MonoidHom.id G.FppfHOne

theorem AlgebraicGeometry.CommGroupScheme.fppfHOneMap_comp {S : Scheme} {G H K : CommGroupScheme S} (f : G ⟶ H) (g : H ⟶ K) : fppfHOneMap (CategoryTheory.CategoryStruct.comp f g) = (fppfHOneMap g).comp (fppfHOneMap f)

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

A morphism of finite-flat commutative group schemes induces the natural transformation of represented point presheaves given by postcomposition.

Equations

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

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.commPointPresheafMap_id {S : Scheme} (G : FiniteFlatCommGroupScheme S) : commPointPresheafMap (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id G.commPointPresheaf

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

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.fppfHOneMap {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : G.FppfHOne →* H.FppfHOne

The map on global fppf H¹ induced by an actual finite-flat group-scheme morphism.

Equations

• AlgebraicGeometry.FiniteFlatCommGroupScheme.fppfHOneMap f = AlgebraicGeometry.Scheme.FppfHOne.mapHom (AlgebraicGeometry.FiniteFlatCommGroupScheme.commPointPresheafMap f)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.commGroupScheme_mapPoint_eq {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CommGroupScheme.mapPoint f.hom = mapPoint f

The ambient and finite-flat actions on test-scheme points agree definitionally.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.commGroupScheme_commPointPresheafMap_eq {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CommGroupScheme.commPointPresheafMap f.hom = commPointPresheafMap f

The ambient and finite-flat natural transformations on represented point presheaves agree definitionally.

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.commGroupScheme_fppfHOneMap_eq {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) : CommGroupScheme.fppfHOneMap f.hom = fppfHOneMap f

Forgetting finite-flat structure does not change the induced map on global fppf H¹. This is the compiled compatibility consumer for ambient coefficient functoriality.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.fppfHOneMap_class {S : Scheme} {G H : FiniteFlatCommGroupScheme S} (f : G ⟶ H) (𝒰 : Scheme.Cover Scheme.fppfPrecoverage S) (x : CategoryTheory.PresheafOfCommGroups.H1 G.commPointPresheaf 𝒰.overFamily) : (fppfHOneMap f) (G.fppfHOneClass 𝒰 x) = H.fppfHOneClass 𝒰 ((CategoryTheory.PresheafOfCommGroups.NatTrans.mapHOneHom (commPointPresheafMap f)) x)

On an actual cover-level class, the group-scheme map acts pointwise on its Čech cocycle.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.fppfHOneMap_id {S : Scheme} (G : FiniteFlatCommGroupScheme S) : fppfHOneMap (CategoryTheory.CategoryStruct.id G) = MonoidHom.id G.FppfHOne

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

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

A certified scheme-theoretic kernel gives an exact pair on points of every test scheme. This is the degree-zero exactness input later consumed by the low-degree fppf sequence.