Documentation

Mathlib.Algebra.Category.ModuleCat.Presheaf

Presheaves of modules over a presheaf of rings. #

Given a presheaf of rings R : Cᵒᵖ ⥤ RingCat, we define the category PresheafOfModules R. An object M : PresheafOfModules R consists of a family of modules M.obj X : ModuleCat (R.obj X) for all X : Cᵒᵖ, together with the data, for all f : X ⟶ Y, of a functorial linear map M.map f from M.obj X to the restriction of scalars of M.obj Y via R.map f.

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 R : Cᵒᵖ ⥤ RingCat consists of family of objects obj X : ModuleCat (R.obj X) for all X : Cᵒᵖ together with functorial maps obj X ⟶ (ModuleCat.restrictScalars (R.map f)).obj (obj Y) for all f : X ⟶ Y in Cᵒᵖ.

Instances For
    theorem PresheafOfModules.map_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X Y) (r : (R.obj X)) (m : (M.obj X)) :
    (M.map f).hom (r m) = (R.map f).hom r (M.map f).hom m
    theorem PresheafOfModules.congr_map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {X Y : Cᵒᵖ} {f g : X Y} (h : f = g) (m : (M.obj X)) :
    (M.map f).hom m = (M.map g).hom m

    A morphism of presheaves of modules consists of a family of linear maps which satisfy the naturality condition.

    Instances For
      theorem PresheafOfModules.Hom.ext {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} {x y : M₁.Hom M₂} (app : x.app = y.app) :
      x = y
      @[simp]
      theorem PresheafOfModules.Hom.naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (self : M₁.Hom M₂) {X Y : Cᵒᵖ} (f : X Y) {Z : ModuleCat (R.obj X)} (h : (ModuleCat.restrictScalars (R.map f).hom).obj (M₂.obj Y) Z) :
      theorem PresheafOfModules.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} {f g : M₁ M₂} (h : ∀ (X : Cᵒᵖ), f.app X = g.app X) :
      f = g
      @[simp]
      theorem PresheafOfModules.comp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ M₃ : PresheafOfModules R} (f : M₁ M₂) (g : M₂ M₃) (X : Cᵒᵖ) :
      theorem PresheafOfModules.naturality_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ M₂) {X Y : Cᵒᵖ} (g : X Y) (x : (M₁.obj X)) :
      (f.app Y).hom ((M₁.map g).hom x) = (M₂.map g).hom ((f.app X).hom x)
      def PresheafOfModules.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (app : (X : Cᵒᵖ) → M₁.obj X M₂.obj X) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y), CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (R.map f).hom).map (app Y).hom) = CategoryTheory.CategoryStruct.comp (app X).hom (M₂.map f) := by aesop_cat) :
      M₁ M₂

      Constructor for isomorphisms in the category of presheaves of modules.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem PresheafOfModules.isoMk_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (app : (X : Cᵒᵖ) → M₁.obj X M₂.obj X) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y), CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (R.map f).hom).map (app Y).hom) = CategoryTheory.CategoryStruct.comp (app X).hom (M₂.map f) := by aesop_cat) (X : Cᵒᵖ) :
        (PresheafOfModules.isoMk app naturality).inv.app X = (app X).inv
        @[simp]
        theorem PresheafOfModules.isoMk_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (app : (X : Cᵒᵖ) → M₁.obj X M₂.obj X) (naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y), CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (R.map f).hom).map (app Y).hom) = CategoryTheory.CategoryStruct.comp (app X).hom (M₂.map f) := by aesop_cat) (X : Cᵒᵖ) :
        (PresheafOfModules.isoMk app naturality).hom.app X = (app X).hom

        The underlying presheaf of abelian groups of a presheaf of modules.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem PresheafOfModules.presheaf_obj_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) (X : Cᵒᵖ) :
          (M.presheaf.obj X) = (M.obj X)
          @[simp]
          theorem PresheafOfModules.presheaf_map_apply_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X Y) (x : (M.obj X)) :
          (M.presheaf.map f) x = (M.map f).hom x
          Equations
          • M.instModuleCarrierObjOppositeRingCatαAddCommGroupAbPresheaf X = inferInstanceAs (Module (R.obj X) (M.obj X))

          The forgetful functor PresheafOfModules R ⥤ Cᵒᵖ ⥤ Ab.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem PresheafOfModules.toPresheaf_map_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ M₂) (X : Cᵒᵖ) (x : (M₁.obj X)) :
            (((PresheafOfModules.toPresheaf R).map f).app X) x = (f.app X).hom x
            def PresheafOfModules.ofPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module (R.obj X) (M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y) (r : (R.obj X)) (m : (M.obj X)), (M.map f) (r m) = (R.map f).hom r (M.map f) m) :

            The object in PresheafOfModules R that is obtained from M : Cᵒᵖ ⥤ Ab.{v} such that for all X : Cᵒᵖ, M.obj X is a R.obj X module, in such a way that the restriction maps are semilinear. (This constructor should be used only in cases when the preferred constructor PresheafOfModules.mk is not as convenient as this one.)

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem PresheafOfModules.ofPresheaf_obj_isModule {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module (R.obj X) (M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y) (r : (R.obj X)) (m : (M.obj X)), (M.map f) (r m) = (R.map f).hom r (M.map f) m) (X : Cᵒᵖ) :
              ((PresheafOfModules.ofPresheaf M map_smul).obj X).isModule = inst✝ X
              @[simp]
              theorem PresheafOfModules.ofPresheaf_map_hom_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module (R.obj X) (M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y) (r : (R.obj X)) (m : (M.obj X)), (M.map f) (r m) = (R.map f).hom r (M.map f) m) {X Y : Cᵒᵖ} (f : X Y) (x : (M.obj X)) :
              ((PresheafOfModules.ofPresheaf M map_smul).map f).hom x = (M.map f) x
              @[simp]
              theorem PresheafOfModules.ofPresheaf_obj_isAddCommGroup {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module (R.obj X) (M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y) (r : (R.obj X)) (m : (M.obj X)), (M.map f) (r m) = (R.map f).hom r (M.map f) m) (X : Cᵒᵖ) :
              ((PresheafOfModules.ofPresheaf M map_smul).obj X).isAddCommGroup = AddCommGrp.addCommGroupInstance (M.obj X)
              @[simp]
              theorem PresheafOfModules.ofPresheaf_obj_carrier {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module (R.obj X) (M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y) (r : (R.obj X)) (m : (M.obj X)), (M.map f) (r m) = (R.map f).hom r (M.map f) m) (X : Cᵒᵖ) :
              ((PresheafOfModules.ofPresheaf M map_smul).obj X) = (M.obj X)
              @[simp]
              theorem PresheafOfModules.ofPresheaf_presheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : CategoryTheory.Functor Cᵒᵖ Ab) [(X : Cᵒᵖ) → Module (R.obj X) (M.obj X)] (map_smul : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X Y) (r : (R.obj X)) (m : (M.obj X)), (M.map f) (r m) = (R.map f).hom r (M.map f) m) :
              (PresheafOfModules.ofPresheaf M map_smul).presheaf = M
              def PresheafOfModules.homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (φ : M₁.presheaf M₂.presheaf) (hφ : ∀ (X : Cᵒᵖ) (r : (R.obj X)) (m : (M₁.obj X)), (φ.app X) (r m) = r (φ.app X) m) :
              M₁ M₂

              The morphism of presheaves of modules M₁ ⟶ M₂ given by a morphism of abelian presheaves M₁.presheaf ⟶ M₂.presheaf which satisfy a suitable linearity condition.

              Equations
              Instances For
                @[simp]
                theorem PresheafOfModules.homMk_app_hom_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (φ : M₁.presheaf M₂.presheaf) (hφ : ∀ (X : Cᵒᵖ) (r : (R.obj X)) (m : (M₁.obj X)), (φ.app X) (r m) = r (φ.app X) m) (X : Cᵒᵖ) (a : (M₁.presheaf.obj X)) :
                ((PresheafOfModules.homMk φ ).app X).hom a = (φ.app X) a
                Equations
                • PresheafOfModules.instZeroHom = { zero := { app := fun (x : Cᵒᵖ) => 0, naturality := } }
                Equations
                • PresheafOfModules.instNegHom = { neg := fun (f : M₁ M₂) => { app := fun (X : Cᵒᵖ) => -f.app X, naturality := } }
                Equations
                • PresheafOfModules.instAddHom = { add := fun (f g : M₁ M₂) => { app := fun (X : Cᵒᵖ) => f.app X + g.app X, naturality := } }
                Equations
                • PresheafOfModules.instSubHom = { sub := fun (f g : M₁ M₂) => { app := fun (X : Cᵒᵖ) => f.app X - g.app X, naturality := } }
                @[simp]
                theorem PresheafOfModules.neg_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ M₂) (X : Cᵒᵖ) :
                (-f).app X = -f.app X
                @[simp]
                theorem PresheafOfModules.add_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f g : M₁ M₂) (X : Cᵒᵖ) :
                (f + g).app X = f.app X + g.app X
                @[simp]
                theorem PresheafOfModules.sub_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f g : M₁ M₂) (X : Cᵒᵖ) :
                (f - g).app X = f.app X - g.app X
                Equations
                Equations
                • PresheafOfModules.instPreadditive = { homGroup := inferInstance, add_comp := , comp_add := }
                theorem PresheafOfModules.zsmul_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (n : ) (f : M₁ M₂) (X : Cᵒᵖ) :
                (n f).app X = n f.app X

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

                Equations
                Instances For

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

                  Equations
                  Instances For

                    The obvious free presheaf of modules of rank 1.

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

                      The type of sections of a presheaf of modules.

                      Equations
                      Instances For
                        @[reducible, inline]

                        Given a presheaf of modules M, s : M.sections and X : Cᵒᵖ, this is the induced element in M.obj X.

                        Equations
                        • s.eval X = s X
                        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 Y : Cᵒᵖ} (f : X Y) :
                          (M.map f).hom (s X) = s Y
                          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).hom (s X) = s Y) :
                          M.sections

                          Constructor for sections of a presheaf of modules.

                          Equations
                          Instances For
                            @[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).hom (s X) = s Y) (X : Cᵒᵖ) :
                            theorem PresheafOfModules.sections_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} (s 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
                              @[simp]
                              theorem PresheafOfModules.sectionsMap_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M N : PresheafOfModules R} (f : M N) (s : M.sections) (X : Cᵒᵖ) :
                              (PresheafOfModules.sectionsMap f s) X = (f.app X).hom (s X)

                              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
                                @[simp]

                                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ᵒᵖ.

                                @[reducible, inline]

                                Auxiliary definition for forgetToPresheafModuleCatObj.

                                Equations
                                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
                                  • 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