Zulip Chat Archive

Stream: maths

Topic: locally ringed spaces


view this post on Zulip Scott Morrison (Sep 01 2018 at 09:45):

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

view this post on Zulip 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)

view this post on Zulip Scott Morrison (Sep 01 2018 at 09:46):

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

view this post on Zulip Scott Morrison (Sep 01 2018 at 09:46):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Sep 01 2018 at 09:46):

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

view this post on Zulip Scott Morrison (Sep 01 2018 at 09:47):

Unfortunately there are going to be some difficulties.

view this post on Zulip 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)

view this post on Zulip 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,

view this post on Zulip Scott Morrison (Sep 01 2018 at 09:49):

and then use general machinery to get colimits.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 01 2018 at 11:12):

I definitely plan to define at least filtered categories and colimits

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.?

view this post on Zulip Scott Morrison (Sep 01 2018 at 11:46):

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

view this post on Zulip 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 :-)

view this post on Zulip Reid Barton (Sep 01 2018 at 11:52):

Ah yes, I see it.

view this post on Zulip Reid Barton (Sep 01 2018 at 11:53):

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

view this post on Zulip Reid Barton (Sep 01 2018 at 11:53):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 09:13):

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

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 09:13):

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

view this post on Zulip 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.

view this post on Zulip 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