First cohomology as a quotient of local sections

For a Mayer–Vietoris square in a site, the connecting map sends a section on the intersection to a first-cohomology class on the covered object. Its kernel consists exactly of differences of restrictions from the two covering objects. If first cohomology vanishes on those two objects, this gives an additive equivalence from sections on the intersection modulo those differences to first cohomology.

For two open subsets of a space this computes first cohomology from a two-member cover. Only vanishing in degree one on the two members is needed; neither vanishing on the intersection nor acyclicity in higher degrees is assumed. The class of a section is characterized by the Mayer–Vietoris connecting homomorphism, fixing its sign.

The construction uses Mathlib's Mayer–Vietoris sequence and first isomorphism theorem for abelian groups, and cohomologyPresheafZeroIso to identify the degree-zero terms and their restriction maps with sections.

Use TauCeti.CategoryTheory.mayerVietorisSectionsQuotientEquiv S F h₂ h₃ for the quotient comparison, where S is the square and F is the coefficient sheaf. Opening TauCeti.CategoryTheory makes the unqualified names available.

References

• R. Hartshorne, Algebraic Geometry, Chapter III, §4 (Čech cohomology).

def TauCeti.CategoryTheory.mayerVietorisSectionsDifference {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) : ↑(F.obj.obj (Opposite.op S.X₂)) × ↑(F.obj.obj (Opposite.op S.X₃)) →+ ↑(F.obj.obj (Opposite.op S.X₁))

The difference of the restrictions of sections from the two covering objects to their intersection.

@[simp]

theorem TauCeti.CategoryTheory.mayerVietorisSectionsDifference_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) (s₂ : ↑(F.obj.obj (Opposite.op S.X₂))) (s₃ : ↑(F.obj.obj (Opposite.op S.X₃))) : (mayerVietorisSectionsDifference S F) (s₂, s₃) = (CategoryTheory.ConcreteCategory.hom (F.obj.map S.f₁₂.op)) s₂ - (CategoryTheory.ConcreteCategory.hom (F.obj.map S.f₁₃.op)) s₃

noncomputable def TauCeti.CategoryTheory.mayerVietorisSectionClass {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) : ↑(F.obj.obj (Opposite.op S.X₁)) →+ ↑(F.H' 1 S.X₄)

The first-cohomology class of a section on the intersection, with the sign of Mathlib's Mayer–Vietoris connecting homomorphism.

@[simp]

theorem TauCeti.CategoryTheory.mayerVietorisSectionClass_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) (s : ↑(F.obj.obj (Opposite.op S.X₁))) : (mayerVietorisSectionClass S F) s = (CategoryTheory.ConcreteCategory.hom (S.δ F 0 1 ⋯)) ((cohomologyZeroSectionsEquiv F S.X₁).symm s)

theorem TauCeti.CategoryTheory.mayerVietorisSectionClass_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) {G : CategoryTheory.Sheaf J AddCommGrpCat} (f : F ⟶ G) (s : ↑(F.obj.obj (Opposite.op S.X₁))) : (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Sheaf.cohomologyPresheafFunctor J 1).map f).app (Opposite.op S.X₄))) ((mayerVietorisSectionClass S F) s) = (mayerVietorisSectionClass S G) ((CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S.X₁))) s)

The connecting class of an overlap section is natural in the coefficient sheaf.

@[simp]

theorem TauCeti.CategoryTheory.mayerVietorisSectionClass_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) (s : ↑(F.obj.obj (Opposite.op S.X₁))) : (mayerVietorisSectionClass S F) s = 0 ↔ ∃ (s₂ : ↑(F.obj.obj (Opposite.op S.X₂))) (s₃ : ↑(F.obj.obj (Opposite.op S.X₃))), (CategoryTheory.ConcreteCategory.hom (F.obj.map S.f₁₂.op)) s₂ - (CategoryTheory.ConcreteCategory.hom (F.obj.map S.f₁₃.op)) s₃ = s

A section on the intersection has zero connecting class exactly when it is a difference of restrictions of sections from the two covering objects. No acyclicity hypothesis is needed for this characterization.

theorem TauCeti.CategoryTheory.range_mayerVietorisSectionsDifference {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) : (mayerVietorisSectionsDifference S F).range = (mayerVietorisSectionClass S F).ker

Differences of local restrictions are exactly the kernel of the connecting class map.

theorem TauCeti.CategoryTheory.mayerVietorisSectionClass_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) (h₂ : Subsingleton ↑(F.H' 1 S.X₂)) (h₃ : Subsingleton ↑(F.H' 1 S.X₃)) : Function.Surjective ⇑(mayerVietorisSectionClass S F)

If first cohomology vanishes on both covering objects, every first-cohomology class on the covered object comes from a section on the intersection.

noncomputable def TauCeti.CategoryTheory.mayerVietorisSectionsQuotientEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) (h₂ : Subsingleton ↑(F.H' 1 S.X₂)) (h₃ : Subsingleton ↑(F.H' 1 S.X₃)) : ↑(F.obj.obj (Opposite.op S.X₁)) ⧸ (mayerVietorisSectionsDifference S F).range ≃+ ↑(F.H' 1 S.X₄)

For a two-member cover whose members have vanishing first cohomology, first cohomology is sections on the intersection modulo differences of local sections.

@[simp]

theorem TauCeti.CategoryTheory.mayerVietorisSectionsQuotientEquiv_mk {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare) (F : CategoryTheory.Sheaf J AddCommGrpCat) (h₂ : Subsingleton ↑(F.H' 1 S.X₂)) (h₃ : Subsingleton ↑(F.H' 1 S.X₃)) (s : ↑(F.obj.obj (Opposite.op S.X₁))) : (mayerVietorisSectionsQuotientEquiv S F h₂ h₃) ↑s = (mayerVietorisSectionClass S F) s

The quotient comparison sends the class of a section to its connecting class.