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)

• obj : (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Submonoid ((CategoryTheory.forget C).obj (F.obj U))
• map : ∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V), TopCat.Presheaf.SubmonoidPresheaf.obj s U ≤ Submonoid.comap (F.map i) (TopCat.Presheaf.SubmonoidPresheaf.obj s V)

A subpresheaf with a submonoid structure on each of the components.

noncomputable def TopCat.Presheaf.SubmonoidPresheaf.localizationPresheaf {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : TopCat.Presheaf.SubmonoidPresheaf F) : TopCat.Presheaf CommRingCat X

The localization of a presheaf of CommRings with respect to a SubmonoidPresheaf.

instance TopCat.Presheaf.instAlgebraObjCommRingCatToQuiverToCategoryStructInstCommRingCatLargeCategoryTypeTypesToPrefunctorForgetInstConcreteCategoryCommRingCatInstCommRingCatLargeCategoryObjOppositeOpensαTopologicalSpaceTopologicalSpace_coeToQuiverToCategoryStructOppositeSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensToPrefunctorCommRingLocalizationPresheafToCommSemiringInstCommRing'ToSemiringInstCommRingα {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : TopCat.Presheaf.SubmonoidPresheaf F) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : Algebra ((CategoryTheory.forget CommRingCat).obj (F.obj U)) ↑((TopCat.Presheaf.SubmonoidPresheaf.localizationPresheaf G).obj U)

instance TopCat.Presheaf.instIsLocalizationObjCommRingCatToQuiverToCategoryStructInstCommRingCatLargeCategoryTypeTypesToPrefunctorForgetInstConcreteCategoryCommRingCatInstCommRingCatLargeCategoryObjOppositeOpensαTopologicalSpaceTopologicalSpace_coeToQuiverToCategoryStructOppositeSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensToPrefunctorToCommSemiringInstCommRing'ObjToMulOneClassToMulZeroOneClassToNonAssocSemiringToSemiringToMonoidHomClassHomCommRingInstCommRingαInstRingHomClassLocalizationPresheafInstAlgebraObjCommRingCatToQuiverToCategoryStructInstCommRingCatLargeCategoryTypeTypesToPrefunctorForgetInstConcreteCategoryCommRingCatInstCommRingCatLargeCategoryObjOppositeOpensαTopologicalSpaceTopologicalSpace_coeToQuiverToCategoryStructOppositeSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensToPrefunctorCommRingLocalizationPresheafToCommSemiringInstCommRing'ToSemiringInstCommRingα {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : TopCat.Presheaf.SubmonoidPresheaf F) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : IsLocalization (TopCat.Presheaf.SubmonoidPresheaf.obj G U) ↑((TopCat.Presheaf.SubmonoidPresheaf.localizationPresheaf G).obj U)

@[simp]

theorem TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf_app {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : TopCat.Presheaf.SubmonoidPresheaf F) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf G).app U = CommRingCat.ofHom (algebraMap (↑(F.obj U)) (Localization (TopCat.Presheaf.SubmonoidPresheaf.obj G U)))

def TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : TopCat.Presheaf.SubmonoidPresheaf F) : F ⟶ TopCat.Presheaf.SubmonoidPresheaf.localizationPresheaf G

The map into the localization presheaf.

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

@[simp]

theorem TopCat.Presheaf.submonoidPresheafOfStalk_obj {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (S : (x : ↑X) → Submonoid ↑(TopCat.Presheaf.stalk F x)) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : TopCat.Presheaf.SubmonoidPresheaf.obj (TopCat.Presheaf.submonoidPresheafOfStalk F S) U = ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (TopCat.Presheaf.germ F x) (S ↑x)

noncomputable def TopCat.Presheaf.submonoidPresheafOfStalk {X : TopCat} (F : TopCat.Presheaf CommRingCat X) (S : (x : ↑X) → Submonoid ↑(TopCat.Presheaf.stalk F x)) : TopCat.Presheaf.SubmonoidPresheaf F

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.

noncomputable instance TopCat.Presheaf.instInhabitedSubmonoidPresheafCommRingCatInstCommRingCatLargeCategoryInstConcreteCategoryCommRingCatInstCommRingCatLargeCategoryToMulOneClassObjToQuiverToCategoryStructTypeTypesToPrefunctorForgetToMulZeroOneClassToNonAssocSemiringToSemiringToCommSemiringInstCommRing'ToMonoidHomClassHomαCommRingInstCommRingαInstRingHomClass {X : TopCat} (F : TopCat.Presheaf CommRingCat X) : Inhabited (TopCat.Presheaf.SubmonoidPresheaf F)

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.

noncomputable def TopCat.Presheaf.toTotalQuotientPresheaf {X : TopCat} (F : TopCat.Presheaf CommRingCat X) : F ⟶ TopCat.Presheaf.totalQuotientPresheaf F

The map into the presheaf of total quotient rings

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

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