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 R, as a presheaf of abelian groups with additional data.

We also provide two alternative constructors :

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
    theorem PresheafOfModules.map_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (self : PresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (r : (R.obj X)) (x : (self.presheaf.obj X)) :
    (self.presheaf.map f) (r x) = (R.map f) r (self.presheaf.map f) x

    The bundled module over an object X.

    Equations
    Instances For
      def PresheafOfModules.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (P : PresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
      (P.obj X) →ₛₗ[R.map f] (P.obj Y)

      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.

      Equations
      • P.map f = { toAddHom := (P.presheaf.map f), map_smul' := }
      Instances For
        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 : (P.obj X)) :
        (P.map f) x = (P.presheaf.map f) x
        @[simp]
        theorem PresheafOfModules.map_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (P : PresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : X Y) (g : Y Z) :
        P.map (CategoryTheory.CategoryStruct.comp f g) = (P.map g).comp (P.map f)

        A morphism of presheaves of modules.

        • hom : P.presheaf Q.presheaf
        • map_smul : ∀ (X : Cᵒᵖ) (r : (R.obj X)) (x : (P.presheaf.obj X)), (self.hom.app X) (r x) = r (self.hom.app X) x
        Instances For
          theorem PresheafOfModules.Hom.map_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (self : P.Hom Q) (X : Cᵒᵖ) (r : (R.obj X)) (x : (P.presheaf.obj X)) :
          (self.hom.app X) (r x) = r (self.hom.app X) x

          The identity morphism on a presheaf of modules.

          Equations
          Instances For
            def PresheafOfModules.Hom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R✝} {Q : PresheafOfModules R✝} {R : PresheafOfModules R✝} (f : P.Hom Q) (g : Q.Hom R) :
            P.Hom R

            Composition of morphisms of presheaves of modules.

            Equations
            Instances For
              def PresheafOfModules.Hom.app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (f : P.Hom Q) (X : Cᵒᵖ) :
              (P.obj X) →ₗ[(R.obj X)] (Q.obj X)

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

              Equations
              • f.app X = { toAddHom := (f.hom.app X), map_smul' := }
              Instances For
                Equations
                • PresheafOfModules.Hom.instZeroHom = { zero := { hom := 0, map_smul := } }
                Equations
                • PresheafOfModules.Hom.instAddHom = { add := fun (f g : P Q) => { hom := f.hom + g.hom, map_smul := } }
                Equations
                • PresheafOfModules.Hom.instSubHom = { sub := fun (f g : P Q) => { hom := f.hom - g.hom, map_smul := } }
                Equations
                • PresheafOfModules.Hom.instNegHom = { neg := fun (f : P Q) => { hom := -f.hom, map_smul := } }
                Equations
                • PresheafOfModules.Hom.instPreadditive = { homGroup := inferInstance, add_comp := , comp_add := }
                theorem PresheafOfModules.naturality_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (f : P Q) {X : Cᵒᵖ} {Y : Cᵒᵖ} (g : X Y) (x : (P.obj X)) :
                (PresheafOfModules.Hom.app f Y) ((P.map g) x) = (Q.map g) ((PresheafOfModules.Hom.app f X) x)

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

                Equations
                Instances For

                  Evaluation on an object X gives a functor PresheafOfModules R ⥤ ModuleCat (R.obj X).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    noncomputable def PresheafOfModules.restrictionApp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (M : PresheafOfModules R) :
                    M.obj X (ModuleCat.restrictScalars (R.map f)).obj (M.obj Y)

                    Given a presheaf of modules M on a category C and f : X ⟶ Y in Cᵒᵖ, this is the restriction map M.obj X ⟶ M.obj Y, considered as a linear map to the restriction of scalars of M.obj Y.

                    Equations
                    Instances For

                      The restriction natural transformation on presheaves of modules, considered as linear maps to restriction of scalars.

                      Equations
                      Instances For
                        def PresheafOfModules.Hom.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (app : (X : Cᵒᵖ) → (P.obj X) →ₗ[(R.obj X)] (Q.obj X)) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y) (x : (P.obj X)), (app Y) ((P.map f) x) = (Q.map f) ((app X) x)) :
                        P Q

                        A constructor for morphisms in PresheafOfModules R that is based on the data of a family of linear maps over the various rings R.obj X.

                        Equations
                        Instances For
                          @[simp]
                          theorem PresheafOfModules.Hom.mk'_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {P : PresheafOfModules R} {Q : PresheafOfModules R} (app : (X : Cᵒᵖ) → (P.obj X) →ₗ[(R.obj X)] (Q.obj X)) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y) (x : (P.obj X)), (app Y) ((P.map f) x) = (Q.map f) ((app X) x)) :
                          @[reducible, inline]

                          A constructor for morphisms in PresheafOfModules R that is based on the data of a family of linear maps over the various rings R.obj X, and for which the naturality condition is stated using the restriction of scalars.

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

                            This structure contains the data and axioms in order to produce a PresheafOfModules R from a collection of types equipped with module structures over the various rings R.obj X. (See the constructor PresheafOfModules.mk'.)

                            Instances For
                              @[simp]

                              map is compatible with the identities

                              @[simp]
                              theorem CorePresheafOfModules.map_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (self : CorePresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : X Y) (g : Y Z) (x : self.obj X) :
                              (self.map (CategoryTheory.CategoryStruct.comp f g)) x = (self.map g) ((self.map f) x)

                              map is compatible with the composition

                              @[simp]
                              theorem CorePresheafOfModules.presheaf_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CorePresheafOfModules R) :
                              ∀ {X Y : Cᵒᵖ} (f : X Y), M.presheaf.map f = AddCommGrp.ofHom (M.map f).toAddMonoidHom

                              The presheaf of abelian groups attached to a CorePresheafOfModules R.

                              Equations
                              Instances For
                                Equations
                                • M.instModuleαRingObjOppositeRingCatAddCommGroupAddCommGrpPresheaf X = M.module X

                                Constructor for PresheafOfModules R based on a collection of types equipped with module structures over the various rings R.obj X, see the structure CorePresheafOfModules.

                                Equations
                                • M.toPresheafOfModules = { presheaf := M.presheaf, module := inferInstance, map_smul := }
                                Instances For
                                  @[simp]
                                  theorem CorePresheafOfModules.toPresheafOfModules_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CorePresheafOfModules R) (X : Cᵒᵖ) :
                                  M.toPresheafOfModules.obj X = ModuleCat.of ((R.obj X)) (M.obj X)
                                  @[simp]
                                  theorem CorePresheafOfModules.toPresheafOfModules_presheaf_map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CorePresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (x : M.obj X) :
                                  (M.toPresheafOfModules.presheaf.map f) x = (M.map f) x
                                  structure BundledCorePresheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) :
                                  Type (max (max (max u u₁) (v + 1)) v₁)

                                  This structure contains the data and axioms in order to produce a PresheafOfModules R from a collection of objects of type ModuleCat (R.obj X) for all X, and restriction maps expressed as linear maps to restriction of scalars. (See the constructor PresheafOfModules.mk''.)

                                  Instances For

                                    map is compatible with the composition

                                    The obvious map BundledCorePresheafOfModules R → CorePresheafOfModules R.

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

                                      Constructor for PresheafOfModules R based on a collection of objects of type ModuleCat (R.obj X) for all X, and restriction maps expressed as linear maps to restriction of scalars, see the structure BundledCorePresheafOfModules.

                                      Equations
                                      • M.toPresheafOfModules = M.toCorePresheafOfModules.toPresheafOfModules
                                      Instances For
                                        @[simp]
                                        theorem BundledCorePresheafOfModules.toPresheafOfModules_presheaf_map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : BundledCorePresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (x : (M.obj X)) :
                                        (M.toPresheafOfModules.presheaf.map f) x = (M.map f) x

                                        Auxiliary definition for unit.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[reducible, inline]

                                          The obvious free presheaf of modules of rank 1.

                                          Equations
                                          Instances For

                                            The type of sections of a presheaf of modules.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem PresheafOfModules.sections_property {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : M.sections) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
                                              (M.map f) (s X) = s Y
                                              @[simp]
                                              theorem PresheafOfModules.sectionsMk_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : (X : Cᵒᵖ) → (M.obj X)) (hs : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y), (M.map f) (s X) = s Y) (X : Cᵒᵖ) :
                                              def PresheafOfModules.sectionsMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : (X : Cᵒᵖ) → (M.obj X)) (hs : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y), (M.map f) (s X) = s Y) :
                                              M.sections

                                              Constructor for sections of a presheaf of modules.

                                              Equations
                                              Instances For
                                                theorem PresheafOfModules.sections_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s : M.sections) (t : M.sections) (h : ∀ (X : Cᵒᵖ), s X = t X) :
                                                s = t

                                                The map M.sections → N.sections induced by a morphisms M ⟶ N of presheaves of modules.

                                                Equations
                                                Instances For

                                                  The bijection (unit R ⟶ M) ≃ M.sections for M : PresheafOfModules R.

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

                                                    PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X) when X is initial #

                                                    When X is initial, we have Module (R.obj X) (M.obj c) for any c : Cᵒᵖ.

                                                    @[simp]
                                                    theorem PresheafOfModules.forgetToPresheafModuleCatObj_map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) {c₁ : Cᵒᵖ} {c₂ : Cᵒᵖ} (f : c₁ c₂) (x : ((fun (c : Cᵒᵖ) => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c)) c₁)) :
                                                    ((PresheafOfModules.forgetToPresheafModuleCatObj X hX M).map f) x = (M.presheaf.map f) x

                                                    Implementation of the functor PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X) when X is initial.

                                                    The functor is implemented as, on object level M ↦ (c ↦ M(c)) where the R(X)-module structure on M(c) is given by restriction of scalars along the unique morphism R(c) ⟶ R(X); and on morphism level (f : M ⟶ N) ↦ (c ↦ f(c)).

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

                                                      Implementation of the functor PresheafOfModules R ⥤ Cᵒᵖ ⥤ ModuleCat (R.obj X) when X is initial.

                                                      The functor is implemented as, on object level M ↦ (c ↦ M(c)) where the R(X)-module structure on M(c) is given by restriction of scalars along the unique morphism R(c) ⟶ R(X); and on morphism level (f : M ⟶ N) ↦ (c ↦ f(c)).

                                                      Equations
                                                      Instances For

                                                        The forgetful functor from presheaves of modules over a presheaf of rings R to presheaves of R(X)-modules where X is an initial object.

                                                        The functor is implemented as, on object level M ↦ (c ↦ M(c)) where the R(X)-module structure on M(c) is given by restriction of scalars along the unique morphism R(c) ⟶ R(X); and on morphism level (f : M ⟶ N) ↦ (c ↦ f(c)).

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