mathlib3 documentation

algebraic_geometry.locally_ringed_space

The category of locally ringed spaces #

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

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))