locally ringed spaces

Stream: maths

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Patrick Massot]

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

[Scott Morrison]

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

[Scott Morrison]

Unfortunately there are going to be some difficulties.

[Scott Morrison]

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]

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

[Scott Morrison]

and then use general machinery to get colimits.

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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]

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]

I definitely plan to define at least filtered categories and colimits

[Scott Morrison]

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

[Scott Morrison]

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

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Reid Barton]

Ah yes, I see it.

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Notification Bot]

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