Sections of a presheaf of modules over a terminal object

When the index category has a terminal object T, a compatible family of sections of a presheaf of modules is determined by its value at T, and every value at T extends by restriction. So M.sections ≃ M.obj (op T). With PresheafOfModules.unitHomEquiv this identifies maps out of the unit module with sections over T, which is what the degree-zero comparison between Ext (unit R) M and sheaf cohomology of M needs.

noncomputable def PresheafOfModules.sectionsEquivOfIsTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : M.sections ≃ ↑(M.obj (Opposite.op T))

Sections of a presheaf of modules on a category with a terminal object are its values at the terminal object.

Equations

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

@[simp]

theorem PresheafOfModules.sectionsEquivOfIsTerminal_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (x : ↑(M.obj (Opposite.op T))) : (M.sectionsEquivOfIsTerminal hT).symm x = sectionsMk (fun (X : Cᵒᵖ) => (CategoryTheory.ConcreteCategory.hom (M.map (hT.from (Opposite.unop X)).op)) x) ⋯

@[simp]

theorem PresheafOfModules.sectionsEquivOfIsTerminal_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (s : M.sections) : (M.sectionsEquivOfIsTerminal hT) s = ↑s (Opposite.op T)