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.

noncomputable def PresheafOfModules.freeYonedaEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {X : C} : ((free R).obj (CategoryTheory.yoneda.obj X) ⟶ M) ≃ ↑(M.obj (Opposite.op X))

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).

theorem PresheafOfModules.freeYonedaEquiv_symm_app {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (X : C) (x : ↑(M.obj (Opposite.op X))) : (CategoryTheory.ConcreteCategory.hom ((freeYonedaEquiv.symm x).app (Opposite.op X))) (ModuleCat.freeMk (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op X)))) = x

theorem PresheafOfModules.freeYonedaEquiv_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M N : PresheafOfModules R} {X : C} (m : (free R).obj (CategoryTheory.yoneda.obj X) ⟶ M) (φ : M ⟶ N) : freeYonedaEquiv (CategoryTheory.CategoryStruct.comp m φ) = (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op X))) (freeYonedaEquiv m)

def PresheafOfModules.freeYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : CategoryTheory.ObjectProperty (PresheafOfModules R)

The set of PresheafOfModules.{v} R consisting of objects of the form (free R).obj (yoneda.obj X) for some X.

instance PresheafOfModules.freeYoneda.instSmall {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} : CategoryTheory.ObjectProperty.Small.{u, max u v, max u (v + 1)} (freeYoneda R)

theorem PresheafOfModules.freeYoneda.isSeparating {C : Type u} [CategoryTheory.Category.{v, u} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : (freeYoneda R).IsSeparating

theorem PresheafOfModules.freeYoneda.isDetecting {C : Type u} [CategoryTheory.Category.{v, u} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : (freeYoneda R).IsDetecting

instance PresheafOfModules.wellPowered {C₀ : Type u} [CategoryTheory.SmallCategory C₀] (R₀ : CategoryTheory.Functor C₀ᵒᵖ RingCat) : CategoryTheory.WellPowered.{u, u, u + 1} (PresheafOfModules R₀)

@[reducible, inline]

abbrev PresheafOfModules.Elements {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : Type (max u₁ v)

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.

@[reducible, inline]

noncomputable abbrev PresheafOfModules.elementsMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (X : Cᵒᵖ) (x : ↑(M.obj X)) : M.Elements

Given a presheaf of modules M, this is a constructor for the type M.Elements.

@[reducible, inline]

noncomputable abbrev PresheafOfModules.Elements.freeYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (m : M.Elements) : PresheafOfModules R

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.

@[reducible, inline]

noncomputable abbrev PresheafOfModules.Elements.fromFreeYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (m : M.Elements) : m.freeYoneda ⟶ M

Given an element m : M.Elements of a presheaf of modules M, this is the canonical morphism m.freeYoneda ⟶ M.

theorem PresheafOfModules.Elements.fromFreeYoneda_app_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (m : M.Elements) : (CategoryTheory.ConcreteCategory.hom (m.fromFreeYoneda.app m.fst)) (ModuleCat.freeMk (CategoryTheory.CategoryStruct.id (Opposite.unop m.fst))) = m.snd

@[reducible, inline]

noncomputable abbrev PresheafOfModules.freeYonedaCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : PresheafOfModules R

Given a presheaf of modules M, this is the coproduct of all free Yoneda presheaves m.freeYoneda for all m : M.Elements.

@[reducible, inline]

noncomputable abbrev PresheafOfModules.ιFreeYonedaCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (m : M.Elements) : m.freeYoneda ⟶ M.freeYonedaCoproduct

Given an element m : M.Elements of a presheaf of modules M, this is the canonical inclusion m.freeYoneda ⟶ M.freeYonedaCoproduct.

noncomputable def PresheafOfModules.fromFreeYonedaCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : M.freeYonedaCoproduct ⟶ M

Given a presheaf of modules M, this is the canonical morphism M.freeYonedaCoproduct ⟶ M.

noncomputable def PresheafOfModules.freeYonedaCoproductMk {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (m : M.Elements) : ↑(M.freeYonedaCoproduct.obj m.fst)

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.

@[simp]

theorem PresheafOfModules.ι_fromFreeYonedaCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (m : M.Elements) : CategoryTheory.CategoryStruct.comp (M.ιFreeYonedaCoproduct m) M.fromFreeYonedaCoproduct = m.fromFreeYoneda

@[simp]

theorem PresheafOfModules.ι_fromFreeYonedaCoproduct_assoc {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (m : M.Elements) {Z : PresheafOfModules R} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.ιFreeYonedaCoproduct m) (CategoryTheory.CategoryStruct.comp M.fromFreeYonedaCoproduct h) = CategoryTheory.CategoryStruct.comp m.fromFreeYoneda h

theorem PresheafOfModules.ι_fromFreeYonedaCoproduct_apply {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (m : M.Elements) (X : Cᵒᵖ) (x : ↑(m.freeYoneda.obj X)) : (CategoryTheory.ConcreteCategory.hom (M.fromFreeYonedaCoproduct.app X)) ((CategoryTheory.ConcreteCategory.hom ((M.ιFreeYonedaCoproduct m).app X)) x) = (CategoryTheory.ConcreteCategory.hom (m.fromFreeYoneda.app X)) x

@[simp]

theorem PresheafOfModules.fromFreeYonedaCoproduct_app_mk {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (m : M.Elements) : (CategoryTheory.ConcreteCategory.hom (M.fromFreeYonedaCoproduct.app m.fst)) (M.freeYonedaCoproductMk m) = m.snd

instance PresheafOfModules.instEpiFromFreeYonedaCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : CategoryTheory.Epi M.fromFreeYonedaCoproduct

noncomputable def PresheafOfModules.toFreeYonedaCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : (CategoryTheory.Limits.kernel M.fromFreeYonedaCoproduct).freeYonedaCoproduct ⟶ M.freeYonedaCoproduct

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.

@[simp]

theorem PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : CategoryTheory.CategoryStruct.comp M.toFreeYonedaCoproduct M.fromFreeYonedaCoproduct = 0

@[simp]

theorem PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {Z : PresheafOfModules R} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp M.toFreeYonedaCoproduct (CategoryTheory.CategoryStruct.comp M.fromFreeYonedaCoproduct h) = CategoryTheory.CategoryStruct.comp 0 h

@[reducible, inline]

noncomputable abbrev PresheafOfModules.freeYonedaCoproductsCokernelCofork {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : CategoryTheory.Limits.CokernelCofork M.toFreeYonedaCoproduct

(Colimit) cofork which gives a presentation of a presheaf of modules M using coproducts of free presheaves of modules on Yoneda presheaves.

noncomputable def PresheafOfModules.isColimitFreeYonedaCoproductsCokernelCofork {C : Type u} [CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) : CategoryTheory.Limits.IsColimit M.freeYonedaCoproductsCokernelCofork

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.