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

• SubmonoidPresheaf : A subpresheaf with a submonoid structure on each of the components.
• LocalizationPresheaf : The localization of a presheaf of commrings at a SubmonoidPresheaf.
• TotalQuotientPresheaf : The presheaf of total quotient rings.

As more results accumulate, please consider splitting this file.

References

• https://stacks.math.columbia.edu/tag/0073

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.

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.

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.

• obj (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : Submonoid ↑(F.obj U)

  The submonoid structure for each component

• map {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V) : self.obj U ≤ Submonoid.comap (CommRingCat.Hom.hom (F.map i)) (self.obj V)

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.

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)

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)

def TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf {X : TopCat} {F : Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) : F ⟶ G.localizationPresheaf

The map into the localization presheaf.

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

instance TopCat.Presheaf.epi_toLocalizationPresheaf {X : TopCat} {F : Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) : CategoryTheory.Epi G.toLocalizationPresheaf

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.

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

noncomputable instance TopCat.Presheaf.instInhabitedSubmonoidPresheaf {X : TopCat} (F : Presheaf CommRingCat X) : Inhabited F.SubmonoidPresheaf

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.

noncomputable def TopCat.Presheaf.toTotalQuotientPresheaf {X : TopCat} (F : Presheaf CommRingCat X) : F ⟶ F.totalQuotientPresheaf

The map into the presheaf of total quotient rings

instance TopCat.Presheaf.instEpiCommRingCatToTotalQuotientPresheaf {X : TopCat} (F : Presheaf CommRingCat X) : CategoryTheory.Epi F.toTotalQuotientPresheaf

instance TopCat.Presheaf.instMonoCommRingCatToTotalQuotientPresheafPresheaf {X : TopCat} (F : Sheaf CommRingCat X) : CategoryTheory.Mono F.presheaf.toTotalQuotientPresheaf

instance TopCat.instNatCastHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : NatCast (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

instance TopCat.instIntCastHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : IntCast (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

instance TopCat.instZeroHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : Zero (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

instance TopCat.instOneHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : One (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

instance TopCat.instNegHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : Neg (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

instance TopCat.instSubHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : Sub (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

instance TopCat.instAddHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : Add (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

instance TopCat.instMulHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : Mul (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

instance TopCat.instSMulNatHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : SMul ℕ (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

instance TopCat.instSMulIntHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : SMul ℤ (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

instance TopCat.instPowHomObjTopCommRingCatForget₂Nat (X : TopCat) (R : TopCommRingCat) : Pow (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R) ℕ

instance TopCat.instCommRingHomObjTopCommRingCatForget₂ (X : TopCat) (R : TopCommRingCat) : CommRing (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

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.

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.

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).

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.

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).

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)

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

def TopCat.Sheaf.objSupIsoProdEqLocus {X : TopCat} (F : Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) : F.val.obj (Opposite.op (U ⊔ V)) ≅ CommRingCat.of ↥(((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.fst ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))).eqLocus ((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.snd ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))))

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

theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst {X : TopCat} (F : Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) (x : ↑(F.val.obj (Opposite.op (U ⊔ V)))) : (↑((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).hom) x)).1 = (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) x

theorem TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd {X : TopCat} (F : Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) (x : ↑(F.val.obj (Opposite.op (U ⊔ V)))) : (↑((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).hom) x)).2 = (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) x

theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst {X : TopCat} (F : Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) (x : ↑(CommRingCat.of ↥(((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.fst ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))).eqLocus ((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.snd ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V))))))) : (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = (↑x).1

theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd {X : TopCat} (F : Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) (x : ↑(CommRingCat.of ↥(((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.fst ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))).eqLocus ((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.snd ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V))))))) : (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = (↑x).2

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.val.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.fst ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))).eqLocus ((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp (RingHom.snd ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V))))))) (y : ↑(F.val.obj (Opposite.op W))) (h₁ : UW = U ⊓ W) (h₂ : VW = V ⊓ W) : (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE e).op)) ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = y ↔ (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) (↑x).1 = (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) y ∧ (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) (↑x).2 = (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) y