Documentation

Mathlib.Algebra.Category.ModuleCat.Presheaf

Presheaves of modules over a presheaf of rings. #

We give a hands-on description of a presheaf of modules over a fixed presheaf of rings, as a presheaf of abelian groups with additional data.

Future work #

structure PresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) :
Type (max (max (max u u₁) (v + 1)) v₁)

A presheaf of modules over a given presheaf of rings, described as a presheaf of abelian groups, and the extra data of the action at each object, and a condition relating functoriality and scalar multiplication.

Instances For

    The bundled module over an object X.

    Instances For

      If P is a presheaf of modules over a presheaf of rings R, both over some category C, and f : X ⟶ Y is a morphism in Cᵒᵖ, we construct the R.map f-semilinear map from the R.obj X-module P.presheaf.obj X to the R.obj Y-module P.presheaf.obj Y.

      Instances For
        @[simp]
        theorem PresheafOfModules.map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (P : PresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (x : ↑(PresheafOfModules.obj P X)) :
        ↑(PresheafOfModules.map P f) x = ↑(P.presheaf.map f) x
        • hom : P.presheaf Q.presheaf
        • map_smul : ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (x : ↑(P.presheaf.obj X)), ↑(s.hom.app X) (r x) = r ↑(s.hom.app X) x

        A morphism of presheaves of modules.

        Instances For

          The identity morphism on a presheaf of modules.

          Instances For

            Composition of morphisms of presheaves of modules.

            Instances For

              The (X : Cᵒᵖ)-component of morphism between presheaves of modules over a presheaf of rings R, as an R.obj X-linear map.

              Instances For

                The functor from presheaves of modules over a specified presheaf of rings, to presheaves of abelian groups.

                Instances For