mathlib3 documentation


Operations on sheaves #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definition #

structure Top.presheaf.submonoid_presheaf {X : Top} {C : Type u} [category_theory.category C] [category_theory.concrete_category C] [Π (X : C), mul_one_class X] [Π (X Y : C), monoid_hom_class (X Y) X Y] (F : Top.presheaf C X) :
Type (max u_1 w)

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

Instances for Top.presheaf.submonoid_presheaf

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


The map into the localization presheaf.

Instances for Top.presheaf.submonoid_presheaf.to_localization_presheaf

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.


The localization of a presheaf of CommRings at locally non-zero-divisor sections.