The free presheaf of modules on a presheaf of sets

In this file, given a presheaf of rings R on a category C, we construct the functor PresheafOfModules.free : (Cᵒᵖ ⥤ Type u) ⥤ PresheafOfModules.{u} R which sends a presheaf of types to the corresponding presheaf of free modules. PresheafOfModules.freeAdjunction shows that this functor is the left adjoint to the forget functor.

Notes

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

noncomputable def PresheafOfModules.freeObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (F : CategoryTheory.Functor Cᵒᵖ (Type u)) : PresheafOfModules R

Given a presheaf of types F : Cᵒᵖ ⥤ Type u, this is the presheaf of modules over R which sends X : Cᵒᵖ to the free R.obj X-module on F.obj X.

@[simp]

theorem PresheafOfModules.freeObj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (F : CategoryTheory.Functor Cᵒᵖ (Type u)) (X : Cᵒᵖ) : (freeObj F).obj X = (ModuleCat.free ↑(R.obj X)).obj (F.obj X)

@[simp]

theorem PresheafOfModules.freeObj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (F : CategoryTheory.Functor Cᵒᵖ (Type u)) {X Y : Cᵒᵖ} (f : X ⟶ Y) : (freeObj F).map f = ModuleCat.freeDesc fun (x : F.obj X) => ModuleCat.freeMk (F.map f x)

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

The free presheaf of modules functor (Cᵒᵖ ⥤ Type u) ⥤ PresheafOfModules.{u} R.

@[simp]

theorem PresheafOfModules.free_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) {F G : CategoryTheory.Functor Cᵒᵖ (Type u)} (φ : F ⟶ G) (X : Cᵒᵖ) : ((free R).map φ).app X = (ModuleCat.free ↑(R.obj X)).map (φ.app X)

@[simp]

theorem PresheafOfModules.free_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (F : CategoryTheory.Functor Cᵒᵖ (Type u)) : (free R).obj F = freeObj F

noncomputable def PresheafOfModules.freeObjDesc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {F : CategoryTheory.Functor Cᵒᵖ (Type u)} {G : PresheafOfModules R} (φ : F ⟶ G.presheaf.comp (CategoryTheory.forget Ab)) : freeObj F ⟶ G

The morphism of presheaves of modules freeObj F ⟶ G corresponding to a morphism F ⟶ G.presheaf ⋙ forget _ of presheaves of types.

@[simp]

theorem PresheafOfModules.freeObjDesc_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {F : CategoryTheory.Functor Cᵒᵖ (Type u)} {G : PresheafOfModules R} (φ : F ⟶ G.presheaf.comp (CategoryTheory.forget Ab)) (X : Cᵒᵖ) : (freeObjDesc φ).app X = ModuleCat.freeDesc (φ.app X)

noncomputable def PresheafOfModules.freeAdjunctionUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (F : CategoryTheory.Functor Cᵒᵖ (Type u)) : F ⟶ (freeObj F).presheaf.comp (CategoryTheory.forget Ab)

The unit of PresheafOfModules.freeAdjunction.

@[simp]

theorem PresheafOfModules.freeAdjunctionUnit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (F : CategoryTheory.Functor Cᵒᵖ (Type u)) (X : Cᵒᵖ) (x : F.obj X) : (freeAdjunctionUnit R F).app X x = ModuleCat.freeMk x

noncomputable def PresheafOfModules.freeHomEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {F : CategoryTheory.Functor Cᵒᵖ (Type u)} {G : PresheafOfModules R} : (freeObj F ⟶ G) ≃ (F ⟶ G.presheaf.comp (CategoryTheory.forget Ab))

The bijection (freeObj F ⟶ G) ≃ (F ⟶ G.presheaf ⋙ forget _) when F is a presheaf of types and G a presheaf of modules.

theorem PresheafOfModules.free_hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {F : CategoryTheory.Functor Cᵒᵖ (Type u)} {G : PresheafOfModules R} {ψ ψ' : freeObj F ⟶ G} (h : CategoryTheory.CategoryStruct.comp (freeAdjunctionUnit R F) (CategoryTheory.Functor.whiskerRight ((toPresheaf R).map ψ) (CategoryTheory.forget Ab)) = CategoryTheory.CategoryStruct.comp (freeAdjunctionUnit R F) (CategoryTheory.Functor.whiskerRight ((toPresheaf R).map ψ') (CategoryTheory.forget Ab))) : ψ = ψ'

noncomputable def PresheafOfModules.freeAdjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : free R ⊣ (toPresheaf R).comp ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (CategoryTheory.forget Ab))

The free presheaf of modules functor is left adjoint to the forget functor PresheafOfModules.{u} R ⥤ Cᵒᵖ ⥤ Type u.

@[simp]

theorem PresheafOfModules.freeAdjunction_homEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (F : CategoryTheory.Functor Cᵒᵖ (Type u)) (G : PresheafOfModules R) : (freeAdjunction R).homEquiv F G = freeHomEquiv

@[simp]

theorem PresheafOfModules.freeAdjunction_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (F : CategoryTheory.Functor Cᵒᵖ (Type u)) : (freeAdjunction R).unit.app F = freeAdjunctionUnit R F