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} : ((PresheafOfModules.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).

Equations

• PresheafOfModules.freeYonedaEquiv = PresheafOfModules.freeHomEquiv.trans CategoryTheory.yonedaEquiv

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))) : ((PresheafOfModules.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 : (PresheafOfModules.free R).obj (CategoryTheory.yoneda.obj X) ⟶ M) (φ : M ⟶ N) : PresheafOfModules.freeYonedaEquiv (CategoryTheory.CategoryStruct.comp m φ) = (φ.app (Opposite.op X)) (PresheafOfModules.freeYonedaEquiv m)

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

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

Equations

• PresheafOfModules.freeYoneda R = Set.range (CategoryTheory.yoneda.comp (PresheafOfModules.free R)).obj

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

@[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.

Equations

• M.Elements = (((PresheafOfModules.toPresheaf R).obj M).comp (CategoryTheory.forget Ab)).Elements

@[reducible, inline]

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.

Equations

• M.elementsMk X x = (((PresheafOfModules.toPresheaf R).obj M).comp (CategoryTheory.forget Ab)).elementsMk X x

@[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.

Equations

• m.freeYoneda = (PresheafOfModules.free R).obj (CategoryTheory.yoneda.obj (Opposite.unop m.fst))

@[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.

Equations

• m.fromFreeYoneda = PresheafOfModules.freeYonedaEquiv.symm m.snd

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

Equations

• M.freeYonedaCoproduct = ∐ PresheafOfModules.Elements.freeYoneda

@[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.

Equations

• M.ιFreeYonedaCoproduct m = CategoryTheory.Limits.Sigma.ι PresheafOfModules.Elements.freeYoneda m

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.

Equations

• M.fromFreeYonedaCoproduct = CategoryTheory.Limits.Sigma.desc PresheafOfModules.Elements.fromFreeYoneda

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.

Equations

• M.freeYonedaCoproductMk m = ((M.ιFreeYonedaCoproduct m).app m.fst) (ModuleCat.freeMk (CategoryTheory.CategoryStruct.id (Opposite.unop m.fst)))

@[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)) : (M.fromFreeYonedaCoproduct.app X) (((M.ιFreeYonedaCoproduct m).app X) x) = (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) : (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

Equations

• ⋯ = ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• M.freeYonedaCoproductsCokernelCofork = CategoryTheory.Limits.CokernelCofork.ofπ M.fromFreeYonedaCoproduct ⋯

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.

Equations

• M.isColimitFreeYonedaCoproductsCokernelCofork = ⋯.gIsCokernel