## Stream: maths

### Topic: sheaves and sites

#### Johan Commelin (Nov 08 2018 at 13:34):

Lol, I'm quite sure that the definition of coverage is wrong. I should demand that the collection of covers contains the singletons {id : U ⟶ U} for every U : X.

#### Johan Commelin (Nov 08 2018 at 13:35):

If I'm right, this is also missing on nLab.

#### Johan Commelin (Nov 12 2018 at 15:28):

I retract this. There is a comment on nLab pointing out that you don't need to demand that identity morphisms cover. It doesn't change your category of sheaves.

#### Kenny Lau (Nov 12 2018 at 15:29):

did you say nlab...

#### Kenny Lau (Nov 12 2018 at 15:30):

man you've gone too far...

#### Johan Commelin (Nov 12 2018 at 19:11):

opens X is now a site!
https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/sheaf.lean#L245

#### Johan Commelin (Nov 12 2018 at 19:11):

This is one of the ugliest proofs I've written in a long time.

#### Johan Commelin (Nov 12 2018 at 19:17):

Also, I would like to get some feedback on the definition of the covers for opens X. This is the actual data that goes into a site. The rest doesn't matter, because it's only proofs. (They should of course be faster then what I have now.)
Basically, there are at least three (equivalent) ways to specify the data of covers:
1) covers := λ U Us, U.val = ⨆u∈Us, (u:over _).left.val — take the union in set X
2) covers := λ U Us, U = ⨆u∈Us, (u:over _).left — take the "union" in opens X
3) covers := λ U Us, U = limits.sigma (λ u∈Us, (u:over _)) — take the "union" as a colimit in the category over U

#### Johan Commelin (Nov 12 2018 at 19:18):

I currently have option (2). But maybe option (3) is actually better, even though it is high-brow; because it would tie in better to all the facts that we (will) have about functors/limits/etc...

#### Reid Barton (Nov 12 2018 at 19:57):

I wonder whether using actual families (instead of set everywhere) would make your life easier

#### Reid Barton (Nov 12 2018 at 20:00):

Maybe this isn't actually causing any difficulty

#### Johan Commelin (Nov 12 2018 at 20:14):

Hmm, I had that before, and it actually became harder... also, you run into more universe issues, I think.

#### Johan Commelin (Nov 13 2018 at 08:09):

sheaf.lean is now sorry-free. In particular, I have defined the site on a basis of a topology.

#### Kevin Buzzard (Nov 13 2018 at 08:10):

@Ramon Fernandez Mir you might be interested in this. @Johan Commelin where is this work? Is it on github?

#### Johan Commelin (Nov 13 2018 at 08:10):

My todo-list:

• Clean up the proofs
• Prove that continuous functions to some space T form a sheaf on X
• Generalise to sheaves with values in C (e.g., C = CommRing or Ab)
• Define stalks
• Build an API around everything

#### Johan Commelin (Nov 13 2018 at 08:11):

https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/sheaf.lean

#### Johan Commelin (Nov 13 2018 at 08:15):

@Scott Morrison Would you mind testing your most powerful version of obviously on (parts) of the proofs at the bottom of sheaf.lean? As you can see I'm mostly doing what tidy would do, except that I sprinkle an occasional rw into the mix.

#### Johan Commelin (Nov 13 2018 at 08:15):

(If you have time for this...)

#### Scott Morrison (Nov 13 2018 at 08:19):

Hi @Johan Commelin , we should combine/adapt the stuff I wrote on bundled presheaves at some point, with a category structure based on:

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

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


#### Scott Morrison (Nov 13 2018 at 08:19):

Am I right that you haven't got this yet?

#### Scott Morrison (Nov 13 2018 at 08:19):

I think most of the other stuff I'd done previously on sheaves is all obsolete by your recent progress.

#### Johan Commelin (Nov 13 2018 at 08:22):

(I don't have stalks yet :lol:)

#### Johan Commelin (Nov 13 2018 at 08:22):

Why would you want the bundled presheaves?

#### Johan Commelin (Nov 13 2018 at 08:23):

To define morphisms of ringed spaces?

#### Johan Commelin (Nov 13 2018 at 08:23):

I think I would first do that unbundled.

#### Johan Commelin (Nov 13 2018 at 08:48):

Hmmm, I just realised that I don't even know what it means to be a sheaf with values in C when working on an arbitrary site.
I can make sense of it

• if the site has pullbacks, or
• if C is concrete in the sense that it comes with a forgetful functor to Type.

#### Johan Commelin (Nov 13 2018 at 09:03):

@Mario Carneiro Do you have any tips on what the right "go-for-it" route would be in this case?

#### Johan Commelin (Nov 13 2018 at 09:03):

We want sheaves of rings.
There are 23 definitions that are all math-equivalent.

#### Harry Gindi (Nov 13 2018 at 09:46):

There's no way to do it as a ring object in sheaves?

#### Johan Commelin (Nov 13 2018 at 09:47):

That is one of the 23 possibilities (-;

#### Johan Commelin (Nov 13 2018 at 09:47):

But then you need to connect it to all the useful things that we know already about rings.

#### Johan Commelin (Nov 13 2018 at 09:47):

This is math-trivial, of course

#### Harry Gindi (Nov 13 2018 at 09:48):

A lot of them aren't true for sheafy rings

#### Johan Commelin (Nov 13 2018 at 09:48):

But now you actually need to justify it to a computer.

#### Johan Commelin (Nov 13 2018 at 09:48):

Sure, but there is an extremely large bunch of trivialities that are true

#### Harry Gindi (Nov 13 2018 at 09:49):

Is there any way to work with sheaves directly as nonclassical types?

#### Harry Gindi (Nov 13 2018 at 09:50):

so that all of the theorems for rings that don't use classical assertions hold?

#### Johan Commelin (Nov 13 2018 at 09:52):

What exactly do you mean?

#### Johan Commelin (Nov 13 2018 at 09:52):

Working internally in some topos?

#### Johan Commelin (Nov 13 2018 at 09:53):

Or you want to lift all constructive results into every topos?

#### Johan Commelin (Nov 13 2018 at 09:53):

Nothing like that currently exists. And pulling it off would be quite a non-trivial project.

Yeah, I agree

#### Johan Commelin (Nov 13 2018 at 09:56):

@Scott Morrison Do you think the current definition of sheaf is ok?

def sheaf (X : Type u) [𝒳 : site.{u} X] :=
{ F : presheaf X (Type u) // nonempty (site.sheaf_condition F) }


I need the ugly nonempty because is.iso is not a Prop. What is the correct Lean-idiom for this?

#### Scott Morrison (Nov 13 2018 at 09:57):

Why not just use a sigma type?

#### Scott Morrison (Nov 13 2018 at 09:57):

The category of presheaves will not care about the evidence you provide

#### Johan Commelin (Nov 13 2018 at 09:57):

I want to use full_subcategory

#### Johan Commelin (Nov 13 2018 at 09:57):

But maybe I shouldn't?

#### Scott Morrison (Nov 13 2018 at 09:57):

so use sigma_category, which I think hasn't landed in mathlib

#### Scott Morrison (Nov 13 2018 at 09:57):

but is the same idea, it just ignores the extra data

#### Scott Morrison (Nov 13 2018 at 09:58):

If you think about it, this is a perfectly sensible thing to do categorically:

#### Johan Commelin (Nov 13 2018 at 09:58):

Ok... I see. Which branch do I need to merge into sheaf to do that?

#### Johan Commelin (Nov 13 2018 at 09:58):

Yeah, the idea is obvious. I just didn't want to roll my own tooling.

#### Scott Morrison (Nov 13 2018 at 09:58):

you can have something that acts as a full subcategory, but actually makes many copies of the objects that you're keeping, according to the different ways to witness that you want them ...

/me is lazy...

#### Scott Morrison (Nov 13 2018 at 09:58):

I think it's only in lean-category-theory

#### Scott Morrison (Nov 13 2018 at 09:59):

so it's not just merging a branch

#### Johan Commelin (Nov 13 2018 at 09:59):

Aaah, then I'll leave a TODO above the current definition.

#### Harry Gindi (Nov 13 2018 at 09:59):

Is there documentation for what a sigma-category is?

#### Scott Morrison (Nov 13 2018 at 09:59):

Copy and paste

instance sigma_category (Z : C → Type w₁) : category.{(max u₁ w₁) v₁} (Σ X : C, Z X) :=
{ hom  := λ X Y, X.1 ⟶ Y.1,
id   := λ X, 𝟙 X.1,
comp := λ _ _ _ f g, f ≫ g }

def sigma_category_inclusion (Z : C → Type u₁) : (Σ X : C, Z X) ⥤ C :=
{ obj := λ X, X.1,
map' := λ _ _ f, f }

instance full_σ        (Z : C → Type u₁) : full    (sigma_category_inclusion Z)    := by obviously
instance faithful_σ    (Z : C → Type u₁) : faithful (sigma_category_inclusion Z)   := by obviously


#### Scott Morrison (Nov 13 2018 at 10:00):

into full_subcategory.lean?

#### Harry Gindi (Nov 13 2018 at 10:00):

does it have a non-type-theoretic analogue?

#### Johan Commelin (Nov 13 2018 at 10:01):

Sure, but I don't know if it actually occurs.

#### Scott Morrison (Nov 13 2018 at 10:02):

Sure. Say you have a set of objects C, and a function f : C \to Set. Make a new category with objects (X, Y), where Y is in f(X), and whose morphisms (X, Y) to (X', Y') are just the C-morphisms from X to X'.

#### Johan Commelin (Nov 13 2018 at 10:02):

It would be like taking the category of groups with all functions as morphisms

#### Scott Morrison (Nov 13 2018 at 10:02):

Does it have a name?

#### Scott Morrison (Nov 13 2018 at 10:02):

It just makes f(X) many copies of the object X.

#### Harry Gindi (Nov 13 2018 at 10:04):

it looks like it's related to the 'anafunctor' version of a subcategory?

#### Johan Commelin (Nov 13 2018 at 10:05):

@Harry Gindi Here is a math question that I don't know the answer to. In what generality do people speak of sheaves on a site $X$ with values in a category $C$?
What assumptions do I need to make on $X$ and/or $C$? Is there some grand theory that unifies everything?

#### Harry Gindi (Nov 13 2018 at 10:07):

people sometimes say "sheaves of X" in all kinds of cases, but it only makes sense when X is a subcategory of algebras for some algebraic theory rel set

#### Johan Commelin (Nov 13 2018 at 10:07):

Well, if the site $X$ has pullbacks, then I guess the sheaf condition makes sense in every category $C$ with equalizers, right?

#### Harry Gindi (Nov 13 2018 at 10:08):

yes, but it is usually the wrong thing

#### Johan Commelin (Nov 13 2018 at 10:08):

Ok, so it works but is useless.

I think so, yes

#### Johan Commelin (Nov 13 2018 at 10:10):

Ok, I'll have to think a bit about how to move this forward. I'm not sure if I'm ready for defining all the stuff related to algebraic theories.

#### Harry Gindi (Nov 13 2018 at 10:12):

It might make more sense if you could relativize algebraic stuff to like parameterized types?

#### Harry Gindi (Nov 13 2018 at 10:12):

I don't know, it's really alien to me

#### Harry Gindi (Nov 13 2018 at 10:13):

probably the easiest way is as you said

#### Harry Gindi (Nov 13 2018 at 10:14):

when the category is concrete, being a sheaf with values in C is the same thing as asking that the underlying sheaf of sets is a sheaf

#### Harry Gindi (Nov 13 2018 at 10:15):

I don't know how well that works with e.g. a sheaf of complexes

#### Harry Gindi (Nov 13 2018 at 10:16):

which is like the most important application of sheafy stuff in alg. geom, I think

#### Scott Morrison (Nov 13 2018 at 10:16):

You have to be pretty careful with this statement. It's not just "concrete" (e.g. topological rings have a faithful functor to Set) You also need that the forgetful functor is continuous and reflects isos.

#### Scott Morrison (Nov 13 2018 at 10:18):

At some point I wrote down the statement, but never attempted to prove it:

variables {V : Type (u+1)} [𝒱 : large_category V] [has_products.{u+1 u} V] (ℱ : V ⥤ (Type u))
[faithful ℱ] [category_theory.limits.preserves_limits ℱ] [reflects_isos ℱ]
include 𝒱

-- This is a good project!
def sheaf.of_sheaf_of_types
(presheaf : (opens X)ᵒᵖ ⥤ V)
(underlying_is_sheaf : is_sheaf (presheaf ⋙ ℱ)) : is_sheaf presheaf := sorry


#### Scott Morrison (Nov 13 2018 at 10:19):

(This won't be compatible with Johan's version of presheaves and sheaves, of course.)

#### Harry Gindi (Nov 13 2018 at 10:19):

I wonder if a good way to do this is with internal objects in a topos after all

#### Harry Gindi (Nov 13 2018 at 10:19):

then you could try to follow Hakim's thesis

#### Johan Commelin (Nov 13 2018 at 10:21):

I challenge you to try it :smiley:

#### Harry Gindi (Nov 13 2018 at 10:21):

I don't understand how you can say something like categories of nonclassical types satisfyinf Giraud's axioms are categories of sheaves on a site

#### Johan Commelin (Nov 13 2018 at 10:22):

What do you mean?

#### Harry Gindi (Nov 13 2018 at 10:22):

like, we might want to work internally to some Grothendieck topos

#### Harry Gindi (Nov 13 2018 at 10:23):

and the objects there would hopefully be of type "type"

#### Johan Commelin (Nov 13 2018 at 10:23):

Sure. And Type is equivalent to sheaves on unit

#### Johan Commelin (Nov 13 2018 at 10:23):

No, for an arbitrary topos the type of the objects wouldn't be Type

#### Johan Commelin (Nov 13 2018 at 10:24):

They would be of type X, where X is your topos.

#### Harry Gindi (Nov 13 2018 at 10:24):

then how can you transfer results from type type to type sheafy type

#### Johan Commelin (Nov 13 2018 at 10:24):

And so you have to develop all of type theory internal to topoi. And this hasn't been done yet in Lean. And I don't think it has been done in any theorem prover.

#### Johan Commelin (Nov 13 2018 at 10:25):

To do that "transfer" you would have to build quite a bit of machinery.

#### Harry Gindi (Nov 13 2018 at 10:25):

exactly, it looks daunting

Very daunting

#### Johan Commelin (Nov 13 2018 at 10:25):

It would take Mario a whole summer, I'm afraid.

#### Harry Gindi (Nov 13 2018 at 10:26):

one way to do it, maybe, would be to try to prove that any nonclassical theorem in type type holds when you substitute type X for type type when X is a topos?

it's not easy

#### Harry Gindi (Nov 13 2018 at 10:29):

It would probably be highly rewarding in terms of work saved

#### Harry Gindi (Nov 13 2018 at 10:34):

I should probably look in e.g. the elephant to see if there is a statement of such a theorem

#### Mario Carneiro (Nov 13 2018 at 10:51):

I'm afraid I have no idea about the math in this area

#### Mario Carneiro (Nov 13 2018 at 10:51):

I'm not sure how much of it is important to the modeling question

#### Mario Carneiro (Nov 13 2018 at 10:54):

Hmmm, I just realised that I don't even know what it means to be a sheaf with values in C when working on an arbitrary site.
I can make sense of it
* if the site has pullbacks, or
* if C is concrete in the sense that it comes with a forgetful functor to Type.

Are these two definitions related to each other? Harry says this is not the right notion in some categories?

#### Mario Carneiro (Nov 13 2018 at 10:55):

If there is a reasonable categorical interpretation of the sheaf operations or what not then that seems like a good place to start

#### Mario Carneiro (Nov 13 2018 at 10:56):

but it sounds like a "sheaf of rings" is not a sheaf over Ring as I would hope, but rather a ring object in sheaves... unfortunately I don't know any way of relating rings and ring objects in a suitably algorithmic way

#### Mario Carneiro (Nov 13 2018 at 10:58):

that is, you can define a group object, ring object etc but nothing about these definitions will connect them to the usual algebraic classes, and there won't be a general procedure for inputting a universal algebra and getting a predicate in category theory language

#### Mario Carneiro (Nov 13 2018 at 10:59):

and "internalization" is not something we can currently do in a nice way, although maybe a tactic could do it in the future

#### Johan Commelin (Nov 13 2018 at 11:36):

@Mario Carneiro Thanks for your input. I think Harry is saying that it would be best to go for the option with concrete categories, and Scott already gave a mockup of the statement.

#### Johan Commelin (Nov 13 2018 at 11:37):

You are right that a sheaf of rings is a ring object in sheaves. (At least that is one way to define it.)

#### Harry Gindi (Nov 13 2018 at 11:45):

I asked a colleague of mine who specializes in topos theory (and has lots of experience with Lean, but the HOTT branch)

#### Harry Gindi (Nov 13 2018 at 11:46):

oh yeah, he's here, Jonas

@Jonas Frey

#### Johan Commelin (Nov 13 2018 at 12:01):

I imagine that a bunch of these problems would go away when using HoTT + univalence

#### Harry Gindi (Nov 13 2018 at 13:00):

@Mario Carneiro I was saying that the notion of a sheaf with values in a category that isn't 'algebraic' in some sense is bad

#### Mario Carneiro (Nov 13 2018 at 13:00):

so what does "algebraic" mean here?

#### Harry Gindi (Nov 13 2018 at 13:01):

admits a finite limit sketch over set, I believe

#### Mario Carneiro (Nov 13 2018 at 13:01):

like what are some simple examples?

#### Harry Gindi (Nov 13 2018 at 13:01):

sheaves of categories are bad, for example

#### Mario Carneiro (Nov 13 2018 at 13:01):

I'm not really sure what the applications are here, what kinds of sheaves are good?

#### Harry Gindi (Nov 13 2018 at 13:02):

the right notion for a sheaf of categories has additional coherence conditions (cocycle conditions) that make them stacks

#### Mario Carneiro (Nov 13 2018 at 13:02):

but I presume these don't come up in the usual cases for some reason?

#### Harry Gindi (Nov 13 2018 at 13:02):

good categories for sheaves: groups, rings, abgroups, things of that nature

yeah, basically

#### Mario Carneiro (Nov 13 2018 at 13:04):

So is the "data" of a sheaf all present in an arbitrary category?

#### Mario Carneiro (Nov 13 2018 at 13:04):

or does pullbacks suffice?

#### Mario Carneiro (Nov 13 2018 at 13:05):

and somehow in a "good" category these operations have additional properties that make it work

(deleted)

#### Harry Gindi (Nov 13 2018 at 13:07):

because you can have infinite covering families

#### Mario Carneiro (Nov 13 2018 at 13:07):

I think the easy route would be to define what a sheaf is in an arbitrary category with the constructions needed in the definition itself, and then add appropriate regularity conditions for the theorems (or just prove the theorems in particular categories when needed)

#### Mario Carneiro (Nov 13 2018 at 13:08):

I would imagine that it will be easy to retrofit the theorems with more generality as needed

#### Harry Gindi (Nov 13 2018 at 13:08):

Scott's version works better than that

#### Harry Gindi (Nov 13 2018 at 13:08):

it hits all of the ones we care about

#### Mario Carneiro (Nov 13 2018 at 13:08):

I'm not sure how well "concrete categories" in the literal sense of functors to Type work in lean

#### Mario Carneiro (Nov 13 2018 at 13:09):

Scott can say better than me

#### Harry Gindi (Nov 13 2018 at 13:10):

the key feature of sheaves and presheaves is exactly that they are set-valued and the sheaf condition says something about sets

#### Harry Gindi (Nov 13 2018 at 13:12):

having a continuous conservative functor to sets is always satisfied when the category is monadic over sets

#### Kevin Buzzard (Nov 13 2018 at 13:13):

In the perfectoid project we need sheaves of topological rings

#### Harry Gindi (Nov 13 2018 at 13:13):

hmm, how are those even defined?

#### Harry Gindi (Nov 13 2018 at 13:14):

that was exactly the example Scott said would be problematic (topological groups)

#### Kevin Buzzard (Nov 13 2018 at 13:14):

well we only need them on topological spaces, so I think there are no technical issues...

#### Harry Gindi (Nov 13 2018 at 13:15):

Are they pro-rings like completions?

#### Harry Gindi (Nov 13 2018 at 13:17):

Can I see where these are defined in ordinary mathematical language?

#### Kevin Buzzard (Nov 13 2018 at 13:17):

Actually there might be some topological issue. Wait a minute, I'll dig up a reference

#### Kevin Buzzard (Nov 13 2018 at 13:19):

The map from F(U) to the stuff in prod_i F(U_i) which agree on overlaps needs to be a homeo rather than just continuous

#### Kevin Buzzard (Nov 13 2018 at 13:20):

I think that this is probably exactly the sheaf axiom for top rings

#### Harry Gindi (Nov 13 2018 at 13:20):

Yeah, I think you could get away with this because they're adic rings

#### Kevin Buzzard (Nov 13 2018 at 13:20):

I am not sure this has anything to do with it

#### Kevin Buzzard (Nov 13 2018 at 13:21):

I think that the point is that to check that a presheaf of top rings is a sheaf, it does not suffice to check that the underlying presheaf of rings is a sheaf

#### Kevin Buzzard (Nov 13 2018 at 13:21):

there is epsilon more to it than this.

#### Harry Gindi (Nov 13 2018 at 13:21):

well, continuous maps between adic rings are the natural transformations between pro-objects

#### Kevin Buzzard (Nov 13 2018 at 13:22):

These rings are not adic rings in general

ah

#### Kevin Buzzard (Nov 13 2018 at 13:22):

They are what used to be called "f-adic", which is _not_ "adic + ...", it's "has a subring which is adic + ..."

mhm

#### Kevin Buzzard (Nov 13 2018 at 13:23):

They're now called Huber rings

#### Kevin Buzzard (Nov 13 2018 at 13:23):

(terminology due to Scholze)

#### Mario Carneiro (Nov 13 2018 at 13:23):

When I said concrete categories in the literal sense I was comparing to categories that are built on actual sets and functions

#### Harry Gindi (Nov 13 2018 at 13:23):

yeah, this looks like a special situation that isn't usually covered in the classical theory, I think

#### Mario Carneiro (Nov 13 2018 at 13:24):

in which case the forgetful functor is implicit

#### Mario Carneiro (Nov 13 2018 at 13:24):

there is quite a lot you can do with concrete categories built like this

#### Harry Gindi (Nov 13 2018 at 13:25):

in that case, Kevin, maybe the answer is to do a common generalization that covers the usual situation and the one for perfectoid spaces.

#### Harry Gindi (Nov 13 2018 at 13:26):

There are also simplicial sheaves, which have a separate homotopy-theoretic component

#### Harry Gindi (Nov 13 2018 at 13:29):

and you'd end up trying to do everything in this article: https://ncatlab.org/nlab/show/model+structure+on+simplicial+presheaves#injectiveprojective__localglobal__presheavessheaves

#### Johan Commelin (Nov 13 2018 at 13:49):

@Mario Carneiro I hope the following code is parseable

T : Top,
U : opens X,
Us : covering_family U,
this : Π (u : over U), u ∈ Us → (opens.to_Top.obj (u.left) ⟶ T)
⊢ opens.to_Top.obj (⨆ (u : over U) (H : u ∈ Us), u.left) ⟶ T


Do you know if we have any stuff in topology that would help here?

#### Johan Commelin (Nov 13 2018 at 13:50):

What this is saying is: I have a bunch of functions to T defined on us that cover U. Now I want to build a function U to T.

#### Johan Commelin (Nov 13 2018 at 13:51):

Of course we need that they agree on overlaps. This is hidden in my context, but it looks ugly, so I didn't paste it.

#### Johan Commelin (Nov 13 2018 at 13:51):

Ok, so here is a more precise question: how do I check continuity locally?

#### Mario Carneiro (Nov 13 2018 at 13:52):

as with opens, I think you want a covering_family U to be a type

#### Harry Gindi (Nov 13 2018 at 13:52):

Can sieves make life easier?

#### Harry Gindi (Nov 13 2018 at 13:54):

because then you might just prove that every covering family determines a sieve

#### Mario Carneiro (Nov 13 2018 at 13:55):

why do sheaf and sieve and stack and site all sound so similar? the alliteration is killing me

#### Johan Commelin (Nov 13 2018 at 13:56):

because then you might just prove that every covering family determines a sieve

#### Harry Gindi (Nov 13 2018 at 13:57):

ah, I see, that's good. Much easier to state the sheaf condition that way!

#### Johan Commelin (Nov 13 2018 at 13:57):

Mario, I was quite happy with covering_family being a set. But maybe it should be a type.

#### Johan Commelin (Nov 13 2018 at 13:57):

ah, I see, that's good. Much easier to state the sheaf condition that way!

Sure, but now I need to actually prove that something is a sheaf :scream:

#### Mario Carneiro (Nov 13 2018 at 13:59):

that statement parses, but it isn't provable without stuff about compatibility

#### Harry Gindi (Nov 13 2018 at 13:59):

test case: Every representable is a sheaf wrt the topology generated by universal epimorphic families?

#### Johan Commelin (Nov 13 2018 at 14:00):

@Mario Carneiro Hence my more precise question...

#### Johan Commelin (Nov 13 2018 at 14:01):

@Harry Gindi Indeed. I'm proving that continuous functions X → T form a sheaf on X, for a given T.

#### Johan Commelin (Nov 13 2018 at 14:01):

So it is not as general as your test case.

#### Harry Gindi (Nov 13 2018 at 14:02):

I guess then you'd first have to define universal epimorphic families :mischievous:

#### Johan Commelin (Nov 13 2018 at 14:03):

Feel free to join in :joy_cat:

#### Harry Gindi (Nov 13 2018 at 14:03):

Talk is cheap, that's why I do it so often

#### Kenny Lau (Nov 13 2018 at 14:04):

let's just define the spectrum of a ring fist

#### Kenny Lau (Nov 13 2018 at 14:04):

(sorry, I'm a more concrete guy)

#### Johan Commelin (Nov 13 2018 at 14:05):

I'm working on it Kenny. I'm trying to define ringed spaces.

#### Harry Gindi (Nov 13 2018 at 14:06):

Hom_CRing(R, -): Ring->Set; where's my big novelty check

#### Johan Commelin (Nov 13 2018 at 14:07):

Harry, one of the first things you learn when working with provers is that there are lots of definitions that are math-trivially equivalent. But proving that they are equivalent in Lean is often very hard.

#### Johan Commelin (Nov 13 2018 at 14:07):

I'm quite sure that there is value in defining a functor from Ring^op to LRS.

#### Harry Gindi (Nov 13 2018 at 14:08):

I know, I'm being silly. This definition I just gave is meaningless even outside a theorem prover

#### Harry Gindi (Nov 13 2018 at 14:18):

Just saw this on MathOverflow, could be a useful guide: https://rawgit.com/iblech/internal-methods/master/notes.pdf

#### Harry Gindi (Nov 13 2018 at 14:18):

especially if you decide to go down the internal logic route

#### Reid Barton (Nov 13 2018 at 14:25):

@Johan Commelin, not sure how much progress you made on your gluing continuous functions question, but step 1 is to just construct the glued function even as a function, i.e., disregarding the topology of X, and then check that the glued function actually restricts to the original guys

#### Reid Barton (Nov 13 2018 at 14:26):

then step 2 would be to check continuity, possibly you can use continuous_subtype_nhds_cover for this

#### Reid Barton (Nov 13 2018 at 14:26):

You might find https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.1/src/homotopy_theory/topological_spaces/inter_union.lean a useful guide though there I was only interested in the case of two (closed) subsets

#### Johan Commelin (Nov 13 2018 at 14:28):

Ok, thanks for the tips.

#### Reid Barton (Nov 13 2018 at 14:28):

Step 1 will require choice

#### Johan Commelin (Nov 13 2018 at 14:28):

I'm currently trying to build a function.

#### Johan Commelin (Nov 13 2018 at 14:28):

And I haven't come to the point yet where I need choice. But I think I'm close

#### Patrick Massot (Nov 13 2018 at 14:28):

I think this was already discussed here, with a student of Kevin

#### Patrick Massot (Nov 13 2018 at 14:31):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/Topology.20-.20Beginner/near/130051069

#### Kevin Buzzard (Nov 13 2018 at 14:32):

@Luca Gerolla wanted to define a continuous function on a closed interval [0,1] by glueing continuous functions on [0,1/2] and [1/2,1]

exactly

#### Patrick Massot (Nov 13 2018 at 14:32):

hopefully this is what I linked to

#### Harry Gindi (Nov 13 2018 at 14:32):

I can't get that link to work on mobile

#### Johan Commelin (Nov 13 2018 at 14:34):

Thanks @Patrick Massot, your memory is better than mine.

#### Reid Barton (Nov 13 2018 at 14:35):

I realize that maybe it's not very obvious what the module I linked to is doing--it's showing that for $A_0$, $A_1$ closed subsets of a space X, there is a pushout square in Top involving $A_0 \cap A_1$, $A_0$, $A_1$, $A_0 \cup A_1$. For open subsets you would use the other lemma from topology I mentioned, and then it's the same as checking the sheaf condition I guess.

#### Harry Gindi (Nov 13 2018 at 14:36):

@Reid Barton you have to use AC to construct glued maps?

#### Harry Gindi (Nov 13 2018 at 14:36):

that's surprising to me

#### Harry Gindi (Nov 13 2018 at 14:37):

or is this "choice" different from the axiom of choice?

#### Reid Barton (Nov 13 2018 at 14:37):

You could construct a glued map on the quotient type (the disjoint union of the subsets) modulo (points with the same image in X) without choice

#### Reid Barton (Nov 13 2018 at 14:38):

Ah, it is a bit different from the axiom of choice

#### Reid Barton (Nov 13 2018 at 14:38):

In Lean, basically, choice = nonconstructive

#### Harry Gindi (Nov 13 2018 at 14:38):

so how do intuitionists glue maps?

#### Reid Barton (Nov 13 2018 at 14:40):

You need choice to go from "for each x there exists a y such that ..." to a function mapping x to the corresponding y, even if you know that the corresponding y is also unique. So in that sense it's not exactly analogous to the axiom of choice in ZFC

#### Reid Barton (Nov 13 2018 at 14:41):

I don't know. I guess you could try to replace "subset of X" by "map to X whose fibers are subsingletons", but I don't know how far you would get with that.

#### Johan Commelin (Nov 13 2018 at 14:43):

I think I want my covers to be defined as U = colimit u \in Us. Then this sort of problems would go away.

#### Reid Barton (Nov 13 2018 at 14:43):

I have this picture in my mind of $A_0 \times \{0\} \cup (A_0 \cap A_1) \times [0, 1] \cup A_1 \times \{1\}$ projecting to $A_0 \cup A_1 \subset X$, and not admitting a continuous section over $A_0 \cup A_1$. Don't know if it means anything though.

#### Mario Carneiro (Nov 13 2018 at 14:44):

I think I gave a proof that gluing in arbitrary topological spaces requires choice using roughly that example

#### Reid Barton (Nov 13 2018 at 14:45):

@Mario Carneiro had a nice example arguing that you really need something noncomputable to glue functions which is ... right.

#### Mario Carneiro (Nov 13 2018 at 14:45):

where by "choice" I mean unique choice

#### Mario Carneiro (Nov 13 2018 at 14:46):

lean doesn't really distinguish between AC, unique choice and LEM

#### Mario Carneiro (Nov 13 2018 at 14:46):

they all follow from the same axiom

#### Harry Gindi (Nov 13 2018 at 14:49):

Can you glue maps of locales without choice?

#### Ramon Fernandez Mir (Nov 13 2018 at 14:54):

I've actually been looking into it. It's in the sheaf branch on the community mathlib.

#### Johan Commelin (Nov 13 2018 at 14:55):

So now I have this goal:

(⨆ (u : {x // x ∈ Us}), (u.val).left) = ⨆ (u : over U) (H : u ∈ Us), u.left


@Mario Carneiro will say: "I told you that covering_family U should be a type." But it's not (at the moment). How do I solve silly goals like this?

#### Johan Commelin (Nov 13 2018 at 14:55):

@Ramon Fernandez Mir Good to see you!

#### Mario Carneiro (Nov 13 2018 at 14:55):

There is a rewrite rule for this

#### Johan Commelin (Nov 13 2018 at 14:55):

I want rewrite_search...

#### Mario Carneiro (Nov 13 2018 at 14:57):

supr_subtype

#### Luca Gerolla (Nov 13 2018 at 14:57):

@Luca Gerolla wanted to define a continuous function on a closed interval [0,1] by glueing continuous functions on [0,1/2] and [1/2,1]

Indeed, I was dealing with continuous functions on two closed sets $V, U$ (where $U, V$ cover the overall domain $X$) agreeing on their intersection $U \cap V$ and I needed to construct a continuous function $X \to Y$. The code (mainly done by Mario and Kevin) is at https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/Topology/Material/pasting_lemma.lean.
Although dealing with a general covering I don't know if it can be of any help.

I don't think so

#### Kenny Lau (Nov 13 2018 at 14:59):

what's Luca doing on an nlab thread...

#### Kenny Lau (Nov 13 2018 at 14:59):

\cap $\cap$

#### Johan Commelin (Nov 13 2018 at 14:59):

His post is about gluing functions.

#### Luca Gerolla (Nov 13 2018 at 15:05):

Also continous_if (from mathlib - topology.continuity) turned out very useful when I had just and ite function.
Look forward to seeing the solution to this more general pasting :)

#### Johan Commelin (Nov 13 2018 at 15:39):

@Scott Morrison Here is something that I find a bit annoying to do. I'm trying to prove that the following functor preserves colimits:

def to_Top : opens X ⥤ Top :=
{ obj := λ U,
{ α := U.val,
str := subtype.topological_space },
map := λ U V i, ⟨λ x, ⟨x.1, (plift.down (ulift.down i)) x.2⟩,
(embedding.continuous_iff embedding_subtype_val).mpr continuous_subtype_val ⟩ }


Here is what I have so far:

def to_Top.preserves_colimits : preserves_colimits (@to_Top X _) :=
{ preserves := λ J _ K c hc,
{ desc := λ s, _ } }


The local context is now:

X : Type u,
_inst_1 : topological_space X,
J : Type u,
_x : small_category J,
K : J ⥤ opens X,
c : limits.cocone K,
hc : limits.is_colimit c,
s : limits.cocone (K ⋙ to_Top)
⊢ (functor.map_cocone to_Top c).X ⟶ s.X


The annoying thing is the pair c, hc. I would much rather work with hc : has_colimit K and c : colimit K. Because then I can use facts about how this colimit is defined. Of course I can build a unique isomorphism between the c that I got from Lean and the one that I'm interested in. But I wonder if it would make sense to change the setup a bit...

#### Johan Commelin (Nov 13 2018 at 15:42):

I've pushed all that I have so far. Now I need to start packing to catch a train.

#### Johan Commelin (Nov 13 2018 at 15:42):

If anyone has good ideas, or wants to refactor this, please go ahead!

#### Johan Commelin (Nov 13 2018 at 15:43):

I'm just trying to push this category stuff to the limit (no pun intended)

#### Reid Barton (Nov 13 2018 at 15:47):

I think we can just add a lemma for that.
You're saying you want to prove: if F : C -> D and C already has_colimits, then to prove F preserves colimits it suffices to consider the ones provided by the has_colimits instance.

#### Johan Commelin (Nov 13 2018 at 15:48):

Yes, but why not just always condider the one provided by has_colimit K, where K is a diagram.

#### Patrick Massot (Nov 13 2018 at 15:48):

I'm just trying to push this category stuff to the limit (no pun intended)

When we'll have that to_dual tactic, you'll be able to pull this category stuff to the colimit without any extra effort!

#### Reid Barton (Nov 13 2018 at 15:49):

Because the concept of preserving colimits doesn't depend on a choice of colimits

#### Johan Commelin (Nov 13 2018 at 15:49):

I see... you're probably right. I don't yet fully grasp the details of the API

#### Johan Commelin (Nov 13 2018 at 15:50):

But your suggested lemma would also fix this problem.

#### Kevin Buzzard (Nov 13 2018 at 16:21):

@Johan Commelin @Kenny Lau -- @Ramon Fernandez Mir asks me exactly what you are going to be doing regarding Spec of a ring. Ramon is supposed to be completely refactoring the scheme project as part of his MSc thesis; I got him to look at locally ringed spaces but now these are done modulo the assertion that the category of rings has all colimits. Then Kenny mentioned Spec -- I think it would just be less nervy for us if we knew exactly what you guys were planning on doing and what Ramon can do (he has written thousands of lines of Coq code but is new to Lean). Currently we need that colimits exist in the category of commutative rings, and that the spectrum of a ring is a locally ringed space (which of course is a lot of work, even though it's in some sense done already). The first step towards this is that the spectrum of a ring has a presheaf of rings on the basis of open sets $D(f)$. Shall I tell him to do this or will someone else do it by the weekend? It would be good if we could work together on this (although of course there is plenty plenty to do -- e.g. this Gamma Spec adjointness is a goal I have in mind for Ramon, something Johan suggested months ago -- and products of schemes is another thing).

#### Kevin Buzzard (Nov 13 2018 at 16:24):

Of course I know all of this is already done in the schemes project -- the point is that we want to do it as a test of the category theory stuff; in the past we did it all "by hand".

#### Kevin Buzzard (Nov 13 2018 at 16:54):

I think I know how to prove that colimits exist in the category of commutative rings -- can I get Ramon to do this or @Kenny Lau are you likely do just randomly do this at some point in the next few days?

#### Kevin Buzzard (Nov 13 2018 at 16:55):

It will be quite a good stress test of Johannes' multivariable polynomial work I think.

#### Johan Commelin (Nov 13 2018 at 17:37):

@Kevin Buzzard Yes, collaboration is good. I have no intention to "mow away the grass" before Ramon's feet.
Here is a question for you: do you intend to make things mathlib-ready? Is the endgoal a PR to mathlib?

My goal is to get a theory of sheaves that is ready for the perfectoid project.

#### Johan Commelin (Nov 13 2018 at 17:38):

Concerning colimits in CommRing: do all of them exist? Or only the directed ones?

#### Kevin Buzzard (Nov 13 2018 at 17:38):

I convinced myself this afternoon that they all existed

#### Johan Commelin (Nov 13 2018 at 17:39):

Sheaves of rings seems to be a bit of an issue. I'm not yet sure how to define them. Once we have those, I'll leave it up to Ramon to define LRS. I will not touch Spec or anything close to it (-;

#### Reid Barton (Nov 13 2018 at 17:39):

They do all exist

#### Johan Commelin (Nov 13 2018 at 17:39):

I do intend to define stalks. So I might get close to LRS...

#### Kevin Buzzard (Nov 13 2018 at 17:39):

via some big standard universal construction -- given a diagram in CommRing, let T0 be the polynomial ring over Z with variables the disjoint union of all the rings in the diagram, and then quotient out by the relations making all of the canonical maps ring homs

#### Johan Commelin (Nov 13 2018 at 17:40):

I would not mind at all if Ramon works on a branch of community mathlib and regularly pull and pushes to the sheaf branch.

#### Kevin Buzzard (Nov 13 2018 at 17:40):

The "bad" news is that this all seems to be some special case of some big theory due to Lawvere and we could spend forever formalising that instead

#### Kevin Buzzard (Nov 13 2018 at 17:40):

(existence of limits and colimits in some big gneerality for some algebraic categories or something)

#### Johan Commelin (Nov 13 2018 at 17:42):

Right. So we just do rings by hand first. Like you did schemes by hand first. This seems to be what Mario would tell us to do anyway.

#### Kevin Buzzard (Nov 13 2018 at 17:42):

Right -- so @Kenny Lau are you happy if @Ramon Fernandez Mir proves existence of colimits in the category of commutative rings?

#### Kevin Buzzard (Nov 13 2018 at 17:42):

In a relatively "hands-on" way, not using Lawvere anything

#### Johan Commelin (Nov 13 2018 at 17:43):

Be aware that Scott already has some general machinery in this direction. I guess you only need coproducts and coequalisers.

#### Kevin Buzzard (Nov 13 2018 at 17:45):

I am not 100% sure whether this makes life any easier in this case

#### Kevin Buzzard (Nov 13 2018 at 17:46):

in the sense that now instead of making one gigantic commutative polynomial ring in a huge set of variables and quotienting out by an ideal generated by terms of two types and then proving something about it, you'll have to build two such rings and prove something about each of them.

#### Johan Commelin (Nov 13 2018 at 17:49):

It would be useful to know that coproducts are defeq to tensor products, I assume...

#### Kevin Buzzard (Nov 13 2018 at 17:55):

funny isn't it. For products and subobjects you feel like you've made progress. But colimits are quotients so it's always going to be a pain I think. I don't even really understand what the coproduct of an arbitrary set of rings looks like -- it seems to be some sort of direct limit of finite tensor products -- but of course we haven't built direct limits yet so there's a danger of going round in circles here.

#### Kevin Buzzard (Nov 13 2018 at 17:57):

Here is a question for you: do you intend to make things mathlib-ready? Is the endgoal a PR to mathlib?

I don't even know if Mario would be interested in hosting schemes (and I've not asked) -- my goal is to take the crappy code which I wrote so I could learn how to write Lean code, and replace it with code which is sufficiently respectable to get a publication. I've not thought about mathlib at all.

#### Johan Commelin (Nov 13 2018 at 18:05):

I think there are two options:

• either stuff like this goes into mathlib,
• or the Lean community comes up with a good strategy to have decentralised libraries that work together nicely as dependencies of other projects.

#### Mario Carneiro (Nov 13 2018 at 18:06):

The construction you sketched is clearly a composition of two constructions, why not formalize that?

#### Johan Commelin (Nov 13 2018 at 18:06):

@Mario Carneiro Do you want schemes in mathlib?

#### Mario Carneiro (Nov 13 2018 at 18:06):

I want polished code in mathlib

#### Johan Commelin (Nov 13 2018 at 18:06):

Do you want polished schemes in mathlib?

#### Mario Carneiro (Nov 13 2018 at 18:07):

sure, if that interests yous

#### Mario Carneiro (Nov 13 2018 at 18:07):

there seem to be a lot of intermediate steps though

#### Johan Commelin (Nov 13 2018 at 18:07):

It interests mes and about 65% of all Field medalists.

#### Johan Commelin (Nov 13 2018 at 18:09):

There's a lot of intermediate steps because I'm trying to write reusable code.

#### Reid Barton (Nov 13 2018 at 18:14):

I'm not sure which construction Mario is referring to

#### Mario Carneiro (Nov 13 2018 at 18:44):

via some big standard universal construction -- given a diagram in CommRing, let T0 be the polynomial ring over Z with variables the disjoint union of all the rings in the diagram, and then quotient out by the relations making all of the canonical maps ring homs

#### Mario Carneiro (Nov 13 2018 at 18:45):

we already have the first part, and the second part should generalize to "given a bunch of functions(?) make them all ring homs"

#### Scott Morrison (Nov 13 2018 at 20:47):

I think, unfortunately, that eventually we will want to do all the varieties of colimits in CommRing separately.

#### Scott Morrison (Nov 13 2018 at 20:48):

We should do the general colimit, we should also do the filtered colimit (which is much easier), we should do coproducts, we should do binary coproducts. General nonsense says you don't need to prove any comparison theorems relating these, happily.

#### Scott Morrison (Nov 13 2018 at 20:49):

Later, various bits of general machinery about algebraic categories will give us the filtered colimits "for free"

#### Scott Morrison (Nov 13 2018 at 20:49):

but someone should do the construction in CommRing first as a warmup.

#### Scott Morrison (Nov 13 2018 at 20:49):

I don't know the Lawvere stuff; maybe later there's some generality that gives us all colimits in CommRing too?

#### Kevin Buzzard (Nov 13 2018 at 21:05):

Ok so Ramon and I will take on the task of general colimits. I'm a bit unsure about whether working in this generality will actually cause problems when we want to prove that the stalks for an affine scheme are local, but let's wait and see!

#### Scott Morrison (Nov 13 2018 at 22:12):

Are you sure you don't want to do filtered colimits first, @Kevin Buzzard? They are both easier to construct, and more useful! (Because they're all that's needed for stalks, and will make arguments about stalks easier.)

#### Kevin Buzzard (Nov 13 2018 at 22:31):

The way Johan or you had set up locally ringed spaces relied on the fact that CommRing had colimits

#### Kevin Buzzard (Nov 13 2018 at 22:32):

I don't know what a filtered colimit is. I know what a directed set is. Is it sort-of the same thing?

#### Kevin Buzzard (Nov 13 2018 at 22:33):

aah I now know that a filtered colimit is a categorification of a directed set

#### Kevin Buzzard (Nov 13 2018 at 22:34):

So I guess I don't know where to stop here. Why not just do colimits over a directed partial order? They are both easier to construct, and more useful! (Because they're all that's needed for stalks, and will make arguments about stalks easier.)

#### Kevin Buzzard (Nov 13 2018 at 22:35):

And Kenny did them already :P

#### Reid Barton (Nov 13 2018 at 22:36):

Well, filtered is the right level of generality for the fact that you can compute the colimit in Set

#### Kevin Buzzard (Nov 13 2018 at 22:37):

but colimits in Set are completely different to colimits in CommRing

#### Kevin Buzzard (Nov 13 2018 at 22:37):

or am I misunderstanding? (presumably)

#### Reid Barton (Nov 13 2018 at 22:37):

General ones are, but filtered ones are not

Oh I see!

#### Scott Morrison (Nov 13 2018 at 22:40):

I will add filtered colimits (in the simplest sense, not Reid's kappa-filtered ones) to the limits branch shortly. (Just the definition!)

#### Scott Morrison (Nov 13 2018 at 22:40):

@Johan Commelin, Johannes asked me to rebase the limits branch; prepare for trouble. :-)

#### Kevin Buzzard (Nov 13 2018 at 22:40):

So @Ramon Fernandez Mir would be interested in this. People seem to be suggesting that the definition here https://github.com/semorrison/lean-category-theory/blob/master/src/category_theory/presheaves/locally_ringed.lean which uses arbitrary colimits is not wise?

Yes

#### Scott Morrison (Nov 13 2018 at 22:40):

That isn't wise. :-)

#### Kevin Buzzard (Nov 13 2018 at 22:41):

and instead of stalk_at one should use something else?

#### Scott Morrison (Nov 13 2018 at 22:41):

I think stalk_at will be exactly the same

#### Scott Morrison (Nov 13 2018 at 22:42):

We'll just change the typeclass provided, from has_colimits to has_filtered_colimits

#### Kevin Buzzard (Nov 13 2018 at 22:42):

I see. And that doesn't break anything else?

#### Kevin Buzzard (Nov 13 2018 at 22:42):

When teaching is finished I'm going to be cloning this repo finally

#### Scott Morrison (Nov 13 2018 at 22:42):

Magic will then notice that the category of open sets containing x is filtered, and so use the has_filtered_colimits instance,

#### Kevin Buzzard (Nov 13 2018 at 22:42):

at the minute cloning it would lead me astray

#### Scott Morrison (Nov 13 2018 at 22:43):

which will provide an nice construction of the colimit (as a quotient of a disjoint union, just like in Set), rather than the huge one in terms of tensor products.

#### Kevin Buzzard (Nov 13 2018 at 22:43):

Would magic work for sheaves on a basis? For sheaves on a site?

#### Scott Morrison (Nov 13 2018 at 22:43):

That I don't know.

#### Kevin Buzzard (Nov 13 2018 at 22:43):

I had never seen the construction of a colimit in CommRing until today, when I figured it out for myself. I did not use tensor products. What trick did I miss?

#### Kevin Buzzard (Nov 13 2018 at 22:43):

I just made a polynomial ring over Z with variables the disjoint union of all the rings in the diagram

#### Kevin Buzzard (Nov 13 2018 at 22:44):

and then quotiented

#### Kevin Buzzard (Nov 13 2018 at 22:44):

I understand that for two rings a coproduct is the tensor product

#### Kevin Buzzard (Nov 13 2018 at 22:44):

but I couldn't see how this generalised to infinitely many rings

#### Kevin Buzzard (Nov 13 2018 at 22:45):

it seemed to be a direct limit of tensor produts, but to make direct limits you want to take coproducts again

#### Scott Morrison (Nov 13 2018 at 22:45):

oh, okay, maybe I didn't think very hard about the infinite diagram case, either :-)

#### Scott Morrison (Nov 13 2018 at 22:45):

(I had never thought about any of this (nor knew what a site was, etc) until Lean came along. :-)

#### Reid Barton (Nov 13 2018 at 22:46):

Well... it's the filtered colimit of all the ways to take a coproduct of finitely many of the rings

#### Reid Barton (Nov 13 2018 at 22:46):

and filtered colimits are easy

#### Kevin Buzzard (Nov 13 2018 at 22:46):

Is there a general story?

#### Reid Barton (Nov 13 2018 at 22:46):

That said, the construction you gave is the simplest one and it has essentially nothing to do with rings in particular

#### Kevin Buzzard (Nov 13 2018 at 22:47):

Reducing a general colimit to a filtered colimit?

#### Kevin Buzzard (Nov 13 2018 at 22:49):

I still don't know whether we should just stick to filtered (0,1)-categories

#### Kevin Buzzard (Nov 13 2018 at 22:49):

i.e. directed sets (I should stop looking at nlab)

#### Kevin Buzzard (Nov 13 2018 at 22:49):

Oh, Reid's argument perhaps resolves this -- if it works over set then take it

#### Reid Barton (Nov 13 2018 at 22:50):

Directed colimits will be somewhat easier notationally and you don't need them unless you want stalks for some site which is not itself a poset. I think.

#### Kevin Buzzard (Nov 13 2018 at 22:50):

I think the etale site is the simplest example of this that I know

#### Reid Barton (Nov 13 2018 at 22:50):

Er, don't need filtered colimits unless ..., of course.

#### Kevin Buzzard (Nov 13 2018 at 22:51):

and next year when we're doing etale cohomology we'll need etale sites

#### Reid Barton (Nov 13 2018 at 22:51):

I think it is safe to assume that by the time we want to do etale cohomology we will have filtered colimits of rings

#### Reid Barton (Nov 13 2018 at 22:52):

You can actually build filtered colimits from directed ones, so it doesn't lose any great generality to work with directed ones for some purposes

#### Kevin Buzzard (Nov 13 2018 at 23:34):

Magic will then notice that the category of open sets containing x is filtered, and so use the has_filtered_colimits instance,

There's something I can't get to add up here. Say there's a has_colimits instance and also a simpler has_filtered_colimits instance. Now let's say I'm trying to take a colimit and it happens to be filtered. If Lean uses the has_colimits instance then the colimit will be constructed in one way, but if Magic notices that the colimit is filtered then it could construct it using the simpler filtered colimit construction. The two constructions will give canonically isomorphic, but probably not defeq, objects, and doesn't this give rise to a diamond?

#### Scott Morrison (Nov 14 2018 at 01:10):

I have to admit I don't know how bad a problem this is going to be!

#### Reid Barton (Nov 14 2018 at 01:34):

You also don't necessarily have to put your filtered colimits into the type class system. You can just define and use them directly.

#### Harry Gindi (Nov 14 2018 at 02:08):

the general statement comes from the theory of locally presentable categories

#### Harry Gindi (Nov 14 2018 at 02:12):

every object can be given as a filtered colimit of finite pushouts of compact (i.e. finitely (resp Kappa)-presentable) objects, iirc the statement correctly

#### Harry Gindi (Nov 14 2018 at 02:12):

and iirc CRing has only a single generator, Z[x]

#### Harry Gindi (Nov 14 2018 at 02:15):

You don't need to work with Lawvere theories to do this stuff, you might be fine doing the locPres machinery and then proving algebraic categories you care about are LocPres

#### Harry Gindi (Nov 14 2018 at 02:17):

It seems a lot less complicated than doing Lawvere theories generally

#### Harry Gindi (Nov 14 2018 at 02:21):

The general argument is useful in other places, iirc. Grothendieck first used this style of argument in the Tohoku paper

#### Harry Gindi (Nov 14 2018 at 02:22):

proving that the category of abelian sheaves has enough injectives, but I forget the details

#### Johan Commelin (Nov 14 2018 at 06:38):

@Kevin Buzzard Maybe we should change the definition of stalk a tiny little bit, and write filtered_colimit instead of colimit. That would take care of your issue, I think.

#### Kevin Buzzard (Nov 14 2018 at 07:06):

This is a diamond-like issue but one level up. With diamonds you might end up with two objects which are equal but the proof isn't rfl. Here the objects are not even equal, merely canonically isomorphic

#### Johan Commelin (Nov 14 2018 at 08:05):

I see what you mean. And I think this is showing that the current type class system might not be a good fit for categorical stuff (wait till we want to do higher-categorical stuff...). But maybe we can just ignore the issue for now, and hope that Lean 4 will solve this issue before we hit serious problems.

#### Johan Commelin (Nov 15 2018 at 13:11):

This is pretty ugly:

def extend : presheaf X C :=
{ obj := λ U, limit ((comma.fst (full_subcategory_inclusion B) (functor.of_obj U)).op ⋙ F),
map := λ U V i,
show (limits.limit (functor.op (comma.fst (full_subcategory_inclusion B) (functor.of_obj U)) ⋙ F) ⟶
limits.limit (functor.op (comma.fst (full_subcategory_inclusion B) (functor.of_obj V)) ⋙ F)),
begin
have foo := limit.pre ((comma.fst (full_subcategory_inclusion B) (functor.of_obj U)).op ⋙ F) (extend.aux i),
dsimp [extend.aux] at foo,
convert foo,
swap 3, assumption
end }


#### Reid Barton (Nov 15 2018 at 13:24):

Why isn't the map field just an application of limit.pre?

#### Reid Barton (Nov 15 2018 at 13:25):

what goal is the last line solving?

#### Reid Barton (Nov 15 2018 at 13:31):

My guess is that representing slice categories as comma categories is actually not a good idea in Lean, because the isomorphism (punit -> a) = a is not enough of an equality

#### Reid Barton (Nov 15 2018 at 13:39):

Did you actually manage to prove the map_id and map_comp fields?

#### Johan Commelin (Nov 15 2018 at 13:44):

Not yet, still working on it.

#### Johan Commelin (Nov 15 2018 at 13:45):

Note that I'm not taking a slice category, although it almost is.

#### Johan Commelin (Nov 15 2018 at 13:46):

This is opens in B that are contained in U, but U is not in B.

Oh, I see

#### Reid Barton (Nov 15 2018 at 13:55):

If these are presheaves of sets, then there's an easier way to write the formula

#### Reid Barton (Nov 15 2018 at 13:55):

it's the same as the right Kan extension, right?

#### Johan Commelin (Nov 15 2018 at 13:56):

Hmmm... I think so.

#### Johan Commelin (Nov 15 2018 at 13:56):

If you want to help, please do so.

#### Johan Commelin (Nov 15 2018 at 13:56):

Lean is fighting back hard (-;

#### Johan Commelin (Nov 15 2018 at 13:57):

Maybe we should do it for a general map between sites, in that case.

#### Reid Barton (Nov 15 2018 at 13:58):

If E is the extended presheaf then we should have E(U) = Hom(yU, E) = Hom(R(yU), F) where R is the restriction of a presheaf on C to a presheaf on B

#### Reid Barton (Nov 15 2018 at 13:58):

so E is the composition y, then R, then Hom(-, F)

#### Reid Barton (Nov 15 2018 at 13:59):

Yes, that might help as well... at least for clarity

#### Johan Commelin (Nov 15 2018 at 14:00):

Ok, I think this is a nice way to do it!

#### Johan Commelin (Nov 15 2018 at 14:00):

I don't yet see why it is the same thing as in my special case

#### Johan Commelin (Nov 15 2018 at 14:02):

Aah, U is the colimit of all the Ui ∈ B that are contained in U. Now pull this through Hom(_, F) and you get a limit.

#### Reid Barton (Nov 15 2018 at 14:06):

You might find it useful to borrow https://github.com/leanprover-community/mathlib/blob/adjunctions/category_theory/presheaf.lean#L85

#### Reid Barton (Nov 15 2018 at 14:06):

I think you will want to apply it twice

#### Reid Barton (Nov 15 2018 at 14:06):

In your setup you have a functor B -> C, right?

#### Johan Commelin (Nov 15 2018 at 14:07):

What do you mean?

#### Johan Commelin (Nov 15 2018 at 14:08):

B is a basis, and it has an inclusion into opens X.

#### Johan Commelin (Nov 15 2018 at 14:08):

I have a presheaf on B

#### Reid Barton (Nov 15 2018 at 14:08):

Okay so let's call opens X C for now

#### Johan Commelin (Nov 15 2018 at 14:09):

Aaah, C was my category of coefficients so far

ah

#### Johan Commelin (Nov 15 2018 at 14:09):

But maybe I should stop worrying about coefficients, and only focus on Type.

#### Reid Barton (Nov 15 2018 at 14:09):

Well this formula won't work unless the values are in Type

#### Johan Commelin (Nov 15 2018 at 14:10):

Right, so I should forget about C

#### Johan Commelin (Nov 15 2018 at 14:10):

And sheaves of rings will require some extra thought

#### Reid Barton (Nov 15 2018 at 14:10):

Okay, in that case let me just use the names from the thing I linked above, so you have a functor C -> D

#### Reid Barton (Nov 15 2018 at 14:11):

If you apply restricted_yoneda to it, you get a functor D -> Set^C^op

#### Reid Barton (Nov 15 2018 at 14:11):

and if you apply restricted_yoneda to that, you get a functor Set^C^op -> Set^D^op

#### Reid Barton (Nov 15 2018 at 14:11):

and that should be the right Kan extension along the original functor

#### Reid Barton (Nov 15 2018 at 14:17):

the thing I called "Ry" earlier is another, possibly better way to write restricted_yoneda

#### Johan Commelin (Nov 15 2018 at 14:17):

Sorry, as student entered my office. So I have to wait a while with this thing.

#### Johan Commelin (Nov 15 2018 at 14:51):

@Reid Barton Hmmm... morphisms of sites seem to be non-trivial. I don't think I want to do them now, unless you want to join in. We would need to explain Lean this definition https://ncatlab.org/nlab/show/flat+functor#SiteValuedFunctors

#### Reid Barton (Nov 15 2018 at 15:02):

Right... so concretely I guess your actual goal is to show that the extended presheaf is actually a sheaf?

#### Reid Barton (Nov 15 2018 at 15:04):

You might want to pick a fact to prove, and work backwards from there

#### Reid Barton (Nov 15 2018 at 15:04):

Otherwise you can enter a swamp of things you could formalize and choices of definitions you could make

#### Johan Commelin (Nov 15 2018 at 15:52):

Right. I want to get an equivalence of categories between sheaf B and sheaf X. That is a concrete goal that I definitely want to reach.

#### Johan Commelin (Nov 15 2018 at 16:16):

@Reid Barton So which approach would you suggest now? Maybe the one with Kan extensions is best? Because it will generalise later on?

#### Johan Commelin (Nov 15 2018 at 16:16):

Hmmm, I'm being called for an early dinner. See you later.

#### Johan Commelin (Nov 15 2018 at 18:41):

:rolling_on_the_floor_laughing: This error is hilarious:

type mismatch at application
set.{u} (over.{u u} U)
term
over.{u u} U
has type
Type u
but is expected to have type
Type u


#### Johan Commelin (Nov 15 2018 at 19:33):

@Reid Barton How does this look?

def restrict : presheaf X ⥤ category_theory.presheaf B :=
{ obj := λ F, (full_subcategory_inclusion B).op ⋙ F,
map := λ _ _ f, whisker_left _ f }

def extend : category_theory.presheaf B ⥤ presheaf X :=
{ obj := λ F, yoneda.op ⋙ restrict.op ⋙ yoneda.obj F,
map := λ F G f, whisker_left _ $whisker_left _$ yoneda.map f }


I think you gave a very good suggestion!

#### Johan Commelin (Nov 15 2018 at 19:42):

@Reid Barton I think it makes sense to merge your presheaf.lean with parts of my sheaf.lean. What would be the best approach? Should I merge your branch into mine?

#### Johan Commelin (Nov 15 2018 at 19:42):

I would like to prove that restrict and extend form an adjunction anyway.

#### Reid Barton (Nov 15 2018 at 23:55):

@Johan Commelin Feel free to merge my branch into yours of course, though I will note that I intend to try out a redesign of adjunctions at some point

#### Johan Commelin (Nov 20 2018 at 08:21):

I'm not sure if I'm using things in the right way. I'm trying to write

let G1 := (equiv_of_iso D).trans (equiv.subtype_equiv_of_subtype.{(u+1) (u+1)} Eeq),


where D : F.obj ≅ {p // horrible p} is isomorphisms between a type and a subtype in the category Type u which I turn into an equiv.
I then want to replace the horrible right hand side with a subtype of something else, so I thought, lets use transitivity of equiv and feed it Eeq, which is:

Eeq : (limits.sigma.{u+1 u} (λ (Ui : {x // x ∈ c}), yoneda.{u u}.obj ((Ui.val).left)) ⟶ F) ≃
Π (a : {x // x ∈ c}), F.obj ((a.val).left) :=
equiv.trans.{u+1 u+1 u+1} (equiv_of_iso.{u} E)
(equiv.Pi_congr_right.{u u+1 u+1}
(λ (Ui : {x // x ∈ c}),
equiv_of_iso.{u}
(nat_iso.app.{u+1 u+1 u u} (yoneda_lemma.{u u} X) ((Ui.val).left, F) ≪≫
ulift_trivial.{u} ((evaluation_uncurried.{u u u+1 u} Xᵒᵖ (Type u)).obj ((Ui.val).left, F))))),


The left hand side of Eeq should be exactly the type of the p in {p // horrible p}.

I get the following error:

type mismatch at application
equiv.subtype_equiv_of_subtype.{u+1 u+1} Eeq
term
Eeq
has type
(limits.sigma.{u+1 u} (λ (Ui : {x // x ∈ c}), yoneda.{u u}.obj ((Ui.val).left)) ⟶ F) ≃
Π (a : {x // x ∈ c}), F.obj ((a.val).left)
but is expected to have type
(limits.sigma.{u+1 u} (λ (Ui : {x // x ∈ c}), yoneda.{u u}.obj ((Ui.val).left)) ⟶ F) ≃ ?m_1


I have tried looking at universes. I have enable pp.all. And I'm clueless. Any suggestions?

#### Kevin Buzzard (Nov 20 2018 at 08:24):

Is it a typeclass issue? That sometimes causes errors that look like that. Lean can't infer a typeclass and so gives up and prints an unhelpful error message

#### Kevin Buzzard (Nov 20 2018 at 08:25):

I mean equiv.subtype_equiv_of_subtype -- does it have some secret inputs that it can't find?

#### Johan Commelin (Nov 20 2018 at 08:26):

Also, why is p not an explicit argument in

def subtype_equiv_of_subtype {p : α → Prop} : Π (e : α ≃ β), {a : α // p a} ≃ {b : β // p (e.symm b)}
| ⟨f, g, l, r⟩ :=
⟨subtype.map f $assume a ha, show p (g (f a)), by rwa [l], subtype.map g$ assume a ha, ha,
assume p, by simp [map_comp, l.comp_eq_id]; rw [map_id]; refl,
assume p, by simp [map_comp, r.comp_eq_id]; rw [map_id]; refl⟩


#### Johan Commelin (Nov 20 2018 at 08:26):

Well, in general it can't infer that p.

#### Chris Hughes (Nov 20 2018 at 08:26):

What universe is ?m_1 expected to be in?

#### Johan Commelin (Nov 20 2018 at 08:26):

Type u

#### Mario Carneiro (Nov 20 2018 at 08:27):

I think Johannes has a bad habit of making lots of things implicit that can't be inferred when used directly

#### Mario Carneiro (Nov 20 2018 at 08:27):

I guess that p is inferrable if you use it as a rewrite, or apply it to something

#### Johan Commelin (Nov 20 2018 at 08:27):

But in my case a smart elaborator should even be able to infer it, because I'm composing with another equiv.

#### Johan Commelin (Nov 20 2018 at 08:28):

Can I rewrite along equivs?

#### Mario Carneiro (Nov 20 2018 at 08:28):

I think? calc for sure

#### Chris Hughes (Nov 20 2018 at 08:28):

Isn't Π (a : {x // x ∈ c}), F.obj ((a.val).left) Type (u + 1). If I'm not mistaken?

#### Johan Commelin (Nov 20 2018 at 08:28):

Hmmm, it says rewrite tactic failed, lemma is not an equality nor a iff

#### Mario Carneiro (Nov 20 2018 at 08:29):

hm, I guess that is probably a // TODO(Leo) somewhere

#### Mario Carneiro (Nov 20 2018 at 08:30):

obviously it's not high on the list of priorities

#### Johan Commelin (Nov 20 2018 at 08:30):

The F.obj ((a.val).left) is Type u, and the product is over c : set (over U) where U : X and X : Type u

#### Johan Commelin (Nov 20 2018 at 08:30):

I hope that doesn't bump up universes...

that sounds fine

#### Mario Carneiro (Nov 20 2018 at 08:31):

you can just check, of course

#### Chris Hughes (Nov 20 2018 at 08:31):

If F.obj ((a.val).left is Type u, then Π (a : {x // x ∈ c}), F.obj ((a.val).left) is Type (u + 1) right?

No it isn't

#### Mario Carneiro (Nov 20 2018 at 08:34):

another trick you can try is by convert at the type mismatch

#### Mario Carneiro (Nov 20 2018 at 08:34):

it should home in on the mismatched part

#### Johan Commelin (Nov 20 2018 at 08:35):

How exactly should I do that?

#### Mario Carneiro (Nov 20 2018 at 08:36):

something like subtype_equiv_of_subtype (by convert Eeq) or refine subtype_equiv_of_subtype _, convert Eeq

#### Johan Commelin (Nov 20 2018 at 08:38):

Cool! That finds the following unsolved goal:

⊢ presheaf.category_theory.limits.has_coproducts.{u} = limits.functor_category_has_coproducts.{u+1 u}


#### Johan Commelin (Nov 20 2018 at 08:38):

That's progress at least.

#### Kevin Buzzard (Nov 20 2018 at 08:39):

I am loving convert. I use it a lot when doing basic UG maths -- "this is basically the answer, now let's see what pieces we have to pick up"

#### Johannes Hölzl (Nov 20 2018 at 09:47):

@Johan Commelin rw only work with = (maybe also ==, and <-> only works due to propext). Rewriting with equiv is hard, one needs to prove that the motive (i.e. context in which the right-hand side appears) can be transported along the equiv. Even ignoring dependencies, parametricity is necessary as it shows that there is no choice involved.

#### Johan Commelin (Nov 20 2018 at 09:49):

Right. That is about what I expected.

#### Johannes Hölzl (Nov 20 2018 at 09:51):

To rewrite along a equiv we could use the param-branch https://github.com/leanprover-community/mathlib/commits/param and transfer.

#### Johannes Hölzl (Nov 20 2018 at 09:54):

One example why it is a problem is:

We want to rewrite e : α ≃ β in {a : α // p a}, but what would be the goal? We get something like{b : β // p (f⁻¹ b)}. But in many cases p itself is also parametric, i.e. we have actually {b : β // @p α (f⁻¹ b)} (not really, as p is describing a term and not a constant, but I hope you get the idea) Now when we can try to adopt the structure of p s.t. α is completely replaced by β, and then f isn't occurring anymore

#### Johannes Hölzl (Nov 20 2018 at 09:55):

This adoption mechanism is the kind of rewrite transfer is intended to do

#### Johannes Hölzl (Nov 20 2018 at 09:55):

and param provides us with the necessary relations

#### Johan Commelin (Nov 20 2018 at 09:58):

I see. But I suspect that param isn't yet ready for prime time.

#### Cyril Cohen (Nov 20 2018 at 10:09):

@Johannes Hölzl @Johan Commelin @Patrick Massot param is not ready yet, the translation of recursors was not as straightforward as I thought.

#### Johan Commelin (Nov 20 2018 at 13:47):

What do you do when Lean doesn't want to plug a morphism in the category C into your contravariant functor F : Cᵒᵖ ⥤ Type u?
You use convert, and let tidy clean up the mess! :tada:

functor.map F (by convert Ui.val.hom; tidy)


#### Johan Commelin (Nov 20 2018 at 14:05):

What's up, @Kenny Lau?

#### Reid Barton (Nov 20 2018 at 15:24):

Cool! That finds the following unsolved goal:

⊢ presheaf.category_theory.limits.has_coproducts.{u} = limits.functor_category_has_coproducts.{u+1 u}


This is probably true by refl

#### Johan Commelin (Nov 20 2018 at 15:26):

invalid apply tactic, failed to unify
presheaf.category_theory.limits.has_coproducts.{u} = limits.functor_category_has_coproducts.{u+1 u}
with
?m_3 = ?m_3


#### Johan Commelin (Nov 20 2018 at 15:26):

instance : has_coproducts.{(u+1) u} (presheaf X) := limits.has_coproducts_of_has_colimits


#### Johan Commelin (Nov 20 2018 at 15:27):

So, I changed that instance, and now I get

tactic failed, there are no goals to be solved
state:
no goals


#### Johan Commelin (Nov 20 2018 at 15:28):

Aaah, lol, that is because I should now remove the refl.

#### Reid Barton (Nov 20 2018 at 15:28):

Oh, I didn't notice "coproducts" rather than "colimits". Still I'm confused. What are the two instances which are not defeq, but equal by tidy?

#### Johan Commelin (Nov 20 2018 at 15:28):

No, they aren't equal by tidy either

#### Reid Barton (Nov 20 2018 at 15:29):

Or rather, what did you change that instance to?

#### Reid Barton (Nov 20 2018 at 15:30):

well, the right hand side of that goal I guess

Exactly

#### Reid Barton (Nov 20 2018 at 15:30):

But I see

instance functor_category_has_coproducts [has_coproducts.{u v} C] : has_coproducts.{(max u v) v} (K ⥤ C) :=
limits.has_coproducts_of_has_colimits


#### Reid Barton (Nov 20 2018 at 15:32):

... I'm really confused now

#### Reid Barton (Nov 20 2018 at 15:35):

Ohh, maybe I get what is going on. I think all this duplication between colimit classes is biting you

#### Reid Barton (Nov 20 2018 at 15:36):

Well, I'm still not sure why that would be a problem either really

#### Reid Barton (Nov 20 2018 at 15:36):

But I still think the duplication is silly anyways

#### Johan Commelin (Nov 20 2018 at 15:37):

Which duplication do you mean exactly?

Good question

#### Reid Barton (Nov 20 2018 at 15:38):

I was thinking of has_colimits_of_shape and has_colimits being unrelated

#### Reid Barton (Nov 20 2018 at 15:39):

But now I see there's also has_colimits which is also unrelated

#### Reid Barton (Nov 20 2018 at 15:39):

Gah, has_coproducts

#### Reid Barton (Nov 20 2018 at 15:43):

Anyways, I'm still confused by the original fact that you replaced an instance by, as far as I can tell, its definition and it changed the behavior of refl

#### Johan Commelin (Nov 20 2018 at 15:44):

Well, I didn't even need refl anymore. convert now took care of everything.

#### Reid Barton (Nov 20 2018 at 15:45):

because congr, which convert uses, will try closing goals with refl for you

#### Johan Commelin (Nov 20 2018 at 15:45):

Currently I'm trying to prove the equivalence of different formulations of the sheaf condition. Math-proof: apply Yoneda; QED. Lean-proof: :scream: :scream: :boom:

#### Reid Barton (Nov 20 2018 at 15:46):

by convert x should be the same as by exact x

#### Johan Commelin (Nov 20 2018 at 15:46):

which apparently is not the same as x

#### Reid Barton (Nov 20 2018 at 17:56):

OK, I got to the same place where you were before changing the instance.

#### Reid Barton (Nov 20 2018 at 17:58):

It's kind of hard to understand what's going on because all the has_blah things are classes, which means they aren't printed except with pp.implicit, which also prints a bunch of other stuff I don't care about...

#### Reid Barton (Nov 20 2018 at 18:00):

I wish you could jump from names in the goal window to their definitions...

#### Johan Commelin (Nov 20 2018 at 18:11):

Right, we should but the "interactive" back in the goal window :grinning:

#### Reid Barton (Nov 20 2018 at 18:16):

My conclusion is that I don't know what is wrong exactly, but all these different has_* need to be rethought (probably there should be far fewer of them)

#### Reid Barton (Nov 20 2018 at 18:17):

Apparently your instances which were not the same reduce to something like the following

#### Reid Barton (Nov 20 2018 at 18:18):

On one side, we have the colimit of a functor on a discrete category defined using the instance that says the category of types has colimits

#### Reid Barton (Nov 20 2018 at 18:19):

On the other side, we're doing something like building a colimit cone from a coproduct thing, which in turn is built from the original colimit somehow

#### Reid Barton (Nov 20 2018 at 18:19):

both of these constructions being nontrivial

#### Reid Barton (Nov 20 2018 at 18:20):

so that they don't just cancel out

#### Reid Barton (Nov 20 2018 at 18:21):

I haven't even seen this file limits/products.lean before

#### Johan Commelin (Nov 20 2018 at 20:25):

Thanks for looking into this! Apparently it's trickier than I thought...

#### Reid Barton (Nov 20 2018 at 20:25):

There are so many instances and it's hard to tell which ones are used where.

#### Reid Barton (Nov 20 2018 at 20:26):

for example, functor_category_has_coproducts uses limits.has_coproducts_of_has_colimits which needs a limits.has_colimits_of_shape.{u v} (discrete β) instance. Does it come from has_colimits_of_shape_of_has_coproducts_of_shape or functor_category_has_colimits_of_shape?

#### Reid Barton (Nov 20 2018 at 20:29):

either way, it will eventually end up at has_coproducts_of_shape for the original category which comes from has_coproducts_of_shape_of_has_coproducts which uses has_coproducts which comes from an unnamed instance with definition has_coproducts_of_has_colimits which finally comes from the one true has_colimits instance for Type. I think.

#### Reid Barton (Nov 20 2018 at 20:30):

So that's how you end up with the has_colimits -> has_coproducts -> has_colimits double translation, which is not refl

#### Johan Commelin (Nov 27 2018 at 14:22):

It's really quite stupid, but I only realised yesterday that all the time I've been working with the wrong map f : presheaf X \functor presheaf Y.

#### Johan Commelin (Nov 27 2018 at 14:23):

We want something like this:

def map' : presheaf X ⥤ presheaf Y :=
{ obj := λ F,
{ obj := λ V, colimit ((comma.snd.{u u u u} (functor.of_obj V) f).op ⋙ F),
map := λ V₁ V₂ j, colimit.pre ((comma.snd.{u u u u} (functor.of_obj V₂) f).op ⋙ F) (comma.map_left f $functor.of_map j).op, map_id' := λ V, begin erw functor.of_map_id, erw colimit.pre_map, tidy, end }, map := _ }  but I find it impossible to get this sorry-free. #### Reid Barton (Nov 27 2018 at 14:23): This is what I implemented in the adjunctions branch, I think? #### Johan Commelin (Nov 27 2018 at 14:23): This is what will give us the pullback of (pre)sheaves. #### Johan Commelin (Nov 27 2018 at 14:24): Aaah, did you? #### Johan Commelin (Nov 27 2018 at 14:24): I didn't look far enough, I'm afraid. #### Reid Barton (Nov 27 2018 at 14:24): I think it is yoneda_extension (F.comp yoneda)? #### Reid Barton (Nov 27 2018 at 14:24): at least, it seems to involve many of the same ingredients :) #### Johan Commelin (Nov 27 2018 at 14:25): In which file? #### Reid Barton (Nov 27 2018 at 14:25): another construction which I am not very happy about, though... #### Reid Barton (Nov 27 2018 at 14:25): presheaf.lean #### Johan Commelin (Nov 27 2018 at 14:27): Aaah, I see. Seems pretty non-trivial... #### Johan Commelin (Nov 27 2018 at 14:27): Also, why do you work with ≃ instead of ≅. Isn't that just as "bad"? #### Reid Barton (Nov 27 2018 at 14:27): Yeah, I did it in a round-about way, in retrospect #### Reid Barton (Nov 27 2018 at 14:28): In general I use equiv because it actually has useful lemmas and also it can relate different universes #### Reid Barton (Nov 27 2018 at 14:28): though I added a couple more lemmas for iso in the limits PR #### Johan Commelin (Nov 27 2018 at 14:29): Hmm, I feel like we should merge your presheaf.lean and my sheaf.lean. Or at least deduplicate. #### Reid Barton (Nov 27 2018 at 14:33): I intend to take a second stab at all the adjunctions and presheaf stuff at some point, but I'm not actively working on it at the moment #### Johan Commelin (Nov 27 2018 at 14:34): Ok, I'll move some stuff from my file to yours. So that sheaf.lean is only about sheaves. #### Johan Commelin (Nov 27 2018 at 14:34): If you start working on it again, please make sure to take a look at the sheaf branch version of your file. #### Reid Barton (Nov 27 2018 at 14:40): FWIW, my conclusion from my first attempt was that it's probably better to do all the constructions in a manifestly natural way, like Scott did in yoneda.lean for example, even though the result is probably pretty unreadable. Then you can add a simp lemma that explains what is actually happening on the level of objects #### Reid Barton (Nov 27 2018 at 14:47): Or at least, don't have a bunch of isomorphisms with the naturality conditions stated separately. That was a big mess #### Johan Commelin (Nov 27 2018 at 14:53): I see. That's what I've been trying to do. But I also got stuck. #### Johan Commelin (Nov 27 2018 at 14:54): The problem with doing things in a "manifestly natural way" is that you get sucked into ever deeper/wider/higher abstractions... #### Reid Barton (Nov 27 2018 at 14:56): it's true #### Reid Barton (Nov 27 2018 at 15:05): And that's sort of why I backed off from my previous comment. It's not obvious how to do this "category of elements" construction functorially #### Reid Barton (Nov 27 2018 at 15:07): The key is to somehow give these things usable and complete instances, so that the way to prove things about them is not to dsimp 100 things #### Reid Barton (Nov 27 2018 at 15:07): and that's where my current version of presheaf.lean sort of fell apart #### Reid Barton (Nov 27 2018 at 15:08): https://github.com/leanprover-community/mathlib/blob/adjunctions/category_theory/presheaf.lean#L310 #### Johan Commelin (Nov 27 2018 at 15:25): @Reid Barton Does this mean that you think we should avoid adjunction.left_adjoint_of_equiv? #### Johan Commelin (Nov 29 2018 at 05:39): Yuchai! This is now sorry-free: https://github.com/leanprover-community/mathlib/blob/sheaf/category_theory/presheaf.lean#L59 But it is slower than slow! Not sure how to speed it up though. I'm chaining a bunch of rewrites. Are there strategies for speeding this up? #### Scott Morrison (Nov 29 2018 at 05:47): One thing that I find often works is to work out why the erw are necessary. This is sometimes unrewarding, but often it is because hidden inside implicit arguments there are things that should dsimp, but you forgot to write the appropriate rfl lemmas. Sometimes you get really lucky, and after diagnosing a problem like this you can not only change the erw to rw, but even to dsimp! #### Johan Commelin (Nov 29 2018 at 05:49): I see. (I've stopped using rw, because erw has more powerful magic (-;) #### Johan Commelin (Nov 29 2018 at 05:49): Is dsimp faster than erw? #### Scott Morrison (Nov 29 2018 at 05:49): Yes. #### Scott Morrison (Nov 29 2018 at 05:50): And erw can be slower than rw, in places where either work. (I think?) #### Scott Morrison (Nov 29 2018 at 05:50): Well, dsimp can be either faster or slower than erw. :-) But _usually_ it seems to be faster to avoid using erw. #### Johan Commelin (Nov 29 2018 at 05:56): @Scott Morrison Do you think we could have a [derive rfl-lemmas]? #### Scott Morrison (Nov 29 2018 at 06:10): I've just had a quick look at that proof, Johan, and I don't seem to be able to make much improvement. :-( There does seem to be a small problem changing between colimit and colim.obj. #### Johan Commelin (Nov 29 2018 at 07:42): So here is what I imagine derive rflsimp (or whatever) should do: it looks at the current definition, and (as far as I thought this through, which is not that far) it does two checks: • the definition is an "abbreviation" (like def presheaf C := C \functor Type v. In this case it looks up all the rflsimp lemmas that it derived for C \functor D and defines copies in the presheaf namespace. • the definition X is a structure. In this case it looks up all the fields. For a field foo it checks whether this is a Pi-type (?) and how many arguments the Pi takes. So if foo := λ a b c, bar(a,b,c) then it will create the appropriate simp-lemma (proved by rfl) that @[simp] lemma X.foo (x : X) (a b c : some_type) : x.foo a b c = bar(a,b,c) := rfl  Of course I don't know how to write meta-code. And of course this is probably a very simplified picture. But I think something like this should be possible, and I think it would result in three things: • less boilerplate (especially in the category library!) • less broken proofs, where tidy doesn't work, because somewhere someone forgot to state the obvious rfl-simp-lemma. • less wasted time in hunting down the brokenness of the preceding point. #### Johan Commelin (Nov 29 2018 at 07:55): @Scott Morrison Thanks for looking into speeding things up. I added a rflsimp-lemma for colim.obj. Do you have any clue why the first line in that proof (with the comment) didn't simplify? #### Scott Morrison (Nov 29 2018 at 10:24): Nope, I couldn't work it out. The next "usual suspect" for simp not working is that the thing that needs to be simped is inside a function that looks superficially dependent but actually isn't when you think about it a bit. simp, which needs to build congruence lemmas to do "rewriting", can't work out what do to, but rw can. This is a "known problem" with simp, apparently. #### Scott Morrison (Nov 29 2018 at 10:24): You know how to use rewrite_search, don't you? :-) #### Keeley Hoek (Nov 29 2018 at 10:41): At some point Johan I made a thing which did this It was a command called rfl_lemma I think. If you have access to rewrite_search you have access to it, too #### Keeley Hoek (Nov 29 2018 at 10:41): It only worked for structures though #### Johan Commelin (Nov 29 2018 at 10:59): @Scott Morrison @Keeley Hoek I don't have rewrite_search. Do you think it is ready to be tested by others? If so, what do I need to do to get started? #### Keeley Hoek (Nov 29 2018 at 12:13): You could always try it out! My understanding is that all you should have to do is add lean-tidy = {git = "https://github.com/semorrison/lean-tidy", rev = "3a69d6241207f0c0758468dce666858027c54909"}  to your leanpkg.toml and run leanpkg configure. (I'm slightly worried though because lean-tidy obviously imports from mathlib, which you are working on... but I suspect it will work find (I think this is what Scott does to get his proofs using it). #### Keeley Hoek (Nov 29 2018 at 12:14): Then import tactic.rewrite_search. You can try to discharge goals with the rewrite_search tactic, but make sure you tag lemmas it is allowed to use with @[search]. There is much more complicated stuff you can do (including more specific tagging), but that's a start! #### Johan Commelin (Nov 29 2018 at 12:23): Thanks for the explanation! #### Scott Morrison (Nov 29 2018 at 12:34): I've actually never used it inside mathlib, I'm very curious if it works. #### Keeley Hoek (Nov 29 2018 at 12:34): ooh Maybe it won't then #### Keeley Hoek (Nov 29 2018 at 12:35): something about "ambiguous import xxxx" #### Johan Commelin (Nov 29 2018 at 12:59): How far are we from a merge request of a (preliminary) version of rewrite_search? #### Johan Commelin (Nov 29 2018 at 13:10): @Keeley Hoek @Scott Morrison I followed the instructions and then ran leanpkg build. I'm getting tons of errors :stuck_out_tongue_wink: #### Keeley Hoek (Nov 29 2018 at 13:14): :D #### Keeley Hoek (Nov 29 2018 at 13:15): yeah, sorry I think what you actually have to do is copy paste the lean-tidy repo over mathlib but probably don't do that it will mess your history #### Johan Commelin (Nov 30 2018 at 12:03): @Scott Morrison @Keeley Hoek I can report that adding that Lean does not outright refuse that repo as a dependency of mathlib. However... there's tons and tons of errors. So it's not really usable in a sense. #### Johan Commelin (Dec 28 2018 at 05:55): After a long period of being distracted by other work, I've returned to the sheaves and sites project. Stuff is now happening on the sheaf-2 branch, which has less dependencies than sheaf. I am currently struggling with defining a pretty non-constructive map. I have a gadget s which comes with a proof that I can perform a certain construction after some choice, and the result of the construction does not depend on the choice. But how do I actually do this? def foo (c : covering_family U) (F : presheaf X) : (matching_sections c F) ⟶ (matching_sections c.generate_sieve.val F) := λ s : matching_sections c F, show matching_sections c.generate_sieve.val F, from { val := λ V H, begin delta matching_sections at s, choose Ui H f using H, refine F.map _ (s.1 _ H), end, property := _ }  Here is what my goal window looks like X : Type u, _inst_1 : small_category X, U : X, c : covering_family U, F : presheaf X, V : over U, s : {s // ∀ (Ui : over U) (H : Ui ∈ c) (Uj : over U) (H_1 : Uj ∈ c) (V : over U) (f : V ⟶ Ui) (g : V ⟶ Uj), F.map (f.left) (s Ui H) = F.map (g.left) (s Uj H_1)}, Ui : over U, H : Ui ∈ c, f : nonempty (V ⟶ Ui) ⊢ Ui.left ⟶ V.left  What I need to do is extract some hom f from V to Ui out of the current f : nonempty (_). I should then be able to close the goal with exact f.left. But I can only eliminate into Prop from nonempty. So how should I set things up? All of this is at https://github.com/leanprover-community/mathlib/blob/sheaf-2/category_theory/sheaf.lean#L190-L199 #### Reid Barton (Dec 28 2018 at 06:14): Are you going to need to prove the resulting construction is independent of the choice? #### Reid Barton (Dec 28 2018 at 06:15): The simple answer is to use choice again, in the form of classical.choice #### Reid Barton (Dec 28 2018 at 06:16): maybe the choose tactic could do this when the final Prop is a nonempty #### Reid Barton (Dec 28 2018 at 06:16): or you could use that \exists blah, blah, blah, true encoding #### Johan Commelin (Dec 28 2018 at 06:18): So nonempty blah is not Lean-equivalent to the \exists blah, blah, blah, true encoding? #### Johan Commelin (Dec 28 2018 at 06:19): The choose tactic doesn't help... :sad: #### Reid Barton (Dec 28 2018 at 06:19): it's not definitionally equivalent, much as p /\ true isn't definitionally equivalent to p #### Johan Commelin (Dec 28 2018 at 06:21): nonempty_of_exists is not an iff... #### Reid Barton (Dec 28 2018 at 06:22): You can just use choice f #### Johan Commelin (Dec 28 2018 at 06:23): Ok, I'll try that. Too bad that choose f does not work. #### Reid Barton (Dec 28 2018 at 06:23): Sometimes when there is going to be a lot of "can only eliminate into Prop" nonsense in a proof, I just put an apply choice at the start #### Reid Barton (Dec 28 2018 at 06:24): or not necessarily at the start of the whole argument, but at the start of some subargument to satisfy some lemma which wants to take an actual map rather than just an existence statement #### Johan Commelin (Dec 28 2018 at 08:22): Ok, that worked. But I still wonder why choose f didn't work. @Patrick Massot Any ideas why choose doesn't work on nonempty? Here's the proof that I have now noncomputable def foo (c : covering_family U) (F : presheaf X) : (matching_sections c F) ⟶ (matching_sections c.generate_sieve.val F) := λ s : matching_sections c F, show matching_sections c.generate_sieve.val F, from { val := λ V H, begin delta matching_sections at s, choose Ui H f using H, refine F.map _ (s.1 _ H), exact (classical.choice f).left, end, property := _ }  #### Kenny Lau (Dec 28 2018 at 08:25): because choose is skolemization? #### Johan Commelin (Dec 28 2018 at 08:32): I don't know what that means. #### Johan Commelin (Dec 28 2018 at 08:47): I love the marvellous power of the underscore: noncomputable def foo (c : covering_family U) (F : presheaf X) : (matching_sections c F) ⟶ (matching_sections c.generate_sieve.val F) := λ s : matching_sections c F, show matching_sections c.generate_sieve.val F, from { val := λ V H, begin choose Ui H f using H, refine F.map _ (s.1 _ H), exact (classical.choice f).left, end, property := begin intros, show (F.map _ ≫ F.map _) _ = (F.map _ ≫ F.map _) _, repeat {rw ← F.map_comp}, exact s.property _ _ _ _ _ (_ ≫ _) (_ ≫ _) end }  #### Johan Commelin (Dec 28 2018 at 18:53): I'm hitting a nasty error again (probably I'm being bitten by choice). Here is the error (code follows below): type mismatch at application ⟨s_val, s_property⟩.val Ui H term H has type Ui_1 ∈ c_1 but is expected to have type Ui ∈ c types contain aliased name(s): Ui U c remark: the tactic dedup can be used to rename aliases  Code: def quux (c : covering_family U) : c.matching_sections ≅ c.generate_sieve.val.matching_sections := { hom := foo c, inv := bar c, hom_inv_id' := begin ext1 F, ext1 s, apply subtype.ext.mpr, funext, convert s.property _ _ _ _ _ _ (𝟙 _), tidy {trace_result := tt} end, inv_hom_id' := begin ext1 F, ext1 s, apply subtype.ext.mpr, funext, dsimp [foo, bar], convert s.property _ _ _ _ _ _ (𝟙 _), -- This line fails tidy {trace_result := tt}, end }  Context, just before the convert: X : Type u, _inst_1 : small_category X, U : X, c : covering_family U, F : presheaf X, s : (matching_sections ((generate_sieve c).val)).obj F, V : over U, H : V ∈ (generate_sieve c).val ⊢ F.map ((classical.choice _).left) (s.val (classical.some H) _) = s.val V H  #### Johan Commelin (Jan 20 2019 at 19:02): @Kevin Buzzard Replying to https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/What's.20new.20in.20Lean.20maths.3F/near/156491890 in this thread. To be precise: I have no trouble at all extending a presheaf from a basis to the whole space. The problem is checking that it sends sheaves to sheaves. The difficulty is probably due to the fact that I do not have a usable API around the sheaf condition. And I guess my sheaf condition is hard to work with right now because I'm trying to be quite general, doing sheaves on an arbitrary site. #### Kevin Buzzard (Jan 20 2019 at 20:02): Oh -- the proof involves some argument on stalks which for a general site is complicated? Are there universe issues or do you only work with small sites? #### Kevin Buzzard (Jan 29 2019 at 18:39): OK so I just spent 2 hours with Ramon going through this proof (sheaf on a basis extends to sheaf on site) again in the case of topological spaces. The ideas are all fresh in my mind at the minute so let me note them down in case there's anything helpful here. Aah -- I now realise that actually I don't know how you're extending the presheaf at all. The way Ramon and I do it is that given a presheaf $F$ on a basis we can define the stalk $F_x$ at a point $x$ via a direct limit construction, and then we define a presheaf $F^+$ on the space by saying that its values on an open $U$ are a subtype of a big Pi type sending $x\in U$ to an element of the stalk $F_x$; it's the subtype consisting of functions which are locally a section of the presheaf-on-a-basis. What both he and I did next was then immediately embarked on a proof that if $F$ is a sheaf on a basis then this extension is a sheaf. This gets really hairy. Say I have a bunch of local sections $s_i$ on opens $U_i$, which agree on overlaps. I want to glue them together to get a section $S$ of $F^+$. Well, a section of $F^+$ is just a subtype of a pi type, so we know how to define it. But the technicality is that to define this function $S$ we want to say $S(x)=s_i(x)$ where we choose some $i$ such that $x\in U_i$. As mathematicians we know that $S(x)$ is independent of the choice, but in computer science this is some classical.indefinite_description blah blah noncomputable crap and we're forced to deal with this. Ramon had written 0 API so at the end of it our goals had all these classical.indefinite_description terms in. He was able to battle past the first few, but checking that $S$ restricted to $s_i$ was really difficult, for a reason which I am only now beginning to understand properly. The issue was that we didn't have the right API for this construction of extending a presheaf-on-a-basis to a presheaf on the space. A general presheaf on a space, when evaluated at some open $U$, is just some random type. But for a presheaf coming from a presheaf-on-a-basis this is far from being true -- the sections are subtypes of pi types, and the restriction maps are literally restrictions. This is all wrapped up in the definition of the construction of a presheaf from a presheaf-on-a-basis. I realised that if $F^+$ is a presheaf coming from a presheaf-on-a-basis then for $x\in U\subseteq X$ and $s\in F^+(X)$ a function, the fact that $(res_U s)(x)=s(x)$ seemed to be true by definition, but Lean would not definitionally unfold the restriction map from $F^+(X)$ to $F^+(U)$ as a restriction of functions. I had to explicitly push Lean in the right direction with lines like dunfold presheaf_on_basis_to_presheaf, dsimp; I was really surprised that this could make progress when a simple dsimp could not. But we shouldn't have been doing this anyway. It seems to me that the correct thing to do is: 1) Define the construction presheaf_on_basis_to_presheaf 2) Define also the actual noncomputable function space, i.e. given $F$ a presheaf on a basis, and an open set$$U$ (not necc in the basis), define the space of functions sending an element $x$ of $U$ to an element of the stalk $F_x$, and have some coercion from $F^+(U)$ to this space of functions.
3) Crucially, prove (by rfl) that the restriction map on $F^+$ really is just restriction of functions. This is some key lemma which if you don't explicitly say it, can get buried. Prove it for values too -- prove that if $S\in F^+(U)$ and $V\subseteq U$ and $x\in V$ then $S(x)=res(S)(x)$. This is how you will eliminate res in practice. We were having to eliminate it using dunfold and then dsimp.
4) Also crucially, you should hide the classical.indefinite_descriptions. Given local sections $s_i$ which agree on overlaps, there's a non-computable function on $U$ which agrees with each $s_i$, but to define it at $x$ you have to choose
$i$ with $x\in U_i$. It's a theorem that the resulting function is independent of all choices. Define the noncomputable function and prove the theorem -- you will need it later!

We'd done none of this, and it was only when struggling through the proof that I began to understand what was missing.

I know you (Johan) are working in a far more complicated situation, but somehow these are the things which seem to me to be necessary to make things work smoothly. Ramon arrived in my office with a goal that had three classical.indefinite_descriptions on one side of an equality, and these are horrible to work with. The idea which Patrick showed so convincingly in his Nantes talk -- hide the nonconstructive stuff with a choose tactic and immediately go to the noncomputable function and the proof that it has the key property you want -- is a really important trick for getting things to run smoothly.

#### Johan Commelin (Jan 29 2019 at 18:45):

Thanks for these detailed comments! They will probably be helpful when I pick up my work on sheaves again in a couple of days!

#### Kevin Buzzard (Jan 29 2019 at 18:45):

How do you extend the presheaf on a basis in your generality?

#### Kevin Buzzard (Jan 29 2019 at 18:45):

Is it still a stalk-valued function?

#### Johan Commelin (Jan 29 2019 at 18:47):

You can take a limit over all basic opens contained in U.

#### Kevin Buzzard (Jan 29 2019 at 18:47):

Does that work for sites?

#### Johan Commelin (Jan 29 2019 at 18:47):

Yes, extending the presheaf is not too hard. What I'm missing is a good API for the sheaf condition.

#### Kevin Buzzard (Jan 29 2019 at 18:48):

What I learnt today was that there are special extra lemmas for presheaves which have come from a presheaf-on-a-basis, and those are what we needed to prove that sheaves go to sheaves.

#### Johan Commelin (Jan 29 2019 at 18:49):

Because it needs to work with abstract sites (where you don't know anything about the opens in your category) and then it should also work for concrete things like the open sets in a concrete topological space (and your presheaf has some concrete interpretation as functions)... somehow these two things don't play nicely together yet.

#### Kevin Buzzard (Jan 29 2019 at 18:49):

But your limit is different. You're taking a subset of a product perhaps.

#### Kevin Buzzard (Jan 29 2019 at 18:52):

Hmm. Maybe the ideas are still the same. I'm perhaps suggesting that you spend some time proving lemmas (by rfl) about the function sending an open U to the product of $F(U_i)$ where the $U_i$ range over the basis elements that are part of a cover. Then prove that if $V$ is a subset of $U$ then the restriction map is something like "restrict to the $U_i$ which map to $V$". Or something.

#### Johan Commelin (Jan 29 2019 at 18:58):

@Kevin Buzzard @Ramon Fernandez Mir Does this mean that you are now rapidly approaching a cleaned up version of schemes? When will there be code that we can look at?

#### Mario Carneiro (Jan 29 2019 at 19:15):

I would also like to see some code, I might be able to give some tips. I think you should define the glue construction for functions, i.e. if you have a bunch of functions that agree on overlaps then you get a function on the union. You can put your choices here and never see them again

#### Kevin Buzzard (Jan 29 2019 at 20:13):

https://github.com/ramonfmir/lean-scheme

#### Kevin Buzzard (Jan 29 2019 at 20:13):

We've only just started really, but we're moving along nicely.

#### Kenny Lau (Jun 23 2019 at 09:44):

do we have sheaves on sites yet? how far are we away from it?

#### Kenny Lau (Jun 23 2019 at 22:53):

import category_theory.limits.limits

universes v w u

namespace category_theory

inductive pullback_diagram : Type v
| base_left | base_right | target

namespace pullback_diagram

inductive hom : pullback_diagram → pullback_diagram → Type v
| id_base_left : hom base_left base_left
| id_base_right : hom base_right base_right
| id_target : hom target target
| to_target_left : hom base_left target
| to_target_right : hom base_right target

def id : Π X : pullback_diagram.{v}, hom X X
| base_left  := hom.id_base_left
| base_right := hom.id_base_right
| target     := hom.id_target

def comp : Π X Y Z : pullback_diagram.{v}, hom X Y → hom Y Z → hom X Z
| _ _ _ hom.id_base_left    g             := g
| _ _ _ hom.id_base_right   g             := g
| _ _ _ hom.id_target       g             := g
| _ _ _ hom.to_target_left  hom.id_target := hom.to_target_left
| _ _ _ hom.to_target_right hom.id_target := hom.to_target_right

instance : small_category pullback_diagram.{v} :=
{ hom := hom,
id := id,
comp := comp,
comp_id' := λ X Y f, by cases f; refl,
id_comp' := λ X Y f, by cases f; refl,
assoc' := λ W X Y Z f g h, by cases f; cases g; cases h; refl }

def to_category {C : Type u} [𝒞 : category.{v} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
pullback_diagram.{w} ⥤ C :=
{ obj := λ p, pullback_diagram.rec_on p X Y Z,
map := λ p q h, @hom.rec_on (λ p' q' h', (pullback_diagram.rec_on p' X Y Z : C) ⟶ pullback_diagram.rec_on q' X Y Z) p q h
(𝟙 X) (𝟙 Y) (𝟙 Z) f g,
map_id' := λ p, by cases p; refl,
map_comp' := λ p q r h1 h2, by cases h1; cases h2; dsimp only [category_struct.comp, comp]; simp only [category.comp_id, category.id_comp] }

def to_category_cone {C : Type u} [𝒞 : category.{v} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (W : C) (f' : W ⟶ X) (g' : W ⟶ Y) (h : f' ≫ f = g' ≫ g) :
limits.cone (to_category f g) :=
{ X := W,
π :=
{ app := λ p, pullback_diagram.rec_on p f' g' (f' ≫ f),
naturality' := λ p q f, by cases f; dsimp only [functor.const, to_category]; simp only [category.comp_id, category.id_comp, h] } }

end pullback_diagram

@[class] def has_pullback (C : Type u) [category.{v} C] : Type (max u v) :=
limits.has_limits_of_shape pullback_diagram.{v} C

section has_pullback

variables {C : Type u} [𝒞 : category.{v} C] [P : has_pullback.{v} C]
include 𝒞 P

def pullback {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : C :=
(P (pullback_diagram.to_category f g)).cone.X

def pullback.fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : pullback f g ⟶ X :=
(P (pullback_diagram.to_category f g)).cone.π.app pullback_diagram.base_left

def pullback.snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : pullback f g ⟶ Y :=
(P (pullback_diagram.to_category f g)).cone.π.app pullback_diagram.base_right

def pullback.corec {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (W : C) (f' : W ⟶ X) (g' : W ⟶ Y) (h : f' ≫ f = g' ≫ g) : W ⟶ pullback f g :=
(P (pullback_diagram.to_category f g)).is_limit.lift (pullback_diagram.to_category_cone f g W f' g' h)

end has_pullback

class has_site (C : Type u) [category.{v} C] [has_pullback C] : Type (max u v) :=
(cov : Π U : C, set (set (Σ V, V ⟶ U)))
(iso_mem : ∀ {U V : C} (e : V ≅ U), { sigma.mk V e.1 } ∈ cov U)
(comp_mem : ∀ {U : C} (S : set (Σ V, V ⟶ U)) (HS : S ∈ cov U)
(F : Π m : Σ V, V ⟶ U, m ∈ S → set (Σ V, V ⟶ m.1)),
(∀ m hm, F m hm ∈ cov m.1) →
{ m | ∃ t ∈ S, ∃ u ∈ F t H, (⟨u.1, u.2 ≫ t.2⟩ : Σ V, V ⟶ U) = m } ∈ cov U)
(pullback_mem : ∀ {U} (S ∈ cov U) (V) (f : V ⟶ U),
{ m | ∃ t ∈ S, (⟨_, pullback.fst f t.2⟩ : Σ W, W ⟶ V) = m } ∈ cov V)

end category_theory

namespace lattice

class Sup_lattice (X : Type u) extends lattice X, has_Sup X :=
(le_Sup : ∀ {s : set X} {a : X}, a ∈ s → a ≤ Sup s)
(Sup_le : ∀ {s : set X} {a : X}, (∀ (b : X), b ∈ s → b ≤ a) → Sup s ≤ a)

class Sup_distrib_lattice (X : Type u) extends Sup_lattice X :=
(inf_Sup_le {} : ∀ {x : X} {s : set X}, x ⊓ lattice.Sup s ≤ lattice.Sup ((⊓) x '' s))

section Sup_lattice

instance complete_lattice.to_Sup_lattice {X : Type u} [complete_lattice X] : Sup_lattice X :=
{ .. (infer_instance : complete_lattice X) }

variables {X : Type u} [Sup_lattice X]

theorem le_Sup' {s : set X} {a : X} : a ∈ s → a ≤ Sup s :=
Sup_lattice.le_Sup

theorem Sup_le' {s : set X} {a : X} : (∀ (b : X), b ∈ s → b ≤ a) → Sup s ≤ a :=
Sup_lattice.Sup_le

theorem Sup_singleton' (x : X) : Sup {x} = x :=
le_antisymm (Sup_le' $λ b hb, set.eq_of_mem_singleton hb ▸ le_refl _)$
le_Sup' $set.mem_singleton x end Sup_lattice section Sup_discrete_lattice instance complete_distrib_lattice.to_Sup_distrib_lattice {X : Type u} [complete_distrib_lattice X] : Sup_distrib_lattice X := { inf_Sup_le := λ x s, by rw [inf_Sup_eq, Sup_image], .. (infer_instance : complete_distrib_lattice X) } variables {X : Type u} [Sup_distrib_lattice X] theorem inf_Sup {x : X} {s : set X} : x ⊓ lattice.Sup s = lattice.Sup ((⊓) x '' s) := le_antisymm Sup_distrib_lattice.inf_Sup_le$ Sup_le' $λ b ⟨c, hcs, hxcb⟩, hxcb ▸ inf_le_inf (le_refl x) (le_Sup' hcs) end Sup_discrete_lattice end lattice namespace category_theory open lattice variables {X : Type u} class is_univalent (X : Type u) [category.{v} X] : Prop := (univalent : ∀ x y : X, ∀ e : x ≅ y, x = y) theorem eq_of_iso [category.{v} X] [is_univalent X] {x y : X} (e : x ≅ y) : x = y := is_univalent.univalent x y e instance is_univalent_partial_order [partial_order X] : is_univalent X := ⟨λ x y e, le_antisymm e.1.1.1 e.2.1.1⟩ instance semilattice_inf.has_pullback [semilattice_inf X] : has_pullback X := λ F, { cone := { X := F.obj pullback_diagram.base_left ⊓ F.obj pullback_diagram.base_right, π := { app := λ p, pullback_diagram.rec_on p ⟨⟨inf_le_left⟩⟩ ⟨⟨inf_le_right⟩⟩ ⟨⟨le_trans inf_le_left (F.map pullback_diagram.hom.to_target_left).down.down⟩⟩, naturality' := by intros; ext } }, is_limit := { lift := λ c, ⟨⟨le_inf (c.π.app pullback_diagram.base_left).down.down (c.π.app pullback_diagram.base_right).down.down⟩⟩, fac' := by intros; ext, uniq' := by intros; ext } } instance Sup_lattice.has_site [Sup_distrib_lattice X] : has_site X := { cov := λ U, { c | U ≤ Sup (sigma.fst '' c) }, iso_mem := λ U V e, show U ≤ _, by rw [set.image_singleton, Sup_singleton']; exact e.2.1.1, comp_mem := λ U S HS F HF, le_trans HS$ Sup_le' $λ x hx, let ⟨m, hmS, hmx⟩ := hx in hmx ▸ le_trans (HF m hmS) (Sup_le'$ λ y hy, let ⟨n, hnFS, hny⟩ := hy in
le_Sup' ⟨⟨n.1, ⟨⟨le_trans n.2.1.1 m.2.1.1⟩⟩⟩, ⟨m, hmS, n, hnFS, rfl⟩, hny⟩),
pullback_mem := λ U S HS V f,
calc  V
≤ V ⊓ Sup (sigma.fst '' S) : le_inf (le_refl V) (le_trans f.1.1 HS)
... = Sup ((⊓) V '' (sigma.fst '' S)) : inf_Sup
... = Sup ((⊓) V ∘ sigma.fst '' S) : congr_arg Sup (set.image_comp _ _ S).symm
... ≤ Sup (sigma.fst '' {m | ∃ t ∈ S, (⟨_, pullback.fst f t.2⟩ : Σ W, W ⟶ V) = m}) :
Sup_le' (λ b ⟨c, hcs, hb⟩, le_Sup' ⟨⟨V ⊓ c.1, ⟨⟨inf_le_left⟩⟩⟩, ⟨c, hcs, rfl⟩, hb⟩) }

end category_theory


#### Kenny Lau (Jun 23 2019 at 23:32):

import category_theory.limits.types

universes u v

namespace category_theory

instance has_pullback_Type : has_pullback (Type u) :=
λ F, by apply_instance

instance has_site_Type : has_site (Type u) :=
{ cov := λ α, { S | ∀ x : α, ∃ (f : Σ β, β ⟶ α), ∃ hf : f ∈ S, x ∈ set.range f.2},
iso_mem := λ α β e x, ⟨⟨β, e.1⟩, set.mem_singleton _, e.2 x, congr_fun e.4 x⟩,
comp_mem := λ α S HS F HF x, let ⟨f, hf, p, hfpx⟩ := HS x in
let ⟨g, hg, q, hgqp⟩ := HF f hf p in
⟨⟨g.1, g.2 ≫ f.2⟩, ⟨f, hf, g, hg, rfl⟩, q, hfpx ▸ hgqp ▸ rfl⟩,
pullback_mem := λ α S HS β f x, let ⟨g, hg, p, hgpx⟩ := HS (f x) in
⟨⟨pullback f g.2, pullback.fst f g.2⟩, ⟨g, hg, rfl⟩,
⟨λ v, pullback_diagram.rec_on v x p (f x),
by intros v w h; cases h; dsimp only [pullback_diagram.to_category]; { refl <|> exact hgpx }⟩,
rfl⟩ }

end category_theory


#### Kenny Lau (Jun 23 2019 at 23:32):

@Johan Commelin Am I duplicating effort?

#### Johan Commelin (Jun 24 2019 at 04:43):

@Kenny Lau Thanks for looking into this. The idea of the is_univalent class is a nice one! Also, as has been mentioned in the other thread, I agree that refining the lattice hierarchy is probably a good idea. (And I hope it doesn't lead to some exponential blow-up down the road.)
I don't think you are duplicating effort. Concerning pullback_diagram: there have been long discussions between @Scott Morrison @Reid Barton and myself and I think we are still not completely clear on what the best way to support special shapes is.
Other thoughts:

• there are different approaches to sites: Grothendieck topologies, coverages, and Grothendieck pretopologies. You have formalised pretopologies but not every site admits a pretopology (e.g. a basis for a topological space can be turned into a site, but doesn't have to be a pretopology).
• When I was working on these things half a year ago, I managed to formalise the definition of a sheaf on site. But I had a hard time actually verifying that certain "trivial" examples are sheaves: e.g. (continuous) functions from a topological space X to (a topological space) Y.
• Currently Kevin and you are thinking/working hard on gluing sheaves, which I think is a perfect way to stress-test the definitions. However, I would really want to add two things to that list: sheafification and the adjunction between pushforward and pullback. Without those, we won't have a reasonable API to sheaves.

In hindsight, I took on a project that was way to big. I'm very excited that there are now more people pouring power into this (-;

#### Scott Morrison (Jun 24 2019 at 05:05):

Regarding is_univalent --- usually this is called skeletal.

#### Kenny Lau (Jun 24 2019 at 08:09):

@Johan Commelin didn't I formalize sites in terms of coverages?

#### Johan Commelin (Jun 24 2019 at 08:25):

You use pullbacks

#### Johan Commelin (Jun 24 2019 at 08:25):

Coverages allow you to define sites on categories that don't have pullbacks

#### Johan Commelin (Jun 24 2019 at 08:25):

E.g. lattices without infs

#### Johan Commelin (Jun 24 2019 at 08:25):

E.g. bases of topologies

#### Kevin Buzzard (Jun 24 2019 at 08:26):

The schemes work that Ramon did about extending sheaves on bases to sheaves was made much easier by the fact that the intersection of two basic open sets was basic open in our situation.

#### Kevin Buzzard (Jun 24 2019 at 08:26):

$D(f)\cap D(g)=D(fg)$.

#### Kevin Buzzard (Jun 24 2019 at 08:27):

Without that, the construction of the sheaf of rings on $\mathrm{Spec}(A)$ would have been harder.

#### Kenny Lau (Jun 24 2019 at 08:29):

I just followed Stacks project

#### Johan Commelin (Jun 24 2019 at 08:31):

https://ncatlab.org/nlab/show/coverage

#### Kenny Lau (Jun 24 2019 at 08:31):

so I should use that definition instead?

#### Kenny Lau (Jun 24 2019 at 08:34):

also where did the first two axioms go?

#### Johan Commelin (Jun 24 2019 at 08:59):

@Kenny Lau You don't need the first two axioms.

#### Kenny Lau (Jun 24 2019 at 08:59):

then why did Stacks include them?

#### Johan Commelin (Jun 24 2019 at 09:01):

It might make sense to browse through the first half of SGA 4 if you want to seriously attempt to build a library for sites.

#### Kevin Buzzard (Jun 24 2019 at 09:01):

SGA 4 you mean? Or not

Fixed :smiley:

#### Kevin Buzzard (Jun 24 2019 at 09:02):

SGA4 is not hard to read

#### Kevin Buzzard (Jun 24 2019 at 09:02):

It's much easier than EGA4

#### Kenny Lau (Jun 24 2019 at 09:03):

is there an English translation?

#### Kevin Buzzard (Jun 24 2019 at 09:04):

I don't know. "Categorie" = category, "morphisme" = morphism, "univers" = universe. Try just taking symmetric difference with {e}.

#### Kenny Lau (Jun 24 2019 at 09:04):

so espace etale = spac tal?

#### Kevin Buzzard (Jun 24 2019 at 09:05):

change e-acute to s

#### Kevin Buzzard (Jun 24 2019 at 09:05):

that sometimes work.

#### Kevin Buzzard (Jun 24 2019 at 09:05):

fenetre -> fenester

#### Kenny Lau (Jun 24 2019 at 09:05):

surely fenetre -> fnstr

#### Kevin Buzzard (Jun 24 2019 at 09:05):

Oh it's e-hat goes to s

#### Johan Commelin (Jun 24 2019 at 09:05):

Come on Kenny, your French is better than mine... and I can read that...

#### Kevin Buzzard (Jun 24 2019 at 09:06):

You're missing off the accents. They're not all e's.

#### Kenny Lau (Jun 24 2019 at 09:09):

how did Grothendieck call Grothendieck topos/topology/etc?

#### Kevin Buzzard (Jun 24 2019 at 09:12):

Probably just topos / topology on a category.

#### Kenny Lau (Jun 24 2019 at 09:12):

et d'ailleurs, quelles pages dois-je lire?

#### Kevin Buzzard (Jun 24 2019 at 09:12):

The definitions are probably only a few pages in.

#### Kenny Lau (Jun 24 2019 at 09:15):

il ne definit faisceaux que dans page 223

#### Kenny Lau (Jun 24 2019 at 09:18):

ok tous ce que j'ai besoin de est dans expose II

#### Johan Commelin (Jun 24 2019 at 09:23):

I'm not saying you should formalise SGA 4.1. But I'm saying that it might be good to be aware of what's in there.

#### Kenny Lau (Jun 24 2019 at 09:24):

Soit C une categorie. On appelle crible de la categorie C une sous-categorie pleine D de C possedant la propriete suivante: tout objet de C tel qu'il existe un morphisme de cet objet dans un objet de D est dans D. Soit X un objet de C; on appelle (par abus de langage) cribles de X les cribles de la categorie C/X.

#### Kenny Lau (Jun 24 2019 at 09:24):

seems complicated

#### Johan Commelin (Jun 24 2019 at 09:26):

Right... another option is to forget about sites for the moment.

#### Johan Commelin (Jun 24 2019 at 09:26):

And focus on sheaves on distrib_inf_lattices or whatever the variant you need.

#### Kenny Lau (Jun 24 2019 at 09:27):

can't I just use some variants of my current definition

Sure, you can

#### Johan Commelin (Jun 24 2019 at 09:27):

But if you want a basis for a topology to be a site, then you need coverages

#### Kenny Lau (Jun 24 2019 at 09:28):

structure sheaf (C : Type u) [category.{v} C] [has_pullback C] [has_site.{v} C] : Type (max u v (w+1)) :=
(to_presheaf : presheaf.{v w} C)
(ext : ∀ U : C, ∀ s t : to_presheaf.eval U, ∀ c ∈ has_site.cov U,
(∀ d : Σ V, V ⟶ U, d ∈ c → to_presheaf.res d.2 s = to_presheaf.res d.2 t) →
s = t)
(glue : ∀ U : C, ∀ c ∈ has_site.cov U, ∀ F : Π d : Σ V, V ⟶ U, d ∈ c → to_presheaf.eval d.1,
(∀ d1 d2 : Σ V, V ⟶ U, ∀ H1 : d1 ∈ c, ∀ H2 : d2 ∈ c,
to_presheaf.res (pullback.fst d1.2 d2.2) (F d1 H1) =
to_presheaf.res (@@pullback.snd _ _inst_2 d1.2 d2.2) (F d2 H2)) →
∃ g : to_presheaf.eval U, ∀ d : Σ V, V ⟶ U, ∀ H : d ∈ c,
to_presheaf.res d.2 g = F d H)


#### Kenny Lau (Jun 24 2019 at 09:28):

But if you want a basis for a topology to be a site, then you need coverages

oh that's for extending a sheaf from a sheaf on basis?

#### Johan Commelin (Jun 24 2019 at 09:28):

Yup, if you want to do that using the general framework

#### Kenny Lau (Jun 24 2019 at 09:28):

how do I do that if I have coverages?

#### Johan Commelin (Jun 24 2019 at 09:28):

We could of course do a hands-on extension

#### Johan Commelin (Jun 24 2019 at 09:29):

how do I do that if I have coverages?

You need to formalise morphism of sites, and then the $site_{basis}$ comes with a geometric morphism (aka morphism of sites/topoi) to $site_{topology}$.

#### Johan Commelin (Jun 24 2019 at 09:29):

You pushforward along this morphism.

#### Kenny Lau (Jun 24 2019 at 09:30):

and how do you show that if I restrict a sheaf to a sheaf on basis then extend it again, I get the "same" sheaf?

#### Johan Commelin (Jun 24 2019 at 09:30):

That's a theorem. I'm not saying it's easy.

#### Johan Commelin (Jun 24 2019 at 09:30):

(It's math easy, of course)

#### Kenny Lau (Jun 24 2019 at 09:31):

how do you do it in maths?

#### Johan Commelin (Jun 24 2019 at 09:32):

"Proof. Follows from the sheaf property. QED" (I guess this is what most people would do...)

#### Johan Commelin (Jun 24 2019 at 09:33):

I think there is a proof in the stacks project. The define a notion of "sheaf on a basis". But what they do is hands on. If you use coverages, then a "sheaf on a basis" is just a sheaf.

#### Johan Commelin (Jun 24 2019 at 09:33):

I don't know if we want to care about sheaves on bases...

#### Kenny Lau (Jun 24 2019 at 09:34):

so what I'm wondering is, if you use this wonderful language of coverage, how do you do it?

#### Johan Commelin (Jun 24 2019 at 09:40):

Well, you will still need to use the sheaf property for coverages

#### Johan Commelin (Jun 24 2019 at 09:41):

But anyway... do you have a good reason to pursue this?

#### Johan Commelin (Jun 24 2019 at 09:41):

Or should we first try to do the push-pull adjunction for sheaves on topological spaces?

I don't know

#### Kenny Lau (Jun 24 2019 at 10:07):

import category_theory.category

universes v u

namespace category_theory

class has_site (C : Type u) [category.{v+1} C] : Type (max u v) :=
(cov : Π U : C, set (set (Σ V : C, V ⟶ U)))
(lift : ∀ U : C, ∀ c ∈ cov U, ∀ V : C, ∀ g : V ⟶ U, ∃ h ∈ cov V,
∀ j ∈ h, ∃ i ∈ c, ∃ k : sigma.fst j ⟶ sigma.fst i, k ≫ i.2 = j.2 ≫ g)

end category_theory


#### Kenny Lau (Jun 24 2019 at 10:07):

@Johan Commelin how does this look?

#### Mario Carneiro (Jun 24 2019 at 10:13):

is that really the only axiom? I would have expected something like "{<U, id>} \in cov U" and possibly something about covers of covers

#### Kenny Lau (Jun 24 2019 at 10:19):

I'm just using https://ncatlab.org/nlab/show/coverage#Definition

#### Kenny Lau (Jun 24 2019 at 10:19):

I believe it's like how you can generate an equivalence relation given just any relation

#### Kenny Lau (Jun 24 2019 at 10:20):

and it's also to allow for a basis to be a site

#### Kenny Lau (Jun 24 2019 at 10:36):

import category_theory.sites.basic topology.bases topology.opens

universes v u

namespace category_theory

open topological_space lattice

@[reducible] def topological_basis (X : Type u) [topological_space X] : Type u :=
{ B : set (opens X) // opens.is_basis B }

instance basis.has_site {X : Type u} [topological_space X] (B : topological_basis X) : has_site B :=
{ cov := λ U, { c | ∀ x ∈ U.1, ∃ i ∈ c, x ∈ subtype.val (sigma.fst i) },
lift := λ U c hc V g, ⟨{ h | ∃ i ∈ c, h.1.1 ≤ V ⊓ i.1.1 },
λ x hxV, let ⟨i, hic, hxi⟩ := hc x (g.1.1 hxV),
⟨W, HWB, hxW, HWVi⟩ := opens.is_basis_iff_nbhd.1 B.2 (show x ∈ V.1 ⊓ i.1.1, from ⟨hxV, hxi⟩) in
⟨⟨⟨W, HWB⟩, ⟨⟨λ y hy, (HWVi hy).1⟩⟩⟩, ⟨i, hic, HWVi⟩, hxW⟩,
λ j ⟨i, hic, hjVi⟩, ⟨i, hic, ⟨⟨λ y hy, (hjVi hy).2⟩⟩, rfl⟩⟩ }

end category_theory


#### Kenny Lau (Jun 24 2019 at 10:37):

looks like it's working

@Kenny Lau Cool!

#### Johan Commelin (Jun 24 2019 at 11:17):

So now you can probably also write down the sheaf axiom(s) in this language.

#### Kevin Buzzard (Jun 24 2019 at 11:18):

But anyway... do you have a good reason to pursue this?

Pushforwards and pullbacks are just adjoint functors. Kenny is flagging the situation where we go from a sheaf on a basis to a sheaf, and in that situation both the functors are equivalences. Is this some sort of Galois connection but one level up?

I guess Grothendieck knew that a top space, and a top-space-with-a-basis, were the same thing as far as sheaf theory goes, so he defined the topos associated to the site to be the category of sheaves on the site, and then we have two different sites with the same topos (and hence the same "geometry").

is that really the only axiom? I would have expected something like "{<U, id>} \in cov U" and possibly something about covers of covers

These are definitely axioms in some of these abstrations. What's a Grothendieck topology? Is this the difference between a Groth Top and a coverage?

#### Johan Commelin (Jun 24 2019 at 11:19):

Galois connections are adjunctions one level down, yes.

#### Johan Commelin (Jun 24 2019 at 11:20):

A coverage is the bare minimum that you need. You can use those to generate a Grothendieck topology.

#### Kevin Buzzard (Jun 24 2019 at 11:20):

Is it a Galois insertion I'm talking about then?

#### Johan Commelin (Jun 24 2019 at 11:20):

A Galois insertion is like an adjunction where the left(?) adjoint is fully faithful.

#### Johan Commelin (Jun 24 2019 at 11:21):

Ad coverage and axioms, see https://ncatlab.org/nlab/show/coverage#saturation_conditions

#### Kevin Buzzard (Jun 24 2019 at 11:24):

I have never used the nlab as a serious reference before (of course this is mostly because I do number theory rather than higher category stuff). I get the impression that there's a small community so probably not much refereeing going on. It would an interesting test for the nlab pages if they were being used as a resource for formalising. How accurate are they? I know that Kenny sees the nlab and can't tell it apart from SGA4, but for me SGA4 is refereed, much used, and trustworthy, whereas nlab is just some random website which might be full of fake news.

#### Kevin Buzzard (Jun 24 2019 at 11:24):

This was also a problem with Wikipedia in the beginning, when it had some maths pages and the quality was extremely variable.

#### Reid Barton (Jun 24 2019 at 12:13):

I would say nlab in general is somewhat more trustworthy than Wikipedia though of course still less trustworthy than peer-reviewed publications. Compared to Wikipedia, the nlab authors are a lot more likely to know what they're talking about in the first place.

#### Kevin Buzzard (Jun 24 2019 at 12:51):

Well that's good to know. With Wikipedia there used to be dozens of inaccuracies in some articles, some were very poor initially, but I could never be bothered to learn how to change them (I had three small kids at the time). Sufficiently many people did learn that Wikipedia is much better now, but I just didn't really know about nLab's record for accuracy, and if I don't know then my default opinion is "do not trust". What I've seen from it does look good though, when I'm reading about stuff I already understand.

Last updated: May 14 2021 at 18:28 UTC