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} : (SheafOfModules.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 : SheafOfModules R} {N : SheafOfModules R} {I : Type u} (f : SheafOfModules.free I ⟶ M) (p : M ⟶ N) (i : I) : N.freeHomEquiv (CategoryTheory.CategoryStruct.comp f p) i = SheafOfModules.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 : SheafOfModules R} {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) => SheafOfModules.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) : (SheafOfModules.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 : Type u} {J : Type u} (f : I → J) : SheafOfModules.free I ⟶ SheafOfModules.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 : Type u} {J : Type u} (f : I → J) : (SheafOfModules.free J).freeHomEquiv (SheafOfModules.freeMap f) = SheafOfModules.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 : Type u} {J : Type u} (f : I → J) (i : I) : SheafOfModules.sectionsMap (SheafOfModules.freeMap f) (SheafOfModules.freeSection i) = SheafOfModules.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} (f : X ⟶ Y) => SheafOfModules.freeMap f, map_id := ⋯, map_comp := ⋯ }