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 asubmonoid_presheaf.total_quotient_presheaf: The presheaf of total quotient rings.
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)
- obj : Π (U : (topological_space.opens ↥X)ᵒᵖ), submonoid ↥(F.obj U)
- map : ∀ {U V : (topological_space.opens ↥X)ᵒᵖ} (i : U ⟶ V), self.obj U ≤ submonoid.comap (F.map i) (self.obj V)
A subpresheaf with a submonoid structure on each of the components.
Instances for Top.presheaf.submonoid_presheaf
- Top.presheaf.submonoid_presheaf.has_sizeof_inst
- Top.presheaf.submonoid_presheaf.inhabited
@[protected]
noncomputable
def
Top.presheaf.submonoid_presheaf.localization_presheaf
{X : Top}
{F : Top.presheaf CommRing X}
(G : F.submonoid_presheaf) :
The localization of a presheaf of CommRings with respect to a submonoid_presheaf.
Equations
- G.localization_presheaf = {obj := λ (U : (topological_space.opens ↥X)ᵒᵖ), CommRing.of (localization (G.obj U)), map := λ (U V : (topological_space.opens ↥X)ᵒᵖ) (i : U ⟶ V), CommRing.of_hom (is_localization.map (localization (G.obj V)) (F.map i) _), map_id' := _, map_comp' := _}
def
Top.presheaf.submonoid_presheaf.to_localization_presheaf
{X : Top}
{F : Top.presheaf CommRing X}
(G : F.submonoid_presheaf) :
The map into the localization presheaf.
Equations
- G.to_localization_presheaf = {app := λ (U : (topological_space.opens ↥X)ᵒᵖ), CommRing.of_hom (algebra_map ↥(F.obj U) (localization (G.obj U))), naturality' := _}
Instances for Top.presheaf.submonoid_presheaf.to_localization_presheaf
@[protected, instance]
@[simp]
theorem
Top.presheaf.submonoid_presheaf_of_stalk_obj
{X : Top}
(F : Top.presheaf CommRing X)
(S : Π (x : ↥X), submonoid ↥(F.stalk x))
(U : (topological_space.opens ↥X)ᵒᵖ) :
(F.submonoid_presheaf_of_stalk S).obj U = ⨅ (x : ↥(opposite.unop U)), submonoid.comap (F.germ x) (S ↑x)
noncomputable
def
Top.presheaf.submonoid_presheaf_of_stalk
{X : Top}
(F : Top.presheaf CommRing 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
- F.submonoid_presheaf_of_stalk S = {obj := λ (U : (topological_space.opens ↥X)ᵒᵖ), ⨅ (x : ↥(opposite.unop U)), submonoid.comap (F.germ x) (S ↑x), map := _}
@[protected, instance]
noncomputable
def
Top.presheaf.submonoid_presheaf.inhabited
{X : Top}
(F : Top.presheaf CommRing X) :
Equations
- Top.presheaf.submonoid_presheaf.inhabited F = {default := F.submonoid_presheaf_of_stalk (λ (_x : ↥X), ⊥)}
The localization of a presheaf of CommRings at locally non-zero-divisor sections.
Equations
- F.total_quotient_presheaf = (F.submonoid_presheaf_of_stalk (λ (x : ↥X), non_zero_divisors ↥(F.stalk x))).localization_presheaf
@[protected, instance]
The map into the presheaf of total quotient rings
Equations
- F.to_total_quotient_presheaf = (F.submonoid_presheaf_of_stalk (λ (x : ↥X), non_zero_divisors ↥(F.stalk x))).to_localization_presheaf
Instances for Top.presheaf.to_total_quotient_presheaf
@[protected, instance]