## Stream: maths

### Topic: locally ringed spaces

#### Scott Morrison (Sep 01 2018 at 09:45):

In lean-category-theory I've added a definition of locally_ringed_space.

#### Scott Morrison (Sep 01 2018 at 09:46):

def structure_sheaf := sheaf.{v+1 v} α Ring

structure ringed_space :=
(𝒪 : structure_sheaf α)

structure locally_ringed_space extends ringed_space α :=
(locality : ∀ x : α, local_ring (stalk_at.{v+1 v} 𝒪 x).1)


#### Scott Morrison (Sep 01 2018 at 09:46):

and that seems to work (without even many sorries in earlier files :-)

#### Scott Morrison (Sep 01 2018 at 09:46):

But there's quite a bit of work to do in order to actually construct examples.

#### Patrick Massot (Sep 01 2018 at 09:46):

Yeah! Let's do that instead of trying to prove 2 is not a square in Z and get depressed

#### Scott Morrison (Sep 01 2018 at 09:46):

I thought I should try to do the sheaf of cts functions on a topological space.

#### Scott Morrison (Sep 01 2018 at 09:47):

Unfortunately there are going to be some difficulties.

#### Scott Morrison (Sep 01 2018 at 09:48):

In particular, at the moment stalk_at is just defined by:

def stalk_at (F : sheaf α V) (x : α) : V :=
colimit (F.near x)


#### Scott Morrison (Sep 01 2018 at 09:49):

Unfortunately general colimits of rings are pretty gross. My plan had been to construct coequalizers and coproducts in CommRing,

#### Scott Morrison (Sep 01 2018 at 09:49):

and then use general machinery to get colimits.

#### Scott Morrison (Sep 01 2018 at 09:49):

However if you do that, it's going to be very hard to show that a stalk of the structure sheaf is actually germs of continuous functions at that point.

#### Scott Morrison (Sep 01 2018 at 09:51):

I think I'll need to change colimit in the definition of stalk_at to directed_colimit (or filtered_colimit?), show that the poset of neighbourhood of x is actually directed, and then separately give a formula for directed colimits of commutative rings.

#### Scott Morrison (Sep 01 2018 at 09:52):

That formula for directed colimits, when applied to the sheaf of continuous functions, should look exactly like germs.

#### Scott Morrison (Sep 01 2018 at 09:54):

But if someone wants to do parts of this:

• define filtered categories, and filtered colimits
• construct instances of has_coproducts, has_coequalizers, and/or has_filtered_limits for Ring
• show that continuous functions from a topological space to a topological ring forms a topological ring
• define germs of continuous functions
• show that germs are a local ring
then it will get done faster. :-)

#### Patrick Massot (Sep 01 2018 at 10:19):

I'd love to work on all that, but I really think I should focus on completions of rings, otherwise the perfectoid project will be really stuck

#### Reid Barton (Sep 01 2018 at 11:12):

I definitely plan to define at least filtered categories and colimits

#### Scott Morrison (Sep 01 2018 at 11:41):

@Reid Barton, great! I just made a primitive first cut at filtered categories, and shows that inhabited directed posets are filtered.

#### Scott Morrison (Sep 01 2018 at 11:41):

I was going to start trying to define filtered limits in Ring, but I think jetlag has caught up with me.

#### Reid Barton (Sep 01 2018 at 11:44):

I'm currently on a train anyways, but is there a branch somewhere where I can follow along with the limits etc.?

#### Scott Morrison (Sep 01 2018 at 11:46):

It's all happening in master of lean-category-theory

#### Scott Morrison (Sep 01 2018 at 11:46):

Although I'm committing less often because I'm trying to be better and checking that it compiles before pushing :-)

#### Reid Barton (Sep 01 2018 at 11:52):

Ah yes, I see it.

#### Reid Barton (Sep 01 2018 at 11:53):

Yes, that's a nice thing to do when you have users :)

#### Reid Barton (Sep 01 2018 at 11:53):

Though maybe I could just work in a branch of your library for now

#### Kevin Buzzard (Jul 22 2020 at 09:11):

We don't seem to have a definition of locally ringed spaces in mathlib. All the work of my students on sheaves of groups, rings etc all define sheaves on each of the different categories using bespoke definitions for each typeclass. Am I right? We have to switch to categories. I think that an interesting challenge would be to define a sheaf of modules over a sheaf of rings on a locally ringed space. Scott can make concrete categories now, so we can have sheaves of rings and sheaves of modules over a fixed ring -- but sheaves of modules on a locally ringed space is a dependent sheaf of some kind.

#### Kevin Buzzard (Jul 22 2020 at 09:13):

Can we define the tensor product of two sheaves of $\mathcal{O}_X$-modules? It's just the sheafification of some presheaf functor.

#### Kevin Buzzard (Jul 22 2020 at 09:13):

I'm not talking about making an API, I'm talking about simply making the definition.

#### Kevin Buzzard (Jul 22 2020 at 09:20):

Ok so apparently none of this is in mathlib, so this isn't really the right place for this thread.

#### Notification Bot (Jul 22 2020 at 09:27):

This topic was moved here from #Is there code for X? > locally ringed spaces by Rob Lewis

Last updated: May 06 2021 at 18:20 UTC