Ringed spaces

We introduce the category of ringed spaces, as an alias for SheafedSpace CommRingCat.

The facts collected in this file are typically stated for locally ringed spaces, but never actually make use of the locality of stalks. See for instance https://stacks.math.columbia.edu/tag/01HZ.

@[reducible, inline]

abbrev AlgebraicGeometry.RingedSpace : Type (max (u + 1) (v + 1))

The type of Ringed spaces, as an abbreviation for SheafedSpace CommRingCat.

Equations

• Eq AlgebraicGeometry.RingedSpace (AlgebraicGeometry.SheafedSpace CommRingCat)

theorem AlgebraicGeometry.RingedSpace.res_zero {X : RingedSpace} {U V : TopologicalSpace.Opens X.carrier.carrier} (hUV : LE.le U V) : Eq (TopCat.Presheaf.restrictOpen 0 U hUV) 0

def AlgebraicGeometry.RingedSpace.instCoeSortType : CoeSort RingedSpace (Type u_1)

Equations

• Eq AlgebraicGeometry.RingedSpace.instCoeSortType { coe := fun (X : AlgebraicGeometry.RingedSpace) => X.carrier.carrier }

theorem AlgebraicGeometry.RingedSpace.exists_res_eq_zero_of_germ_eq_zero (X : RingedSpace) (U : TopologicalSpace.Opens X.carrier.carrier) (f : (X.presheaf.obj { unop := U }).carrier) (x : Subtype fun (x : X.carrier.carrier) => Membership.mem U x) (h : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x.val ⋯)) f) 0) : Exists fun (V : TopologicalSpace.Opens X.carrier.carrier) => Exists fun (i : Quiver.Hom V U) => Exists fun (x : Membership.mem V x.val) => Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) f) 0

If the germ of a section f is zero in the stalk at x, then f is zero on some neighbourhood around x.

theorem AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ (X : RingedSpace) (U : TopologicalSpace.Opens X.carrier.carrier) (f : (X.presheaf.obj { unop := U }).carrier) (x : X.carrier.carrier) (hx : Membership.mem U x) (h : IsUnit (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f)) : Exists fun (V : TopologicalSpace.Opens X.carrier.carrier) => Exists fun (i : Quiver.Hom V U) => Exists fun (x : Membership.mem V x) => IsUnit (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) f)

If the germ of a section f is a unit in the stalk at x, then f must be a unit on some small neighborhood around x.

@[deprecated TopCat.Presheaf.germ_res_apply (since := "2025-02-08")]

theorem CommRingCat.germ_res_apply {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens X.carrier} (i : Quiver.Hom U V) (x : X.carrier) (hx : Membership.mem U x) [CategoryTheory.ConcreteCategory C FC] (s : CC (F.obj { unop := V })) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (F.map i.op)) s)) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (F.germ V x ⋯)) s)

Alias of TopCat.Presheaf.germ_res_apply.

@[deprecated TopCat.Presheaf.germ_res_apply' (since := "2025-02-08")]

theorem CommRingCat.germ_res_apply' {C : Type u} [CategoryTheory.Category C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type u_2} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens X.carrier} (i : Quiver.Hom { unop := V } { unop := U }) (x : X.carrier) (hx : Membership.mem U x) [CategoryTheory.ConcreteCategory C FC] (s : CC (F.obj { unop := V })) : Eq (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (F.map i)) s)) (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (F.germ V x ⋯)) s)

Alias of TopCat.Presheaf.germ_res_apply'.

theorem AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ (X : RingedSpace) (U : TopologicalSpace.Opens X.carrier.carrier) (f : (X.presheaf.obj { unop := U }).carrier) (h : ∀ (x : X.carrier.carrier) (hx : Membership.mem U x), IsUnit (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f)) : IsUnit f

If a section f is a unit in each stalk, f must be a unit.

def AlgebraicGeometry.RingedSpace.basicOpen (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (f : (X.presheaf.obj { unop := U }).carrier) : TopologicalSpace.Opens X.carrier.carrier

The basic open of a section f is the set of all points x, such that the germ of f at x is a unit.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.RingedSpace.mem_basicOpen (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (f : (X.presheaf.obj { unop := U }).carrier) (x : X.carrier.carrier) (hx : Membership.mem U x) : Iff (Membership.mem (X.basicOpen f) x) (IsUnit (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f))

theorem AlgebraicGeometry.RingedSpace.mem_basicOpen' (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (f : (X.presheaf.obj { unop := U }).carrier) (x : Subtype fun (x : X.carrier.carrier) => Membership.mem U x) : Iff (Membership.mem (X.basicOpen f) x.val) (IsUnit (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x.val ⋯)) f))

A variant of mem_basicOpen with bundled x : U.

theorem AlgebraicGeometry.RingedSpace.mem_top_basicOpen (X : RingedSpace) (f : (X.presheaf.obj { unop := Top.top }).carrier) (x : X.carrier.carrier) : Iff (Membership.mem (X.basicOpen f) x) (IsUnit (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.Γgerm x)) f))

theorem AlgebraicGeometry.RingedSpace.basicOpen_le (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (f : (X.presheaf.obj { unop := U }).carrier) : LE.le (X.basicOpen f) U

theorem AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (f : (X.presheaf.obj { unop := U }).carrier) : IsUnit (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) f)

The restriction of a section f to the basic open of f is a unit.

theorem AlgebraicGeometry.RingedSpace.basicOpen_res (X : RingedSpace) {U V : Opposite (TopologicalSpace.Opens X.carrier.carrier)} (i : Quiver.Hom U V) (f : (X.presheaf.obj U).carrier) : Eq (X.basicOpen (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i)) f)) (Min.min (Opposite.unop V) (X.basicOpen f))

theorem AlgebraicGeometry.RingedSpace.basicOpen_res_eq (X : RingedSpace) {U V : Opposite (TopologicalSpace.Opens X.carrier.carrier)} (i : Quiver.Hom U V) [CategoryTheory.IsIso i] (f : (X.presheaf.obj U).carrier) : Eq (X.basicOpen (DFunLike.coe (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i)) f)) (X.basicOpen f)

theorem AlgebraicGeometry.RingedSpace.basicOpen_mul (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (f g : (X.presheaf.obj { unop := U }).carrier) : Eq (X.basicOpen (HMul.hMul f g)) (Min.min (X.basicOpen f) (X.basicOpen g))

theorem AlgebraicGeometry.RingedSpace.basicOpen_pow (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (f : (X.presheaf.obj { unop := U }).carrier) (n : Nat) (h : LT.lt 0 n) : Eq (X.basicOpen (HPow.hPow f n)) (X.basicOpen f)

theorem AlgebraicGeometry.RingedSpace.basicOpen_of_isUnit (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} {f : (X.presheaf.obj { unop := U }).carrier} (hf : IsUnit f) : Eq (X.basicOpen f) U

def AlgebraicGeometry.RingedSpace.zeroLocus (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (s : Set (X.presheaf.obj { unop := U }).carrier) : Set X.carrier.carrier

The zero locus of a set of sections s over an open set U is the closed set consisting of the complement of U and of all points of U, where all elements of f vanish.

Equations

• Eq (X.zeroLocus s) (Set.iInter fun (f : (X.presheaf.obj { unop := U }).carrier) => Set.iInter fun (h : Membership.mem s f) => HasCompl.compl (SetLike.coe (X.basicOpen f)))

theorem AlgebraicGeometry.RingedSpace.zeroLocus_isClosed (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (s : Set (X.presheaf.obj { unop := U }).carrier) : IsClosed (X.zeroLocus s)

theorem AlgebraicGeometry.RingedSpace.zeroLocus_singleton (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (f : (X.presheaf.obj { unop := U }).carrier) : Eq (X.zeroLocus (Singleton.singleton f)) (HasCompl.compl (X.basicOpen f).carrier)

theorem AlgebraicGeometry.RingedSpace.zeroLocus_empty_eq_univ (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} : Eq (X.zeroLocus EmptyCollection.emptyCollection) Set.univ

theorem AlgebraicGeometry.RingedSpace.mem_zeroLocus_iff (X : RingedSpace) {U : TopologicalSpace.Opens X.carrier.carrier} (s : Set (X.presheaf.obj { unop := U }).carrier) (x : X.carrier.carrier) : Iff (Membership.mem (X.zeroLocus s) x) (∀ (f : (X.presheaf.obj { unop := U }).carrier), Membership.mem s f → Not (Membership.mem (X.basicOpen f) x))