The free abelian sheaf generated by an object of a site

The source object in Mathlib's CategoryTheory.Sheaf.H' is obtained by applying the free abelian group functor to a representable presheaf and then sheafifying. This file packages those objects as a functor of the object of the site and records their universal property and its naturality.

Main declarations

• TauCeti.CategoryTheory.freeYonedaSheafFunctor J, the functor sending U to the sheafification of the free abelian presheaf on yoneda.obj U;
• TauCeti.CategoryTheory.sheafH'_eq, identifying Mathlib's Sheaf.H' with Ext from that functor;
• TauCeti.CategoryTheory.freeYonedaSheafSectionsEquiv, the additive equivalence between morphisms from that sheaf to F and sections of F over U, and TauCeti.CategoryTheory.freeYonedaSheafCorepresentableBy, the same universal property phrased as a corepresentation of the sections functor;
• TauCeti.CategoryTheory.mono_freeYonedaSheafFunctor_map, saying that a monomorphism of site objects induces a monomorphism between the corresponding free abelian sheaves.

The equivalence composes the sheafification adjunction, the free-forgetful adjunction for abelian groups, and the Yoneda equivalence. This is the same model of the free abelian sheaf used definitionally by Mathlib's Sheaf.cohomologyPresheafFunctor.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer B, "coherent sheaves and cohomology Hⁱ(X, ℱ)": it is the input to the acyclicity of flasque sheaves in TauCeti/Topology/Sheaves/Flasque.lean. No formalization is vendored.

noncomputable def TauCeti.CategoryTheory.freeYonedaSheafFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] : CategoryTheory.Functor C (CategoryTheory.Sheaf J AddCommGrpCat)

The sheafification of the free abelian presheaf on yoneda.obj U, functorial in U. This is the source-object functor used in Mathlib's definition of Sheaf.H'.

Equations

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

theorem TauCeti.CategoryTheory.cohomologyPresheafFunctor_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (n : ℕ) : CategoryTheory.Sheaf.cohomologyPresheafFunctor J n = ((freeYonedaSheafFunctor J).op.comp (CategoryTheory.Abelian.extFunctor n)).flip

Mathlib's cohomology presheaf is the Ext bifunctor from free abelian representable sheaves.

theorem TauCeti.CategoryTheory.sheafH'_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (F : CategoryTheory.Sheaf J AddCommGrpCat) (n : ℕ) (U : C) : F.H' n U = ↧(CategoryTheory.Abelian.Ext ((freeYonedaSheafFunctor J).obj U) F n)

Mathlib's sheaf cohomology over an object of a site is Ext from the corresponding free abelian sheaf.

noncomputable def TauCeti.CategoryTheory.freeYonedaSheafSectionsEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] (U : C) (F : CategoryTheory.Sheaf J AddCommGrpCat) : ((freeYonedaSheafFunctor J).obj U ⟶ F) ≃+ ↑(F.obj.obj (Opposite.op U))

Morphisms from the free abelian sheaf on U to an abelian sheaf F are additively equivalent to the sections of F over U.

Equations

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

@[simp]

theorem TauCeti.CategoryTheory.freeYonedaSheafSectionsEquiv_naturality_right {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] {U : C} {F G : CategoryTheory.Sheaf J AddCommGrpCat} (f : (freeYonedaSheafFunctor J).obj U ⟶ F) (g : F ⟶ G) : (freeYonedaSheafSectionsEquiv J U G) (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.ConcreteCategory.hom (g.hom.app (Opposite.op U))) ((freeYonedaSheafSectionsEquiv J U F) f)

The equivalence freeYonedaSheafSectionsEquiv is natural in the coefficient sheaf.

noncomputable def TauCeti.CategoryTheory.freeYonedaSheafCorepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J AddCommGrpCat] (U : C) : (((CategoryTheory.sheafSections J AddCommGrpCat).obj (Opposite.op U)).comp (CategoryTheory.forget AddCommGrpCat)).CorepresentableBy ((freeYonedaSheafFunctor J).obj U)

The free abelian sheaf on U corepresents the functor of sections over U.

Equations

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

theorem TauCeti.CategoryTheory.freeYonedaSheafSectionsEquiv_naturality_left {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) (f : (freeYonedaSheafFunctor J).obj V ⟶ F) : (freeYonedaSheafSectionsEquiv J U F) (CategoryTheory.CategoryStruct.comp ((freeYonedaSheafFunctor J).map i) f) = (CategoryTheory.ConcreteCategory.hom (F.obj.map i.op)) ((freeYonedaSheafSectionsEquiv J V F) f)

The equivalence freeYonedaSheafSectionsEquiv is natural in the object of the site: precomposing with the map induced by i : U ⟶ V is restricting sections along i.

instance TauCeti.CategoryTheory.mono_freeYonedaSheafFunctor_map {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] : CategoryTheory.Mono ((freeYonedaSheafFunctor J).map i)

A monomorphism of site objects induces a monomorphism between the corresponding free abelian sheaves.