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.

@[reducible, inline]

abbrev TopCat.Presheaf.restrictOpenCommRingCat {X : TopCat} {F : TopCat.Presheaf CommRingCat X} {V : TopologicalSpace.Opens ↑X} (f : ↑(F.obj (Opposite.op V))) (U : TopologicalSpace.Opens ↑X) (e : U ≤ V := by restrict_tac) : ↑(F.obj (Opposite.op U))

Specialize restrictOpen to CommRingCat because inferring C := CommRingCat isn't reliable. 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

• TopCat.Presheaf.restrictOpenCommRingCat f U e = TopCat.Presheaf.restrictOpen f U e

def AlgebraicGeometry.«term_|_ᵣ_» : Lean.TrailingParserDescr

Notation for TopCat.Presheaf.restrictOpenCommRingCat.

Equations

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

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

theorem CommRingCat.presheaf_restrict_restrict (X : TopCat) {F : TopCat.Presheaf CommRingCat X} {U V W : TopologicalSpace.Opens ↑X} (e₁ : U ≤ V := by restrict_tac) (e₂ : V ≤ W := by restrict_tac) (f : ↑(F.obj (Opposite.op W))) : TopCat.Presheaf.restrictOpenCommRingCat (TopCat.Presheaf.restrictOpenCommRingCat f V e₂) U e₁ = TopCat.Presheaf.restrictOpenCommRingCat f U ⋯

structure TopCat.Presheaf.SubmonoidPresheaf {X : TopCat} (F : TopCat.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)
• map {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V) : self.obj U ≤ Submonoid.comap (F.map i).hom (self.obj V)

noncomputable def TopCat.Presheaf.SubmonoidPresheaf.localizationPresheaf {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) : TopCat.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.instAlgebraCarrierObjOppositeOpensαTopologicalSpaceCommRingCatLocalizationPresheaf {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : Algebra ↑(F.obj U) ↑(G.localizationPresheaf.obj U)

Equations

• TopCat.Presheaf.instAlgebraCarrierObjOppositeOpensαTopologicalSpaceCommRingCatLocalizationPresheaf G U = inferInstance

instance TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensαTopologicalSpaceCommRingCatObjLocalizationPresheaf {X : TopCat} {F : TopCat.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 : TopCat.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 : TopCat.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 : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) : CategoryTheory.Epi G.toLocalizationPresheaf

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

• 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 := ⋯ }

@[simp]

theorem TopCat.Presheaf.submonoidPresheafOfStalk_obj {X : TopCat} (F : TopCat.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 (F.germ (Opposite.unop U) ↑x ⋯).hom (S ↑x)

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

Equations

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

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

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

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)

instance TopCat.continuousFunctions.instCommRingHomUnopObjTopCommRingCatForget₂ (X : TopCatᵒᵖ) (R : TopCommRingCat) : CommRing (Opposite.unop X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

Equations

• TopCat.continuousFunctions.instCommRingHomUnopObjTopCommRingCatForget₂ X R = inferInstanceAs (CommRing C(↑(Opposite.unop X), ↑((CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)))

def TopCat.continuousFunctions.pullback {X Y : TopCatᵒᵖ} (f : X ⟶ Y) (R : TopCommRingCat) : TopCat.continuousFunctions X R ⟶ TopCat.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) : TopCat.continuousFunctions X R ⟶ TopCat.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) : TopCat.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 : TopCat.Presheaf CommRingCat X) {U : TopologicalSpace.Opens ↑X} (x : ↥U) : Algebra ↑(F.obj (Opposite.op U)) ↑(F.stalk ↑x)

Equations

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

@[simp]

theorem TopCat.Presheaf.stalk_open_algebraMap {X : TopCat} (F : TopCat.Presheaf CommRingCat X) {U : TopologicalSpace.Opens ↑X} (x : ↥U) : algebraMap ↑(F.obj (Opposite.op U)) ↑(F.stalk ↑x) = (F.germ U ↑x ⋯).hom

def TopCat.Sheaf.objSupIsoProdEqLocus {X : TopCat} (F : TopCat.Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) : F.val.obj (Opposite.op (U ⊔ V)) ≅ CommRingCat.of ↥(((F.val.map (CategoryTheory.homOfLE ⋯).op).hom.comp (RingHom.fst ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))).eqLocus ((F.val.map (CategoryTheory.homOfLE ⋯).op).hom.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 : TopCat.Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X) (x : ↑(F.val.obj (Opposite.op (U ⊔ V)))) : (↑((F.objSupIsoProdEqLocus U V).hom.hom x)).1 = (F.val.map (CategoryTheory.homOfLE ⋯).op).hom x

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

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

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

theorem TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff {X : TopCat} (F : TopCat.Sheaf CommRingCat X) {U V W UW VW : TopologicalSpace.Opens ↑X} (e : W ≤ U ⊔ V) (x : ↑(CommRingCat.of ↥(((F.val.map (CategoryTheory.homOfLE ⋯).op).hom.comp (RingHom.fst ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))).eqLocus ((F.val.map (CategoryTheory.homOfLE ⋯).op).hom.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) : (F.val.map (CategoryTheory.homOfLE e).op).hom ((F.objSupIsoProdEqLocus U V).inv.hom x) = y ↔ (F.val.map (CategoryTheory.homOfLE ⋯).op).hom (↑x).1 = (F.val.map (CategoryTheory.homOfLE ⋯).op).hom y ∧ (F.val.map (CategoryTheory.homOfLE ⋯).op).hom (↑x).2 = (F.val.map (CategoryTheory.homOfLE ⋯).op).hom y