The cohomology of a sheaf of groups in degree 1

In this file, we shall define the cohomology in degree 1 of a sheaf of groups (TODO).

Currently, given a presheaf of groups G : Cᵒᵖ ⥤ GrpCat and a family of objects U : I → C, we define 1-cochains/1-cocycles/H^1 with values in G over U. (This definition neither requires the assumption that G is a sheaf, nor that U covers the terminal object.) As we do not assume that G is a presheaf of abelian groups, this cohomology theory is only defined in low degrees; in the abelian case, it would be a particular case of Čech cohomology (TODO).

TODO

• show that if 1 ⟶ G₁ ⟶ G₂ ⟶ G₃ ⟶ 1 is a short exact sequence of sheaves of groups, and x₃ is a global section of G₃ which can be locally lifted to a section of G₂, there is an associated canonical cohomology class of G₁ which is trivial iff x₃ can be lifted to a global section of G₂. (This should hold more generally if G₂ is a sheaf of sets on which G₁ acts freely, and G₃ is the quotient sheaf.)
• deduce a similar result for abelian sheaves
• when the notion of quasi-coherent sheaves on schemes is defined, show that if 0 ⟶ Q ⟶ M ⟶ N ⟶ 0 is an exact sequence of abelian sheaves over a scheme X and Q is the underlying sheaf of a quasi-coherent sheaf, then M(U) ⟶ N(U) is surjective for any affine open U.
• take the colimit of OneCohomology G U over all covering families U (for a Grothendieck topology)

References

• [J. Frenkel, Cohomologie non abélienne et espaces fibrés][frenkel1957]

def CategoryTheory.PresheafOfGroups.ZeroCochain {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) : Type (max w w')

A zero cochain consists of a family of sections.

instance CategoryTheory.PresheafOfGroups.instGroupZeroCochain {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) : Group (ZeroCochain G U)

@[simp]

theorem CategoryTheory.PresheafOfGroups.Cochain₀.one_apply {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) (i : I) : 1 i = 1

@[simp]

theorem CategoryTheory.PresheafOfGroups.Cochain₀.inv_apply {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) (γ : ZeroCochain G U) (i : I) : γ⁻¹ i = (γ i)⁻¹

@[simp]

theorem CategoryTheory.PresheafOfGroups.Cochain₀.mul_apply {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) (γ₁ γ₂ : ZeroCochain G U) (i : I) : (γ₁ * γ₂) i = γ₁ i * γ₂ i

structure CategoryTheory.PresheafOfGroups.OneCochain {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) : Type (max (max (max u v) w) w')

A 1-cochain of a presheaf of groups G : Cᵒᵖ ⥤ GrpCat on a family U : I → C of objects consists of the data of an element in G.obj (Opposite.op T) whenever we have elements i and j in I and maps a : T ⟶ U i and b : T ⟶ U j, and it must satisfy a compatibility with respect to precomposition. (When the binary product of U i and U j exists, this data for all T, a and b corresponds to the data of a section of G on this product.)

• ev (i j : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) : ↑(G.obj (Opposite.op T))

  the data involved in a 1-cochain

• ev_precomp (i j : I) ⦃T T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i) (b : T' ⟶ U j) : (ConcreteCategory.hom (G.map φ.op)) (self.ev i j a b) = self.ev i j (CategoryStruct.comp φ a) (CategoryStruct.comp φ b)

theorem CategoryTheory.PresheafOfGroups.OneCochain.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} {x y : OneCochain G U} : x = y ↔ x.ev = y.ev

theorem CategoryTheory.PresheafOfGroups.OneCochain.ext {C : Type u} {inst✝ : Category.{v, u} C} {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} {x y : OneCochain G U} (ev : x.ev = y.ev) : x = y

instance CategoryTheory.PresheafOfGroups.OneCochain.instOne {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) : One (OneCochain G U)

@[simp]

theorem CategoryTheory.PresheafOfGroups.OneCochain.one_ev {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) (i j : I) {T : C} (a : T ⟶ U i) (b : T ⟶ U j) : ev 1 i j a b = 1

instance CategoryTheory.PresheafOfGroups.OneCochain.instMul {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} : Mul (OneCochain G U)

@[simp]

theorem CategoryTheory.PresheafOfGroups.OneCochain.mul_ev {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} (γ₁ γ₂ : OneCochain G U) (i j : I) {T : C} (a : T ⟶ U i) (b : T ⟶ U j) : (γ₁ * γ₂).ev i j a b = γ₁.ev i j a b * γ₂.ev i j a b

instance CategoryTheory.PresheafOfGroups.OneCochain.instInv {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} : Inv (OneCochain G U)

@[simp]

theorem CategoryTheory.PresheafOfGroups.OneCochain.inv_ev {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} (γ : OneCochain G U) (i j : I) {T : C} (a : T ⟶ U i) (b : T ⟶ U j) : γ⁻¹.ev i j a b = (γ.ev i j a b)⁻¹

instance CategoryTheory.PresheafOfGroups.OneCochain.instGroup {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} : Group (OneCochain G U)

structure CategoryTheory.PresheafOfGroups.OneCocycle {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) extends CategoryTheory.PresheafOfGroups.OneCochain G U : Type (max (max (max u v) w) w')

A 1-cocycle is a 1-cochain which satisfies the cocycle condition.

• ev (i j : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) : ↑(G.obj (Opposite.op T))
• ev_precomp (i j : I) ⦃T T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i) (b : T' ⟶ U j) : (ConcreteCategory.hom (G.map φ.op)) (self.ev i j a b) = self.ev i j (CategoryStruct.comp φ a) (CategoryStruct.comp φ b)
• ev_trans (i j k : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) (c : T ⟶ U k) : self.ev i j a b * self.ev j k b c = self.ev i k a c

instance CategoryTheory.PresheafOfGroups.OneCocycle.instOne {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) : One (OneCocycle G U)

@[simp]

theorem CategoryTheory.PresheafOfGroups.OneCocycle.one_toOneCochain {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) : toOneCochain 1 = 1

@[simp]

theorem CategoryTheory.PresheafOfGroups.OneCocycle.ev_refl {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) (γ : OneCocycle G U) (i : I) ⦃T : C⦄ (a : T ⟶ U i) : γ.ev i i a a = 1

theorem CategoryTheory.PresheafOfGroups.OneCocycle.ev_symm {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) (γ : OneCocycle G U) (i j : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j) : γ.ev i j a b = (γ.ev j i b a)⁻¹

def CategoryTheory.PresheafOfGroups.OneCohomologyRelation {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} (γ₁ γ₂ : OneCochain G U) (α : ZeroCochain G U) : Prop

The assertion that two cochains in OneCochain G U are cohomologous via an explicit zero-cochain.

theorem CategoryTheory.PresheafOfGroups.OneCohomologyRelation.refl {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} (γ : OneCochain G U) : OneCohomologyRelation γ γ 1

theorem CategoryTheory.PresheafOfGroups.OneCohomologyRelation.symm {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} {γ₁ γ₂ : OneCochain G U} {α : ZeroCochain G U} (h : OneCohomologyRelation γ₁ γ₂ α) : OneCohomologyRelation γ₂ γ₁ α⁻¹

theorem CategoryTheory.PresheafOfGroups.OneCohomologyRelation.trans {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} {γ₁ γ₂ γ₃ : OneCochain G U} {α β : ZeroCochain G U} (h₁₂ : OneCohomologyRelation γ₁ γ₂ α) (h₂₃ : OneCohomologyRelation γ₂ γ₃ β) : OneCohomologyRelation γ₁ γ₃ (β * α)

def CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} (γ₁ γ₂ : OneCocycle G U) : Prop

The cohomology (equivalence) relation on 1-cocycles.

theorem CategoryTheory.PresheafOfGroups.OneCocycle.equivalence_isCohomologous {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) : _root_.Equivalence IsCohomologous

def CategoryTheory.PresheafOfGroups.H1 {C : Type u} [Category.{v, u} C] (G : Functor Cᵒᵖ GrpCat) {I : Type w'} (U : I → C) : Type (max (max (max u v) w) w')

The cohomology in degree 1 of a presheaf of groups G : Cᵒᵖ ⥤ GrpCat on a family of objects U : I → C.

def CategoryTheory.PresheafOfGroups.OneCocycle.class {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} (γ : OneCocycle G U) : H1 G U

The cohomology class of a 1-cocycle.

instance CategoryTheory.PresheafOfGroups.instOneH1 {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} : One (H1 G U)

theorem CategoryTheory.PresheafOfGroups.OneCocycle.class_eq_iff {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} (γ₁ γ₂ : OneCocycle G U) : γ₁.class = γ₂.class ↔ γ₁.IsCohomologous γ₂

theorem CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous.class_eq {C : Type u} [Category.{v, u} C] {G : Functor Cᵒᵖ GrpCat} {I : Type w'} {U : I → C} {γ₁ γ₂ : OneCocycle G U} (h : γ₁.IsCohomologous γ₂) : γ₁.class = γ₂.class