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ᵒᵖ ⥤ Grp 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} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ Grp) {I : Type w'} (U : I → C) : Type (max w w')

A zero cochain consists of a family of sections.

Equations

• CategoryTheory.PresheafOfGroups.ZeroCochain G U = ((i : I) → ↑(G.obj { unop := U i }))

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

Equations

• CategoryTheory.PresheafOfGroups.instGroupZeroCochain G U = Pi.group

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

A 1-cochain of a presheaf of groups G : Cᵒᵖ ⥤ Grp 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⦄ → (T ⟶ U i) → (T ⟶ U j) → ↑(G.obj { unop := 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), (G.map φ.op) (self.ev i j a b) = self.ev i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b)

@[simp]

theorem CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp {C : Type u} [CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ Grp} {I : Type w'} {U : I → C} (self : CategoryTheory.PresheafOfGroups.OneCochain G U) (i : I) (j : I) ⦃T : C⦄ ⦃T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i) (b : T' ⟶ U j) : (G.map φ.op) (self.ev i j a b) = self.ev i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b)

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

Equations

• CategoryTheory.PresheafOfGroups.OneCochain.instOne G U = { one := { ev := fun (x x_1 : I) (x_2 : C) (x : x_2 ⟶ U x) (x : x_2 ⟶ U x_1) => 1, ev_precomp := ⋯ } }

@[simp]

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

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

Equations

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

@[simp]

theorem CategoryTheory.PresheafOfGroups.OneCochain.mul_ev {C : Type u} [CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ Grp} {I : Type w'} {U : I → C} (γ₁ : CategoryTheory.PresheafOfGroups.OneCochain G U) (γ₂ : CategoryTheory.PresheafOfGroups.OneCochain G U) (i : 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} [CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ Grp} {I : Type w'} {U : I → C} : Inv (CategoryTheory.PresheafOfGroups.OneCochain G U)

Equations

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

@[simp]

theorem CategoryTheory.PresheafOfGroups.OneCochain.inv_ev {C : Type u} [CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ Grp} {I : Type w'} {U : I → C} (γ : CategoryTheory.PresheafOfGroups.OneCochain G U) (i : 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} [CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ Grp} {I : Type w'} {U : I → C} : Group (CategoryTheory.PresheafOfGroups.OneCochain G U)

Equations

• CategoryTheory.PresheafOfGroups.OneCochain.instGroup = Group.mk ⋯

structure CategoryTheory.PresheafOfGroups.OneCocycle {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ Grp) {I : Type w'} (U : I → C) extends CategoryTheory.PresheafOfGroups.OneCochain : 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⦄ → (T ⟶ U i) → (T ⟶ U j) → ↑(G.obj { unop := T })
• ev_precomp : ∀ (i j : I) ⦃T T' : C⦄ (φ : T ⟶ T') (a : T' ⟶ U i) (b : T' ⟶ U j), (G.map φ.op) (self.ev i j a b) = self.ev i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.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

theorem CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans {C : Type u} [CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ Grp} {I : Type w'} {U : I → C} (self : CategoryTheory.PresheafOfGroups.OneCocycle G U) (i : I) (j : I) (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} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ Grp) {I : Type w'} (U : I → C) : One (CategoryTheory.PresheafOfGroups.OneCocycle G U)

Equations

• CategoryTheory.PresheafOfGroups.OneCocycle.instOne G U = { one := { toOneCochain := 1, ev_trans := ⋯ } }

@[simp]

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

@[simp]

theorem CategoryTheory.PresheafOfGroups.OneCocycle.ev_refl {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ Grp) {I : Type w'} (U : I → C) (γ : CategoryTheory.PresheafOfGroups.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} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ Grp) {I : Type w'} (U : I → C) (γ : CategoryTheory.PresheafOfGroups.OneCocycle G U) (i : 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} [CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ Grp} {I : Type w'} {U : I → C} (γ₁ : CategoryTheory.PresheafOfGroups.OneCochain G U) (γ₂ : CategoryTheory.PresheafOfGroups.OneCochain G U) (α : CategoryTheory.PresheafOfGroups.ZeroCochain G U) : Prop

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

Equations

• CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₁ γ₂ α = ∀ (i j : I) ⦃T : C⦄ (a : T ⟶ U i) (b : T ⟶ U j), (G.map a.op) (α i) * γ₁.ev i j a b = γ₂.ev i j a b * (G.map b.op) (α j)

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

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

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

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

The cohomology (equivalence) relation on 1-cocycles.

Equations

• γ₁.IsCohomologous γ₂ = ∃ (α : CategoryTheory.PresheafOfGroups.ZeroCochain G U), CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₁.toOneCochain γ₂.toOneCochain α

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

def CategoryTheory.PresheafOfGroups.H1 {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ Grp) {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ᵒᵖ ⥤ Grp on a family of objects U : I → C.

Equations

• CategoryTheory.PresheafOfGroups.H1 G U = Quot CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous

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

The cohomology class of a 1-cocycle.

Equations

• γ.class = Quot.mk CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous γ

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

Equations

• CategoryTheory.PresheafOfGroups.instOneH1 = { one := CategoryTheory.PresheafOfGroups.OneCocycle.class 1 }

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

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