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 objectX
, promotefreeHomEquiv
into an adjunction betweenfreeFunctor
and the evaluation functor atX
. (Alternatively, assuming specific universe parameters, we could show thatfreeHomEquiv
is a left adjoint toSheafOfModules.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)
:
The free sheaf of modules on a certain type I
.
Equations
- SheafOfModules.free I = ∐ fun (x : I) => SheafOfModules.unit R
Instances For
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.
Instances For
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
Instances For
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)
:
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)
Instances For
@[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)
:
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)]
:
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.82} (f : X ⟶ Y) => SheafOfModules.freeMap f, map_id := ⋯, map_comp := ⋯ }