Free sheaves of modules

In this file, we construct the functor SheafOfModules.freeFunctor : Type u ⥤ SheafOfModules.{u} R which sends a type I to the coproduct of copies indexed by I of unit R.

TODO

• In case the category C has a terminal object X, promote freeHomEquiv into an adjunction between freeFunctor and the evaluation functor at X. (Alternatively, assuming specific universe parameters, we could show that freeHomEquiv is a left adjoint to SheafOfModules.sectionsFunctor.)

noncomputable def SheafOfModules.free {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] (I : Type u) : SheafOfModules R

The free sheaf of modules on a certain type I.

Equations

• SheafOfModules.free I = ∐ fun (x : I) => SheafOfModules.unit R

noncomputable def SheafOfModules.freeHomEquiv {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] (M : SheafOfModules R) {I : Type u} : (free I ⟶ M) ≃ (I → M.sections)

The data of a morphism free I ⟶ M from a free sheaf of modules is equivalent to the data of a family I → M.sections of sections of M.

Equations

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

theorem SheafOfModules.freeHomEquiv_comp_apply {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M N : SheafOfModules R} {I : Type u} (f : free I ⟶ M) (p : M ⟶ N) (i : I) : N.freeHomEquiv (CategoryTheory.CategoryStruct.comp f p) i = sectionsMap p (M.freeHomEquiv f i)

theorem SheafOfModules.freeHomEquiv_symm_comp {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M N : SheafOfModules R} {I : Type u} (s : I → M.sections) (p : M ⟶ N) : CategoryTheory.CategoryStruct.comp (M.freeHomEquiv.symm s) p = N.freeHomEquiv.symm fun (i : I) => sectionsMap p (s i)

@[reducible, inline]

noncomputable abbrev SheafOfModules.freeSection {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {I : Type u} (i : I) : (free I).sections

The tautological section of free I : SheafOfModules R corresponding to i : I.

Equations

• SheafOfModules.freeSection i = (SheafOfModules.free I).freeHomEquiv (CategoryTheory.CategoryStruct.id (SheafOfModules.free I)) i

noncomputable def SheafOfModules.freeMap {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {I J✝ : Type u} (f : I → J✝) : free I ⟶ free J✝

The morphism of presheaves of R-modules free I ⟶ free J induced by a map f : I → J.

Equations

• SheafOfModules.freeMap f = (SheafOfModules.free J).freeHomEquiv.symm fun (i : I) => SheafOfModules.freeSection (f i)

@[simp]

theorem SheafOfModules.freeHomEquiv_freeMap {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {I J✝ : Type u} (f : I → J✝) : (free J✝).freeHomEquiv (freeMap f) = freeSection ∘ f

@[simp]

theorem SheafOfModules.sectionMap_freeMap_freeSection {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {I J✝ : Type u} (f : I → J✝) (i : I) : sectionsMap (freeMap f) (freeSection i) = freeSection (f i)

noncomputable def SheafOfModules.freeFunctor {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] : CategoryTheory.Functor (Type u) (SheafOfModules R)

The functor Type u ⥤ SheafOfModules.{u} R which sends a type I to free I which is a coproduct indexed by I of copies of R (thought as a presheaf of modules over itself).

Equations

• SheafOfModules.freeFunctor = { obj := SheafOfModules.free, map := fun {X Y : Type ?u.94} (f : X ⟶ Y) => SheafOfModules.freeMap f, map_id := ⋯, map_comp := ⋯ }