Generators for the category of presheaves of modules #
In this file, given a presheaf of rings R on a category C,
we study the set freeYoneda R of presheaves of modules
of form (free R).obj (yoneda.obj X) for X : C, i.e.
free presheaves of modules generated by the Yoneda
presheaf represented by some X : C (the functor
represented by such a presheaf of modules is the evaluation
functor M ↦ M.obj (op X), see freeYonedaEquiv).
Lemmas PresheafOfModules.freeYoneda.isSeparating and
PresheafOfModules.freeYoneda.isDetecting assert that this
set freeYoneda R is separating and detecting.
We deduce that if C : Type u is a small category,
and R : Cᵒᵖ ⥤ RingCat.{u}, then PresheafOfModules.{u} R
is a well-powered category.
Finally, given M : PresheafOfModules.{u} R, we consider
the canonical epimorphism of presheaves of modules
M.fromFreeYonedaCoproduct : M.freeYonedaCoproduct ⟶ M
where M.freeYonedaCoproduct is a coproduct indexed
by elements of M, i.e. pairs ⟨X : Cᵒᵖ, a : M.obj X⟩,
of the objects (free R).obj (yoneda.obj X.unop).
This is used in the definition
PresheafOfModules.isColimitFreeYonedaCoproductsCokernelCofork
in order to obtain that any presheaf of modules is a cokernel
of a morphism between coproducts of objects in freeYoneda R.
When R : Cᵒᵖ ⥤ RingCat, M : PresheafOfModules R, and X : C, this is the
bijection ((free R).obj (yoneda.obj X) ⟶ M) ≃ M.obj (Opposite.op X).
The set of PresheafOfModules.{v} R consisting of objects of the
form (free R).obj (yoneda.obj X) for some X.
Equations
The type of elements of a presheaf of modules. A term of this type is a pair
⟨X, a⟩ with X : Cᵒᵖ and a : M.obj X.
Equations
- M.Elements = (((PresheafOfModules.toPresheaf R).obj M).comp (CategoryTheory.forget Ab)).Elements
Given a presheaf of modules M, this is a constructor for the type M.Elements.
Equations
- M.elementsMk X x = (((PresheafOfModules.toPresheaf R).obj M).comp (CategoryTheory.forget Ab)).elementsMk X x
Given an element m : M.Elements of a presheaf of modules M, this is the
free presheaf of modules on the Yoneda presheaf of types corresponding to the
underlying object of m.
Equations
- m.freeYoneda = (PresheafOfModules.free R).obj (CategoryTheory.yoneda.obj (Opposite.unop m.fst))
Given an element m : M.Elements of a presheaf of modules M, this is
the canonical morphism m.freeYoneda ⟶ M.
Equations
Given a presheaf of modules M, this is the coproduct of
all free Yoneda presheaves m.freeYoneda for all m : M.Elements.
Given an element m : M.Elements of a presheaf of modules M, this is the
canonical inclusion m.freeYoneda ⟶ M.freeYonedaCoproduct.
Given a presheaf of modules M, this is the
canonical morphism M.freeYonedaCoproduct ⟶ M.
Given an element m of a presheaf of modules M, this is the associated
canonical section of the presheaf M.freeYonedaCoproduct over the object m.1.
Equations
Given a presheaf of modules M, this is a morphism between coproducts
of free presheaves of modules on Yoneda presheaves which gives a presentation
of the module M, see isColimitFreeYonedaCoproductsCokernelCofork.
Equations
- One or more equations did not get rendered due to their size.
(Colimit) cofork which gives a presentation of a presheaf of modules M using
coproducts of free presheaves of modules on Yoneda presheaves.
If M is a presheaf of modules, the cokernel cofork
M.freeYonedaCoproductsCokernelCofork is a colimit, which means that
M can be expressed as a cokernel of the morphism M.toFreeYonedaCoproduct
between coproducts of free presheaves of modules on Yoneda presheaves.