Refinement maps and global fppf cohomology in degree one

Mathlib defines nonabelian H¹ on one indexed family, but at the pinned revision leaves its globalization over covering families as a TODO. This file supplies the missing transition maps: a refinement of indexed families pulls zero-cochains, one-cochains, cocycles, and cohomology classes back. The construction is contravariantly functorial and sends the trivial class to the trivial class.

For actual fppf covers of a scheme X, FppfHOne is the filtered-colimit quotient of all cover-level classes by common refinement. Crucially, a cover component Uᵢ ⟶ X is regarded as an object of Over X, and coefficients are presheaves on (Over X)ᵒᵖ. Thus the test morphisms in a one-cochain are morphisms over X; the resulting overlaps are fibre products Uᵢ ×_X Uⱼ, not absolute products of schemes.

We use the explicit quotient presentation of a colimit of types, rather than asking Lean for a small category of all covers. The latter would require a smallness instance which the large indexed-cover category does not possess. The relation is generated only by genuine Scheme.Cover.Hom refinements. The final section checks the intended coefficient system: the point presheaf represented by a finite-flat commutative group scheme over X.

structure CategoryTheory.PresheafOfGroups.FamilyRefinement {C : Type u} [Category.{v, u} C] {I : Type wI} {J : Type wJ} (V : J → C) (U : I → C) : Type (max (max v wI) wJ)

A refinement of an indexed family U by an indexed family V.

• index : J → I

  Index of the old family containing a member of the refined family.

• map (j : J) : V j ⟶ U (self.index j)

  The refinement morphism.

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.oneCocycle_ext {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {U : I → C} {c d : OneCocycle G U} (h : c.toOneCochain = d.toOneCochain) : c = d

Equality of one-cocycles is detected on the underlying one-cochain.

def CategoryTheory.PresheafOfGroups.FamilyRefinement.refl {C : Type u} [Category.{v, u} C] {I : Type wI} (U : I → C) : FamilyRefinement U U

The identity refinement.

Equations

• CategoryTheory.PresheafOfGroups.FamilyRefinement.refl U = { index := id, map := fun (x : I) => CategoryTheory.CategoryStruct.id (U x) }

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.refl_index {C : Type u} [Category.{v, u} C] {I : Type wI} (U : I → C) (a : I) : (refl U).index a = id a

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.refl_map {C : Type u} [Category.{v, u} C] {I : Type wI} (U : I → C) (x✝ : I) : (refl U).map x✝ = CategoryStruct.id (U x✝)

def CategoryTheory.PresheafOfGroups.FamilyRefinement.comp {C : Type u} [Category.{v, u} C] {I : Type wI} {J : Type wJ} {K : Type wK} {U : I → C} {V : J → C} {W : K → C} (VU : FamilyRefinement V U) (WV : FamilyRefinement W V) : FamilyRefinement W U

Composition of refinements.

Equations

• VU.comp WV = { index := VU.index ∘ WV.index, map := fun (k : K) => CategoryTheory.CategoryStruct.comp (WV.map k) (VU.map (WV.index k)) }

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.comp_map {C : Type u} [Category.{v, u} C] {I : Type wI} {J : Type wJ} {K : Type wK} {U : I → C} {V : J → C} {W : K → C} (VU : FamilyRefinement V U) (WV : FamilyRefinement W V) (k : K) : (VU.comp WV).map k = CategoryStruct.comp (WV.map k) (VU.map (WV.index k))

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.comp_index {C : Type u} [Category.{v, u} C] {I : Type wI} {J : Type wJ} {K : Type wK} {U : I → C} {V : J → C} {W : K → C} (VU : FamilyRefinement V U) (WV : FamilyRefinement W V) (a✝ : K) : (VU.comp WV).index a✝ = (VU.index ∘ WV.index) a✝

def CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackZeroCochain {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) (a : ZeroCochain G U) : ZeroCochain G V

Pull a zero-cochain back along a refinement.

Equations

• VU.pullbackZeroCochain a j = (CategoryTheory.ConcreteCategory.hom (G.map (VU.map j).op)) (a (VU.index j))

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackZeroCochain_apply {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) (a : ZeroCochain G U) (j : J) : VU.pullbackZeroCochain a j = (ConcreteCategory.hom (G.map (VU.map j).op)) (a (VU.index j))

def CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackOneCochain {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) (c : OneCochain G U) : OneCochain G V

Pull a one-cochain back along a refinement.

Equations

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

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackOneCochain_ev {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) (c : OneCochain G U) (i j : J) {T : C} (a : T ⟶ V i) (b : T ⟶ V j) : (VU.pullbackOneCochain c).ev i j a b = c.ev (VU.index i) (VU.index j) (CategoryStruct.comp a (VU.map i)) (CategoryStruct.comp b (VU.map j))

def CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackOneCocycle {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) (c : OneCocycle G U) : OneCocycle G V

Pull a one-cocycle back along a refinement.

Equations

• VU.pullbackOneCocycle c = { toOneCochain := VU.pullbackOneCochain c.toOneCochain, ev_trans := ⋯ }

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackOneCocycle_toOneCochain {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) (c : OneCocycle G U) : (VU.pullbackOneCocycle c).toOneCochain = VU.pullbackOneCochain c.toOneCochain

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullback_oneCohomologyRelation {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) {c d : OneCochain G U} {a : ZeroCochain G U} (h : OneCohomologyRelation c d a) : OneCohomologyRelation (VU.pullbackOneCochain c) (VU.pullbackOneCochain d) (VU.pullbackZeroCochain a)

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullback_isCohomologous {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) {c d : OneCocycle G U} (h : c.IsCohomologous d) : (VU.pullbackOneCocycle c).IsCohomologous (VU.pullbackOneCocycle d)

def CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackHOne {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) : H1 G U → H1 G V

Pull a cover-level H¹ class back along a refinement.

Equations

• VU.pullbackHOne = Quot.lift (fun (c : CategoryTheory.PresheafOfGroups.OneCocycle G U) => (VU.pullbackOneCocycle c).class) ⋯

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackHOne_class {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) (c : OneCocycle G U) : VU.pullbackHOne c.class = (VU.pullbackOneCocycle c).class

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackOneCocycle_one {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) : VU.pullbackOneCocycle 1 = 1

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackHOne_one {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU : FamilyRefinement V U) : VU.pullbackHOne 1 = 1

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackOneCocycle_refl {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {U : I → C} (c : OneCocycle G U) : (refl U).pullbackOneCocycle c = c

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackOneCocycle_comp {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {K : Type wK} {U : I → C} {V : J → C} {W : K → C} (VU : FamilyRefinement V U) (WV : FamilyRefinement W V) (c : OneCocycle G U) : (VU.comp WV).pullbackOneCocycle c = WV.pullbackOneCocycle (VU.pullbackOneCocycle c)

@[simp]

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackHOne_refl {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {U : I → C} (x : H1 G U) : (refl U).pullbackHOne x = x

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackHOne_comp {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {K : Type wK} {U : I → C} {V : J → C} {W : K → C} (VU : FamilyRefinement V U) (WV : FamilyRefinement W V) (x : H1 G U) : (VU.comp WV).pullbackHOne x = WV.pullbackHOne (VU.pullbackHOne x)

def CategoryTheory.PresheafOfGroups.FamilyRefinement.comparisonZeroCochain {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU VU' : FamilyRefinement V U) (c : OneCocycle G U) : ZeroCochain G V

The zero-cochain comparing the pullbacks of a cocycle along two refinement choices.

Equations

• VU.comparisonZeroCochain VU' c i = c.ev (VU'.index i) (VU.index i) (VU'.map i) (VU.map i)

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackOneCocycle_isCohomologous {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU VU' : FamilyRefinement V U) (c : OneCocycle G U) : (VU.pullbackOneCocycle c).IsCohomologous (VU'.pullbackOneCocycle c)

Two choices of refinement map pull a cocycle back to cohomologous cocycles. This is the degree-one Čech homotopy which makes the global common-refinement relation transitive.

theorem CategoryTheory.PresheafOfGroups.FamilyRefinement.pullbackHOne_eq {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type wI} {J : Type wJ} {U : I → C} {V : J → C} (VU VU' : FamilyRefinement V U) (x : H1 G U) : VU.pullbackHOne x = VU'.pullbackHOne x

Cover-level H¹ pullback is independent of the chosen refinement morphism.

def CategoryTheory.PreZeroHypercover.Hom.toFamilyRefinement {C : Type u} [Category.{v, u} C] {S : C} {𝒰 : PreZeroHypercover S} {𝒱 : PreZeroHypercover S} (r : 𝒱.Hom 𝒰) : PresheafOfGroups.FamilyRefinement 𝒱.X 𝒰.X

The indexed-family refinement underlying a morphism of pre-zero-hypercovers.

Equations

• r.toFamilyRefinement = { index := r.s₀, map := r.h₀ }

@[simp]

theorem CategoryTheory.PreZeroHypercover.Hom.toFamilyRefinement_index {C : Type u} [Category.{v, u} C] {S : C} {𝒰 : PreZeroHypercover S} {𝒱 : PreZeroHypercover S} (r : 𝒱.Hom 𝒰) (i : 𝒱.I₀) : r.toFamilyRefinement.index i = r.s₀ i

@[simp]

theorem CategoryTheory.PreZeroHypercover.Hom.toFamilyRefinement_map {C : Type u} [Category.{v, u} C] {S : C} {𝒰 : PreZeroHypercover S} {𝒱 : PreZeroHypercover S} (r : 𝒱.Hom 𝒰) (i : 𝒱.I₀) : r.toFamilyRefinement.map i = r.h₀ i

theorem CategoryTheory.PreZeroHypercover.Hom.toFamilyRefinement_id {C : Type u} [Category.{v, u} C] {S : C} {𝒰 : PreZeroHypercover S} : (id 𝒰).toFamilyRefinement = PresheafOfGroups.FamilyRefinement.refl 𝒰.X

theorem CategoryTheory.PreZeroHypercover.Hom.toFamilyRefinement_comp {C : Type u} [Category.{v, u} C] {S : C} {𝒰 : PreZeroHypercover S} {𝒱 : PreZeroHypercover S} {𝒲 : PreZeroHypercover S} (r : 𝒱.Hom 𝒰) (s : 𝒲.Hom 𝒱) : (s.comp r).toFamilyRefinement = r.toFamilyRefinement.comp s.toFamilyRefinement

def CategoryTheory.PreZeroHypercover.Hom.pullbackHOne {C : Type u} [Category.{v, u} C] {S : C} {𝒰 : PreZeroHypercover S} {𝒱 : PreZeroHypercover S} (G : Functor Cᵒᵖ GrpCat) (r : 𝒱.Hom 𝒰) : PresheafOfGroups.H1 G 𝒰.X → PresheafOfGroups.H1 G 𝒱.X

Pull a family-level H¹ class back along a morphism of pre-zero-hypercovers.

Equations

• CategoryTheory.PreZeroHypercover.Hom.pullbackHOne G r = r.toFamilyRefinement.pullbackHOne

@[simp]

theorem CategoryTheory.PreZeroHypercover.Hom.pullbackHOne_id {C : Type u} [Category.{v, u} C] {S : C} {𝒰 : PreZeroHypercover S} (G : Functor Cᵒᵖ GrpCat) (x : PresheafOfGroups.H1 G 𝒰.X) : pullbackHOne G (id 𝒰) x = x

theorem CategoryTheory.PreZeroHypercover.Hom.pullbackHOne_comp {C : Type u} [Category.{v, u} C] {S : C} {𝒰 : PreZeroHypercover S} {𝒱 : PreZeroHypercover S} {𝒲 : PreZeroHypercover S} (G : Functor Cᵒᵖ GrpCat) (r : 𝒱.Hom 𝒰) (s : 𝒲.Hom 𝒱) (x : PresheafOfGroups.H1 G 𝒰.X) : pullbackHOne G (s.comp r) x = pullbackHOne G s (pullbackHOne G r x)

theorem CategoryTheory.PreZeroHypercover.Hom.pullbackHOne_eq {C : Type u} [Category.{v, u} C] {S : C} {𝒰 : PreZeroHypercover S} {𝒱 : PreZeroHypercover S} (G : Functor Cᵒᵖ GrpCat) (r r' : 𝒱.Hom 𝒰) (x : PresheafOfGroups.H1 G 𝒰.X) : pullbackHOne G r x = pullbackHOne G r' x

@[simp]

theorem CategoryTheory.PreZeroHypercover.Hom.pullbackHOne_one {C : Type u} [Category.{v, u} C] {S : C} {𝒰 : PreZeroHypercover S} {𝒱 : PreZeroHypercover S} (G : Functor Cᵒᵖ GrpCat) (r : 𝒱.Hom 𝒰) : pullbackHOne G r 1 = 1

def AlgebraicGeometry.Scheme.Cover.overFamily {X : Scheme} (𝒰 : Cover fppfPrecoverage X) : 𝒰.I₀ → CategoryTheory.Over X

Regard the components of an fppf cover of X as objects in the slice category Over X. Keeping the structure maps in the objects is essential: morphisms between components must commute with their maps to X.

Equations

• 𝒰.overFamily i = CategoryTheory.Over.mk (𝒰.f i)

def AlgebraicGeometry.Scheme.Cover.Hom.toOverFamilyRefinement {X : Scheme} {𝒰 𝒱 : Cover fppfPrecoverage X} (r : 𝒱.Hom 𝒰) : CategoryTheory.PresheafOfGroups.FamilyRefinement 𝒱.overFamily 𝒰.overFamily

A refinement of fppf covers induces a refinement of their component families in Over X. The proof field r.w₀ is precisely what makes every component map a morphism over X.

Equations

• r.toOverFamilyRefinement = { index := r.s₀, map := fun (i : 𝒱.I₀) => CategoryTheory.Over.homMk (r.h₀ i) ⋯ }

theorem AlgebraicGeometry.Scheme.Cover.Hom.toOverFamilyRefinement_id {X : Scheme} {𝒰 : Cover fppfPrecoverage X} : toOverFamilyRefinement (CategoryTheory.PreZeroHypercover.Hom.id 𝒰.toPreZeroHypercover) = CategoryTheory.PresheafOfGroups.FamilyRefinement.refl 𝒰.overFamily

theorem AlgebraicGeometry.Scheme.Cover.Hom.toOverFamilyRefinement_comp {X : Scheme} {𝒰 𝒱 𝒲 : Cover fppfPrecoverage X} (r : 𝒱.Hom 𝒰) (s : 𝒲.Hom 𝒱) : toOverFamilyRefinement (CategoryTheory.PreZeroHypercover.Hom.comp s r) = r.toOverFamilyRefinement.comp s.toOverFamilyRefinement

def AlgebraicGeometry.Scheme.Cover.Hom.pullbackHOne {X : Scheme} {𝒰 𝒱 : Cover fppfPrecoverage X} (G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat) (r : 𝒱.Hom 𝒰) : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily → CategoryTheory.PresheafOfGroups.H1 G 𝒱.overFamily

Pull a relative cover-level H¹ class back along a refinement of fppf covers.

Equations

• AlgebraicGeometry.Scheme.Cover.Hom.pullbackHOne G r = r.toOverFamilyRefinement.pullbackHOne

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.Hom.pullbackHOne_id {X : Scheme} {𝒰 : Cover fppfPrecoverage X} (G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat) (x : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily) : pullbackHOne G (CategoryTheory.PreZeroHypercover.Hom.id 𝒰.toPreZeroHypercover) x = x

theorem AlgebraicGeometry.Scheme.Cover.Hom.pullbackHOne_comp {X : Scheme} {𝒰 𝒱 𝒲 : Cover fppfPrecoverage X} (G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat) (r : 𝒱.Hom 𝒰) (s : 𝒲.Hom 𝒱) (x : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily) : pullbackHOne G (CategoryTheory.PreZeroHypercover.Hom.comp s r) x = pullbackHOne G s (pullbackHOne G r x)

theorem AlgebraicGeometry.Scheme.Cover.Hom.pullbackHOne_eq {X : Scheme} {𝒰 𝒱 : Cover fppfPrecoverage X} (G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat) (r r' : 𝒱.Hom 𝒰) (x : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily) : pullbackHOne G r x = pullbackHOne G r' x

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.Hom.pullbackHOne_one {X : Scheme} {𝒰 𝒱 : Cover fppfPrecoverage X} (G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat) (r : 𝒱.Hom 𝒰) : pullbackHOne G r 1 = 1

structure AlgebraicGeometry.Scheme.FppfHOneRepresentative (X : Scheme) (G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat) : Type (max (max (u + 1) (v + 1)) w)

One cover-level representative of a prospective global fppf H¹ class.

• cover : Cover fppfPrecoverage X

  The fppf covering family on which the cocycle is defined.

• value : CategoryTheory.PresheafOfGroups.H1 G self.cover.overFamily

  Its relative cover-level nonabelian cohomology class.

def AlgebraicGeometry.Scheme.FppfHOneRepresentative.IsEquivalent {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} (a b : X.FppfHOneRepresentative G) : Prop

Two representatives agree if their classes agree after pullback to one genuine common fppf refinement.

Equations

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

theorem AlgebraicGeometry.Scheme.FppfHOneRepresentative.isEquivalent_refl {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} (a : X.FppfHOneRepresentative G) : a.IsEquivalent a

theorem AlgebraicGeometry.Scheme.FppfHOneRepresentative.isEquivalent_symm {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} {a b : X.FppfHOneRepresentative G} (h : a.IsEquivalent b) : b.IsEquivalent a

theorem AlgebraicGeometry.Scheme.FppfHOneRepresentative.isEquivalent_trans {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} {a b c : X.FppfHOneRepresentative G} (hab : a.IsEquivalent b) (hbc : b.IsEquivalent c) : a.IsEquivalent c

theorem AlgebraicGeometry.Scheme.FppfHOneRepresentative.equivalence_isEquivalent {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} : Equivalence IsEquivalent

The common-refinement relation is an equivalence relation, using intersections of actual fppf covers and independence of refinement choices on cover-level H¹.

def AlgebraicGeometry.Scheme.FppfHOne (X : Scheme) (G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat) : Type (max (max (u + 1) (v + 1)) w)

Global nonabelian fppf cohomology in degree one, presented as the filtered-colimit quotient of relative cover-level classes by genuine common refinement. The cover index universe is explicit.

Equations

• X.FppfHOne G = Quot AlgebraicGeometry.Scheme.FppfHOneRepresentative.IsEquivalent

def AlgebraicGeometry.Scheme.FppfHOne.mk {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} (𝒰 : Cover fppfPrecoverage X) (x : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily) : X.FppfHOne G

Send one cover-level class into global fppf H¹.

Equations

• AlgebraicGeometry.Scheme.FppfHOne.mk 𝒰 x = Quot.mk AlgebraicGeometry.Scheme.FppfHOneRepresentative.IsEquivalent { cover := 𝒰, value := x }

def AlgebraicGeometry.Scheme.FppfHOne.identityCover (X : Scheme) : Cover fppfPrecoverage X

The singleton identity cover, constructed directly from the checked fppf-cover theorem for an identity morphism.

Equations

• AlgebraicGeometry.Scheme.FppfHOne.identityCover X = CategoryTheory.Precoverage.ZeroHypercover.singleton (CategoryTheory.CategoryStruct.id X) ⋯

def AlgebraicGeometry.Scheme.FppfHOne.toIdentityCover {X : Scheme} (𝒰 : Cover fppfPrecoverage X) : 𝒰.Hom (identityCover X)

Every fppf cover refines the singleton identity cover.

Equations

• AlgebraicGeometry.Scheme.FppfHOne.toIdentityCover 𝒰 = { s₀ := fun (x : 𝒰.I₀) => PUnit.unit, h₀ := fun (i : 𝒰.I₀) => 𝒰.f i, w₀ := ⋯ }

@[instance_reducible]

instance AlgebraicGeometry.Scheme.FppfHOne.instOne {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} : One (X.FppfHOne G)

The distinguished trivial global fppf class.

Equations

• AlgebraicGeometry.Scheme.FppfHOne.instOne = { one := AlgebraicGeometry.Scheme.FppfHOne.mk (AlgebraicGeometry.Scheme.FppfHOne.identityCover X) 1 }

@[simp]

theorem AlgebraicGeometry.Scheme.FppfHOne.mk_one {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} (𝒰 : Cover fppfPrecoverage X) : mk 𝒰 1 = 1

The trivial cover-level class maps to the distinguished global class on every fppf cover.

theorem AlgebraicGeometry.Scheme.FppfHOne.class_pullback {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} (𝒰 𝒱 : Cover fppfPrecoverage X) (r : 𝒱.Hom 𝒰) (x : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily) : mk 𝒱 (Cover.Hom.pullbackHOne G r x) = mk 𝒰 x

A class and its pullback to a refinement define the same global fppf class.

theorem AlgebraicGeometry.Scheme.FppfHOne.class_eq_iff {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} (𝒰 𝒱 : Cover fppfPrecoverage X) (x : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily) (y : CategoryTheory.PresheafOfGroups.H1 G 𝒱.overFamily) : mk 𝒰 x = mk 𝒱 y ↔ ∃ (𝒲 : Cover fppfPrecoverage X) (r : 𝒲.Hom 𝒰) (s : 𝒲.Hom 𝒱), Cover.Hom.pullbackHOne G r x = Cover.Hom.pullbackHOne G s y

Two cover-level classes have the same global class exactly when they agree after one common fppf refinement.

def AlgebraicGeometry.Scheme.FppfHOne.lift {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} {Y : Sort u_1} (f : (𝒰 : Cover fppfPrecoverage X) → CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily → Y) (compatible : ∀ (𝒰 𝒱 : Cover fppfPrecoverage X) (r : 𝒱.Hom 𝒰) (x : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily), f 𝒱 (Cover.Hom.pullbackHOne G r x) = f 𝒰 x) : X.FppfHOne G → Y

The eliminator expressing the colimit universal property at the level of types: a compatible family of maps out of all cover-level H¹ types descends to global fppf H¹.

Equations

• AlgebraicGeometry.Scheme.FppfHOne.lift f compatible = Quot.lift (fun (a : X.FppfHOneRepresentative G) => f a.cover a.value) ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.FppfHOne.lift_mk {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} {Y : Sort u_1} (f : (𝒰 : Cover fppfPrecoverage X) → CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily → Y) (compatible : ∀ (𝒰 𝒱 : Cover fppfPrecoverage X) (r : 𝒱.Hom 𝒰) (x : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily), f 𝒱 (Cover.Hom.pullbackHOne G r x) = f 𝒰 x) (𝒰 : Cover fppfPrecoverage X) (x : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily) : lift f compatible (mk 𝒰 x) = f 𝒰 x

theorem AlgebraicGeometry.Scheme.FppfHOne.funext {X : Scheme} {G : CategoryTheory.Functor (CategoryTheory.Over X)ᵒᵖ GrpCat} {Y : Sort u_1} {f g : X.FppfHOne G → Y} (h : ∀ (𝒰 : Cover fppfPrecoverage X) (x : CategoryTheory.PresheafOfGroups.H1 G 𝒰.overFamily), f (mk 𝒰 x) = g (mk 𝒰 x)) : f = g

Maps out of global fppf H¹ are determined by all cover-level classes.

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.commPointPresheaf {S : Scheme} (G : FiniteFlatCommGroupScheme S) : CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ CommGrpCat

The presheaf of commutative groups on Over S represented by a finite-flat commutative group scheme. Its value on T ⟶ S is the actual commutative group of S-morphisms T ⟶ G.

Equations

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

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.pointPresheaf {S : Scheme} (G : FiniteFlatCommGroupScheme S) : CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ GrpCat

The representable point presheaf, forgotten from commutative groups to groups.

Equations

• G.pointPresheaf = G.commPointPresheaf.comp (CategoryTheory.forget₂ CommGrpCat GrpCat)

@[simp]

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.pointPresheaf_obj {S : Scheme} (G : FiniteFlatCommGroupScheme S) (T : CategoryTheory.Over S) : G.pointPresheaf.obj (Opposite.op T) = GrpCat.of (G.Point T)

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.pointPresheaf_isFppfSheaf {S : Scheme} (G : FiniteFlatCommGroupScheme S) : CategoryTheory.Presieve.IsSheaf (Scheme.fppfTopology.over S) (G.pointPresheaf.comp (CategoryTheory.forget GrpCat))

The underlying type-valued point presheaf of a finite-flat group scheme is an fppf sheaf on the slice site. This records that the coefficient system used below is genuinely representable, not an arbitrary family of groups.

@[reducible, inline]

abbrev AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfHOne {S : Scheme} (G : FiniteFlatCommGroupScheme S) : Type (max (u + 1) (v + 1))

Global fppf H¹ of the representable point presheaf of a finite-flat commutative group scheme. This is a pointed type; its canonical commutative group structure is separate work.

Equations

• G.FppfHOne = S.FppfHOne G.pointPresheaf

noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.fppfHOneClass {S : Scheme} (G : FiniteFlatCommGroupScheme S) (𝒰 : Scheme.Cover Scheme.fppfPrecoverage S) (x : CategoryTheory.PresheafOfGroups.H1 G.pointPresheaf 𝒰.overFamily) : G.FppfHOne

Send an actual relative cover-level class for a finite-flat group scheme to global fppf H¹. This is the representable downstream consumer of the globalization interface.

Equations

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

theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.fppfHOneClass_pullback {S : Scheme} (G : FiniteFlatCommGroupScheme S) (𝒰 𝒱 : Scheme.Cover Scheme.fppfPrecoverage S) (r : 𝒱.Hom 𝒰) (x : CategoryTheory.PresheafOfGroups.H1 G.pointPresheaf 𝒰.overFamily) : G.fppfHOneClass 𝒱 (Scheme.Cover.Hom.pullbackHOne G.pointPresheaf r x) = G.fppfHOneClass 𝒰 x

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