mathlib docs: algebraic_geometry.sheafed

source

structure algebraic_geometry.SheafedSpace (C : Type u) [category_theory.category C] [category_theory.limits.has_products C] :

Type (max u (v+1))

to_PresheafedSpace : algebraic_geometry.PresheafedSpace C
sheaf_condition : c.to_PresheafedSpace.presheaf.sheaf_condition

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

source

@[instance]

def algebraic_geometry.SheafedSpace.coe_carrier {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] :

has_coe (algebraic_geometry.SheafedSpace C) Top

Equations

algebraic_geometry.SheafedSpace.coe_carrier = {coe := λ (X : algebraic_geometry.SheafedSpace C), X.to_PresheafedSpace.carrier}

source

def algebraic_geometry.SheafedSpace.sheaf {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (X : algebraic_geometry.SheafedSpace C) :

Top.sheaf C ↑X

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

Equations

X.sheaf = {presheaf := X.to_PresheafedSpace.presheaf, sheaf_condition := X.sheaf_condition}

source

@[simp]

theorem algebraic_geometry.SheafedSpace.as_coe {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (X : algebraic_geometry.SheafedSpace C) :

X.to_PresheafedSpace.carrier = ↑X

source

@[simp]

theorem algebraic_geometry.SheafedSpace.mk_coe {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (carrier : Top) (presheaf : Top.presheaf C carrier) (h : {carrier := carrier, presheaf := presheaf}.presheaf.sheaf_condition) :

↑{to_PresheafedSpace := {carrier := carrier, presheaf := presheaf}, sheaf_condition := h} = carrier

source

@[instance]

def algebraic_geometry.SheafedSpace.topological_space {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (X : algebraic_geometry.SheafedSpace C) :

topological_space ↥X

Equations

X.topological_space = X.to_PresheafedSpace.carrier.str

source

def algebraic_geometry.SheafedSpace.punit (X : Top) :

algebraic_geometry.SheafedSpace (category_theory.discrete punit)

The trivial punit valued sheaf on any topological space.

Equations

source

@[instance]

def algebraic_geometry.SheafedSpace.inhabited :

inhabited (algebraic_geometry.SheafedSpace (category_theory.discrete punit))

Equations

algebraic_geometry.SheafedSpace.inhabited = {default := algebraic_geometry.SheafedSpace.punit (Top.of pempty)}

source

@[instance]

def algebraic_geometry.SheafedSpace.category_theory.category {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] :

category_theory.category (algebraic_geometry.SheafedSpace C)

Equations

algebraic_geometry.SheafedSpace.category_theory.category = show category_theory.category (category_theory.induced_category (algebraic_geometry.PresheafedSpace C) algebraic_geometry.SheafedSpace.to_PresheafedSpace), from category_theory.induced_category.category algebraic_geometry.SheafedSpace.to_PresheafedSpace

source

def algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] :

algebraic_geometry.SheafedSpace C ⥤ algebraic_geometry.PresheafedSpace C

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

Equations

algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace = category_theory.induced_functor algebraic_geometry.SheafedSpace.to_PresheafedSpace

source

@[simp]

theorem algebraic_geometry.SheafedSpace.id_base {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (X : algebraic_geometry.SheafedSpace C) :

(𝟙 X).base = 𝟙 ↑X

source

@[simp]

theorem algebraic_geometry.SheafedSpace.id_c_app {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (X : algebraic_geometry.SheafedSpace C) (U : (topological_space.opens ↥(X.to_PresheafedSpace.carrier))ᵒᵖ) :

(𝟙 X).c.app U = category_theory.eq_to_hom _

source

@[simp]

theorem algebraic_geometry.SheafedSpace.comp_base {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] {X Y Z : algebraic_geometry.SheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) :

(f ≫ g).base = f.base ≫ g.base

source

@[simp]

theorem algebraic_geometry.SheafedSpace.comp_c_app {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] {X Y Z : algebraic_geometry.SheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U : (topological_space.opens ↥(Z.to_PresheafedSpace.carrier))ᵒᵖ) :

(α ≫ β).c.app U = β.c.app U ≫ α.c.app (opposite.op ((topological_space.opens.map β.base).obj (opposite.unop U))) ≫ (Top.presheaf.pushforward.comp X.to_PresheafedSpace.presheaf α.base β.base).inv.app U

source

def algebraic_geometry.SheafedSpace.forget (C : Type u) [category_theory.category C] [category_theory.limits.has_products C] :

algebraic_geometry.SheafedSpace C ⥤ Top

The forgetful functor from SheafedSpace to Top.

Equations

algebraic_geometry.SheafedSpace.forget C = {obj := λ (X : algebraic_geometry.SheafedSpace C), ↑X, map := λ (X Y : algebraic_geometry.SheafedSpace C) (f : X ⟶ Y), f.base, map_id' := _, map_comp' := _}

source

def algebraic_geometry.SheafedSpace.restrict {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] {U : Top} (X : algebraic_geometry.SheafedSpace C) (f : U ⟶ ↑X) (h : open_embedding ⇑f) :

algebraic_geometry.SheafedSpace C

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

Equations

X.restrict f h = {to_PresheafedSpace := {carrier := (X.to_PresheafedSpace.restrict f h).carrier, presheaf := (X.to_PresheafedSpace.restrict f h).presheaf}, sheaf_condition := λ (ι : Type v) (𝒰 : ι → topological_space.opens ↥({carrier := (X.to_PresheafedSpace.restrict f h).carrier, presheaf := (X.to_PresheafedSpace.restrict f h).presheaf}.carrier)), ((category_theory.limits.is_limit.postcompose_inv_equiv (Top.presheaf.sheaf_condition_equalizer_products.diagram.iso_of_open_embedding h 𝒰) (Top.presheaf.sheaf_condition_equalizer_products.fork X.to_PresheafedSpace.presheaf (Top.presheaf.sheaf_condition_equalizer_products.cover.of_open_embedding h 𝒰))).inv_fun (X.sheaf_condition (Top.presheaf.sheaf_condition_equalizer_products.cover.of_open_embedding h 𝒰))).of_iso_limit (Top.presheaf.sheaf_condition_equalizer_products.fork.iso_of_open_embedding h 𝒰).symm}

source

def algebraic_geometry.SheafedSpace.Γ {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] :

(algebraic_geometry.SheafedSpace C)ᵒᵖ ⥤ C

The global sections, notated Gamma.

Equations

algebraic_geometry.SheafedSpace.Γ = algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace.op ⋙ algebraic_geometry.PresheafedSpace.Γ

source

theorem algebraic_geometry.SheafedSpace.Γ_def {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] :

algebraic_geometry.SheafedSpace.Γ = algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace.op ⋙ algebraic_geometry.PresheafedSpace.Γ

source

@[simp]

theorem algebraic_geometry.SheafedSpace.Γ_obj {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (X : (algebraic_geometry.SheafedSpace C)ᵒᵖ) :

algebraic_geometry.SheafedSpace.Γ.obj X = (opposite.unop X).to_PresheafedSpace.presheaf.obj (opposite.op ⊤)

source

theorem algebraic_geometry.SheafedSpace.Γ_obj_op {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (X : algebraic_geometry.SheafedSpace C) :

algebraic_geometry.SheafedSpace.Γ.obj (opposite.op X) = X.to_PresheafedSpace.presheaf.obj (opposite.op ⊤)

source

@[simp]

theorem algebraic_geometry.SheafedSpace.Γ_map {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] {X Y : (algebraic_geometry.SheafedSpace C)ᵒᵖ} (f : X ⟶ Y) :

algebraic_geometry.SheafedSpace.Γ.map f = f.unop.c.app (opposite.op ⊤) ≫ (opposite.unop Y).to_PresheafedSpace.presheaf.map (topological_space.opens.le_map_top f.unop.base ⊤).op

source

theorem algebraic_geometry.SheafedSpace.Γ_map_op {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] {X Y : algebraic_geometry.SheafedSpace C} (f : X ⟶ Y) :

algebraic_geometry.SheafedSpace.Γ.map f.op = f.c.app (opposite.op ⊤) ≫ X.to_PresheafedSpace.presheaf.map (topological_space.opens.le_map_top f.base ⊤).op

mathlib documentation

Sheafed spaces