# mathlib3documentation

topology.sheaves.operations

# Operations on sheaves #

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

## Main definition #

• submonoid_presheaf : A subpresheaf with a submonoid structure on each of the components.
• localization_presheaf : The localization of a presheaf of commrings at a submonoid_presheaf.
• total_quotient_presheaf : The presheaf of total quotient rings.
structure Top.presheaf.submonoid_presheaf {X : Top} {C : Type u} [Π (X : C), ] [Π (X Y : C), monoid_hom_class (X Y) X Y] (F : X) :
Type (max u_1 w)

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

Instances for Top.presheaf.submonoid_presheaf
@[protected]

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

Equations

The map into the localization presheaf.

Equations
Instances for Top.presheaf.submonoid_presheaf.to_localization_presheaf
@[protected, instance]
@[simp]
theorem Top.presheaf.submonoid_presheaf_of_stalk_obj {X : Top} (F : X) (S : Π (x : X), submonoid (F.stalk x)) (U : ᵒᵖ) :
U = (x : (opposite.unop U)), submonoid.comap (F.germ x) (S x)
noncomputable def Top.presheaf.submonoid_presheaf_of_stalk {X : Top} (F : X) (S : Π (x : X), submonoid (F.stalk x)) :

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
@[protected, instance]
noncomputable def Top.presheaf.submonoid_presheaf.inhabited {X : Top} (F : X) :
Equations
noncomputable def Top.presheaf.total_quotient_presheaf {X : Top} (F : X) :

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

Equations
@[protected, instance]
noncomputable def Top.presheaf.to_total_quotient_presheaf {X : Top} (F : X) :

The map into the presheaf of total quotient rings

Equations
Instances for Top.presheaf.to_total_quotient_presheaf
@[protected, instance]