algebraic_geometry.sheafed_space

source

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

Type (max u (v+1))

to_PresheafedSpace : algebraic_geometry.PresheafedSpace C
is_sheaf : self.to_PresheafedSpace.presheaf.is_sheaf

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

Instances for algebraic_geometry.SheafedSpace

algebraic_geometry.SheafedSpace.has_sizeof_inst
algebraic_geometry.SheafedSpace.coe_carrier
algebraic_geometry.SheafedSpace.inhabited
algebraic_geometry.SheafedSpace.category_theory.category
algebraic_geometry.SheafedSpace.category_theory.limits.has_colimits

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.coe_carrier {C : Type u} [category_theory.category 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] (X : algebraic_geometry.SheafedSpace C) :

Top.sheaf C ↑X

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

Equations

X.sheaf = {val := X.to_PresheafedSpace.presheaf, cond := _}

source

@[simp]

theorem algebraic_geometry.SheafedSpace.as_coe {C : Type u} [category_theory.category 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] (carrier : Top) (presheaf : Top.presheaf C carrier) (h : {carrier := carrier, presheaf := presheaf}.presheaf.is_sheaf) :

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

source

@[protected, instance]

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

topological_space ↥X

Equations

X.topological_space = X.to_PresheafedSpace.carrier.str

source

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

algebraic_geometry.SheafedSpace (category_theory.discrete unit)

The trivial unit valued sheaf on any topological space.

Equations

algebraic_geometry.SheafedSpace.unit X = {to_PresheafedSpace := {carrier := (algebraic_geometry.PresheafedSpace.const X {as := punit.star}).carrier, presheaf := (algebraic_geometry.PresheafedSpace.const X {as := punit.star}).presheaf}, is_sheaf := _}

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.inhabited :

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

Equations

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

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.category_theory.category {C : Type u} [category_theory.category 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

@[protected, instance]

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

category_theory.full algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace

source

def algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace {C : Type u} [category_theory.category 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

Instances for algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace

source

@[protected, instance]

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

category_theory.faithful algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace

source

@[protected, instance]

def algebraic_geometry.SheafedSpace.is_PresheafedSpace_iso {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.SheafedSpace C} (f : X ⟶ Y) [category_theory.is_iso f] :

category_theory.is_iso f

source

@[simp]

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

(𝟙 X).base = 𝟙 ↑X

source

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

(𝟙 X).c = category_theory.eq_to_hom _

source

@[simp]

theorem algebraic_geometry.SheafedSpace.id_c_app {C : Type u} [category_theory.category 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] {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] {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)))

source

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

(α ≫ β).c.app (opposite.op U) = β.c.app (opposite.op U) ≫ α.c.app (opposite.op ((topological_space.opens.map β.base).obj U))

source

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

α.c.app U = β.c.app U ≫ X.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom _)

source

def algebraic_geometry.SheafedSpace.forget (C : Type u) [category_theory.category 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' := _}

Instances for algebraic_geometry.SheafedSpace.forget

source

def algebraic_geometry.SheafedSpace.restrict {C : Type u} [category_theory.category 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 h = {to_PresheafedSpace := {carrier := (X.to_PresheafedSpace.restrict h).carrier, presheaf := (X.to_PresheafedSpace.restrict h).presheaf}, is_sheaf := _}

source

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

X.restrict _ ≅ X

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

Equations

X.restrict_top_iso = algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace.preimage_iso X.to_PresheafedSpace.restrict_top_iso

source

def algebraic_geometry.SheafedSpace.Γ {C : Type u} [category_theory.category 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] :

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] (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] (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] {X Y : (algebraic_geometry.SheafedSpace C)ᵒᵖ} (f : X ⟶ Y) :

algebraic_geometry.SheafedSpace.Γ.map f = f.unop.c.app (opposite.op ⊤)

source

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

algebraic_geometry.SheafedSpace.Γ.map f.op = f.c.app (opposite.op ⊤)

source

@[protected, instance]

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

category_theory.creates_colimits algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace

Equations

algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace.category_theory.creates_colimits = {creates_colimits_of_shape := λ (J : Type v) (hJ : category_theory.category J), {creates_colimit := λ (K : J ⥤ algebraic_geometry.SheafedSpace C), category_theory.creates_colimit_of_fully_faithful_of_iso {to_PresheafedSpace := (algebraic_geometry.PresheafedSpace.colimit_cocone (K ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)).X, is_sheaf := _} (category_theory.limits.colimit.iso_colimit_cocone {cocone := algebraic_geometry.PresheafedSpace.colimit_cocone (K ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace), is_colimit := algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit (K ⋙ algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace)}).symm}}

source

@[protected, instance]

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

category_theory.limits.has_colimits (algebraic_geometry.SheafedSpace C)

source

@[protected, instance]

noncomputable def algebraic_geometry.SheafedSpace.forget.category_theory.limits.preserves_colimits {C : Type u} [category_theory.category C] [category_theory.limits.has_limits C] :

category_theory.limits.preserves_colimits (algebraic_geometry.SheafedSpace.forget C)

Equations

algebraic_geometry.SheafedSpace.forget.category_theory.limits.preserves_colimits = category_theory.limits.comp_preserves_colimits algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace (algebraic_geometry.PresheafedSpace.forget C)

mathlib3 documentation

Sheafed spaces #