Free presheaves of modules on representable presheaves

Let R be a presheaf of rings on a category C and let U be an object of C. The free presheaf of modules PresheafOfModules.freeObj (yoneda.obj U) on the presheaf of sets represented by U has, over V, the free module on the morphisms V ⟶ U, and Mathlib's PresheafOfModules.freeYonedaEquiv identifies morphisms out of it with sections over U. This file records how its basis elements behave.

Main declarations

• TauCeti.PresheafOfModules.freeObj_yoneda_map_freeMk: restriction along f sends the basis element indexed by g to the basis element indexed by f.unop ≫ g;
• TauCeti.PresheafOfModules.freeYonedaEquiv_symm_app_freeMk: the morphism attached to a section x sends the basis element indexed by g to the restriction of x along g, generalizing Mathlib's PresheafOfModules.freeYonedaEquiv_symm_app from the identity to any index;
• TauCeti.PresheafOfModules.freeYonedaEquiv_symm_comp: the morphism attached to a section composed with φ is the morphism attached to the image of the section under φ;
• TauCeti.PresheafOfModules.freeYoneda: the free presheaf of modules on the presheaf represented by U, over a presheaf of commutative rings, for use with the monoidal structure of PresheafOfModulesOfCommRing.

theorem TauCeti.PresheafOfModules.freeObj_yoneda_map_freeMk {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {U : C} {X Y : Cᵒᵖ} (f : X ⟶ Y) (g : Opposite.unop X ⟶ U) : (CategoryTheory.ConcreteCategory.hom ((PresheafOfModules.freeObj (CategoryTheory.yoneda.obj U)).map f)) (ModuleCat.freeMk g) = ModuleCat.freeMk (CategoryTheory.CategoryStruct.comp f.unop g)

The free presheaf of modules on the presheaf of sets represented by U restricts the basis element indexed by g : X.unop ⟶ U along f : X ⟶ Y to the basis element indexed by f.unop ≫ g.

This is not a simp lemma: PresheafOfModules.freeObj_map already unfolds the restriction map of a free presheaf, so the left-hand side is not in simp normal form.

@[simp]

theorem TauCeti.PresheafOfModules.freeYonedaEquiv_symm_app_freeMk {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {U V : C} (x : ↑(P.obj (Opposite.op U))) (g : V ⟶ U) : (CategoryTheory.ConcreteCategory.hom ((PresheafOfModules.freeYonedaEquiv.symm x).app (Opposite.op V))) (ModuleCat.freeMk g) = (CategoryTheory.ConcreteCategory.hom (P.map g.op)) x

The morphism out of the free presheaf of modules on the presheaf of sets represented by U corresponding to a section x over U sends the basis element indexed by g : V ⟶ U to the restriction of x along g.

theorem TauCeti.PresheafOfModules.freeYonedaEquiv_symm_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P Q : PresheafOfModules R} {U : C} (x : ↑(P.obj (Opposite.op U))) (φ : P ⟶ Q) : CategoryTheory.CategoryStruct.comp (PresheafOfModules.freeYonedaEquiv.symm x) φ = PresheafOfModules.freeYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op U))) x)

Composing the morphism out of the free presheaf on the presheaf represented by U corresponding to a section x with φ gives the morphism corresponding to the image of x under φ.

@[reducible, inline]

noncomputable abbrev TauCeti.PresheafOfModules.freeYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (R : CategoryTheory.Functor Cᵒᵖ CommRingCat) (U : C) : PresheafOfModulesOfCommRing R

The free presheaf of modules on the presheaf of sets represented by U, over a presheaf of commutative rings.

Equations

• TauCeti.PresheafOfModules.freeYoneda R U = PresheafOfModules.freeObj (CategoryTheory.yoneda.obj U)