Zulip Chat Archive

Stream: general

Topic: universes in structures


view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:36):

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?

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:36):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:38):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:38):

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?

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:38):

and we will see if an issue arises later

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:39):

So you are (1)-averse?

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:39):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:39):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:39):

I think the friction isn't worth it to you

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:40):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:40):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:40):

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?

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:41):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:42):

@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?

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:42):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:42):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:42):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:43):

That's what I mean

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:43):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:43):

and I am pain averse

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:43):

you have to use ulift

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:43):

ulift is a closed book to me

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:43):

it's a universe shifting function that preserves all structure

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:43):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:44):

is it canonical?

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:44):

ah, there is that

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:44):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:44):

sure it's canonical

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:44):

it's like the canonical injection map

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:44):

they are taking values in a totally ordered monoid

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:45):

I love that I managed to get you to say canonical

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:45):

in ZFC it is just inclusion

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:45):

when neither of us know what it means

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:45):

that's just how it works in maths too

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:45):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:45):

we sagely nod and agree that it's canonical

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:46):

is it functorial?

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:46):

yep, it is all the things

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:46):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:46):

it's also a thing

view this post on Zulip Mario Carneiro (Apr 04 2019 at 07:47):

which is one more than no thing

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:47):

You can look forward to the "ulift hell" thread

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:47):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 07:49):

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...

view this post on Zulip Scott Morrison (Apr 04 2019 at 13:17):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 13:17):

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 := ...

view this post on Zulip Scott Morrison (Apr 04 2019 at 13:18):

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

view this post on Zulip Johan Commelin (Apr 04 2019 at 13:19):

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

view this post on Zulip Johan Commelin (Apr 04 2019 at 13:19):

I.e. unbundled presheaves on bundled spaces.

view this post on Zulip Johan Commelin (Apr 04 2019 at 13:19):

Of course this is just a functor category...

view this post on Zulip Johan Commelin (Apr 04 2019 at 13:19):

But we might want some specialised coercions/simp lemmas

view this post on Zulip Scott Morrison (Apr 04 2019 at 13:21):

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

view this post on Zulip Johan Commelin (Apr 04 2019 at 13:22):

The push-forward functor should be easily accessible

view this post on Zulip Johan Commelin (Apr 04 2019 at 13:23):

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

view this post on Zulip Johan Commelin (Apr 04 2019 at 13:23):

I didn't experiment with it though

view this post on Zulip Johan Commelin (Apr 04 2019 at 13:24):

Need to run to catch a train

view this post on Zulip Reid Barton (Apr 04 2019 at 14:27):

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

view this post on Zulip Reid Barton (Apr 04 2019 at 14:28):

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

view this post on Zulip Reid Barton (Apr 04 2019 at 14:34):

(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.)

view this post on Zulip Reid Barton (Apr 04 2019 at 14:36):

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

view this post on Zulip Reid Barton (Apr 04 2019 at 14:38):

maybe this opens too many cans of worms at once

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:45):

I wrote an unbundled version of presheaves of types.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:46):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:47):

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.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:53):

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.

view this post on Zulip Mario Carneiro (Apr 04 2019 at 18:54):

heqs sounds bad, where did they come up?

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:56):

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).

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:56):

heqs came up because I was changing X.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:57):

I instantly turned every heq into an eq

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:57):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:58):

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 ==

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 18:59):

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.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:04):

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

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 19:05):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:05):

Yeah, I couldn't find that!

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:06):

I read all of topology.opens :-)

view this post on Zulip Mario Carneiro (Apr 04 2019 at 19:06):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 19:06):

you may also want to bundle continuous maps for this purpose

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:07):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:07):

Oh -- you mean continuous_map X Y?

view this post on Zulip Mario Carneiro (Apr 04 2019 at 19:07):

yes

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:10):

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.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:24):

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 :-)

view this post on Zulip Mario Carneiro (Apr 04 2019 at 19:25):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 19:27):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:27):

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.

view this post on Zulip Mario Carneiro (Apr 04 2019 at 19:29):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:30):

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.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:32):

Lovely lines such as

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

now don't compile at all :-(

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:44):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:47):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:47):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 19:47):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 20:02):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 20:03):

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))

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 20:12):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 20:13):

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

view this post on Zulip Johan Commelin (Apr 04 2019 at 20:14):

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

view this post on Zulip Johan Commelin (Apr 04 2019 at 20:15):

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

view this post on Zulip Johan Commelin (Apr 04 2019 at 20:15):

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

view this post on Zulip Johan Commelin (Apr 04 2019 at 20:16):

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.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 20:16):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 20:18):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 20:35):

@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?

view this post on Zulip Scott Morrison (Apr 04 2019 at 20:36):

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.

view this post on Zulip Scott Morrison (Apr 04 2019 at 20:37):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 20:39):

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.

view this post on Zulip Scott Morrison (Apr 04 2019 at 20:40):

@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.

view this post on Zulip Scott Morrison (Apr 04 2019 at 20:41):

Please tell me if I'm missing something.

view this post on Zulip Mario Carneiro (Apr 04 2019 at 20:42):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 20:43):

Grah!!!

view this post on Zulip Mario Carneiro (Apr 04 2019 at 20:43):

Where is opens.map?

view this post on Zulip Scott Morrison (Apr 04 2019 at 20:44):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 20:44):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 20:45):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 20:46):

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....)

view this post on Zulip Mario Carneiro (Apr 04 2019 at 20:55):

@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.

view this post on Zulip Mario Carneiro (Apr 04 2019 at 20:56):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 20:59):

@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.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 21:01):

@[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.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 21:01):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 21:03):

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?

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 21:06):

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

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:09):

@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.

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:10):

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.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 21:10):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 21:13):

oops, I missed that one

view this post on Zulip Patrick Massot (Apr 04 2019 at 21:14):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 21:15):

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 :-)

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 21:16):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 21:16):

Ok now to brave Scott's :-/

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 21:22):

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.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 21:25):

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.

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:26):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:27):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:28):

(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.)

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:28):

is the functor arrow

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:28):

is the natural transformation arrow.

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:29):

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)

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:29):

is composition of functors.

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:30):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:30):

is "vertical composition of natural transformations"

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:32):

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. :-)

view this post on Zulip Mario Carneiro (Apr 04 2019 at 21:32):

and .op?

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:34):

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!)

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:35):

@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.

view this post on Zulip Mario Carneiro (Apr 04 2019 at 21:35):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 21:36):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:44):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:44):

This was recently fixed.

view this post on Zulip Patrick Massot (Apr 04 2019 at 21:44):

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"

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:45):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:45):

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. :-)

view this post on Zulip Patrick Massot (Apr 04 2019 at 21:46):

Who checks naturality squares anyway?

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:46):

...

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:46):

mostly tidy, to be honest.

view this post on Zulip Scott Morrison (Apr 04 2019 at 21:46):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 22:01):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 22:08):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 22:22):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 22:30):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 22:32):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 22:40):

I think Ramon wrote colimits for rings ages ago

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 22:44):

Do we have the category of topological rings?

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 22:53):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 22:58):

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.

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 22:59):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 23:00):

But the axioms are in the perfectoid project

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 23:02):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 23:05):

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

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 23:10):

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!

view this post on Zulip Mario Carneiro (Apr 04 2019 at 23:40):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 23:41):

There is no category Type* that spans multiple universes anyway

view this post on Zulip Mario Carneiro (Apr 04 2019 at 23:41):

aka "Type u is a large_category"

view this post on Zulip Kevin Buzzard (Apr 04 2019 at 23:44):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 23:46):

Okay, I will definitely need to look at comp_id.

view this post on Zulip Mario Carneiro (Apr 04 2019 at 23:47):

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

view this post on Zulip Scott Morrison (Apr 04 2019 at 23:47):

I agree mine is bad. :-(

view this post on Zulip Mario Carneiro (Apr 04 2019 at 23:48):

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

view this post on Zulip Mario Carneiro (Apr 04 2019 at 23:48):

You can use ulift to recover some universe polymorphism

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:03):

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).

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:03):

The proofs are much simpler now.

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:03):

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!)

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:03):

I wrote some stuff about stalks.

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:04):

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

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:05):

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

view this post on Zulip Johan Commelin (Apr 05 2019 at 11:08):

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

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:11):

I knew you wouldn't like this.

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:11):

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

view this post on Zulip Johan Commelin (Apr 05 2019 at 11:12):

That doesn't sound good

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:12):

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

view this post on Zulip Johan Commelin (Apr 05 2019 at 11:12):

What if we want to do the etale site?

view this post on Zulip Johan Commelin (Apr 05 2019 at 11:12):

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

view this post on Zulip Johan Commelin (Apr 05 2019 at 11:13):

But we can worry about that in the future.

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:13):

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

view this post on Zulip Johan Commelin (Apr 05 2019 at 11:13):

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

view this post on Zulip Johan Commelin (Apr 05 2019 at 11:14):

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

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:39):

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

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:39):

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

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:39):

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

view this post on Zulip Patrick Massot (Apr 05 2019 at 11:39):

Thank you very much Scott

view this post on Zulip Johan Commelin (Apr 05 2019 at 11:40):

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

view this post on Zulip Scott Morrison (Apr 05 2019 at 11:40):

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

view this post on Zulip Reid Barton (Apr 05 2019 at 12:33):

Nooooo you need the ops

view this post on Zulip Reid Barton (Apr 05 2019 at 12:34):

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

view this post on Zulip Reid Barton (Apr 05 2019 at 12:35):

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

view this post on Zulip Reid Barton (Apr 05 2019 at 15:43):

@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

view this post on Zulip Reid Barton (Apr 05 2019 at 15:44):

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

view this post on Zulip Reid Barton (Apr 05 2019 at 17:05):

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

Yes.

view this post on Zulip Scott Morrison (Apr 05 2019 at 22:22):

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.

view this post on Zulip Kevin Buzzard (Apr 05 2019 at 22:23):

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 :-)

view this post on Zulip Scott Morrison (Apr 05 2019 at 22:24):

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.

view this post on Zulip Scott Morrison (Apr 05 2019 at 22:27):

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.

view this post on Zulip Scott Morrison (Apr 05 2019 at 22:28):

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. :-)

view this post on Zulip Kevin Buzzard (Apr 05 2019 at 22:29):

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

view this post on Zulip Scott Morrison (Apr 05 2019 at 22:37):

I'm just doing more fields, too.

view this post on Zulip Kevin Buzzard (Apr 05 2019 at 22:45):

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

view this post on Zulip Scott Morrison (Apr 05 2019 at 22:46):

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

view this post on Zulip Kevin Buzzard (Apr 05 2019 at 22:49):

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

view this post on Zulip Kevin Buzzard (Apr 05 2019 at 22:49):

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

view this post on Zulip Scott Morrison (Apr 06 2019 at 02:34):

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

view this post on Zulip Scott Morrison (Apr 06 2019 at 02:34):

Can we PR it?


Last updated: May 10 2021 at 00:31 UTC