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.

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• TopCat.Presheaf.instAlgebraCarrierObjOppositeOpensCarrierCommRingCatLocalizationPresheaf G U = inferInstance

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.

Equations

• G.toLocalizationPresheaf = { app := fun (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) => CommRingCat.ofHom (algebraMap (↑(F.obj U)) (Localization (G.obj U))), naturality := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• F.instInhabitedSubmonoidPresheaf = { default := F.submonoidPresheafOfStalk fun (x : ↑X) => ⊥ }

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.

Equations

• F.totalQuotientPresheaf = (F.submonoidPresheafOfStalk fun (x : ↑X) => nonZeroDivisors ↑(F.stalk x)).localizationPresheaf

noncomputable def TopCat.Presheaf.toTotalQuotientPresheaf {X : TopCat} (F : 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

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

Equations

• ⋯ = ⋯

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)

Equations

• X.instNatCastHomObjTopCommRingCatForget₂ R = { natCast := fun (n : ℕ) => TopCat.ofHom ↑n }

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

Equations

• X.instIntCastHomObjTopCommRingCatForget₂ R = { intCast := fun (n : ℤ) => TopCat.ofHom ↑n }

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

Equations

• X.instZeroHomObjTopCommRingCatForget₂ R = { zero := TopCat.ofHom 0 }

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

Equations

• X.instOneHomObjTopCommRingCatForget₂ R = { one := TopCat.ofHom 1 }

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

Equations

• X.instNegHomObjTopCommRingCatForget₂ R = { neg := fun (f : X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R) => TopCat.ofHom (-TopCat.Hom.hom f) }

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

Equations

• X.instSubHomObjTopCommRingCatForget₂ R = { sub := fun (f g : X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R) => TopCat.ofHom (TopCat.Hom.hom f - TopCat.Hom.hom g) }

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

Equations

• X.instAddHomObjTopCommRingCatForget₂ R = { add := fun (f g : X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R) => TopCat.ofHom (TopCat.Hom.hom f + TopCat.Hom.hom g) }

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

Equations

• X.instMulHomObjTopCommRingCatForget₂ R = { mul := fun (f g : X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R) => TopCat.ofHom (TopCat.Hom.hom f * TopCat.Hom.hom g) }

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

Equations

• X.instSMulNatHomObjTopCommRingCatForget₂ R = { smul := fun (n : ℕ) (f : X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R) => TopCat.ofHom (n • TopCat.Hom.hom f) }

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

Equations

• X.instSMulIntHomObjTopCommRingCatForget₂ R = { smul := fun (n : ℤ) (f : X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R) => TopCat.ofHom (n • TopCat.Hom.hom f) }

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

Equations

• X.instPowHomObjTopCommRingCatForget₂Nat R = { pow := fun (f : X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R) (n : ℕ) => TopCat.ofHom (TopCat.Hom.hom f ^ n) }

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

Equations

• X.instCommRingHomObjTopCommRingCatForget₂ R = Function.Injective.commRing CategoryTheory.ConcreteCategory.hom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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.

Equations

• TopCat.continuousFunctions X R = CommRingCat.of (Opposite.unop X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• X.presheafToTopCommRing T = (TopologicalSpace.Opens.toTopCat X).op.comp (TopCat.commRingYoneda.obj T)

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)

Equations

• F.algebra_section_stalk x = (CommRingCat.Hom.hom (F.germ U ↑x ⋯)).toAlgebra

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

Equations

• One or more equations did not get rendered due to their size.

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