Documentation

Mathlib.Topology.Sheaves.Operations

Operations on sheaves #

Main definition #

A subpresheaf with a submonoid structure on each of the components.

Instances For
    theorem TopCat.Presheaf.SubmonoidPresheaf.map {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [(X : C) → MulOneClass ((CategoryTheory.forget C).obj X)] [∀ (X Y : C), MonoidHomClass (X Y) ((CategoryTheory.forget C).obj X) ((CategoryTheory.forget C).obj Y)] {F : TopCat.Presheaf C X} (self : F.SubmonoidPresheaf) {U : (TopologicalSpace.Opens X)ᵒᵖ} {V : (TopologicalSpace.Opens X)ᵒᵖ} (i : U V) :
    self.obj U Submonoid.comap (F.map i) (self.obj V)

    The localization of a presheaf of CommRings with respect to a SubmonoidPresheaf.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) (U : (TopologicalSpace.Opens X)ᵒᵖ) :
      G.toLocalizationPresheaf.app U = CommRingCat.ofHom (algebraMap (↑(F.obj U)) (Localization (G.obj U)))
      def TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) :
      F G.localizationPresheaf

      The map into the localization presheaf.

      Equations
      Instances For
        instance TopCat.Presheaf.epi_toLocalizationPresheaf {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) :
        CategoryTheory.Epi G.toLocalizationPresheaf
        Equations
        • =
        @[simp]
        theorem TopCat.Presheaf.submonoidPresheafOfStalk_obj {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (S : (x : X) → Submonoid (F.stalk x)) (U : (TopologicalSpace.Opens X)ᵒᵖ) :
        (F.submonoidPresheafOfStalk S).obj U = ⨅ (x : (Opposite.unop U)), Submonoid.comap (F.germ (Opposite.unop U) x ) (S x)
        noncomputable def TopCat.Presheaf.submonoidPresheafOfStalk {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (S : (x : X) → Submonoid (F.stalk x)) :
        F.SubmonoidPresheaf

        Given a submonoid at each of the stalks, we may define a submonoid presheaf consisting of sections whose restriction onto each stalk falls in the given submonoid.

        Equations
        Instances For
          Equations
          • F.instInhabitedSubmonoidPresheafCommRingCat = { default := F.submonoidPresheafOfStalk fun (x : X) => }

          The localization of a presheaf of CommRings at locally non-zero-divisor sections.

          Equations
          • F.totalQuotientPresheaf = (F.submonoidPresheafOfStalk fun (x : X) => nonZeroDivisors (F.stalk x)).localizationPresheaf
          Instances For
            noncomputable def TopCat.Presheaf.toTotalQuotientPresheaf {X : TopCat} (F : TopCat.Presheaf CommRingCat X) :
            F F.totalQuotientPresheaf

            The map into the presheaf of total quotient rings

            Equations
            • F.toTotalQuotientPresheaf = (F.submonoidPresheafOfStalk fun (x : X) => nonZeroDivisors (F.stalk x)).toLocalizationPresheaf
            Instances For