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).toPrefunctor.obj X)] [∀ (X Y : C), MonoidHomClass (X ⟶ Y) ((CategoryTheory.forget C).toPrefunctor.obj X) ((CategoryTheory.forget C).toPrefunctor.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).toPrefunctor.obj (F.toPrefunctor.obj U))
• map : ∀ {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V), self.obj U ≤ Submonoid.comap (F.toPrefunctor.map i) (self.obj V)

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.

Equations

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

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).toPrefunctor.obj (F.toPrefunctor.obj U)) ↑((TopCat.Presheaf.SubmonoidPresheaf.localizationPresheaf G).toPrefunctor.obj U)

Equations

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

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

Equations

• (_ : IsLocalization (G.obj U) ↑((TopCat.Presheaf.SubmonoidPresheaf.localizationPresheaf G).toPrefunctor.obj U)) = (_ : IsLocalization (G.obj U) (Localization (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.toPrefunctor.obj U)) (Localization (G.obj 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.

Equations

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

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

Equations

• (_ : CategoryTheory.Epi (TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf G)) = (_ : 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.submonoidPresheafOfStalk F S).obj U = ⨅ (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.

Equations

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

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

Equations

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

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

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

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

Equations

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

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

Equations

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

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

Equations

• (_ : CategoryTheory.Mono (TopCat.Presheaf.toTotalQuotientPresheaf (TopCat.Sheaf.presheaf F))) = (_ : CategoryTheory.Mono (TopCat.Presheaf.toTotalQuotientPresheaf (TopCat.Sheaf.presheaf F)))