Operations on sheaves

Main definition

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

structure TopCat.Presheaf.SubmonoidPresheaf {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [(X : C) → MulOneClass ((CategoryTheory.forget C).obj X)] [∀ (X Y : C), MonoidHomClass (X ⟶ Y) ((CategoryTheory.forget C).obj X) ((CategoryTheory.forget C).obj Y)] (F : TopCat.Presheaf C X) : Type (max u_1 w)

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)

theorem TopCat.Presheaf.SubmonoidPresheaf.map {X : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [(X : C) → MulOneClass ((CategoryTheory.forget C).obj X)] [∀ (X Y : C), MonoidHomClass (X ⟶ Y) ((CategoryTheory.forget C).obj X) ((CategoryTheory.forget C).obj Y)] {F : TopCat.Presheaf C X} (self : F.SubmonoidPresheaf) {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} {V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V) : self.obj U ≤ Submonoid.comap (F.map i) (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.instAlgebraObjCommRingCatForgetOppositeOpensαTopologicalSpaceCommRingLocalizationPresheaf {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : Algebra ((CategoryTheory.forget CommRingCat).obj (F.obj U)) ↑(G.localizationPresheaf.obj U)

Equations

• TopCat.Presheaf.instAlgebraObjCommRingCatForgetOppositeOpensαTopologicalSpaceCommRingLocalizationPresheaf G U = let_fun this := inferInstance; this

instance TopCat.Presheaf.instIsLocalizationObjCommRingCatForgetOppositeOpensαTopologicalSpaceObjCommRingLocalizationPresheaf {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : IsLocalization (G.obj U) ↑(G.localizationPresheaf.obj U)

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

@[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 : ↥U.unop), Submonoid.comap (F.germ x) (S ↑x)

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 : ↥U.unop), Submonoid.comap (F.germ x) (S ↑x), map := ⋯ }

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

Equations

• F.instInhabitedSubmonoidPresheafCommRingCat = { 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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯