mathlib documentation

algebraic_geometry.locally_ringed_space

The category of locally ringed spaces #

We define (bundled) locally ringed spaces (as SheafedSpace CommRing along with the fact that the stalks are local rings), and morphisms between these (morphisms in SheafedSpace with is_local_ring_hom on the stalk maps).

@[nolint]

structure algebraic_geometry.LocallyRingedSpace :

Type (u_1+1)

to_SheafedSpace : algebraic_geometry.SheafedSpace CommRing
local_ring : ∀ (x : ↥(self.to_SheafedSpace.to_PresheafedSpace.carrier)), local_ring ↥(self.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk x)

A LocallyRingedSpace is a topological space equipped with a sheaf of commutative rings such that all the stalks are local rings.

A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphisms induced on stalks are local ring homomorphisms.

Instances for algebraic_geometry.LocallyRingedSpace

def algebraic_geometry.LocallyRingedSpace.to_RingedSpace (X : algebraic_geometry.LocallyRingedSpace) :

algebraic_geometry.RingedSpace

An alias for to_SheafedSpace, where the result type is a RingedSpace. This allows us to use dot-notation for the RingedSpace namespace.

Equations

X.to_RingedSpace = X.to_SheafedSpace

def algebraic_geometry.LocallyRingedSpace.to_Top (X : algebraic_geometry.LocallyRingedSpace) :

The underlying topological space of a locally ringed space.

Equations

X.to_Top = X.to_SheafedSpace.to_PresheafedSpace.carrier

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.has_coe_to_sort :

has_coe_to_sort algebraic_geometry.LocallyRingedSpace (Type u)

Equations

algebraic_geometry.LocallyRingedSpace.has_coe_to_sort = {coe := λ (X : algebraic_geometry.LocallyRingedSpace), ↥(X.to_Top)}

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.stalk.local_ring (X : algebraic_geometry.LocallyRingedSpace) (x : ↥X) :

local_ring ↥(X.to_SheafedSpace.to_PresheafedSpace.stalk x)

def algebraic_geometry.LocallyRingedSpace.𝒪 (X : algebraic_geometry.LocallyRingedSpace) :

Top.sheaf CommRing X.to_Top

The structure sheaf of a locally ringed space.

Equations

X.𝒪 = X.to_SheafedSpace.sheaf

@[ext]

structure algebraic_geometry.LocallyRingedSpace.hom (X Y : algebraic_geometry.LocallyRingedSpace) :

val : X.to_SheafedSpace ⟶ Y.to_SheafedSpace
prop : ∀ (x : ↥(X.to_SheafedSpace.to_PresheafedSpace)), is_local_ring_hom (algebraic_geometry.PresheafedSpace.stalk_map self.val x)

A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphims induced on stalks are local ring homomorphisms.

Instances for algebraic_geometry.LocallyRingedSpace.hom

algebraic_geometry.LocallyRingedSpace.hom.has_sizeof_inst
algebraic_geometry.LocallyRingedSpace.hom.inhabited

theorem algebraic_geometry.LocallyRingedSpace.hom.ext {X Y : algebraic_geometry.LocallyRingedSpace} (x y : X.hom Y) (h : x.val = y.val) :

x = y

theorem algebraic_geometry.LocallyRingedSpace.hom.ext_iff {X Y : algebraic_geometry.LocallyRingedSpace} (x y : X.hom Y) :

x = y ↔ x.val = y.val

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.quiver :

quiver algebraic_geometry.LocallyRingedSpace

Equations

algebraic_geometry.LocallyRingedSpace.quiver = {hom := algebraic_geometry.LocallyRingedSpace.hom}

noncomputable def algebraic_geometry.LocallyRingedSpace.stalk (X : algebraic_geometry.LocallyRingedSpace) (x : ↥X) :

The stalk of a locally ringed space, just as a CommRing.

Equations

X.stalk x = X.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk x

noncomputable def algebraic_geometry.LocallyRingedSpace.stalk_map {X Y : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↥X) :

Y.stalk (⇑(f.val.base) x) ⟶ X.stalk x

A morphism of locally ringed spaces f : X ⟶ Y induces a local ring homomorphism from Y.stalk (f x) to X.stalk x for any x : X.

Equations

algebraic_geometry.LocallyRingedSpace.stalk_map f x = algebraic_geometry.PresheafedSpace.stalk_map f.val x

Instances for algebraic_geometry.LocallyRingedSpace.stalk_map

algebraic_geometry.LocallyRingedSpace.stalk_map.is_local_ring_hom

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.stalk_map.is_local_ring_hom {X Y : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↥X) :

is_local_ring_hom (algebraic_geometry.LocallyRingedSpace.stalk_map f x)

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.algebraic_geometry.PresheafedSpace.stalk_map.is_local_ring_hom {X Y : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↥X) :

is_local_ring_hom (algebraic_geometry.PresheafedSpace.stalk_map f.val x)

def algebraic_geometry.LocallyRingedSpace.id (X : algebraic_geometry.LocallyRingedSpace) :

X.hom X

The identity morphism on a locally ringed space.

Equations

X.id = {val := 𝟙 X.to_SheafedSpace, prop := _}

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.id_val (X : algebraic_geometry.LocallyRingedSpace) :

X.id.val = 𝟙 X.to_SheafedSpace

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.hom.inhabited (X : algebraic_geometry.LocallyRingedSpace) :

inhabited (X.hom X)

Equations

algebraic_geometry.LocallyRingedSpace.hom.inhabited X = {default := X.id}

def algebraic_geometry.LocallyRingedSpace.comp {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X.hom Y) (g : Y.hom Z) :

X.hom Z

Composition of morphisms of locally ringed spaces.

Equations

algebraic_geometry.LocallyRingedSpace.comp f g = {val := f.val ≫ g.val, prop := _}

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.category_theory.category :

category_theory.category algebraic_geometry.LocallyRingedSpace

The category of locally ringed spaces.

Equations

algebraic_geometry.LocallyRingedSpace.category_theory.category = {to_category_struct := {to_quiver := {hom := algebraic_geometry.LocallyRingedSpace.hom}, id := algebraic_geometry.LocallyRingedSpace.id, comp := λ (X Y Z : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y) (g : Y ⟶ Z), algebraic_geometry.LocallyRingedSpace.comp f g}, id_comp' := algebraic_geometry.LocallyRingedSpace.category_theory.category._proof_1, comp_id' := algebraic_geometry.LocallyRingedSpace.category_theory.category._proof_2, assoc' := algebraic_geometry.LocallyRingedSpace.category_theory.category._proof_3}

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace_map (X Y : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y) :

algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.map f = f.val

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace_obj (X : algebraic_geometry.LocallyRingedSpace) :

algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.obj X = X.to_SheafedSpace

def algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace :

algebraic_geometry.LocallyRingedSpace ⥤ algebraic_geometry.SheafedSpace CommRing

The forgetful functor from LocallyRingedSpace to SheafedSpace CommRing.

Equations

algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace = {obj := λ (X : algebraic_geometry.LocallyRingedSpace), X.to_SheafedSpace, map := λ (X Y : algebraic_geometry.LocallyRingedSpace) (f : X ⟶ Y), f.val, map_id' := algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace._proof_1, map_comp' := algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace._proof_2}

Instances for algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.category_theory.faithful :

category_theory.faithful algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.forget_to_Top_obj (X : algebraic_geometry.LocallyRingedSpace) :

algebraic_geometry.LocallyRingedSpace.forget_to_Top.obj X = (algebraic_geometry.SheafedSpace.forget CommRing).obj X.to_SheafedSpace

def algebraic_geometry.LocallyRingedSpace.forget_to_Top :

algebraic_geometry.LocallyRingedSpace ⥤ Top

The forgetful functor from LocallyRingedSpace to Top.

Equations

algebraic_geometry.LocallyRingedSpace.forget_to_Top = algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace ⋙ algebraic_geometry.SheafedSpace.forget CommRing

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.forget_to_Top_map (_x _x_1 : algebraic_geometry.LocallyRingedSpace) (f : _x ⟶ _x_1) :

algebraic_geometry.LocallyRingedSpace.forget_to_Top.map f = (algebraic_geometry.SheafedSpace.forget CommRing).map f.val

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.comp_val {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) :

(f ≫ g).val = f.val ≫ g.val

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.comp_val_c {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) :

(f ≫ g).val.c = g.val.c ≫ (Top.presheaf.pushforward CommRing g.val.base).map f.val.c

theorem algebraic_geometry.LocallyRingedSpace.comp_val_c_app {X Y Z : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (topological_space.opens ↥Z)ᵒᵖ) :

(f ≫ g).val.c.app U = g.val.c.app U ≫ f.val.c.app (opposite.op ((topological_space.opens.map g.val.base).obj (opposite.unop U)))

def algebraic_geometry.LocallyRingedSpace.hom_of_SheafedSpace_hom_of_is_iso {X Y : algebraic_geometry.LocallyRingedSpace} (f : X.to_SheafedSpace ⟶ Y.to_SheafedSpace) [category_theory.is_iso f] :

X ⟶ Y

Given two locally ringed spaces X and Y, an isomorphism between X and Y as sheafed spaces can be lifted to a morphism X ⟶ Y as locally ringed spaces.

See also iso_of_SheafedSpace_iso.

Equations

algebraic_geometry.LocallyRingedSpace.hom_of_SheafedSpace_hom_of_is_iso f = {val := f, prop := _}

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.hom_of_SheafedSpace_hom_of_is_iso_val {X Y : algebraic_geometry.LocallyRingedSpace} (f : X.to_SheafedSpace ⟶ Y.to_SheafedSpace) [category_theory.is_iso f] :

(algebraic_geometry.LocallyRingedSpace.hom_of_SheafedSpace_hom_of_is_iso f).val = f

def algebraic_geometry.LocallyRingedSpace.iso_of_SheafedSpace_iso {X Y : algebraic_geometry.LocallyRingedSpace} (f : X.to_SheafedSpace ≅ Y.to_SheafedSpace) :

X ≅ Y

Given two locally ringed spaces X and Y, an isomorphism between X and Y as sheafed spaces can be lifted to an isomorphism X ⟶ Y as locally ringed spaces.

This is related to the property that the functor forget_to_SheafedSpace reflects isomorphisms. In fact, it is slightly stronger as we do not require f to come from a morphism between locally ringed spaces.

Equations

algebraic_geometry.LocallyRingedSpace.iso_of_SheafedSpace_iso f = {hom := algebraic_geometry.LocallyRingedSpace.hom_of_SheafedSpace_hom_of_is_iso f.hom _, inv := algebraic_geometry.LocallyRingedSpace.hom_of_SheafedSpace_hom_of_is_iso f.inv _, hom_inv_id' := _, inv_hom_id' := _}

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.category_theory.reflects_isomorphisms :

category_theory.reflects_isomorphisms algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.is_SheafedSpace_iso {X Y : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) [category_theory.is_iso f] :

category_theory.is_iso f.val

def algebraic_geometry.LocallyRingedSpace.restrict {U : Top} (X : algebraic_geometry.LocallyRingedSpace) {f : U ⟶ X.to_Top} (h : open_embedding ⇑f) :

algebraic_geometry.LocallyRingedSpace

The restriction of a locally ringed space along an open embedding.

Equations

X.restrict h = {to_SheafedSpace := X.to_SheafedSpace.restrict h, local_ring := _}

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.restrict_to_SheafedSpace {U : Top} (X : algebraic_geometry.LocallyRingedSpace) {f : U ⟶ X.to_Top} (h : open_embedding ⇑f) :

(X.restrict h).to_SheafedSpace = X.to_SheafedSpace.restrict h

def algebraic_geometry.LocallyRingedSpace.of_restrict {U : Top} (X : algebraic_geometry.LocallyRingedSpace) {f : U ⟶ X.to_Top} (h : open_embedding ⇑f) :

X.restrict h ⟶ X

The canonical map from the restriction to the supspace.

Equations

X.of_restrict h = {val := X.to_SheafedSpace.to_PresheafedSpace.of_restrict h, prop := _}

def algebraic_geometry.LocallyRingedSpace.restrict_top_iso (X : algebraic_geometry.LocallyRingedSpace) :

X.restrict _ ≅ X

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

Equations

X.restrict_top_iso = algebraic_geometry.LocallyRingedSpace.iso_of_SheafedSpace_iso X.to_SheafedSpace.restrict_top_iso

def algebraic_geometry.LocallyRingedSpace.Γ :

algebraic_geometry.LocallyRingedSpace ᵒᵖ ⥤ CommRing

The global sections, notated Gamma.

Equations

algebraic_geometry.LocallyRingedSpace.Γ = algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.op ⋙ algebraic_geometry.SheafedSpace.Γ

theorem algebraic_geometry.LocallyRingedSpace.Γ_def :

algebraic_geometry.LocallyRingedSpace.Γ = algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace.op ⋙ algebraic_geometry.SheafedSpace.Γ

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.Γ_obj (X : algebraic_geometry.LocallyRingedSpace ᵒᵖ) :

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

theorem algebraic_geometry.LocallyRingedSpace.Γ_obj_op (X : algebraic_geometry.LocallyRingedSpace) :

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

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.Γ_map {X Y : algebraic_geometry.LocallyRingedSpace ᵒᵖ} (f : X ⟶ Y) :

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

theorem algebraic_geometry.LocallyRingedSpace.Γ_map_op {X Y : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) :

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

theorem algebraic_geometry.LocallyRingedSpace.preimage_basic_open {X Y : algebraic_geometry.LocallyRingedSpace} (f : X ⟶ Y) {U : topological_space.opens ↥Y} (s : ↥(Y.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

(topological_space.opens.map f.val.base).obj (Y.to_RingedSpace.basic_open s) = X.to_RingedSpace.basic_open (⇑(f.val.c.app (opposite.op U)) s)

@[simp]

theorem algebraic_geometry.LocallyRingedSpace.basic_open_zero (X : algebraic_geometry.LocallyRingedSpace) (U : topological_space.opens ↥(X.to_SheafedSpace.to_PresheafedSpace.carrier)) :

X.to_RingedSpace.basic_open 0 = ⊥

@[protected, instance]

def algebraic_geometry.LocallyRingedSpace.component_nontrivial (X : algebraic_geometry.LocallyRingedSpace) (U : topological_space.opens ↥(X.to_SheafedSpace.to_PresheafedSpace.carrier)) [hU : nonempty ↥U] :

nontrivial ↥(X.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))