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, andx₃
is a global section ofG₃
which can be locally lifted to a section ofG₂
, there is an associated canonical cohomology class ofG₁
which is trivial iffx₃
can be lifted to a global section ofG₂
. (This should hold more generally ifG₂
is a sheaf of sets on whichG₁
acts freely, andG₃
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 schemeX
andQ
is the underlying sheaf of a quasi-coherent sheaf, thenM(U) ⟶ N(U)
is surjective for any affine openU
. - take the colimit of
OneCohomology G U
over all covering familiesU
(for a Grothendieck topology)
References #
- [J. Frenkel, Cohomologie non abélienne et espaces fibrés][frenkel1957]
A zero cochain consists of a family of sections.
Equations
- CategoryTheory.PresheafOfGroups.ZeroCochain G U = ((i : I) → ↑(G.obj (Opposite.op (U i))))
Instances For
Equations
- CategoryTheory.PresheafOfGroups.instGroupZeroCochain G U = Pi.group
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 (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), (G.map φ.op) (self.ev i j a b) = self.ev i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b)
Instances For
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 := ⋯ } }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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 (Opposite.op 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)
Instances For
Equations
- CategoryTheory.PresheafOfGroups.OneCocycle.instOne G U = { one := { toOneCochain := 1, ev_trans := ⋯ } }
The assertion that two cochains in OneCochain G U
are cohomologous via
an explicit zero-cochain.
Equations
Instances For
The cohomology (equivalence) relation on 1-cocycles.
Equations
- γ₁.IsCohomologous γ₂ = ∃ (α : CategoryTheory.PresheafOfGroups.ZeroCochain G U), CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₁.toOneCochain γ₂.toOneCochain α
Instances For
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
Instances For
The cohomology class of a 1-cocycle.
Instances For
Equations
- CategoryTheory.PresheafOfGroups.instOneH1 = { one := CategoryTheory.PresheafOfGroups.OneCocycle.class 1 }