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 aSubmonoidPresheaf.TotalQuotientPresheaf: The presheaf of total quotient rings.
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.
Deprecated: usage of this definition should be replaceable with TopCat.Presheaf.restrictOpen.
Before, we had to specialze restrictOpen to CommRingCat because inferring C := CommRingCat
was not reliable. Unification hints appear to solve that issue.
The following still holds for restrictOpen: instead of unfolding the definition, rewrite with
restrictOpenCommRingCat_apply to ensure the correct coercion to functions is taken.
(The correct fix in the longer term is to redesign concrete categories so we don't use forget
everywhere, but the correct FunLike instance for the morphisms of those categories.)
Equations
Instances For
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.
A subpresheaf with a submonoid structure on each of the components.
- obj (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : Submonoid ↑(F.obj U)
- map {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V) : self.obj U ≤ Submonoid.comap (F.map i).hom (self.obj V)
Instances For
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
The map into the localization presheaf.
Equations
- G.toLocalizationPresheaf = { app := fun (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) => CommRingCat.ofHom (algebraMap (↑(F.obj U)) (Localization (G.obj U))), naturality := ⋯ }
Instances For
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
- F.submonoidPresheafOfStalk S = { obj := fun (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) => ⨅ (x : ↥(Opposite.unop U)), Submonoid.comap (F.germ (Opposite.unop U) ↑x ⋯).hom (S ↑x), map := ⋯ }
Instances For
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
The map into the presheaf of total quotient rings
Equations
- F.toTotalQuotientPresheaf = (F.submonoidPresheafOfStalk fun (x : ↑X) => nonZeroDivisors ↑(F.stalk x)).toLocalizationPresheaf
Instances For
The (bundled) commutative ring of continuous functions from a topological space to a topological commutative ring, with pointwise multiplication.
Equations
Instances For
Pulling back functions into a topological ring along a continuous map is a ring homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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).
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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).
Equations
- X.presheafToTopCommRing T = (TopologicalSpace.Opens.toTopCat X).op.comp (TopCat.commRingYoneda.obj T)
Instances For
Equations
- F.algebra_section_stalk x = (F.germ U ↑x ⋯).hom.toAlgebra
F(U ⊔ V) is isomorphic to the eq_locus of the two maps F(U) × F(V) ⟶ F(U ⊓ V).
Equations
- One or more equations did not get rendered due to their size.