Documentation

Mathlib.Algebra.Category.ModuleCat.Sheaf

Sheaves of modules over a sheaf of rings #

In this file, we define the category SheafOfModules R when R : Sheaf J RingCat is a sheaf of rings on a category C equipped with a Grothendieck topology J.

structure SheafOfModules {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) :
Type (max (max (max u u₁) (v + 1)) v₁)

A sheaf of modules is a presheaf of modules such that the underlying presheaf of abelian groups is a sheaf.

Instances For
    theorem SheafOfModules.Hom.ext_iff {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} {x y : X.Hom Y}, x = y x.val = y.val
    theorem SheafOfModules.Hom.ext {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} {x y : X.Hom Y}, x.val = y.valx = y

    A morphism between sheaves of modules is a morphism between the underlying presheaves of modules.

    • val : X.val Y.val

      a morphism between the underlying presheaves of modules

    Instances For

      The forgetful functor SheafOfModules.{v} R ⥤ PresheafOfModules R.val.

      Equations
      Instances For

        The forget functor SheafOfModules R ⥤ PresheafOfModules R.val is fully faithful.

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

          The forget functor SheafOfModules R ⥤ Sheaf J AddCommGrp.

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

            The forgetful functor from sheaves of modules over sheaf of ring R to sheaves of R(X)-module when X is initial.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem SheafOfModules.add_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {M : SheafOfModules R} {N : SheafOfModules R} (f : M N) (g : M N) :
              (f + g).val = f.val + g.val
              @[reducible, inline]

              The type of sections of a sheaf of modules.

              Equations
              • M.sections = M.val.sections
              Instances For
                @[reducible, inline]

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

                Equations
                Instances For

                  The functor which sends a sheaf of modules to its type of sections.

                  Equations
                  Instances For

                    The obvious free sheaf of modules of rank 1.

                    Equations
                    Instances For

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

                      Equations
                      Instances For
                        @[reducible, inline]

                        A morphism of presheaves of modules is locally surjective if the underlying morphism of presheaves of abelian groups is.

                        Equations
                        Instances For
                          @[reducible, inline]

                          A morphism of presheaves of modules is locally injective if the underlying morphism of presheaves of abelian groups is.

                          Equations
                          Instances For

                            The bijection (M₂ ⟶ N) ≃ (M₁ ⟶ N) induced by a locally bijective morphism f : M₁ ⟶ M₂ of presheaves of modules, when N is a sheaf.

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