Sheaf cohomology along an equivalence of sites

An equivalence of categories e : C ≌ D, compatible with Grothendieck topologies J on C and K on D, induces Mathlib's equivalence e.sheafCongr J K of categories of abelian sheaves, sending a sheaf F on C to the sheaf V ↦ F(e.inverse V) on D. This file shows that sheaf cohomology is invariant under this transport: the cohomology of the transported sheaf at V is the cohomology of F at e.inverse V.

The comparison applies whenever e.inverse is a dense subsite. Its direction transports a sheaf from C to D and identifies its cohomology over V : D with the original sheaf's cohomology over e.inverse.obj V.

Main declarations

• TauCeti.CategoryTheory.sheafCongrInverseFreeYonedaIso: the transport back of the free abelian sheaf on V is the free abelian sheaf on e.inverse V.
• TauCeti.CategoryTheory.cohomologyPresheafEvaluationIsoSheafCongr: the comparison, natural in the coefficient sheaf.
• TauCeti.CategoryTheory.cohomologyPresheafObjIsoSheafCongr: the comparison Hⁿ(V, e_* F) ≅ Hⁿ(e.inverse V, F) for a single sheaf F.

noncomputable def TauCeti.CategoryTheory.sheafCongrInverseFreeYonedaIso {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasSheafify K AddCommGrpCat] (V : D) : (CategoryTheory.Equivalence.sheafCongr J K e AddCommGrpCat).inverse.obj ((freeYonedaSheafFunctor K).obj V) ≅ (freeYonedaSheafFunctor J).obj (e.inverse.obj V)

Transporting the free abelian sheaf on V : D back along e.sheafCongr J K gives the free abelian sheaf on e.inverse.obj V.

Equations

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

theorem TauCeti.CategoryTheory.instAdditiveSheafAddCommGrpCatFunctorSymmSheafCongr_tauCeti {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasSheafify K AddCommGrpCat] : (CategoryTheory.Equivalence.sheafCongr J K e AddCommGrpCat).symm.functor.Additive

theorem TauCeti.CategoryTheory.instAdditiveSheafAddCommGrpCatInverseSymmSheafCongr_tauCeti {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasSheafify K AddCommGrpCat] : (CategoryTheory.Equivalence.sheafCongr J K e AddCommGrpCat).symm.inverse.Additive

noncomputable def TauCeti.CategoryTheory.cohomologyPresheafEvaluationIsoSheafCongr {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasSheafify K AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] [CategoryTheory.HasExt (CategoryTheory.Sheaf K AddCommGrpCat)] (n : ℕ) (V : D) : (CategoryTheory.Equivalence.sheafCongr J K e AddCommGrpCat).functor.comp ((CategoryTheory.Sheaf.cohomologyPresheafFunctor K n).comp ((CategoryTheory.evaluation Dᵒᵖ AddCommGrpCat).obj (Opposite.op V))) ≅ (CategoryTheory.Sheaf.cohomologyPresheafFunctor J n).comp ((CategoryTheory.evaluation Cᵒᵖ AddCommGrpCat).obj (Opposite.op (e.inverse.obj V)))

Sheaf cohomology is invariant under an equivalence of sites: the cohomology at V : D of the sheaf transported along e.sheafCongr J K is the cohomology of the original sheaf at e.inverse.obj V, naturally in the coefficient sheaf.

Equations

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

noncomputable def TauCeti.CategoryTheory.cohomologyPresheafObjIsoSheafCongr {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] [CategoryTheory.HasSheafify J AddCommGrpCat] [CategoryTheory.HasSheafify K AddCommGrpCat] [CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] [CategoryTheory.HasExt (CategoryTheory.Sheaf K AddCommGrpCat)] (F : CategoryTheory.Sheaf J AddCommGrpCat) (n : ℕ) (V : D) : ((CategoryTheory.Equivalence.sheafCongr J K e AddCommGrpCat).functor.obj F).H' n V ≅ F.H' n (e.inverse.obj V)

Sheaf cohomology is invariant under an equivalence of sites: the cohomology at V : D of the sheaf transported along e.sheafCongr J K is the cohomology of the original sheaf at e.inverse.obj V.

Equations

• TauCeti.CategoryTheory.cohomologyPresheafObjIsoSheafCongr J K e F n V = (TauCeti.CategoryTheory.cohomologyPresheafEvaluationIsoSheafCongr J K e n V).app F