Documentation

Mathlib.Topology.Sheaves.CommRingCat

Sheaves of (commutative) rings. #

Results specific to sheaves of commutative rings including sheaves of continuous functions TopCat.continuousFunctions with natural operations of pullback and map and sub, quotient, and localization operations on sheaves of rings with

As more results accumulate, please consider splitting this file.

References #

As an example, we now have everything we need to check the sheaf condition for a presheaf of commutative rings, merely by checking the sheaf condition for the underlying sheaf of types.

Note that the universes for TopCat and CommRingCat must be the same for this argument to go through.

source
📐 coverage
theorem TopCat.Presheaf.restrictOpenCommRingCat_apply {X : TopCat} {F : Presheaf CommRingCat X} {V : TopologicalSpace.Opens ↑X} (f : ↑(F.obj (Opposite.op V))) (U : TopologicalSpace.Opens ↑X) (e : U ≤ V := by restrict_tac) :
restrictOpen f U e = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE e).op)) f

Unfold restrictOpen in the category of commutative rings (with the correct carrier type).

Although unification hints help with applying TopCat.Presheaf.restrictOpenCommRingCat, so it can be safely de-specialized, this lemma needs to be kept to ensure rewrites go right.

source
🔶 coverage
structure TopCat.Presheaf.SubmonoidPresheaf {X : TopCat} (F : Presheaf CommRingCat X) :
Type (max u_1 w)

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

Instances For
    source
    🔸 coverage
    noncomputable def TopCat.Presheaf.SubmonoidPresheaf.localizationPresheaf {X : TopCat} {F : Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) :
    Presheaf CommRingCat X

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

    Instances For
      source
      🔸 coverage
      @[implicit_reducible]
      instance TopCat.Presheaf.instAlgebraCarrierObjOppositeOpensCarrierCommRingCatLocalizationPresheaf {X : TopCat} {F : Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) :
      Algebra ↑(F.obj U) ↑(G.localizationPresheaf.obj U)
      source
      📐 coverage
      instance TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf {X : TopCat} {F : Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) :
      IsLocalization (G.obj U) ↑(G.localizationPresheaf.obj U)
      source
      🔸 coverage
      def TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf {X : TopCat} {F : Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) :
      F ⟶ G.localizationPresheaf

      The map into the localization presheaf.

      Instances For
        source
        📐 coverage
        @[simp]
        theorem TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app {X : TopCat} {F : Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) :
        G.toLocalizationPresheaf.app U = CommRingCat.ofHom (algebraMap (↑(F.obj U)) (Localization (G.obj U)))
        source
        📐 coverage
        instance TopCat.Presheaf.epi_toLocalizationPresheaf {X : TopCat} {F : Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) :
        CategoryTheory.Epi G.toLocalizationPresheaf
        source
        🔸 coverage
        noncomputable def TopCat.Presheaf.submonoidPresheafOfStalk {X : TopCat} (F : 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.

        Instances For
          source
          📐 coverage
          @[simp]
          theorem TopCat.Presheaf.submonoidPresheafOfStalk_obj {X : TopCat} (F : 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 (CommRingCat.Hom.hom (F.germ (Opposite.unop U) ↑x ⋯)) (S ↑x)
          source
          🔸 coverage
          @[implicit_reducible]
          noncomputable instance TopCat.Presheaf.instInhabitedSubmonoidPresheaf {X : TopCat} (F : Presheaf CommRingCat X) :
          Inhabited F.SubmonoidPresheaf
          source
          🔸 coverage
          noncomputable def TopCat.Presheaf.totalQuotientPresheaf {X : TopCat} (F : Presheaf CommRingCat X) :
          Presheaf CommRingCat X

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

          Instances For
            source
            🔸 coverage
            noncomputable def TopCat.Presheaf.toTotalQuotientPresheaf {X : TopCat} (F : Presheaf CommRingCat X) :
            F ⟶ F.totalQuotientPresheaf

            The map into the presheaf of total quotient rings

            Instances For
              source
              🔸 coverage
              @[implicit_reducible]
              noncomputable instance TopCat.Presheaf.instEpiCommRingCatToTotalQuotientPresheaf {X : TopCat} (F : Presheaf CommRingCat X) :
              CategoryTheory.Epi F.toTotalQuotientPresheaf
              source
              📐 coverage
              instance TopCat.Presheaf.instMonoCommRingCatToTotalQuotientPresheafPresheaf {X : TopCat} (F : Sheaf CommRingCat X) :
              CategoryTheory.Mono F.presheaf.toTotalQuotientPresheaf
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instNatCastHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              NatCast (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instIntCastHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              IntCast (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instZeroHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              Zero (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instOneHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              One (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instNegHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              Neg (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instSubHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              Sub (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instAddHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              Add (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instMulHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              Mul (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instSMulNatHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              SMul ℕ (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instSMulIntHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              SMul ℤ (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instPowHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrierNat (X : TopCat) (R : TopCommRingCat) :
              Pow (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R) ℕ
              source
              🔸 coverage
              @[implicit_reducible]
              instance TopCat.instCommRingHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier (X : TopCat) (R : TopCommRingCat) :
              CommRing (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
              source
              🔸 coverage
              def TopCat.continuousFunctions (X : TopCatᵒᵖ) (R : TopCommRingCat) :
              CommRingCat

              The (bundled) commutative ring of continuous functions from a topological space to a topological commutative ring, with pointwise multiplication.

              Instances For
                source
                🔸 coverage
                def TopCat.continuousFunctions.pullback {X Y : TopCatᵒᵖ} (f : X ⟶ Y) (R : TopCommRingCat) :
                continuousFunctions X R ⟶ continuousFunctions Y R

                Pulling back functions into a topological ring along a continuous map is a ring homomorphism.

                Instances For
                  source
                  🔸 coverage
                  def TopCat.continuousFunctions.map (X : TopCatᵒᵖ) {R S : TopCommRingCat} (φ : R ⟶ S) :
                  continuousFunctions X R ⟶ continuousFunctions X S

                  A homomorphism of topological rings can be postcomposed with functions from a source space X; this is a ring homomorphism (with respect to the pointwise ring operations on functions).

                  Instances For
                    source
                    🔸 coverage
                    def TopCat.commRingYoneda :
                    CategoryTheory.Functor TopCommRingCat (CategoryTheory.Functor TopCatᵒᵖ CommRingCat)

                    An upgraded version of the Yoneda embedding, observing that the continuous maps from X : TopCat to R : TopCommRingCat form a commutative ring, functorial in both X and R.

                    Instances For
                      source
                      🔸 coverage
                      def TopCat.presheafToTopCommRing (X : TopCat) (T : TopCommRingCat) :
                      Presheaf CommRingCat X

                      The presheaf (of commutative rings), consisting of functions on an open set U ⊆ X with values in some topological commutative ring T.

                      For example, we could construct the presheaf of continuous complex-valued functions of X as

                      presheafToTopCommRing X (TopCommRingCat.of ℂ)

                      (this requires import Topology.Instances.Complex).

                      Instances For
                        source
                        🔸 coverage
                        @[implicit_reducible]
                        noncomputable instance TopCat.Presheaf.algebra_section_stalk {X : TopCat} (F : Presheaf CommRingCat X) {U : TopologicalSpace.Opens ↑X} (x : ↥U) :
                        Algebra ↑(F.obj (Opposite.op U)) ↑(F.stalk ↑x)
                        source
                        📐 coverage
                        @[simp]
                        theorem TopCat.Presheaf.stalk_open_algebraMap {X : TopCat} (F : Presheaf CommRingCat X) {U : TopologicalSpace.Opens ↑X} (x : ↥U) :
                        algebraMap ↑(F.obj (Opposite.op U)) ↑(F.stalk ↑x) = CommRingCat.Hom.hom (F.germ U ↑x ⋯)
                        source
                        🔸 coverage
                        noncomputable def TopCat.Sheaf.objSupIsoProdEqLocus {X : TopCat} (F : Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) :
                        F.obj.obj (Opposite.op (U ⊔ V)) ≅ CommRingCat.of ↥(((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.fst ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))).eqLocus ((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.snd ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))))

                        F(U ⊔ V) is isomorphic to the eq_locus of the two maps F(U) × F(V) ⟶ F(U ⊓ V).

                        Instances For
                          source
                          📐 coverage
                          theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst {X : TopCat} (F : Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) (x : ↑(F.obj.obj (Opposite.op (U ⊔ V)))) :
                          (↑((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).hom) x)).1 = (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) x
                          source
                          📐 coverage
                          theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd {X : TopCat} (F : Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) (x : ↑(F.obj.obj (Opposite.op (U ⊔ V)))) :
                          (↑((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).hom) x)).2 = (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) x
                          source
                          📐 coverage
                          theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst {X : TopCat} (F : Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) (x : ↑(CommRingCat.of ↥(((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.fst ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))).eqLocus ((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.snd ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V))))))) :
                          (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = (↑x).1
                          source
                          📐 coverage
                          theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd {X : TopCat} (F : Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) (x : ↑(CommRingCat.of ↥(((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.fst ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))).eqLocus ((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.snd ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V))))))) :
                          (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = (↑x).2
                          source
                          📐 coverage
                          theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff {X : TopCat} (F : Sheaf CommRingCat X) {U V W UW VW : TopologicalSpace.Opens ↑X} (e : W ≤ U ⊔ V) (x : ↑(CommRingCat.of ↥(((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.fst ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))).eqLocus ((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.snd ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V))))))) (y : ↑(F.obj.obj (Opposite.op W))) (h₁ : UW = U ⊓ W) (h₂ : VW = V ⊓ W) :
                          (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE e).op)) ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = y ↔ (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) (↑x).1 = (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) y ∧ (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) (↑x).2 = (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)) y