## Stream: general

### Topic: universes in structures

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

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

#### Mario Carneiro (Apr 04 2019 at 07:38):

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

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

#### Mario Carneiro (Apr 04 2019 at 07:38):

and we will see if an issue arises later

#### Kevin Buzzard (Apr 04 2019 at 07:39):

So you are (1)-averse?

#### Mario Carneiro (Apr 04 2019 at 07:39):

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

#### Kevin Buzzard (Apr 04 2019 at 07:39):

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

#### Mario Carneiro (Apr 04 2019 at 07:39):

I think the friction isn't worth it to you

#### Kevin Buzzard (Apr 04 2019 at 07:40):

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

#### Mario Carneiro (Apr 04 2019 at 07:40):

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

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

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

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

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

#### Mario Carneiro (Apr 04 2019 at 07:42):

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

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

#### Mario Carneiro (Apr 04 2019 at 07:43):

That's what I mean

#### Kevin Buzzard (Apr 04 2019 at 07:43):

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

#### Kevin Buzzard (Apr 04 2019 at 07:43):

and I am pain averse

#### Mario Carneiro (Apr 04 2019 at 07:43):

you have to use ulift

#### Kevin Buzzard (Apr 04 2019 at 07:43):

ulift is a closed book to me

#### Mario Carneiro (Apr 04 2019 at 07:43):

it's a universe shifting function that preserves all structure

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

is it canonical?

#### Mario Carneiro (Apr 04 2019 at 07:44):

ah, there is that

#### Kevin Buzzard (Apr 04 2019 at 07:44):

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

#### Mario Carneiro (Apr 04 2019 at 07:44):

sure it's canonical

#### Mario Carneiro (Apr 04 2019 at 07:44):

it's like the canonical injection map

#### Kevin Buzzard (Apr 04 2019 at 07:44):

they are taking values in a totally ordered monoid

#### Kevin Buzzard (Apr 04 2019 at 07:45):

I love that I managed to get you to say canonical

#### Mario Carneiro (Apr 04 2019 at 07:45):

in ZFC it is just inclusion

#### Kevin Buzzard (Apr 04 2019 at 07:45):

when neither of us know what it means

#### Kevin Buzzard (Apr 04 2019 at 07:45):

that's just how it works in maths too

#### Mario Carneiro (Apr 04 2019 at 07:45):

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

#### Kevin Buzzard (Apr 04 2019 at 07:45):

we sagely nod and agree that it's canonical

#### Kevin Buzzard (Apr 04 2019 at 07:46):

is it functorial?

#### Mario Carneiro (Apr 04 2019 at 07:46):

yep, it is all the things

#### Kevin Buzzard (Apr 04 2019 at 07:46):

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

#### Mario Carneiro (Apr 04 2019 at 07:46):

it's also a thing

#### Mario Carneiro (Apr 04 2019 at 07:47):

which is one more than no thing

#### Kevin Buzzard (Apr 04 2019 at 07:47):

You can look forward to the "ulift hell" thread

#### Kevin Buzzard (Apr 04 2019 at 07:47):

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

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

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

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


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

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

#### Johan Commelin (Apr 04 2019 at 13:19):

I.e. unbundled presheaves on bundled spaces.

#### Johan Commelin (Apr 04 2019 at 13:19):

Of course this is just a functor category...

#### Johan Commelin (Apr 04 2019 at 13:19):

But we might want some specialised coercions/simp lemmas

#### Scott Morrison (Apr 04 2019 at 13:21):

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

#### Johan Commelin (Apr 04 2019 at 13:22):

The push-forward functor should be easily accessible

#### Johan Commelin (Apr 04 2019 at 13:23):

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

#### Johan Commelin (Apr 04 2019 at 13:23):

I didn't experiment with it though

#### Johan Commelin (Apr 04 2019 at 13:24):

Need to run to catch a train

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

#### Reid Barton (Apr 04 2019 at 14:28):

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

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

#### Reid Barton (Apr 04 2019 at 14:36):

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

#### Reid Barton (Apr 04 2019 at 14:38):

maybe this opens too many cans of worms at once

#### Kevin Buzzard (Apr 04 2019 at 18:45):

I wrote an unbundled version of presheaves of types.

#### Kevin Buzzard (Apr 04 2019 at 18:46):

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

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

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

#### Mario Carneiro (Apr 04 2019 at 18:54):

heqs sounds bad, where did they come up?

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

#### Kevin Buzzard (Apr 04 2019 at 18:56):

heqs came up because I was changing X.

#### Kevin Buzzard (Apr 04 2019 at 18:57):

I instantly turned every heq into an eq

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

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

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

#### Kevin Buzzard (Apr 04 2019 at 19:04):

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 (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⟩


#### Kevin Buzzard (Apr 04 2019 at 19:05):

Yeah, I couldn't find that!

#### Kevin Buzzard (Apr 04 2019 at 19:06):

I read all of topology.opens :-)

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

#### Mario Carneiro (Apr 04 2019 at 19:06):

you may also want to bundle continuous maps for this purpose

#### Kevin Buzzard (Apr 04 2019 at 19:07):

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

#### Kevin Buzzard (Apr 04 2019 at 19:07):

Oh -- you mean continuous_map X Y?

yes

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

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

#### 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 _

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

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

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

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

#### 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 :-(

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

#### Kevin Buzzard (Apr 04 2019 at 19:47):

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

#### Kevin Buzzard (Apr 04 2019 at 19:47):

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

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

#### Mario Carneiro (Apr 04 2019 at 20:02):

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

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


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

#### Kevin Buzzard (Apr 04 2019 at 20:13):

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

#### Johan Commelin (Apr 04 2019 at 20:14):

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

#### Johan Commelin (Apr 04 2019 at 20:15):

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

#### Johan Commelin (Apr 04 2019 at 20:15):

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

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

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

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

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

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

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

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

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

#### Scott Morrison (Apr 04 2019 at 20:41):

Please tell me if I'm missing something.

#### Mario Carneiro (Apr 04 2019 at 20:42):

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

Grah!!!

#### Mario Carneiro (Apr 04 2019 at 20:43):

Where is opens.map?

#### Scott Morrison (Apr 04 2019 at 20:44):

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

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

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

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

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

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

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

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

#### Kevin Buzzard (Apr 04 2019 at 21:01):

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

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

#### Kevin Buzzard (Apr 04 2019 at 21:06):

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

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

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

#### Mario Carneiro (Apr 04 2019 at 21:13):

oops, I missed that one

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

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

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

#### Kevin Buzzard (Apr 04 2019 at 21:16):

Ok now to brave Scott's :-/

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

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

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

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

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

#### Scott Morrison (Apr 04 2019 at 21:28):

⥤ is the functor arrow

#### Scott Morrison (Apr 04 2019 at 21:28):

⟹ is the natural transformation arrow.

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

#### Scott Morrison (Apr 04 2019 at 21:29):

⋙ is composition of functors.

#### Scott Morrison (Apr 04 2019 at 21:30):

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

#### Scott Morrison (Apr 04 2019 at 21:30):

⊟ is "vertical composition of natural transformations"

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

#### Mario Carneiro (Apr 04 2019 at 21:32):

and .op?

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

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

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

#### Mario Carneiro (Apr 04 2019 at 21:36):

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

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

#### Scott Morrison (Apr 04 2019 at 21:44):

This was recently fixed.

#### 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"

#### Scott Morrison (Apr 04 2019 at 21:45):

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

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

#### Patrick Massot (Apr 04 2019 at 21:46):

Who checks naturality squares anyway?

...

#### Scott Morrison (Apr 04 2019 at 21:46):

mostly tidy, to be honest.

#### Scott Morrison (Apr 04 2019 at 21:46):

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

#### Kevin Buzzard (Apr 04 2019 at 22:01):

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

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

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

#### Kevin Buzzard (Apr 04 2019 at 22:30):

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

#### Kevin Buzzard (Apr 04 2019 at 22:32):

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

#### Kevin Buzzard (Apr 04 2019 at 22:40):

I think Ramon wrote colimits for rings ages ago

#### Kevin Buzzard (Apr 04 2019 at 22:44):

Do we have the category of topological rings?

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

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

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

#### Kevin Buzzard (Apr 04 2019 at 23:00):

But the axioms are in the perfectoid project

#### Kevin Buzzard (Apr 04 2019 at 23:02):

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

#### Kevin Buzzard (Apr 04 2019 at 23:05):

Mario'scomp_id is

lemma comp_id (fℱ𝒢 : f_map ℱ 𝒢) : comp fℱ𝒢 (f_map.id 𝒢) = fℱ𝒢 :=

#### Mario Carneiro (Apr 04 2019 at 23:48):

You can use ulift to recover some universe polymorphism

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

#### Scott Morrison (Apr 05 2019 at 11:03):

The proofs are much simpler now.

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

#### Scott Morrison (Apr 05 2019 at 11:03):

I wrote some stuff about stalks.

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

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

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

#### Scott Morrison (Apr 05 2019 at 11:11):

I knew you wouldn't like this.

#### Scott Morrison (Apr 05 2019 at 11:11):

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

#### Johan Commelin (Apr 05 2019 at 11:12):

That doesn't sound good

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

#### Johan Commelin (Apr 05 2019 at 11:12):

What if we want to do the etale site?

#### Johan Commelin (Apr 05 2019 at 11:12):

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

#### Johan Commelin (Apr 05 2019 at 11:13):

But we can worry about that in the future.

#### Scott Morrison (Apr 05 2019 at 11:13):

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

#### Johan Commelin (Apr 05 2019 at 11:13):

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

#### Johan Commelin (Apr 05 2019 at 11:14):

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

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

#### Scott Morrison (Apr 05 2019 at 11:39):

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

#### Scott Morrison (Apr 05 2019 at 11:39):

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

#### Patrick Massot (Apr 05 2019 at 11:39):

Thank you very much Scott

#### Johan Commelin (Apr 05 2019 at 11:40):

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

#### Scott Morrison (Apr 05 2019 at 11:40):

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

#### Reid Barton (Apr 05 2019 at 12:33):

Nooooo you need the ops

#### Reid Barton (Apr 05 2019 at 12:34):

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

#### Reid Barton (Apr 05 2019 at 12:35):

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

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

#### Reid Barton (Apr 05 2019 at 15:44):

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

#### Reid Barton (Apr 05 2019 at 17:05):

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

Yes.

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

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

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

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

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

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

#### Scott Morrison (Apr 05 2019 at 22:37):

I'm just doing more fields, too.

#### Kevin Buzzard (Apr 05 2019 at 22:45):

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

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

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

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

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

#### Scott Morrison (Apr 06 2019 at 02:34):

Can we PR it?

Last updated: May 10 2021 at 00:31 UTC