Čech connecting classes for geometric group-scheme kernels

Let P be a geometric presentation of the kernel of a morphism G ⟶ H of ambient commutative group schemes. A section of H with actual lifts to G on an fppf cover produces overlap differences in G. The kernel universal property lifts each difference uniquely to P.kernel; uniqueness proves naturality and the cocycle law. Thus the construction below is an actual Čech connecting class in global fppf H¹, not an abstract map supplied as an assumption.

This low-level file constructs the class associated to supplied local lifts and proves that it is independent of every choice. A family of local lifts therefore determines a genuine connecting homomorphism. Its values on globally lifted sections are trivial, and extending a boundary class along the certified kernel inclusion is also trivial. No finiteness or flatness property of the three coefficient schemes is used here; those properties enter only through later quotient and cardinality consumers.

def AlgebraicGeometry.CommGroupScheme.baseObject (S : Scheme) : CategoryTheory.Over S

The identity object of the slice, used for global sections over the base.

Equations

• AlgebraicGeometry.CommGroupScheme.baseObject S = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S)

@[reducible, inline]

abbrev AlgebraicGeometry.CommGroupScheme.BasePoint {S : Scheme} (G : CommGroupScheme S) : Type u

Global sections of an ambient commutative group scheme over its base.

Equations

• G.BasePoint = G.Point (AlgebraicGeometry.CommGroupScheme.baseObject S)

noncomputable def AlgebraicGeometry.CommGroupScheme.fppfHOneClass {S : Scheme} (G : CommGroupScheme S) (𝒰 : Scheme.Cover Scheme.fppfPrecoverage S) (x : CategoryTheory.PresheafOfCommGroups.H1 G.commPointPresheaf 𝒰.overFamily) : G.FppfHOne

Send an ambient group-scheme cover-level class to global fppf H¹.

Equations

• G.fppfHOneClass 𝒰 x = AlgebraicGeometry.Scheme.FppfHOne.mk 𝒰 x

theorem AlgebraicGeometry.CommGroupScheme.fppfHOneClass_pullback {S : Scheme} (G : CommGroupScheme S) (𝒰 𝒱 : Scheme.Cover Scheme.fppfPrecoverage S) (r : 𝒱.Hom 𝒰) (x : CategoryTheory.PresheafOfCommGroups.H1 G.commPointPresheaf 𝒰.overFamily) : G.fppfHOneClass 𝒱 ((Scheme.Cover.Hom.pullbackCommHOneHom G.commPointPresheaf r) x) = G.fppfHOneClass 𝒰 x

Pulling an ambient group-scheme cocycle to a genuine refinement does not change its global fppf class.

theorem AlgebraicGeometry.CommGroupScheme.fppfHOneClass_mul_of_commonRefinement {S : Scheme} (G : CommGroupScheme S) (𝒰 𝒱 𝒲 : Scheme.Cover Scheme.fppfPrecoverage S) (r : 𝒲.Hom 𝒰) (s : 𝒲.Hom 𝒱) (x : CategoryTheory.PresheafOfCommGroups.H1 G.commPointPresheaf 𝒰.overFamily) (y : CategoryTheory.PresheafOfCommGroups.H1 G.commPointPresheaf 𝒱.overFamily) : G.fppfHOneClass 𝒰 x * G.fppfHOneClass 𝒱 y = G.fppfHOneClass 𝒲 ((Scheme.Cover.Hom.pullbackCommHOneHom G.commPointPresheaf r) x * (Scheme.Cover.Hom.pullbackCommHOneHom G.commPointPresheaf s) y)

Multiplication of ambient group-scheme fppf classes is computed on any supplied common refinement of their representing covers.

noncomputable def AlgebraicGeometry.CommGroupScheme.pullPoint {S : Scheme} (G : CommGroupScheme S) {T U : CategoryTheory.Over S} (g : T ⟶ U) : G.Point U →* G.Point T

Pull a represented point back along a morphism of test schemes over the base.

Equations

• G.pullPoint g = CommGrpCat.Hom.hom (G.commPointPresheaf.map g.op)

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.pullPoint_apply {S : Scheme} (G : CommGroupScheme S) {T U : CategoryTheory.Over S} (g : T ⟶ U) (x : G.Point U) : (G.pullPoint g) x = CategoryTheory.CategoryStruct.comp g x

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.pullPoint_id {S : Scheme} (G : CommGroupScheme S) {T : CategoryTheory.Over S} (x : G.Point T) : (G.pullPoint (CategoryTheory.CategoryStruct.id T)) x = x

theorem AlgebraicGeometry.CommGroupScheme.pullPoint_comp {S : Scheme} (G : CommGroupScheme S) {T U V : CategoryTheory.Over S} (g : T ⟶ U) (h : U ⟶ V) (x : G.Point V) : (G.pullPoint (CategoryTheory.CategoryStruct.comp g h)) x = (G.pullPoint g) ((G.pullPoint h) x)

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

Pullback along an isomorphism of test objects is an equivalence on the represented commutative groups.

Equations

• G.pointMulEquivOfOverIso e = { toFun := ⇑(G.pullPoint e.inv), invFun := ⇑(G.pullPoint e.hom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

theorem AlgebraicGeometry.CommGroupScheme.mapPoint_pullPoint {S : Scheme} {G H : CommGroupScheme S} (f : G ⟶ H) {T U : CategoryTheory.Over S} (g : T ⟶ U) (x : G.Point U) : (mapPoint f T) ((G.pullPoint g) x) = (H.pullPoint g) ((mapPoint f U) x)

Postcomposition by a group-scheme morphism commutes with restriction of points.

def AlgebraicGeometry.CommGroupScheme.coverToBase {S : Scheme} (𝒰 : Scheme.Cover Scheme.fppfPrecoverage S) (i : 𝒰.I₀) : 𝒰.overFamily i ⟶ baseObject S

The canonical map from a member of an fppf cover to the identity object of the slice.

Equations

• AlgebraicGeometry.CommGroupScheme.coverToBase 𝒰 i = (AlgebraicGeometry.Scheme.FppfHOne.toIdentityCover 𝒰).toOverFamilyRefinement.map i

noncomputable def AlgebraicGeometry.CommGroupScheme.restrictBasePoint {S : Scheme} (G : CommGroupScheme S) (𝒰 : Scheme.Cover Scheme.fppfPrecoverage S) (i : 𝒰.I₀) (x : G.BasePoint) : G.Point (𝒰.overFamily i)

Restriction of a global point to one member of an fppf cover.

Equations

• G.restrictBasePoint 𝒰 i x = (G.pullPoint (AlgebraicGeometry.CommGroupScheme.coverToBase 𝒰 i)) x

structure AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (q : H.BasePoint) : Type (max (u + 1) (v + 1))

Actual local lifts of a global target section through an ambient group-scheme morphism.

• cover : Scheme.Cover Scheme.fppfPrecoverage S

  The genuine fppf cover on which the section lifts.

• lift (i : self.cover.I₀) : G.Point (self.cover.overFamily i)

  One source-group point on each cover member.

• maps_to (i : self.cover.I₀) : (mapPoint f (self.cover.overFamily i)) (self.lift i) = H.restrictBasePoint self.cover i q

  Each local source point maps to the restriction of the original global target section.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.pullPoint_liftPoint {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) {T U : CategoryTheory.Over S} (g : T ⟶ U) (x : G.Point U) (hx : (mapPoint f U) x = 1) : (P.kernel.pullPoint g) (P.liftPoint x hx) = P.liftPoint ((G.pullPoint g) x) ⋯

Pullback of the chosen kernel lift is the chosen lift of the pulled-back point; uniqueness removes all dependence on the Classical.choose witnesses.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.mapPoint_pull_lift_eq {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) (i j : L.cover.I₀) {T : CategoryTheory.Over S} (a : T ⟶ L.cover.overFamily i) (b : T ⟶ L.cover.overFamily j) : (mapPoint f T) ((G.pullPoint a) (L.lift i)) = (mapPoint f T) ((G.pullPoint b) (L.lift j))

The two restrictions of local lifts have the same image in the target group.

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.difference {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) (i j : L.cover.I₀) {T : CategoryTheory.Over S} (a : T ⟶ L.cover.overFamily i) (b : T ⟶ L.cover.overFamily j) : G.Point T

The overlap difference between two local lifts.

Equations

• L.difference i j a b = ((G.pullPoint a) (L.lift i))⁻¹ * (G.pullPoint b) (L.lift j)

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.mapPoint_difference_eq_one {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) (i j : L.cover.I₀) {T : CategoryTheory.Over S} (a : T ⟶ L.cover.overFamily i) (b : T ⟶ L.cover.overFamily j) : (mapPoint f T) (L.difference i j a b) = 1

Every overlap difference is killed by the original group-scheme morphism.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.pullPoint_difference {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) (i j : L.cover.I₀) {T U : CategoryTheory.Over S} (φ : T ⟶ U) (a : U ⟶ L.cover.overFamily i) (b : U ⟶ L.cover.overFamily j) : (G.pullPoint φ) (L.difference i j a b) = L.difference i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b)

Overlap differences commute with further pullback of the test scheme.

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.cocycle {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) : CategoryTheory.PresheafOfGroups.OneCocycle (CategoryTheory.PresheafOfCommGroups.toGroups P.kernel.commPointPresheaf) L.cover.overFamily

The actual kernel-valued Čech cocycle attached to local lifts of one target section.

Equations

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

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.boundaryClass {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) : P.kernel.FppfHOne

The global fppf connecting class produced by genuine local lifts and the certified kernel universal property.

Equations

• L.boundaryClass = P.kernel.fppfHOneClass L.cover L.cocycle.class

def AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.withLift {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) (b : (i : L.cover.I₀) → G.Point (L.cover.overFamily i)) (hb : ∀ (i : L.cover.I₀), (mapPoint f (L.cover.overFamily i)) (b i) = H.restrictBasePoint L.cover i q) : P.LocalLift q

Replace the chosen local lifts while keeping the same genuine cover.

Equations

• L.withLift b hb = { cover := L.cover, lift := b, maps_to := hb }

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.comparisonZeroCochain {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) (b : (i : L.cover.I₀) → G.Point (L.cover.overFamily i)) (hb : ∀ (i : L.cover.I₀), (mapPoint f (L.cover.overFamily i)) (b i) = H.restrictBasePoint L.cover i q) (i : L.cover.I₀) : P.kernel.Point (L.cover.overFamily i)

The pointwise gauge between two systems of local lifts on the same cover, lifted uniquely to the certified kernel.

Equations

• L.comparisonZeroCochain b hb i = P.liftPoint ((b i)⁻¹ * L.lift i) ⋯

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.cocycle_isCohomologous {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) (b' : (i : L.cover.I₀) → G.Point (L.cover.overFamily i)) (hb' : ∀ (i : L.cover.I₀), (mapPoint f (L.cover.overFamily i)) (b' i) = H.restrictBasePoint L.cover i q) : L.cocycle.IsCohomologous (L.withLift b' hb').cocycle

Two choices of local lifts on one cover give cohomologous kernel cocycles.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.boundaryClass_eq_withLift {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) (b : (i : L.cover.I₀) → G.Point (L.cover.overFamily i)) (hb : ∀ (i : L.cover.I₀), (mapPoint f (L.cover.overFamily i)) (b i) = H.restrictBasePoint L.cover i q) : L.boundaryClass = (L.withLift b hb).boundaryClass

Consequently the global connecting class is independent of local lifts made on a fixed cover.

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.pullback {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) {𝒱 : Scheme.Cover Scheme.fppfPrecoverage S} (r : 𝒱.Hom L.cover) : P.LocalLift q

Pull a chosen system of local lifts to a genuine refinement of its fppf cover.

Equations

• L.pullback r = { cover := 𝒱, lift := fun (i : 𝒱.I₀) => have rr := r.toOverFamilyRefinement; (G.pullPoint (rr.map i)) (L.lift (rr.index i)), maps_to := ⋯ }

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.cocycle_pullback {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) {𝒱 : Scheme.Cover Scheme.fppfPrecoverage S} (r : 𝒱.Hom L.cover) : (L.pullback r).cocycle = r.toOverFamilyRefinement.pullbackOneCocycle L.cocycle

The cocycle built after refining local lifts is the actual pullback of the original cocycle.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.boundaryClass_pullback {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) {𝒱 : Scheme.Cover Scheme.fppfPrecoverage S} (r : 𝒱.Hom L.cover) : (L.pullback r).boundaryClass = L.boundaryClass

Refining the cover and the chosen local lifts does not change the global connecting class.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.boundaryClass_eq {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L M : P.LocalLift q) : L.boundaryClass = M.boundaryClass

The global connecting class is independent of both the fppf cover and all chosen local lifts.

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.one {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) : P.LocalLift 1

The trivial target section has its tautological lift on the identity fppf cover.

Equations

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

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.one_cocycle {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) : (one P).cocycle = 1

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.one_boundaryClass {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) : (one P).boundaryClass = 1

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.mul {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q r : H.BasePoint} (L : P.LocalLift q) (M : P.LocalLift r) : P.LocalLift (q * r)

Multiply two locally lifted sections after passing to the intersection of their covers.

Equations

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

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.mul_cocycle {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q r : H.BasePoint} (L : P.LocalLift q) (M : P.LocalLift r) : (L.mul M).cocycle = CategoryTheory.PresheafOfCommGroups.OneCocycle.mul P.kernel.commPointPresheaf (L.pullback (L.cover.interFst M.cover)).cocycle (M.pullback (L.cover.interSnd M.cover)).cocycle

The overlap cocycle of a product of local lifts is the pointwise product of the two pulled-back overlap cocycles on the common refinement.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.mul_boundaryClass {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q r : H.BasePoint} (L : P.LocalLift q) (M : P.LocalLift r) : (L.mul M).boundaryClass = L.boundaryClass * M.boundaryClass

The connecting class respects multiplication. Both sides are computed on the actual intersection cover used to multiply the local lifts.

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.ofBasePoint {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (x : G.BasePoint) : P.LocalLift ((mapPoint f (baseObject S)) x)

A global source section gives a local lift of its image on the identity cover.

Equations

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

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.ofBasePoint_cocycle {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (x : G.BasePoint) : (ofBasePoint P x).cocycle = 1

The overlap cocycle of a genuinely global lift is trivial.

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.ofBasePoint_boundaryClass {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} (P : KernelPresentation f) (x : G.BasePoint) : (ofBasePoint P x).boundaryClass = 1

A global lift therefore has the trivial global connecting class.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.map_cocycle_isCohomologous_one {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) : (CategoryTheory.PresheafOfCommGroups.NatTrans.mapOneCocycle (commPointPresheafMap P.inclusion) L.cocycle).IsCohomologous 1

After applying the kernel inclusion to coefficients, a boundary cocycle is cohomologous to the trivial cocycle; the original local source points are the explicit gauge.

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocalLift.fppfHOneMap_boundaryClass {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} {q : H.BasePoint} (L : P.LocalLift q) : (fppfHOneMap P.inclusion) L.boundaryClass = 1

The induced H¹ map along the kernel inclusion kills every constructed boundary class.

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

Local surjectivity on represented points, with the actual fppf cover and local lifts retained for every global target section.

• localLift (q : H.BasePoint) : P.LocalLift q

  A genuine local lift of each global target section.

noncomputable def AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocallyLiftable.boundaryHom {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} (E : P.LocallyLiftable) : H.BasePoint →* P.kernel.FppfHOne

The connecting homomorphism obtained from actual local lifts and their kernel-valued Čech cocycles. Independence of all choices, rather than an assumed map, supplies its group laws.

Equations

• E.boundaryHom = { toFun := fun (q : H.BasePoint) => (E.localLift q).boundaryClass, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocallyLiftable.boundaryHom_apply {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} (E : P.LocallyLiftable) (q : H.BasePoint) : E.boundaryHom q = (E.localLift q).boundaryClass

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocallyLiftable.boundaryHom_mapPoint {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} (E : P.LocallyLiftable) (x : G.BasePoint) : E.boundaryHom ((mapPoint f (baseObject S)) x) = 1

A section already lifted globally has zero boundary. This is the checked image(H⁰(G)) ⊆ kernel(δ) half of exactness at H⁰(H).

@[simp]

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocallyLiftable.fppfHOneMap_boundaryHom {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} (E : P.LocallyLiftable) (q : H.BasePoint) : (fppfHOneMap P.inclusion) (E.boundaryHom q) = 1

Every constructed connecting class maps to zero in H¹(G). This is the checked image(δ) ⊆ kernel(H¹(P.kernel) → H¹(G)) half of the next exactness assertion.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocallyLiftable.exists_source_of_boundaryHom_eq_one {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} (E : P.LocallyLiftable) (q : H.BasePoint) (hq : E.boundaryHom q = 1) : ∃ (x : G.BasePoint), (mapPoint f (baseObject S)) x = q

If a locally liftable section has trivial connecting class, an fppf refinement and a zero-cochain gauge make its local lifts agree. Subcanonical descent then glues those lifts to a global source section.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocallyLiftable.boundaryHom_eq_one_iff_exists_source {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} (E : P.LocallyLiftable) (q : H.BasePoint) : E.boundaryHom q = 1 ↔ ∃ (x : G.BasePoint), (mapPoint f (baseObject S)) x = q

Exactness at global target sections for every locally liftable group-scheme morphism.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocallyLiftable.exact_mapPoint_boundaryHom {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} (E : P.LocallyLiftable) : Function.MulExact ⇑(mapPoint f (baseObject S)) ⇑E.boundaryHom

The represented-point map followed by its checked connecting homomorphism is exact.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocallyLiftable.exists_boundary_of_fppfHOneMap_eq_one {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} (E : P.LocallyLiftable) (z : P.kernel.FppfHOne) (hz : (fppfHOneMap P.inclusion) z = 1) : ∃ (q : H.BasePoint), E.boundaryHom q = z

Every global kernel H¹ class killed by extension to the source group is represented by a boundary of a global target section.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocallyLiftable.fppfHOneMap_eq_one_iff_exists_boundaryHom {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} (E : P.LocallyLiftable) (z : P.kernel.FppfHOne) : (fppfHOneMap P.inclusion) z = 1 ↔ ∃ (q : H.BasePoint), E.boundaryHom q = z

A kernel H¹ class dies in source-group H¹ exactly when it is a connecting class.

theorem AlgebraicGeometry.CommGroupScheme.KernelPresentation.LocallyLiftable.exact_boundaryHom_fppfHOneMap {S : Scheme} {G H : CommGroupScheme S} {f : G ⟶ H} {P : KernelPresentation f} (E : P.LocallyLiftable) : Function.MulExact ⇑E.boundaryHom ⇑(fppfHOneMap P.inclusion)

Exactness at kernel-valued H¹ for every locally liftable ambient group-scheme morphism.