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.
A subpresheaf with a submonoid structure on each of the components.
- obj : (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Submonoid ((CategoryTheory.forget C).obj (F.obj U))
- map : ∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V), self.obj U ≤ Submonoid.comap (F.map i) (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
Equations
Equations
- ⋯ = ⋯
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
Equations
- ⋯ = ⋯
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 ⋯) (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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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 = RingHom.toAlgebra (F.germ U ↑x ⋯)
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.