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 freeFunctor 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 AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (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.ιFree {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {I : Type u} (i : I) : unit R ⟶ free I

The inclusions unit R ⟶ free I.

Equations

• SheafOfModules.ιFree i = CategoryTheory.Limits.Sigma.ι (fun (x : I) => SheafOfModules.unit R) i

noncomputable def SheafOfModules.freeCofan {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (I : Type u) : CategoryTheory.Limits.Cofan fun (x : I) => unit R

The tautological cofan with point free I : SheafOfModules R.

Equations

• SheafOfModules.freeCofan I = CategoryTheory.Limits.Cofan.mk (SheafOfModules.free I) SheafOfModules.ιFree

@[simp]

theorem SheafOfModules.freeCofan_inj {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {I : Type u} (i : I) : (freeCofan I).inj i = ιFree i

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

free I is the colimit of copies of unit R indexed by I.

Equations

• SheafOfModules.isColimitFreeCofan I = CategoryTheory.Limits.coproductIsCoproduct 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 AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (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 AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {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 AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {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 AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {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

theorem SheafOfModules.unitHomEquiv_symm_freeHomEquiv_apply {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {I : Type u} {M : SheafOfModules R} (f : free I ⟶ M) (i : I) : M.unitHomEquiv.symm (M.freeHomEquiv f i) = CategoryTheory.CategoryStruct.comp (ιFree i) f

noncomputable def SheafOfModules.freeMap {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {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 AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {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 AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {I J✝ : Type u} (f : I → J✝) (i : I) : sectionsMap (freeMap f) (freeSection i) = freeSection (f i)

@[simp]

theorem SheafOfModules.ιFree_freeMap {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {I J✝ : Type u} (f : I → J✝) (i : I) : CategoryTheory.CategoryStruct.comp (ιFree i) (freeMap f) = ιFree (f i)

@[simp]

theorem SheafOfModules.ιFree_freeMap_assoc {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {I J✝ : Type u} (f : I → J✝) (i : I) {Z : SheafOfModules R} (h : free J✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (ιFree i) (CategoryTheory.CategoryStruct.comp (freeMap f) h) = CategoryTheory.CategoryStruct.comp (ιFree (f i)) h

noncomputable def SheafOfModules.freeFunctor {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] : 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 of as a presheaf of modules over itself).

Equations

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

@[simp]

theorem SheafOfModules.freeFunctor_map {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : freeFunctor.map f = freeMap f

@[simp]

theorem SheafOfModules.freeFunctor_obj {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (I : Type u) : freeFunctor.obj I = free I