universes in structures

Stream: general

[Kevin Buzzard]

I defined a presheaf like this:

structure presheaf_of_types (X : Type u) [topological_space X] :=
(F : opens X → Type u)
(res : ∀ {U V : opens X} (h : V ⊆ U), F U → F V)
(id : ∀ (U : opens X) (x : F U), res (le_refl U) x = x)
(comp : ∀ {U V W : opens X} (hUV : V ⊆ U) (hVW : W ⊆ V) (x : F U),
  res hVW (res hUV x) = res (set.subset.trans hVW hUV) x)

I had to make a call about the target of presheaf_of_types.F. I went for the same universe as X, because I have this vaguely uncomfortable feeling about having universes in my structures which are not extractable from the input data.

I now realise that I can't define pushforwards of presheaves along continuous maps, at least continuous maps X -> Y where X is in universe u1 and Y in universe u2.

There are lots of solutions to this.

1) Let F take values in universe v (and then feed in v manually later)
2) Restrict the theory to continuous maps X -> Y living in universe u
3) Openly question this whole universe polymorphism stuff and let everything take values in Type.

I developed a bunch of the schemes repo over Type and never had any problems.

@Mario Carneiro any comments?

[Kevin Buzzard]

I should stress that I spent 25 years doing research whilst living in Type and I never had any problems.

[Mario Carneiro]

I will tentatively recommend that you restrict the theory to continuous maps in Type u

[Kevin Buzzard]

If I bundle everything, and I'm going to try, then I feel like I'll be spending my life feeding universes into things anyway. It seems to me that (2) is a cop-out, I am either polymorphic or I am not, and (2) seems like a half way house that will satisfy nobody. I am unclear about the dangers of (1). Is it simply that I have to just put {u v} in a few places?

[Mario Carneiro]

and we will see if an issue arises later

[Kevin Buzzard]

So you are (1)-averse?

[Mario Carneiro]

(1) will cause you to put .{u v} in lots of places

[Kevin Buzzard]

Keep in mind that Scott convinced me on the equiv thread in #maths to try bundling.

[Mario Carneiro]

I think the friction isn't worth it to you

[Kevin Buzzard]

If the friction isn't worth it then you're telling me I should use (3)

[Mario Carneiro]

(2) is about as good as (3) in terms of "don't worry about it" ism

[Kevin Buzzard]

Or are you saying the philosophy is that I should be as polymorphic as possible whilst avoiding at all costs the pain of having to annotate my universes?

[Mario Carneiro]

There are still ways to recover maps between different universes with (2), but they are more cumbersome

[Kevin Buzzard]

@Scott Morrison if I were approaching these definitions with bundling and categories in mind (I want to define an equiv of presheaves of types) then what would your choice be?

[Mario Carneiro]

and that seems like a reasonable tradeoff: make additional universes cumbersome in order to make the common case nicer

[Mario Carneiro]

if indeed everything is in Type eventually then this shouldn't ever happen anyway

[Kevin Buzzard]

Grothendieck would have just observed that (1) and (2) were the same because you can just move to a bigger universe

[Mario Carneiro]

That's what I mean

[Kevin Buzzard]

but I have no experience of the pain that this would involve in Lean

[Kevin Buzzard]

and I am pain averse

[Mario Carneiro]

you have to use ulift

[Kevin Buzzard]

ulift is a closed book to me

[Mario Carneiro]

it's a universe shifting function that preserves all structure

[Kevin Buzzard]

I thought Reid's comment was telling in the other thread -- he stuck to Type because he could not be bothered to ulift the reals

[Kevin Buzzard]

is it canonical?

[Mario Carneiro]

ah, there is that

[Kevin Buzzard]

Fortunately the valuations I have on my stalks are not real-valued

[Mario Carneiro]

sure it's canonical

[Mario Carneiro]

it's like the canonical injection map

[Kevin Buzzard]

they are taking values in a totally ordered monoid

[Kevin Buzzard]

I love that I managed to get you to say canonical

[Mario Carneiro]

in ZFC it is just inclusion

[Kevin Buzzard]

when neither of us know what it means

[Kevin Buzzard]

that's just how it works in maths too

[Mario Carneiro]

it's canonical in lean because it's a function :P

[Kevin Buzzard]

we sagely nod and agree that it's canonical

[Kevin Buzzard]

is it functorial?

[Mario Carneiro]

yep, it is all the things

[Kevin Buzzard]

I don't know why people are so afraid of it then

[Mario Carneiro]

it's also a thing

[Mario Carneiro]

which is one more than no thing

[Kevin Buzzard]

You can look forward to the "ulift hell" thread

[Kevin Buzzard]

Thanks for the comments. Scott, I'd be interested to hear yours.

[Kevin Buzzard]

I guess one final observation is that I have now coded up presheaves of types twice (once for schemes, once for this), Ramon coded it up for Schemes Reloaded, Johan did it, probably Scott did it, and somehow it's still not in mathlib. Maybe it's time someone PR'ed it...

[Scott Morrison]

Ok, per request, I PR'd one version of (bundled) presheaves. The definition is I hope inarguably the correct one. :-)

[Scott Morrison]

The essential definitions are:

structure Presheaf :=
(X : Top.{v})
(𝒪 : (opens X)ᵒᵖ ⥤ C)

structure Presheaf_hom (F G : Presheaf.{v} C) :=
(f : F.X ⟶ G.X)
(c : G.𝒪 ⟹ ((opens.map f).op ⋙ F.𝒪))

instance category_of_presheaves : category (Presheaf.{v} C) :=
{ hom := Presheaf_hom,
  ... }

and

def functor.map_presheaf (F : C ⥤ D) : Presheaf.{v} C ⥤ Presheaf.{v} D := ...

[Scott Morrison]

There are still some things I'm unhappy with --- some places I need to use erw, where simp should suffice.

[Johan Commelin]

Scott, I think what we are probably also interested in is the category of presheaves on a space X.

[Johan Commelin]

I.e. unbundled presheaves on bundled spaces.

[Johan Commelin]

Of course this is just a functor category...

[Johan Commelin]

But we might want some specialised coercions/simp lemmas

[Scott Morrison]

Hmm... so what do you want besides def presheaf (X : Top) := (opens X)^op \func C?

[Johan Commelin]

The push-forward functor should be easily accessible

[Johan Commelin]

And maybe for terms of type presheaf we can actually make F.obj a coercion?

[Johan Commelin]

I didn't experiment with it though

[Johan Commelin]

Need to run to catch a train

[Reid Barton]

I actually don't see what this particular bundled Presheaf is useful for, other than as an example

[Reid Barton]

For example, I don't see how you could build "Sheaf" out of "Presheaf"

[Reid Barton]

(Also, "presheaf" for me just means a (contravariant) functor from some category to sets. So there isn't really anything to define for presheaves that we don't have already.)

[Reid Barton]

It might make sense though to define pseudofunctors to categories and the Grothendieck construction

[Reid Barton]

maybe this opens too many cans of worms at once

[Kevin Buzzard]

I wrote an unbundled version of presheaves of types.

[Kevin Buzzard]

https://gist.github.com/kbuzzard/567b88f2afae5730016c392ec2efc851

[Kevin Buzzard]

I needed the notion of an equiv for them. But I was not convinced I had got it right until I had proved refl, symm and trans. They took me some time. I had to deal with heqs.

[Kevin Buzzard]

My understanding is that Scott has done something less general than what I need. I need the notion of an equiv of pairs (X,F), i.e. two possibly distinct topological spaces equipped with presheaves.

[Mario Carneiro]

heqs sounds bad, where did they come up?

[Kevin Buzzard]

In fact Scott it makes sense to tell you exactly what I need, just out of interest. I need the notion of an isomorphism of the following data: a topological space X, a presheaf of topological rings on X, and an equivalence class of valuations on the stalks (where the direct limits are the limit of a direct system of rings only, not topological rings). I know how to do this. It's just a case of working out what is the best way to do this.

I have never used the category theory library. I did equivs of data (X,F) with X a top space and F a presheaf on X today so I know it can all be done. I went with Mario's annoying solution to the universe issue by staying in one universe for everything (X : type u and F U : type u).

[Kevin Buzzard]

heqs came up because I was changing X.

[Kevin Buzzard]

I instantly turned every heq into an eq

[Kevin Buzzard]

structure f_map (𝒢 : presheaf_of_typesU Y) (ℱ : presheaf_of_typesU X) :=
(f : X → Y)
[hf : continuous f]
(ρ : ∀ V : opens Y, 𝒢.F V → ℱ.F ⟨f ⁻¹' V, hf _ V.2⟩)
(nat : ∀ U V : opens Y, ∀ hUV : V ⊆ U,
  ∀ x : 𝒢.F U, ρ V (𝒢.res hUV x) = ℱ.res (by {intros x hx, exact hUV hx}) (ρ U x))

That's a definition of a morphism in my category

[Kevin Buzzard]

But when defining equivs I wanted to say that two morphisms were equal, and this involved saying the f's were equal and then the rho's were ==

[Kevin Buzzard]

rho is not a good notation, it's not a restriction, rho is the map between the presheaves. f is the map between the spaces and rho, soon to be renamed, is the map between the presheaves. I think heq is inevitable here. But I managed to battle all of them off.

[Kevin Buzzard]

def ext (α β : f_map 𝒢 ℱ) (hf : α.f = β.f) (hρ : α.ρ == β.ρ) : α = β :=
begin
  cases α with αf αhf αρ αnat, cases β with βf βhf βρ βnat,
  rw presheaf_of_typesU.f_map.mk.inj_eq,
  exact ⟨hf, hρ⟩,
end

That was what Lean gave me, so I went with it.

[Mario Carneiro]

first observation: this should be a definition

def opens.comap {α β} [topological_space α] [topological_space β]
  (f : α → β) (hf : continuous f) (U : opens β) : opens α :=
⟨f ⁻¹' U, hf _ U.2⟩

[Kevin Buzzard]

Yeah, I couldn't find that!

[Kevin Buzzard]

I read all of topology.opens :-)

[Mario Carneiro]

It's not very complete, I think it's just what is needed to define the category

[Mario Carneiro]

you may also want to bundle continuous maps for this purpose

[Kevin Buzzard]

I'm still not very good at understanding sentences with the word bundle in.

[Kevin Buzzard]

Oh -- you mean continuous_map X Y?

[Mario Carneiro]

yes

[Kevin Buzzard]

I am very interested in hearing the way Scott would handle this stuff. My understanding of his PR is that he has not yet defined the morphisms I need -- f_map. They caused me some pain, I don't know whether they will cause him more or less pain, or whether he can use my work.

[Kevin Buzzard]

first observation: this should be a definition

def opens.comap {α β} [topological_space α] [topological_space β]
  (f : α → β) (hf : continuous f) (U : opens β) : opens α :=
⟨f ⁻¹' U, hf _ U.2⟩

Is {f : α → β} ok here? It was only after reading your code that I discovered that continuous wasn't a typeclass :-)

[Mario Carneiro]

It can be, but you end up with unhelpful opens.comap _ U terms in your goal, like classical.some _

[Mario Carneiro]

also opens seems to be a bit indecisive about whether to use \sub or \le for subsets

[Kevin Buzzard]

And why is this called opens.comap (which I assume is topological_space.opens.comap) and not continuous.comap? I am still not very good at naming.

[Mario Carneiro]

You can use projection notation either way, but the distinguishing feature is that opens is the thing being comapped. You aren't going to comap opens with something other than a continuous function, but continuous functions can comap other things

[Kevin Buzzard]

I make your change and I now have to fix errors like

type mismatch at application
  ℱ.res _ x
term
  x
has type
  ℱ.F V
but is expected to have type
  ℱ.F (topological_space.opens.comap (λ (x : X), x) continuous_id V)

I guess this is to be expected.

[Kevin Buzzard]

Lovely lines such as

    change ℱ.res _ (ℱ.res _ (ℱ.res _ x)) = ℱ.res _ x,

now don't compile at all :-(

[Kevin Buzzard]

no that's a complete lie, I fixed the first error and all the other errors magically fixed themselves. I've got it working :D

[Kevin Buzzard]

Revised version at https://gist.github.com/kbuzzard/567b88f2afae5730016c392ec2efc851

[Kevin Buzzard]

@Reid Barton would using category theory stuff make any of this easier?

[Kevin Buzzard]

Conversely, could I use this to make a bundled version of presheaves of types easier to implement? I think what I have that Scott doesn't have is that I am allowed to change my base with morphisms

[Mario Carneiro]

I'm working on a more complete working-out of the proposal

[Mario Carneiro]

namespace topological_space.opens
variables {α : Type*} {β : Type*} {γ : Type*}
variables [topological_space α] [topological_space β] [topological_space γ]

def comap (f : α → β) (hf : continuous f) (U : opens β) : opens α :=
⟨f ⁻¹' U, hf _ U.2⟩

theorem comap_id (U : opens α) : comap id continuous_id U = U := ext rfl

theorem comap_comp {f : α → β} {g : β → γ}
  {hf : continuous f} {hg : continuous g} (U : opens γ) :
  comap _ (hf.comp hg) U = comap _ hf (comap _ hg U) := ext rfl

theorem comap_mono {α β} [topological_space α] [topological_space β]
  {f : α → β} {hf : continuous f} {U V : opens β}
  (h : U ≤ V) : U.comap f hf ≤ V.comap f hf :=
λ x hx, h hx

end topological_space.opens



structure f_map (𝒢 : presheaf_of_typesU Y) (ℱ : presheaf_of_typesU X) :=
(f : X → Y)
(hf : continuous f)
(ρ : ∀ V : opens Y, 𝒢.F V → ℱ.F (V.comap f hf))
(nat : ∀ U V : opens Y, ∀ hUV : V ≤ U,
  ∀ x : 𝒢.F U, ρ V (𝒢.res hUV x) = ℱ.res (comap_mono hUV) (ρ U x))

[Kevin Buzzard]

It seems to me that the only thing category theory can offer me here is free proofs of refl symm and trans given comp_id and comp_assoc

[Kevin Buzzard]

I don't see the benefit of using it here.

[Johan Commelin]

I think Scott also allows you to change the base space.

[Johan Commelin]

In fact, opens X \func Type u is defeq to your definition (modulo iota for records).

[Johan Commelin]

So I think it also doesn't hurt to use the category lib

[Johan Commelin]

I found it incredibly hard to construct a certain adjunction using the category lib. I don't think that would become any easier by avoiding the category lib.

[Kevin Buzzard]

Remark : I think you can prove refl symm and trans for equiv using only comp_assoc and id_comp -- you don't seem to need comp_id

[Kevin Buzzard]

The thing I took from Scott's comments were that I could define an equiv as a morphism with a two sided inverse instead of having to write down what I mean by an isomorphism

[Scott Morrison]

@Kevin Buzzard, sorry, I haven't caught up everything here --- but your first comment:

My understanding is that Scott has done something less general than what I need. I need the notion of an equiv of pairs (X,F), i.e. two possibly distinct topological spaces equipped with presheaves.

is exactly wrong. Did you look at my definition?

[Scott Morrison]

A morphism is exactly:

structure Presheaf_hom (F G : Presheaf.{v} C) :=
(f : F.X ⟶ G.X)
(c : G.𝒪 ⟹ ((opens.map f).op ⋙ F.𝒪))

i.e. a pair, a continuous map, changing the topological space, along with a map from the presheaf on the target space to the pushforward of the presheaf on the source space.

[Scott Morrison]

I then define a category structure on these, so you get the notion of an equivalence of pairs simply by writing \iso.

[Scott Morrison]

Sorry if I sound a bit grumpy, but as far as I can tell what you guys have been talking about needing since I went to bed last night is exactly what I PR'd.

[Scott Morrison]

@Mario Carneiro's

structure f_map (𝒢 : presheaf_of_typesU Y) (ℱ : presheaf_of_typesU X) :=
(f : X → Y)
(hf : continuous f)
(ρ : ∀ V : opens Y, 𝒢.F V → ℱ.F (V.comap f hf))
(nat : ∀ U V : opens Y, ∀ hUV : V ≤ U,
  ∀ x : 𝒢.F U, ρ V (𝒢.res hUV x) = ℱ.res (comap_mono hUV) (ρ U x))

is exactly a long winded way of saying my Presheaf_hom, and _less_ general, since it restricts to presheaves valued in Type, rather than an arbitrary category.

[Scott Morrison]

Please tell me if I'm missing something.

[Mario Carneiro]

Here's a completed revision of Kevin's file: https://gist.github.com/digama0/9bfe808e7e51fecc001d8ac8976db19c

[Scott Morrison]

Grah!!!

[Mario Carneiro]

Where is opens.map?

[Scott Morrison]

Where it's been for months, in category_theory/instances/topological_spaces.lean.

[Mario Carneiro]

I can definitely believe that these are the same issues that come up in the categorical formulation

[Mario Carneiro]

For the record, I'm just making epsilon improvements to Kevin's proposal, not a complete rewrite. I haven't looked in detail at the stuff in this area, I'm just talking about how to deal with dependent types

[Scott Morrison]

Okay... but as far as I can tell it's all done in my PR from last night. (Which was just a tidy up of a file I showed people months ago....)

[Mario Carneiro]

@Kevin Buzzard, I'm inclined to believe that Scott has already done all the hard work of these definitions in the category theory lib, and handled the dependencies right because they have been an issue from day one. As for friction of using category theory here: opens is already a category (it was designed to be one), and Type is a category. So those shouldn't cause a problem. You shouldn't have to deal with universe issues since you only care about Type u which has homs in the same universe. Unfolding these morphisms into continuous functions and such is probably going to be a little bit of boilerplate; hopefully this doesn't come up too often, especially if you care about the global structure more than individual morphisms. So I say try Scott's proposal for presheaves and see what happens.

[Mario Carneiro]

I will be very happy if we see a real use of the category theory lib outside of category theory

[Kevin Buzzard]

@Scott Morrison I can't read the category theory code easily -- I did look at it, but all this whiskering stuff etc and the completely new language and notation basically means that I have to sit down and study it more carefully than I had time to (I was on a train when I saw your message and about to get off; I'd spent the journey finishing my own code and wasn't connected to the internet) and then when I got it I had family stuff. I'll try to get to it this evening but basically, due to my lack of experience, the code looked mostly incomprehensible to me. I'm sure I can change this.

The work I did has basically taught me what needs to be done to define an equiv of these objects. I had to deal with heqs, although they turned out painless, and some proofs really had me scratching my head for a while, but I got through them all in the end. Once I have wrestled through all the foreign notation, which I will have to do at some stage, I'll be able to make some kind of judgement as to what this category theory stuff is buying me.

[Kevin Buzzard]

@[simp] theorem id' (U : opens X) (x : ℱ.F U) (h) : ℱ.res h x = x := ℱ.id _ _

That's a crazy use of h :-) I hadn't really internalised that trick until now.

[Kevin Buzzard]

Lean infers it must be a proof of U \sub U

[Kevin Buzzard]

def pushforward (f : X → Y) [hf : continuous f] (ℱ : presheaf_of_typesU X) :
  presheaf_of_typesU Y :=
{ F := λ V, ℱ.F ⟨f ⁻¹' V, hf _ V.2⟩,
  res := λ _ _ hUV, ℱ.res (λ _ hx, hUV hx),
  id := λ _, ℱ.id _,
  comp := λ U V W hUV hVW, ℱ.comp _ _,
}

Any reason why you didn't use opens.comap in the definition of F?

[Kevin Buzzard]

theorem ext {α β : f_map 𝒢 ℱ} (hf : α.f = β.f)
(hρ : ∀ V x, α.ρ V x = ℱ.res (le_of_eq (by congr')) (β.ρ V x)) : α = β :=

You have a heq-free ext! Probably very wise :-)

[Scott Morrison]

@Kevin Buzzard --- stop reading Mario's version, and start reading mine. :-) You'll see the same tricks being used, because Mario showed them to me when I wrote my version last year.

[Scott Morrison]

And you'll see I do use opens.map (which is the already-in-mathlib synonym for the opens.comap you've been using) in the definition of the pushforward.

[Kevin Buzzard]

I want to read Mario's first because it's much easier for me :-) I'll read yours next!

[Mario Carneiro]

oops, I missed that one

[Patrick Massot]

I would love to use the category theory Scott, Reid and Johan worked on. But I totally understand Kevin's reaction. Clearly the code is frightening. I hope one day I'll learn to read it

[Kevin Buzzard]

My proof of equiv.refl was much worse than Mario's because I had not yet proved id_comp -- I only realised I needed it when I was proving equiv.trans :-)

[Kevin Buzzard]

OK so I just read all of Mario's code and the main thing I learnt was that the heq can be avoided.

[Kevin Buzzard]

Ok now to brave Scott's :-/

[Kevin Buzzard]

After 2 minutes I have decided that I cannot possibly read Scott's code unless I read it in Lean, but I thankfully now understand git well enough nowadays to pull his PR branch and compile it. Back in 15 minutes.

[Kevin Buzzard]

Until then, Scott let me give you some idea what I think when I look at your code:

structure Presheaf :=
(X : Top.{v})
(𝒪 : (opens X)ᵒᵖ ⥤ C)

structure Presheaf_hom (F G : Presheaf.{v} C) :=
(f : F.X ⟶ G.X)
(c : G.𝒪 ⟹ ((opens.map f).op ⋙ F.𝒪))

I think "What is ⥤, I guess it must be a functor, what is that insane arrow ⟶, I have no idea, what is ⟹, what is ⋙. That's why I can't just sit down and read your code. But you have made it amply clear that now is the time to start finding out.

[Scott Morrison]

Oh dear. I'm sorry, I had no idea you didn't even know the arrows. :-) Sorry.

[Scott Morrison]

The insane arrow ⟶ is just the "morphism in a category" arrow. Think of it just like the usual arrow in Type, but on steroids.

[Scott Morrison]

(In fact, you can use the "insane" arrow in place of the normal arrow, for types. This will pull in the category instance on Type, and be definitionally equal to the normal arrow.)

[Scott Morrison]

⥤ is the functor arrow

[Scott Morrison]

⟹ is the natural transformation arrow.

[Scott Morrison]

≫ is composition of morphisms (so if f : X \hom Y, and g : Y \hom Z, you can write f ≫ g to get a X \hom Z)

[Scott Morrison]

⋙ is composition of functors.

[Scott Morrison]

and finally, in the definition of composition of Presheaf_hom, (and in ext),

[Scott Morrison]

⊟ is "vertical composition of natural transformations"

[Scott Morrison]

Finally, the last piece of notation is the one you've been asking about: ≅, which gives you all the different notations of equivalence, all with uniform notation. :-)

[Mario Carneiro]

and .op?

[Scott Morrison]

As an example, we have

/-- `opens.map f` gives the functor from open sets in Y to open set in X,
    given by taking preimages under f. -/
def map
  {X Y : Top.{u}} (f : X ⟶ Y) : opens Y ⥤ opens X :=
{ obj := λ U, ⟨ f.val ⁻¹' U, f.property _ U.property ⟩,
  map := λ U V i, ⟨ ⟨ λ a b, i.down.down b ⟩ ⟩ }.

def map_iso {X Y : Top.{u}} (f g : X ⟶ Y) (h : f = g) : map f ≅ map g := ...

In the last line there is an appearance of ≅. Lean looks at this, realises that both map f and map g are functors from opens Y to opens X, successfully realises there are category structures on both of these, whose morphisms are natural transformations, so ≅ must mean an isomorphism in that category, i.e., a natural isomorphism. (No special notation or special cases for functor_equiv!)

[Scott Morrison]

@Mario Carneiro, unfortunately there are several ops, and it's still too confusing. This .op is applied as field notation to a functor, so it must be functor.op, which takes a F : C \func D and spits out a functor C^\op \func D^\op.

[Mario Carneiro]

I guess this isn't going to give you a generic function from A ≅ B to the plain equiv A ~= B?

[Mario Carneiro]

what's the .down.down in the definition of opens.map for?

[Scott Morrison]

We can possibly fix that .down.down now, actually. We used to not be able to define categories with morphisms in Prop.

[Scott Morrison]

This was recently fixed.

[Patrick Massot]

I find it strange that I used to think I knew what was a sheaf but never needed to learn "vertical composition of natural transformations"

[Scott Morrison]

So the definition of hom in opens X is ulift (plift X <= Y)

[Scott Morrison]

Okay, but if you don't learn the definition of "vertical composition of natural transformations" you will spend the rest of your life checking more naturality squares than you need to. :-)

[Patrick Massot]

Who checks naturality squares anyway?

[Scott Morrison]

...

[Scott Morrison]

mostly tidy, to be honest.

[Scott Morrison]

It exists precisely because I don't check naturality squares either.

[Kevin Buzzard]

Is "vertical composition of natural transformations" the same as "composition of natural transformations"?

[Kevin Buzzard]

Thanks a lot for the notation cheat sheet. I have been doing housework but am now desperate to get back to this

[Kevin Buzzard]

I did look at some category theory last summer when an UG got interested in it, and I did pick up some of the notation then, but I didn't use it since then and if I don't use things regularly then I forget them quite efficiently nowadays

[Kevin Buzzard]

So topological spaces have all limits and colimits in Lean? Do commutative rings?

[Kevin Buzzard]

Would tidy have been any use to Mario or me in our approach?

[Kevin Buzzard]

I think Ramon wrote colimits for rings ages ago

[Kevin Buzzard]

Do we have the category of topological rings?

[Kevin Buzzard]

I will be very happy if we see a real use of the category theory lib outside of category theory

Yeah but the problem is that it's a real PITA to use some unmerged branch of mathlib and we want them ASAP. I've got too used to having olean files on tap, it has made a huge difference to my workflow

[Kevin Buzzard]

I see now that it should be possible to build a category of topological rings and to make the category of presheaves of topological rings. But how to put this extra structure of an equivalence class of valuations on the stalks? Can one modify the presheaf category or does one have to start again? Am object of the category we want is a space with a presheaf of topological rings plus this extra data of valuations on the stalks and I don't immediately see how to add it.

[Kevin Buzzard]

One can pull back an equivalence class of valuations via a morphism of rings. You can think of an equivalence class of valuations on a commutative ring as just being a binary relation on the ring satisfying some axioms by the way

[Kevin Buzzard]

But the axioms are in the perfectoid project

[Kevin Buzzard]

I could never write that proof of comp_id -- it looks terrifying

[Kevin Buzzard]

Mario'scomp_id is

lemma comp_id (fℱ𝒢 : f_map ℱ 𝒢) : comp fℱ𝒢 (f_map.id 𝒢) = fℱ𝒢 :=
f_map.ext rfl $ λ V x, begin
  simp, dsimp [comp, id], simp [𝒢.comp]
end

basically painless

[Kevin Buzzard]

You shouldn't have to deal with universe issues since you only care about Type u which has homs in the same universe.

Wait wait wait I'm only sticking to Type u because you told me to! I thought I was supposed to care about being maximally polymorphic!

[Mario Carneiro]

I mean that the homs of the category Type u live in a particular universe, namely Type u, rather than some arbitrary other universe. So you don't have to deal with the two-variable problem that appears in general categories

[Mario Carneiro]

There is no category Type* that spans multiple universes anyway

[Mario Carneiro]

aka "Type u is a large_category"

[Kevin Buzzard]

But there's some other two variable problem -- aah but maybe Scott's approach solves this correctly?

[Scott Morrison]

Okay, I will definitely need to look at comp_id.

[Mario Carneiro]

What scott's approach will not give you is a way to talk about homs between presheaves living in different universes. There is basically no way to have a holistic view of these cross-universe homs

[Scott Morrison]

I agree mine is bad. :-(

[Mario Carneiro]

it's basically the same problem as why functor in core only has a <$> acting on functions between types in the same universe

[Mario Carneiro]

You can use ulift to recover some universe polymorphism

[Scott Morrison]

Okay, @Kevin Buzzard, @Johan Commelin, I have refactored quite a bit, pulling out the stuff that is about presheaves on a fixed space, and then later doing pairs (space, presheaf on it).

[Scott Morrison]

The proofs are much simpler now.

[Scott Morrison]

e.g. my comp_id and so on are so much simpler they have disappeared :-) (Once they are down to ext; dsimp; simp I'm happy to omit them and let tidy fill them in!)

[Scott Morrison]

I wrote some stuff about stalks.

[Scott Morrison]

And got as far as constructing
def stalk_map {F G : Presheaf.{v} C} (α : F ⟶ G) (x : F.X) : stalk (α.f x) ⟶ stalk x := ...

[Scott Morrison]

I have proved nothing about about that map, at this point, however, so I don't know whether it is usable.

[Johan Commelin]

I'm not sure if I like your "hack" where you replace opens X with its opposite...

[Scott Morrison]

I knew you wouldn't like this.

[Scott Morrison]

It just saves so so much pain, you wouldn't believe.

[Johan Commelin]

That doesn't sound good

[Scott Morrison]

I can rename it if you like, but I'm not going to be able to write this stuff with explicit ops everywhere.

[Johan Commelin]

What if we want to do the etale site?

[Johan Commelin]

We will need to deal with the ops there...

[Johan Commelin]

But we can worry about that in the future.

[Scott Morrison]

That sounds like a good place to deal with them. :-)

[Johan Commelin]

So... let's redefine stalks using filtered colimits...

[Johan Commelin]

That means we first need a definition of filtered colimit in mathlib

[Scott Morrison]

I should sleep soon, but I agree this is a good thing to do, and we're actually not that far.

[Scott Morrison]

Do you want to talk about it tomorrow? I can probably find some time.

[Scott Morrison]

We could even try out the new VS Code collaborative mode :-)

[Patrick Massot]

Thank you very much Scott

[Johan Commelin]

I'm not sure if I have time tomorrow... maybe...

[Scott Morrison]

I'm doing presheaves with preorders on the stalks right now. :-)

[Reid Barton]

Nooooo you need the ops

[Reid Barton]

How would you even define sheaves? "A collection of maps $\{U \to U_\alpha\}$ is a co-cover if ..."?

[Reid Barton]

Does it save real pain, or does it just save writing op a lot?

[Reid Barton]

@Scott Morrison I'm not sure how far you got with filtered colimits, but I pushed my old implementation which I never got around to PRing to the filtered-colimits branch

[Reid Barton]

https://github.com/leanprover-community/mathlib/commit/bc457fb5716fbffe63cbcc10b4ce7a253c720f84

[Reid Barton]

Is "vertical composition of natural transformations" the same as "composition of natural transformations"?

Yes.

[Scott Morrison]

Ok, I think while walking the dog I understood what my problem with the ops has been, and I hope that I can restore them. The price that is I will have to define opens.op_map : (opens X)^op \func (opens Y)^op separately from opens.map, rather than just using (opens.map).op as I have been. This is only a few lines of duplication.

[Kevin Buzzard]

I should say that in contrast to Johan, I don't mind at all about you having reversed the arrows in opens X -- you could even have just defined opens_op X. But if you think you've figured out what's going on then great :-)

[Scott Morrison]

The underlying problem is that opens.map is really a 2-functor from {topological spaces}<={continuous maps}<={equalities} to {categories}<={functors}<={nat trans}, and so we have some dependent type theory hell waiting the break loose. Too many ops in the wrong places prevent things simplifying at the right moments.

[Scott Morrison]

Another realisation while walking the dog is that since we've generalised the category theory library to allow Prop valued homs, the avenue is open to using "functor extensionality" for functors into Prop-level categories. The point is that you only need to check equality on objects, and then proof irrelevance guarantees equality of morphisms. This means that the usual eq.rec balrog that functor extensionality rouses should not be a problem.

[Scott Morrison]

I'm not quite there with "bundled presheaves whose stalks have preorders, and whose morphisms preserve the preorders", but I think I'm pretty close. Hopefully this afternoon. :-)

[Kevin Buzzard]

Yes, I didn't know how you were going to do this. I did wonder whether doing presheaves in the funky functor way would somehow not really help, whereas with the structures Mario and I made you can just add more fields

[Scott Morrison]

I'm just doing more fields, too.

[Kevin Buzzard]

I don't know how to add more fields to the objects of a category

[Scott Morrison]

Just bundle more. A object of the new category is an object of the old category, along with some extra piece of data.

[Kevin Buzzard]

I just didn't know how easy this was to do in practice. Of course the morphisms change too etc.

[Kevin Buzzard]

With structures I can see how it all would work but in this bundled setting I don't have the experience.

[Scott Morrison]

Hi @Reid Barton, no I've done basically nothing on filtered colimits yet, so this is great.

[Scott Morrison]

Can we PR it?