Documentation

Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

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 #

References #

A zero cochain consists of a family of sections.

Equations
Instances For
    structure CategoryTheory.PresheafOfGroups.OneCochain {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ Grp) {I : Type w'} (U : IC) :
    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.)

    Instances For
      @[simp]
      theorem CategoryTheory.PresheafOfGroups.OneCochain.ev_precomp {C : Type u} [CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ Grp} {I : Type w'} {U : IC} (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)
      Equations
      @[simp]
      theorem CategoryTheory.PresheafOfGroups.OneCochain.one_ev {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ Grp) {I : Type w'} (U : IC) (i : I) (j : I) {T : C} (a : T U i) (b : T U j) :
      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 : IC} (γ₁ : 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
      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 : IC} (γ : 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)⁻¹
      Equations
      • CategoryTheory.PresheafOfGroups.OneCochain.instGroup = Group.mk

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

      Instances For
        theorem CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans {C : Type u} [CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ Grp} {I : Type w'} {U : IC} (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
        @[simp]
        theorem CategoryTheory.PresheafOfGroups.OneCocycle.ev_refl {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ Grp) {I : Type w'} (U : IC) (γ : 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 : IC) (γ : 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)⁻¹

        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
          Instances For
            theorem CategoryTheory.PresheafOfGroups.OneCocycle.equivalence_isCohomologous {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ Grp) {I : Type w'} (U : IC) :
            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 : IC) :
            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
            Instances For

              The cohomology class of a 1-cocycle.

              Equations
              • γ.class = Quot.mk CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous γ
              Instances For