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
    @[simp]
    theorem PresheafOfModules.map_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (self : PresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (f : X Y) (g : Y Z) :
    self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (R.map f)).map (self.map g)) ((ModuleCat.restrictScalarsComp' (R.map f) (R.map g) (R.map (CategoryTheory.CategoryStruct.comp f g)) ).inv.app (self.obj Z)))
    theorem PresheafOfModules.map_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (r : (R.obj X)) (m : (M.obj X)) :
    (M.map f) (r m) = (R.map f) r (M.map f) m
    theorem PresheafOfModules.congr_map_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (M : PresheafOfModules R) {X : Cᵒᵖ} {Y : Cᵒᵖ} {f : X Y} {g : X Y} (h : f = g) (m : (M.obj X)) :
    (M.map f) m = (M.map g) m
    theorem PresheafOfModules.Hom.ext_iff {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} {x y : M₁.Hom M₂}, x = y x.app = y.app
    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₂}, x.app = y.appx = y

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

    Instances For
      @[simp]
      theorem PresheafOfModules.Hom.naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} (self : M₁.Hom M₂) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
      CategoryTheory.CategoryStruct.comp (M₁.map f) ((ModuleCat.restrictScalars (R.map f)).map (self.app Y)) = CategoryTheory.CategoryStruct.comp (self.app X) (M₂.map f)
      @[simp]
      theorem PresheafOfModules.Hom.naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} (self : M₁.Hom M₂) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) {Z : ModuleCat (R.obj X)} (h : (ModuleCat.restrictScalars (R.map f)).obj (M₂.obj Y) Z) :
      theorem PresheafOfModules.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} {f : M₁ M₂} {g : M₁ M₂} :
      f = g ∀ (X : Cᵒᵖ), f.app X = g.app X
      theorem PresheafOfModules.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} {f : M₁ M₂} {g : M₁ M₂} (h : ∀ (X : Cᵒᵖ), f.app X = g.app X) :
      f = g
      theorem PresheafOfModules.naturality_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} (f : M₁ M₂) {X : Cᵒᵖ} {Y : Cᵒᵖ} (g : X Y) (x : (M₁.obj X)) :
      (f.app Y) ((M₁.map g) x) = (M₂.map g) ((f.app X) x)

      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 : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) (x : (M.obj X)) :
        (M.presheaf.map f) x = (M.map f) x
        Equations
        • M.instModuleαRingObjOppositeRingCatAddCommGroupAbPresheaf 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₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} (f : M₁ M₂) (X : Cᵒᵖ) (x : (M₁.obj X)) :
          (((PresheafOfModules.toPresheaf R).map f).app X) x = (f.app X) x
          @[simp]
          theorem PresheafOfModules.ofPresheaf_obj {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) r (M.map f) m) (X : Cᵒᵖ) :
          (PresheafOfModules.ofPresheaf M map_smul).obj X = ModuleCat.of (R.obj X) (M.obj X)
          @[simp]
          theorem PresheafOfModules.ofPresheaf_map_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) r (M.map f) m) :
          ∀ {X Y : Cᵒᵖ} (f : X Y) (x : ((fun (X : Cᵒᵖ) => ModuleCat.of (R.obj X) (M.obj X)) X)), ((PresheafOfModules.ofPresheaf M map_smul).map f) x = (M.map f) 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) 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_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) r (M.map f) m) :
            (PresheafOfModules.ofPresheaf M map_smul).presheaf = M
            @[simp]
            theorem PresheafOfModules.homMk_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ : PresheafOfModules R} {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) a = (φ.app X) a
            def PresheafOfModules.homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ : PresheafOfModules R} {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
              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₁ : PresheafOfModules R} {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₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} (f : M₁ M₂) (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₁ : PresheafOfModules R} {M₂ : PresheafOfModules R} (f : M₁ M₂) (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₁ : PresheafOfModules R} {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 : 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_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {s : M.sections} {t : M.sections} :
                          s = t ∀ (X : Cᵒᵖ), s X = t X
                          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
                          @[simp]
                          theorem PresheafOfModules.sectionsMap_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M : PresheafOfModules R} {N : PresheafOfModules R} (f : M N) (s : M.sections) (X : Cᵒᵖ) :
                          (PresheafOfModules.sectionsMap f s) X = (f.app X) (s X)

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

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