mathlib3documentation

algebraic_geometry.sheafed_space

Sheafed spaces #

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

Introduces the category of topological spaces equipped with a sheaf (taking values in an arbitrary target category C.)

We further describe how to apply functors and natural transformations to the values of the presheaves.

structure algebraic_geometry.SheafedSpace (C : Type u)  :
Type (max u (v+1))
• to_PresheafedSpace :
• is_sheaf :

A SheafedSpace C is a topological space equipped with a sheaf of Cs.

Instances for algebraic_geometry.SheafedSpace
@[protected, instance]
Equations

Extract the sheaf C (X : Top) from a SheafedSpace C.

Equations
@[simp]
@[simp]
theorem algebraic_geometry.SheafedSpace.mk_coe {C : Type u} (carrier : Top) (presheaf : carrier) (h : {carrier := carrier, presheaf := presheaf}.presheaf.is_sheaf) :
{to_PresheafedSpace := {carrier := carrier, presheaf := presheaf}, is_sheaf := h} = carrier
@[protected, instance]
Equations

The trivial unit valued sheaf on any topological space.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]

Forgetting the sheaf condition is a functor from SheafedSpace C to PresheafedSpace C.

Equations
Instances for algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace
@[protected, instance]
@[simp]
@[simp]
theorem algebraic_geometry.SheafedSpace.comp_base {C : Type u} {X Y Z : algebraic_geometry.SheafedSpace C} (f : X Y) (g : Y Z) :
(f g).base = f.base g.base
@[simp]
theorem algebraic_geometry.SheafedSpace.comp_c_app {C : Type u} {X Y Z : algebraic_geometry.SheafedSpace C} (α : X Y) (β : Y Z) (U : ᵒᵖ) :
β).c.app U = β.c.app U α.c.app (opposite.op (opposite.unop U)))
theorem algebraic_geometry.SheafedSpace.comp_c_app' {C : Type u} {X Y Z : algebraic_geometry.SheafedSpace C} (α : X Y) (β : Y Z)  :
β).c.app (opposite.op U) = β.c.app (opposite.op U) α.c.app (opposite.op U))
theorem algebraic_geometry.SheafedSpace.congr_app {C : Type u} {X Y : algebraic_geometry.SheafedSpace C} {α β : X Y} (h : α = β) (U : ᵒᵖ) :
α.c.app U =

The forgetful functor from SheafedSpace to Top.

Equations
Instances for algebraic_geometry.SheafedSpace.forget

The restriction of a sheafed space along an open embedding into the space.

Equations

The restriction of a sheafed space X to the top subspace is isomorphic to X itself.

Equations

The global sections, notated Gamma.

Equations
@[simp]
@[simp]
theorem algebraic_geometry.SheafedSpace.Γ_map {C : Type u} {X Y : ᵒᵖ} (f : X Y) :
@[protected, instance]
@[protected, instance]
Equations