The commutative group law on global fppf H¹

For a presheaf of commutative groups, pointwise multiplication and inversion preserve Čech one-cocycles and cohomology. This file first constructs that group law on Mathlib's cover-level PresheafOfGroups.H1, then proves that genuine cover refinements act by homomorphisms.

The global law is descended through the common-refinement quotient defining Scheme.FppfHOne. Products of classes represented on two covers are computed after pullback to their intersection. No group structure is transported from an unrelated type.

@[reducible, inline]

abbrev CategoryTheory.PresheafOfCommGroups.toGroups {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) : Functor Cᵒᵖ GrpCat

Forget a presheaf of commutative groups to a presheaf of groups.

Equations

• CategoryTheory.PresheafOfCommGroups.toGroups A = A.comp (CategoryTheory.forget₂ CommGrpCat GrpCat)

@[instance_reducible]

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

Equations

• CategoryTheory.PresheafOfCommGroups.coefficientCommGroup A X = id inferInstance

@[reducible, inline]

abbrev CategoryTheory.PresheafOfCommGroups.H1 {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} (U : I → C) : Type (max (max (max u v) w) wI)

Cover-level degree-one cohomology with commutative coefficients.

Equations

• CategoryTheory.PresheafOfCommGroups.H1 A U = CategoryTheory.PresheafOfGroups.H1 (CategoryTheory.PresheafOfCommGroups.toGroups A) U

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

Pointwise multiplication of one-cocycles with commutative coefficients.

Equations

• CategoryTheory.PresheafOfCommGroups.OneCocycle.mul A c d = { toOneCochain := c.toOneCochain * d.toOneCochain, ev_trans := ⋯ }

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

Pointwise inversion of a one-cocycle with commutative coefficients.

Equations

• CategoryTheory.PresheafOfCommGroups.OneCocycle.inv A c = { toOneCochain := c.toOneCochain⁻¹, ev_trans := ⋯ }

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.OneCocycle.mul_toOneCochain {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} (c d : PresheafOfGroups.OneCocycle (toGroups A) U) : (mul A c d).toOneCochain = c.toOneCochain * d.toOneCochain

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.OneCocycle.inv_toOneCochain {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} (c : PresheafOfGroups.OneCocycle (toGroups A) U) : (inv A c).toOneCochain = c.toOneCochain⁻¹

theorem CategoryTheory.PresheafOfCommGroups.OneCocycle.ext {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} {c d : PresheafOfGroups.OneCocycle (toGroups A) U} (h : c.toOneCochain = d.toOneCochain) : c = d

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.OneCocycle.one_mul {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} (c : PresheafOfGroups.OneCocycle (toGroups A) U) : mul A 1 c = c

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.OneCocycle.mul_one {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} (c : PresheafOfGroups.OneCocycle (toGroups A) U) : mul A c 1 = c

theorem CategoryTheory.PresheafOfCommGroups.OneCocycle.mul_assoc {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} (a b c : PresheafOfGroups.OneCocycle (toGroups A) U) : mul A (mul A a b) c = mul A a (mul A b c)

theorem CategoryTheory.PresheafOfCommGroups.OneCocycle.mul_comm {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} (a b : PresheafOfGroups.OneCocycle (toGroups A) U) : mul A a b = mul A b a

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.OneCocycle.inv_mul {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} (c : PresheafOfGroups.OneCocycle (toGroups A) U) : mul A (inv A c) c = 1

theorem CategoryTheory.PresheafOfCommGroups.isCohomologous_mul {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} {a b c d : PresheafOfGroups.OneCocycle (toGroups A) U} (hab : a.IsCohomologous b) (hcd : c.IsCohomologous d) : (OneCocycle.mul A a c).IsCohomologous (OneCocycle.mul A b d)

Cohomologous cocycles may be multiplied when the coefficient groups are commutative.

theorem CategoryTheory.PresheafOfCommGroups.isCohomologous_inv {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} {a b : PresheafOfGroups.OneCocycle (toGroups A) U} (hab : a.IsCohomologous b) : (OneCocycle.inv A a).IsCohomologous (OneCocycle.inv A b)

Cohomologous cocycles may be inverted when the coefficient groups are commutative.

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

Multiplication on cover-level H¹, descended from pointwise multiplication of cocycles.

Equations

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

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

Inversion on cover-level H¹, descended from pointwise inversion of cocycles.

Equations

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

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.hOneMul_class {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} (a b : PresheafOfGroups.OneCocycle (toGroups A) U) : hOneMul A a.class b.class = (OneCocycle.mul A a b).class

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.hOneInv_class {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} (a : PresheafOfGroups.OneCocycle (toGroups A) U) : hOneInv A a.class = (OneCocycle.inv A a).class

@[instance_reducible]

noncomputable instance CategoryTheory.PresheafOfCommGroups.hOneCommGroup {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {U : I → C} : CommGroup (H1 A U)

The canonical commutative group structure on cover-level degree-one cohomology.

Equations

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

theorem CategoryTheory.PresheafOfCommGroups.pullbackOneCocycle_mul {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : PresheafOfGroups.FamilyRefinement V U) (a b : PresheafOfGroups.OneCocycle (toGroups A) U) : VU.pullbackOneCocycle (OneCocycle.mul A a b) = OneCocycle.mul A (VU.pullbackOneCocycle a) (VU.pullbackOneCocycle b)

Pullback of commutative-coefficient cocycles preserves pointwise multiplication.

def CategoryTheory.PresheafOfCommGroups.pullbackHOneHom {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : PresheafOfGroups.FamilyRefinement V U) : H1 A U →* H1 A V

Cover-level H¹ pullback is a homomorphism for commutative coefficients.

Equations

• CategoryTheory.PresheafOfCommGroups.pullbackHOneHom A VU = { toFun := VU.pullbackHOne, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.PresheafOfCommGroups.pullbackHOneHom_apply {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ CommGrpCat) {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : PresheafOfGroups.FamilyRefinement V U) (x : H1 A U) : (pullbackHOneHom A VU) x = VU.pullbackHOne x

noncomputable def AlgebraicGeometry.Scheme.Cover.interFst {X : Scheme} (𝒰 𝒱 : Cover fppfPrecoverage X) : Hom (CategoryTheory.Precoverage.ZeroHypercover.inter 𝒰 𝒱) 𝒰

First projection from the intersection of two genuine fppf covers.

Equations

• 𝒰.interFst 𝒱 = 𝒰.interFst 𝒱.toPreZeroHypercover

noncomputable def AlgebraicGeometry.Scheme.Cover.interSnd {X : Scheme} (𝒰 𝒱 : Cover fppfPrecoverage X) : Hom (CategoryTheory.Precoverage.ZeroHypercover.inter 𝒰 𝒱) 𝒱

Second projection from the intersection of two genuine fppf covers.

Equations

• 𝒰.interSnd 𝒱 = 𝒰.interSnd 𝒱.toPreZeroHypercover

noncomputable def AlgebraicGeometry.Scheme.Cover.interLift {X : Scheme} {𝒰 𝒱 𝒲 : Cover fppfPrecoverage X} (r : 𝒲.Hom 𝒰) (s : 𝒲.Hom 𝒱) : 𝒲.Hom (CategoryTheory.Precoverage.ZeroHypercover.inter 𝒰 𝒱)

A cover refining each of two covers refines their intersection.

Equations

• AlgebraicGeometry.Scheme.Cover.interLift r s = CategoryTheory.PreZeroHypercover.interLift r s

def AlgebraicGeometry.Scheme.Cover.Hom.pullbackCommHOneHom {X : Scheme} {𝒰 𝒱 : Cover fppfPrecoverage X} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (r : 𝒱.Hom 𝒰) : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily →* CategoryTheory.PresheafOfCommGroups.H1 A 𝒱.overFamily

Relative cover-level pullback as a homomorphism for commutative coefficients.

Equations

• AlgebraicGeometry.Scheme.Cover.Hom.pullbackCommHOneHom A r = CategoryTheory.PresheafOfCommGroups.pullbackHOneHom A r.toOverFamilyRefinement

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.Hom.pullbackCommHOneHom_apply {X : Scheme} {𝒰 𝒱 : Cover fppfPrecoverage X} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (r : 𝒱.Hom 𝒰) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) : (pullbackCommHOneHom A r) x = pullbackHOne (CategoryTheory.PresheafOfCommGroups.toGroups A) r x

theorem AlgebraicGeometry.Scheme.Cover.Hom.pullbackHOne_inv {X : Scheme} {𝒰 𝒱 : Cover fppfPrecoverage X} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (r : 𝒱.Hom 𝒰) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) : pullbackHOne (CategoryTheory.PresheafOfCommGroups.toGroups A) r x⁻¹ = (pullbackHOne (CategoryTheory.PresheafOfCommGroups.toGroups A) r x)⁻¹

noncomputable def AlgebraicGeometry.Scheme.FppfHOne.mulClass {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (𝒰 𝒱 : Cover fppfPrecoverage X) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) (y : CategoryTheory.PresheafOfCommGroups.H1 A 𝒱.overFamily) : X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A)

Multiply two cover-level classes after pulling them to the intersection of their covers, then send the result to global fppf H¹.

Equations

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

theorem AlgebraicGeometry.Scheme.FppfHOne.mulClass_eq_mk_of_commonRefinement {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (𝒰 𝒱 𝒲 : Cover fppfPrecoverage X) (r : 𝒲.Hom 𝒰) (s : 𝒲.Hom 𝒱) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) (y : CategoryTheory.PresheafOfCommGroups.H1 A 𝒱.overFamily) : mulClass A 𝒰 𝒱 x y = mk 𝒲 ((Cover.Hom.pullbackCommHOneHom A r) x * (Cover.Hom.pullbackCommHOneHom A s) y)

The product may be computed on any genuine common refinement of the two representing covers. This theorem removes all dependence on the chosen intersection presentation.

theorem AlgebraicGeometry.Scheme.FppfHOne.mulClass_pullback_right {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (𝒰 𝒱 𝒱' : Cover fppfPrecoverage X) (r : 𝒱'.Hom 𝒱) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) (y : CategoryTheory.PresheafOfCommGroups.H1 A 𝒱.overFamily) : mulClass A 𝒰 𝒱' x ((Cover.Hom.pullbackCommHOneHom A r) y) = mulClass A 𝒰 𝒱 x y

Refining the right-hand representative does not change its global product.

theorem AlgebraicGeometry.Scheme.FppfHOne.mulClass_pullback_left {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (𝒰 𝒰' 𝒱 : Cover fppfPrecoverage X) (r : 𝒰'.Hom 𝒰) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) (y : CategoryTheory.PresheafOfCommGroups.H1 A 𝒱.overFamily) : mulClass A 𝒰' 𝒱 ((Cover.Hom.pullbackCommHOneHom A r) x) y = mulClass A 𝒰 𝒱 x y

Refining the left-hand representative does not change its global product.

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

Multiplication on global fppf H¹, descended from multiplication on cover-level classes.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.FppfHOne.mul_mk {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (𝒰 𝒱 : Cover fppfPrecoverage X) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) (y : CategoryTheory.PresheafOfCommGroups.H1 A 𝒱.overFamily) : mul A (mk 𝒰 x) (mk 𝒱 y) = mulClass A 𝒰 𝒱 x y

theorem AlgebraicGeometry.Scheme.FppfHOne.mul_mk_eq_mk_of_commonRefinement {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (𝒰 𝒱 𝒲 : Cover fppfPrecoverage X) (r : 𝒲.Hom 𝒰) (s : 𝒲.Hom 𝒱) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) (y : CategoryTheory.PresheafOfCommGroups.H1 A 𝒱.overFamily) : mul A (mk 𝒰 x) (mk 𝒱 y) = mk 𝒲 ((Cover.Hom.pullbackCommHOneHom A r) x * (Cover.Hom.pullbackCommHOneHom A s) y)

Global multiplication may be evaluated on any supplied common refinement.

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

Inversion on global fppf H¹, descended on each representative cover.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.FppfHOne.inv_mk {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (𝒰 : Cover fppfPrecoverage X) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) : inv A (mk 𝒰 x) = mk 𝒰 x⁻¹

theorem AlgebraicGeometry.Scheme.FppfHOne.one_mul_global {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (z : X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A)) : mul A 1 z = z

theorem AlgebraicGeometry.Scheme.FppfHOne.mul_one_global {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (z : X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A)) : mul A z 1 = z

theorem AlgebraicGeometry.Scheme.FppfHOne.inv_mul_cancel_global {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (z : X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A)) : mul A (inv A z) z = 1

theorem AlgebraicGeometry.Scheme.FppfHOne.mul_comm_global {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (x y : X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A)) : mul A x y = mul A y x

theorem AlgebraicGeometry.Scheme.FppfHOne.mul_assoc_global {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (x y z : X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A)) : mul A (mul A x y) z = mul A x (mul A y z)

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.FppfHOne.commGroup {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) : CommGroup (X.FppfHOne (CategoryTheory.PresheafOfCommGroups.toGroups A))

The canonical commutative group structure on relative global fppf H¹ with commutative coefficients. Its operations are descended from the actual cover-level cocycle operations.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.FppfHOne.mk_mul_mk {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (𝒰 𝒱 : Cover fppfPrecoverage X) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) (y : CategoryTheory.PresheafOfCommGroups.H1 A 𝒱.overFamily) : mk 𝒰 x * mk 𝒱 y = mulClass A 𝒰 𝒱 x y

theorem AlgebraicGeometry.Scheme.FppfHOne.mk_mul_mk_eq_mk_of_commonRefinement {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (𝒰 𝒱 𝒲 : Cover fppfPrecoverage X) (r : 𝒲.Hom 𝒰) (s : 𝒲.Hom 𝒱) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) (y : CategoryTheory.PresheafOfCommGroups.H1 A 𝒱.overFamily) : mk 𝒰 x * mk 𝒱 y = mk 𝒲 ((Cover.Hom.pullbackCommHOneHom A r) x * (Cover.Hom.pullbackCommHOneHom A s) y)

@[simp]

theorem AlgebraicGeometry.Scheme.FppfHOne.inv_mk' {X : Scheme} (A : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ CommGrpCat) (𝒰 : Cover fppfPrecoverage X) (x : CategoryTheory.PresheafOfCommGroups.H1 A 𝒰.overFamily) : (mk 𝒰 x)⁻¹ = mk 𝒰 x⁻¹

@[instance_reducible]

noncomputable instance AlgebraicGeometry.FiniteFlatCommGroupScheme.fppfHOneCommGroup {S : Scheme} (G : FiniteFlatCommGroupScheme S) : CommGroup G.FppfHOne

The canonical commutative group structure on fppf H¹ of an actual finite-flat commutative group scheme.

Equations

• G.fppfHOneCommGroup = AlgebraicGeometry.Scheme.FppfHOne.commGroup G.commPointPresheaf

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.fppfHOneClass_mul_of_commonRefinement {S : Scheme} (G : FiniteFlatCommGroupScheme 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 global finite-flat group-scheme classes is computed by pulling their actual cover-level cocycles to any supplied common refinement.

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.fppfHOneClass_inv {S : Scheme} (G : FiniteFlatCommGroupScheme S) (𝒰 : Scheme.Cover Scheme.fppfPrecoverage S) (x : CategoryTheory.PresheafOfCommGroups.H1 G.commPointPresheaf 𝒰.overFamily) : (G.fppfHOneClass 𝒰 x)⁻¹ = G.fppfHOneClass 𝒰 x⁻¹

Inversion of a global finite-flat group-scheme class is induced by inversion of its actual cover-level cocycle class.