Relative sheaf cohomology of a morphism of a site

Let i : U ⟶ V be a morphism in a site (C, J), and write ℤ_U, ℤ_V for the free abelian sheaves generated by U and V (TauCeti.CategoryTheory.freeYonedaSheafFunctor). The relative free sheaf ℤ_{V,U} is the cokernel of the induced map ℤ_U ⟶ ℤ_V. Morphisms out of it are the sections over V whose restriction along i vanishes, and the relative cohomology of an abelian sheaf F is defined as Hⁿ(V, U; F) = Extⁿ(ℤ_{V,U}, F).

When i is a monomorphism, 0 ⟶ ℤ_U ⟶ ℤ_V ⟶ ℤ_{V,U} ⟶ 0 is short exact, and the contravariant long exact Ext sequence becomes the long exact sequence of the pair

⋯ ⟶ Hⁿ(V, U; F) ⟶ Hⁿ(V, F) ⟶ Hⁿ(U, F) ⟶ Hⁿ⁺¹(V, U; F) ⟶ ⋯.

Here Hⁿ(V, F) is Mathlib's CategoryTheory.Sheaf.H', which is by definition Ext out of the free abelian sheaf on V (CategoryTheory.Sheaf.H'AddEquivExt), and the middle map is the restriction map of the cohomology presheaf, which is precomposition with ℤ_U ⟶ ℤ_V (CategoryTheory.Sheaf.cohomologyPresheaf_map_apply).

For a triple i : U ⟶ U', j : U' ⟶ V with j a monomorphism, the maps of pairs (U', U) ⟶ (V, U) ⟶ (V, U') induce a short exact sequence 0 ⟶ ℤ_{U',U} ⟶ ℤ_{V,U} ⟶ ℤ_{V,U'} ⟶ 0, and its long exact Ext sequence is the long exact sequence of the triple

⋯ ⟶ Hⁿ(V, U'; F) ⟶ Hⁿ(V, U; F) ⟶ Hⁿ(U', U; F) ⟶ Hⁿ⁺¹(V, U'; F) ⟶ ⋯.

For the site of open subsets of a topological space, an open W and a closed subset S, the morphism W ∖ S ⟶ W gives the cohomology of F on W with supports in S; this is developed in TauCeti.Topology.Sheaves.SupportedCohomology.

Main declarations

• TauCeti.CategoryTheory.relativeFreeYonedaSheaf J i: the relative free sheaf ℤ_{V,U};
• TauCeti.CategoryTheory.relativeFreeYonedaSheafHomEquiv: morphisms ℤ_{V,U} ⟶ F are the sections of F over V restricting to zero along i;
• TauCeti.CategoryTheory.relativeFreeYonedaSequence_shortExact: the sequence 0 ⟶ ℤ_U ⟶ ℤ_V ⟶ ℤ_{V,U} ⟶ 0 is short exact for a monomorphism i;
• CategoryTheory.Sheaf.relativeH' F i n: the relative cohomology Hⁿ(V, U; F);
• CategoryTheory.Sheaf.relativeH'.toH' and CategoryTheory.Sheaf.relativeH'.δ: the maps of the long exact sequence of the pair, whose exactness is relativeH'.exact_toH'_cohomologyPresheaf_map, relativeH'.exact_cohomologyPresheaf_map_δ and relativeH'.exact_δ_toH';
• CategoryTheory.Sheaf.relativeH'.zeroEquiv: H⁰(V, U; F) is the group of sections over V restricting to zero along i, naturally in F (relativeH'.coe_zeroEquiv_naturality_right);
• CategoryTheory.Sheaf.relativeH'.subsingleton_one and relativeH'.subsingleton_add_two: vanishing of relative cohomology from vanishing of absolute cohomology.
• TauCeti.CategoryTheory.relativeFreeYonedaSheafMap: the map ℤ_{V',U'} ⟶ ℤ_{V,U} induced by a commutative square from i' : U' ⟶ V' to i : U ⟶ V, and TauCeti.CategoryTheory.isIso_relativeFreeYonedaSheafMap_iff, its Yoneda criterion for being an isomorphism in terms of sections restricting to zero;
• CategoryTheory.Sheaf.relativeH'.map and CategoryTheory.Sheaf.relativeH'.mapAddEquiv: the induced map Hⁿ(V, U; F) ⟶ Hⁿ(V', U'; F), and the equivalence it gives when the map of relative free sheaves is an isomorphism;
• TauCeti.CategoryTheory.relativeFreeYonedaTripleSequence_shortExact: the sequence 0 ⟶ ℤ_{U',U} ⟶ ℤ_{V,U} ⟶ ℤ_{V,U'} ⟶ 0 of a triple U ⟶ U' ⟶ V is short exact when U' ⟶ V is a monomorphism;
• CategoryTheory.Sheaf.relativeH'.tripleδ: the connecting map Hⁿ(U', U; F) ⟶ Hⁿ⁺¹(V, U'; F) of the long exact sequence of the triple, whose exactness is relativeH'.exact_map_map, relativeH'.exact_map_tripleδ and relativeH'.exact_tripleδ_map.

References

• A. Grothendieck, Local cohomology, Lecture Notes in Mathematics 41, §1.
• M. Kashiwara and P. Schapira, Sheaves on Manifolds, §2.6.

@[reducible, inline]

noncomputable abbrev TauCeti.CategoryTheory.relativeFreeYonedaSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U V : C} (i : U ⟶ V) : CategoryTheory.Sheaf J AddCommGrpCat

The free abelian sheaf on V relative to U: the cokernel of the map ℤ_U ⟶ ℤ_V of free abelian sheaves induced by i : U ⟶ V.

noncomputable def TauCeti.CategoryTheory.relativeFreeYonedaSheafHomEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U V : C} (i : U ⟶ V) (F : CategoryTheory.Sheaf J AddCommGrpCat) : (relativeFreeYonedaSheaf J i ⟶ F) ≃+ ↥(AddCommGrpCat.Hom.hom (F.obj.map i.op)).ker

Morphisms from the relative free sheaf of i : U ⟶ V to an abelian sheaf F are additively equivalent to the sections of F over V whose restriction along i vanishes.

@[simp]

theorem TauCeti.CategoryTheory.coe_relativeFreeYonedaSheafHomEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U V : C} (i : U ⟶ V) (F : CategoryTheory.Sheaf J AddCommGrpCat) (g : relativeFreeYonedaSheaf J i ⟶ F) : ↑((relativeFreeYonedaSheafHomEquiv J i F) g) = (freeYonedaSheafSectionsEquiv J V F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((freeYonedaSheafFunctor J).map i)) g)

@[simp]

theorem TauCeti.CategoryTheory.cokernel_π_comp_relativeFreeYonedaSheafHomEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U V : C} (i : U ⟶ V) (F : CategoryTheory.Sheaf J AddCommGrpCat) (s : ↥(AddCommGrpCat.Hom.hom (F.obj.map i.op)).ker) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((freeYonedaSheafFunctor J).map i)) ((relativeFreeYonedaSheafHomEquiv J i F).symm s) = (freeYonedaSheafSectionsEquiv J V F).symm ↑s

theorem TauCeti.CategoryTheory.relativeFreeYonedaSheafHomEquiv_naturality_right {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U V : C} (i : U ⟶ V) {F G : CategoryTheory.Sheaf J AddCommGrpCat} (g : relativeFreeYonedaSheaf J i ⟶ F) (f : F ⟶ G) : ↑((relativeFreeYonedaSheafHomEquiv J i G) (CategoryTheory.CategoryStruct.comp g f)) = (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op V))) ↑((relativeFreeYonedaSheafHomEquiv J i F) g)

The equivalence relativeFreeYonedaSheafHomEquiv is natural in the coefficient sheaf.

@[reducible, inline]

noncomputable abbrev TauCeti.CategoryTheory.relativeFreeYonedaSequence {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U V : C} (i : U ⟶ V) : CategoryTheory.ShortComplex (CategoryTheory.Sheaf J AddCommGrpCat)

The sequence ℤ_U ⟶ ℤ_V ⟶ ℤ_{V,U} of free abelian sheaves attached to i : U ⟶ V.

theorem TauCeti.CategoryTheory.relativeFreeYonedaSequence_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U V : C} (i : U ⟶ V) [CategoryTheory.Mono i] : (relativeFreeYonedaSequence J i).ShortExact

For a monomorphism i : U ⟶ V, the sequence 0 ⟶ ℤ_U ⟶ ℤ_V ⟶ ℤ_{V,U} ⟶ 0 is short exact.

theorem TauCeti.CategoryTheory.isZero_relativeFreeYonedaSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U V : C} (i : U ⟶ V) [CategoryTheory.IsIso i] : CategoryTheory.Limits.IsZero (relativeFreeYonedaSheaf J i)

If i is an isomorphism, the relative free sheaf of i is zero.

noncomputable def TauCeti.CategoryTheory.relativeFreeYonedaSheafMap {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U' V' U V : C} (i' : U' ⟶ V') (i : U ⟶ V) (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryTheory.CategoryStruct.comp i' b = CategoryTheory.CategoryStruct.comp a i) : relativeFreeYonedaSheaf J i' ⟶ relativeFreeYonedaSheaf J i

The map of relative free sheaves ℤ_{V',U'} ⟶ ℤ_{V,U} induced by a commutative square i' ≫ b = a ≫ i from i' : U' ⟶ V' to i : U ⟶ V.

@[simp]

theorem TauCeti.CategoryTheory.cokernel_π_relativeFreeYonedaSheafMap {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U' V' U V : C} (i' : U' ⟶ V') (i : U ⟶ V) (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryTheory.CategoryStruct.comp i' b = CategoryTheory.CategoryStruct.comp a i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((freeYonedaSheafFunctor J).map i')) (relativeFreeYonedaSheafMap J i' i a b w) = CategoryTheory.CategoryStruct.comp ((freeYonedaSheafFunctor J).map b) (CategoryTheory.Limits.cokernel.π ((freeYonedaSheafFunctor J).map i))

@[simp]

theorem TauCeti.CategoryTheory.cokernel_π_relativeFreeYonedaSheafMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U' V' U V : C} (i' : U' ⟶ V') (i : U ⟶ V) (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryTheory.CategoryStruct.comp i' b = CategoryTheory.CategoryStruct.comp a i) {Z : CategoryTheory.Sheaf J AddCommGrpCat} (h : relativeFreeYonedaSheaf J i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((freeYonedaSheafFunctor J).map i')) (CategoryTheory.CategoryStruct.comp (relativeFreeYonedaSheafMap J i' i a b w) h) = CategoryTheory.CategoryStruct.comp ((freeYonedaSheafFunctor J).map b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π ((freeYonedaSheafFunctor J).map i)) h)

@[simp]

theorem TauCeti.CategoryTheory.relativeFreeYonedaSheafMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U V : C} (i : U ⟶ V) : relativeFreeYonedaSheafMap J i i (CategoryTheory.CategoryStruct.id U) (CategoryTheory.CategoryStruct.id V) ⋯ = CategoryTheory.CategoryStruct.id (relativeFreeYonedaSheaf J i)

theorem TauCeti.CategoryTheory.relativeFreeYonedaSheafMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U' V' U V : C} (i' : U' ⟶ V') (i : U ⟶ V) (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryTheory.CategoryStruct.comp i' b = CategoryTheory.CategoryStruct.comp a i) {U'' V'' : C} (i'' : U'' ⟶ V'') (a' : U'' ⟶ U') (b' : V'' ⟶ V') (w' : CategoryTheory.CategoryStruct.comp i'' b' = CategoryTheory.CategoryStruct.comp a' i') : CategoryTheory.CategoryStruct.comp (relativeFreeYonedaSheafMap J i'' i' a' b' w') (relativeFreeYonedaSheafMap J i' i a b w) = relativeFreeYonedaSheafMap J i'' i (CategoryTheory.CategoryStruct.comp a' a) (CategoryTheory.CategoryStruct.comp b' b) ⋯

theorem TauCeti.CategoryTheory.coe_relativeFreeYonedaSheafHomEquiv_map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U' V' U V : C} (i' : U' ⟶ V') (i : U ⟶ V) (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryTheory.CategoryStruct.comp i' b = CategoryTheory.CategoryStruct.comp a i) (F : CategoryTheory.Sheaf J AddCommGrpCat) (g : relativeFreeYonedaSheaf J i ⟶ F) : ↑((relativeFreeYonedaSheafHomEquiv J i' F) (CategoryTheory.CategoryStruct.comp (relativeFreeYonedaSheafMap J i' i a b w) g)) = (CategoryTheory.ConcreteCategory.hom (F.obj.map b.op)) ↑((relativeFreeYonedaSheafHomEquiv J i F) g)

Under relativeFreeYonedaSheafHomEquiv, precomposition with relativeFreeYonedaSheafMap is the restriction of sections along b.

theorem TauCeti.CategoryTheory.isIso_relativeFreeYonedaSheafMap_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U' V' U V : C} (i' : U' ⟶ V') (i : U ⟶ V) (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryTheory.CategoryStruct.comp i' b = CategoryTheory.CategoryStruct.comp a i) : CategoryTheory.IsIso (relativeFreeYonedaSheafMap J i' i a b w) ↔ ∀ (F : CategoryTheory.Sheaf J AddCommGrpCat), ∀ s ∈ (AddCommGrpCat.Hom.hom (F.obj.map i'.op)).ker, ∃! t : ↑(F.obj.obj (Opposite.op V)), t ∈ (AddCommGrpCat.Hom.hom (F.obj.map i.op)).ker ∧ (CategoryTheory.ConcreteCategory.hom (F.obj.map b.op)) t = s

The map of relative free sheaves induced by a commutative square is an isomorphism if and only if, for every abelian sheaf F, restriction along b is a bijection from the sections over V vanishing along i to the sections over V' vanishing along i'.

instance TauCeti.CategoryTheory.isIso_relativeFreeYonedaSheafMap {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U' V' U V : C} (i' : U' ⟶ V') (i : U ⟶ V) (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryTheory.CategoryStruct.comp i' b = CategoryTheory.CategoryStruct.comp a i) [CategoryTheory.IsIso a] [CategoryTheory.IsIso b] : CategoryTheory.IsIso (relativeFreeYonedaSheafMap J i' i a b w)

A commutative square i' ≫ b = a ≫ i in which a and b are isomorphisms induces an isomorphism of relative free sheaves.

@[reducible, inline]

noncomputable abbrev TauCeti.CategoryTheory.relativeFreeYonedaTripleSequence {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U U' V : C} (i : U ⟶ U') (j : U' ⟶ V) : CategoryTheory.ShortComplex (CategoryTheory.Sheaf J AddCommGrpCat)

The sequence ℤ_{U',U} ⟶ ℤ_{V,U} ⟶ ℤ_{V,U'} of relative free sheaves attached to a triple U ⟶ U' ⟶ V, whose maps are induced by the morphisms of pairs (U', U) ⟶ (V, U) and (V, U) ⟶ (V, U').

theorem TauCeti.CategoryTheory.relativeFreeYonedaTripleSequence_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U U' V : C} (i : U ⟶ U') (j : U' ⟶ V) [CategoryTheory.Mono j] : (relativeFreeYonedaTripleSequence J i j).ShortExact

For morphisms i : U ⟶ U' and j : U' ⟶ V with j a monomorphism, the sequence 0 ⟶ ℤ_{U',U} ⟶ ℤ_{V,U} ⟶ ℤ_{V,U'} ⟶ 0 is short exact.

@[reducible, inline]

abbrev CategoryTheory.Sheaf.relativeH' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) (n : ℕ) : Type w

The relative cohomology Hⁿ(V, U; F) of an abelian sheaf F for a morphism i : U ⟶ V of the site: the n-th Ext group from the relative free sheaf ℤ_{V,U} to F.

noncomputable def CategoryTheory.Sheaf.relativeH'.toH' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) (n : ℕ) : F.relativeH' i n →+ ↑(F.H' n V)

The map Hⁿ(V, U; F) ⟶ Hⁿ(V, F) of the long exact sequence of the pair, induced by ℤ_V ⟶ ℤ_{V,U}.

theorem CategoryTheory.Sheaf.relativeH'.H'AddEquivExt_toH' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) {n : ℕ} (x : F.relativeH' i n) : (F.H'AddEquivExt n V) ((toH' F i n) x) = (Abelian.Ext.mk₀ (Limits.cokernel.π ((TauCeti.CategoryTheory.freeYonedaSheafFunctor J).map i))).comp x ⋯

noncomputable def CategoryTheory.Sheaf.relativeH'.δ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) [Mono i] {n₀ n₁ : ℕ} (h : 1 + n₀ = n₁) : ↑(F.H' n₀ U) →+ F.relativeH' i n₁

The connecting map Hⁿ(U, F) ⟶ Hⁿ⁺¹(V, U; F) of the long exact sequence of the pair.

theorem CategoryTheory.Sheaf.relativeH'.δ_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) [Mono i] {n₀ n₁ : ℕ} (h : 1 + n₀ = n₁) (x : ↑(F.H' n₀ U)) : (δ F i h) x = ⋯.extClass.comp ((F.H'AddEquivExt n₀ U) x) h

theorem CategoryTheory.Sheaf.relativeH'.exact_toH'_cohomologyPresheaf_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) [Mono i] (n : ℕ) : Function.Exact ⇑(toH' F i n) ⇑(ConcreteCategory.hom ((F.cohomologyPresheaf n).map i.op))

The long exact sequence of the pair is exact at Hⁿ(V, F): a class on V comes from relative cohomology exactly when its restriction to U vanishes.

theorem CategoryTheory.Sheaf.relativeH'.exact_cohomologyPresheaf_map_δ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) [Mono i] {n₀ n₁ : ℕ} (h : 1 + n₀ = n₁) : Function.Exact ⇑(ConcreteCategory.hom ((F.cohomologyPresheaf n₀).map i.op)) ⇑(δ F i h)

The long exact sequence of the pair is exact at Hⁿ(U, F): the kernel of the connecting map consists of the restrictions of classes on V.

theorem CategoryTheory.Sheaf.relativeH'.exact_δ_toH' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) [Mono i] {n₀ n₁ : ℕ} (h : 1 + n₀ = n₁) : Function.Exact ⇑(δ F i h) ⇑(toH' F i n₁)

The long exact sequence of the pair is exact at Hⁿ⁺¹(V, U; F).

noncomputable def CategoryTheory.Sheaf.relativeH'.zeroEquiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) : F.relativeH' i 0 ≃+ ↥(AddCommGrpCat.Hom.hom (F.obj.map i.op)).ker

Degree-zero relative cohomology is the group of sections over V whose restriction along i vanishes.

@[simp]

theorem CategoryTheory.Sheaf.relativeH'.coe_zeroEquiv_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) (x : F.relativeH' i 0) : ↑((zeroEquiv F i) x) = (TauCeti.CategoryTheory.freeYonedaSheafSectionsEquiv J V F) (CategoryStruct.comp (Limits.cokernel.π ((TauCeti.CategoryTheory.freeYonedaSheafFunctor J).map i)) (Abelian.Ext.addEquiv₀ x))

theorem CategoryTheory.Sheaf.relativeH'.coe_zeroEquiv_naturality_right {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {U V : C} (i : U ⟶ V) {F G : Sheaf J AddCommGrpCat} (f : F ⟶ G) (x : F.relativeH' i 0) : ↑((zeroEquiv G i) (Abelian.Ext.comp x (Abelian.Ext.mk₀ f) ⋯)) = (ConcreteCategory.hom (f.hom.app (Opposite.op V))) ↑((zeroEquiv F i) x)

The equivalence zeroEquiv is natural in the coefficient sheaf.

theorem CategoryTheory.Sheaf.relativeH'.freeYonedaSheafSectionsEquiv_addEquiv₀_toH' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) (x : F.relativeH' i 0) : (TauCeti.CategoryTheory.freeYonedaSheafSectionsEquiv J V F) (Abelian.Ext.addEquiv₀ ((F.H'AddEquivExt 0 V) ((toH' F i 0) x))) = ↑((zeroEquiv F i) x)

Under zeroEquiv and the identification of degree-zero cohomology with sections, the map toH' is the inclusion of the sections restricting to zero.

instance CategoryTheory.Sheaf.relativeH'.subsingleton_of_isIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) [IsIso i] (n : ℕ) : Subsingleton (F.relativeH' i n)

Relative cohomology vanishes for an isomorphism.

noncomputable def CategoryTheory.Sheaf.relativeH'.map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) {U' V' : C} (i' : U' ⟶ V') (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryStruct.comp i' b = CategoryStruct.comp a i) (n : ℕ) : F.relativeH' i n →+ F.relativeH' i' n

The map Hⁿ(V, U; F) ⟶ Hⁿ(V', U'; F) induced by a commutative square i' ≫ b = a ≫ i: precomposition with the map ℤ_{V',U'} ⟶ ℤ_{V,U} of relative free sheaves.

theorem CategoryTheory.Sheaf.relativeH'.map_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) {U' V' : C} (i' : U' ⟶ V') (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryStruct.comp i' b = CategoryStruct.comp a i) {n : ℕ} (x : F.relativeH' i n) : (map F i i' a b w n) x = (Abelian.Ext.mk₀ (TauCeti.CategoryTheory.relativeFreeYonedaSheafMap J i' i a b w)).comp x ⋯

@[simp]

theorem CategoryTheory.Sheaf.relativeH'.map_id {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) {n : ℕ} (x : F.relativeH' i n) : (map F i i (CategoryStruct.id U) (CategoryStruct.id V) ⋯ n) x = x

theorem CategoryTheory.Sheaf.relativeH'.map_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) {U' V' : C} (i' : U' ⟶ V') (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryStruct.comp i' b = CategoryStruct.comp a i) {U'' V'' : C} (i'' : U'' ⟶ V'') (a' : U'' ⟶ U') (b' : V'' ⟶ V') (w' : CategoryStruct.comp i'' b' = CategoryStruct.comp a' i') {n : ℕ} (x : F.relativeH' i n) : (map F i' i'' a' b' w' n) ((map F i i' a b w n) x) = (map F i i'' (CategoryStruct.comp a' a) (CategoryStruct.comp b' b) ⋯ n) x

theorem CategoryTheory.Sheaf.relativeH'.coe_zeroEquiv_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) {U' V' : C} (i' : U' ⟶ V') (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryStruct.comp i' b = CategoryStruct.comp a i) (x : F.relativeH' i 0) : ↑((zeroEquiv F i') ((map F i i' a b w 0) x)) = (ConcreteCategory.hom (F.obj.map b.op)) ↑((zeroEquiv F i) x)

Under zeroEquiv, the induced map in degree zero is the restriction of sections along b.

noncomputable def CategoryTheory.Sheaf.relativeH'.mapAddEquiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) {U' V' : C} (i' : U' ⟶ V') (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryStruct.comp i' b = CategoryStruct.comp a i) [IsIso (TauCeti.CategoryTheory.relativeFreeYonedaSheafMap J i' i a b w)] (n : ℕ) : F.relativeH' i n ≃+ F.relativeH' i' n

When the square induces an isomorphism of relative free sheaves (see TauCeti.CategoryTheory.isIso_relativeFreeYonedaSheafMap_iff), the induced map on relative cohomology is an equivalence.

@[simp]

theorem CategoryTheory.Sheaf.relativeH'.mapAddEquiv_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) {U' V' : C} (i' : U' ⟶ V') (a : U' ⟶ U) (b : V' ⟶ V) (w : CategoryStruct.comp i' b = CategoryStruct.comp a i) [IsIso (TauCeti.CategoryTheory.relativeFreeYonedaSheafMap J i' i a b w)] {n : ℕ} (x : F.relativeH' i n) : (mapAddEquiv F i i' a b w n) x = (map F i i' a b w n) x

theorem CategoryTheory.Sheaf.relativeH'.subsingleton_one {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) [Mono i] (hF : Function.Surjective ⇑(ConcreteCategory.hom (F.obj.map i.op))) (hV : Subsingleton ↑(F.H' 1 V)) : Subsingleton (F.relativeH' i 1)

If restriction of sections along i is surjective and H¹(V, F) vanishes, then so does H¹(V, U; F).

theorem CategoryTheory.Sheaf.relativeH'.subsingleton_add_two {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V : C} (i : U ⟶ V) [Mono i] {n : ℕ} (hU : Subsingleton ↑(F.H' (n + 1) U)) (hV : Subsingleton ↑(F.H' (n + 2) V)) : Subsingleton (F.relativeH' i (n + 2))

If Hⁿ⁺¹(U, F) and Hⁿ⁺²(V, F) vanish, then so does Hⁿ⁺²(V, U; F).

noncomputable def CategoryTheory.Sheaf.relativeH'.tripleδ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V U' : C} (i : U ⟶ U') (j : U' ⟶ V) [Mono j] {n₀ n₁ : ℕ} (h : 1 + n₀ = n₁) : F.relativeH' i n₀ →+ F.relativeH' j n₁

The connecting map Hⁿ(U', U; F) ⟶ Hⁿ⁺¹(V, U'; F) of the long exact sequence of a triple U ⟶ U' ⟶ V whose second morphism is a monomorphism.

theorem CategoryTheory.Sheaf.relativeH'.tripleδ_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V U' : C} (i : U ⟶ U') (j : U' ⟶ V) [Mono j] {n₀ n₁ : ℕ} (h : 1 + n₀ = n₁) (x : F.relativeH' i n₀) : (tripleδ F i j h) x = ⋯.extClass.comp x h

theorem CategoryTheory.Sheaf.relativeH'.exact_map_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V U' : C} (i : U ⟶ U') (j : U' ⟶ V) [Mono j] (n : ℕ) : Function.Exact ⇑(map F j (CategoryStruct.comp i j) i (CategoryStruct.id V) ⋯ n) ⇑(map F (CategoryStruct.comp i j) i (CategoryStruct.id U) j ⋯ n)

The long exact sequence of a triple U ⟶ U' ⟶ V is exact at Hⁿ(V, U; F): a class restricts to zero on the pair (U', U) exactly when it comes from Hⁿ(V, U'; F).

theorem CategoryTheory.Sheaf.relativeH'.exact_map_tripleδ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V U' : C} (i : U ⟶ U') (j : U' ⟶ V) [Mono j] {n₀ n₁ : ℕ} (h : 1 + n₀ = n₁) : Function.Exact ⇑(map F (CategoryStruct.comp i j) i (CategoryStruct.id U) j ⋯ n₀) ⇑(tripleδ F i j h)

The long exact sequence of a triple U ⟶ U' ⟶ V is exact at Hⁿ(U', U; F): the kernel of the connecting map consists of the restrictions of classes on the pair (V, U).

theorem CategoryTheory.Sheaf.relativeH'.exact_tripleδ_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (F : Sheaf J AddCommGrpCat) {U V U' : C} (i : U ⟶ U') (j : U' ⟶ V) [Mono j] {n₀ n₁ : ℕ} (h : 1 + n₀ = n₁) : Function.Exact ⇑(tripleδ F i j h) ⇑(map F j (CategoryStruct.comp i j) i (CategoryStruct.id V) ⋯ n₁)

The long exact sequence of a triple U ⟶ U' ⟶ V is exact at Hⁿ⁺¹(V, U'; F).