Zulip Chat Archive

Stream: maths

Topic: sheaves and sites


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 08 2018 at 13:35):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Nov 12 2018 at 15:29):

did you say nlab...

view this post on Zulip Kenny Lau (Nov 12 2018 at 15:30):

man you've gone too far...

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 12 2018 at 19:11):

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

view this post on Zulip 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
Do people already see reasons to choose/discard one of these options?

view this post on Zulip 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...

view this post on Zulip Reid Barton (Nov 12 2018 at 19:57):

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

view this post on Zulip Reid Barton (Nov 12 2018 at 20:00):

Maybe this isn't actually causing any difficulty

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 13 2018 at 08:11):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 13 2018 at 08:15):

(If you have time for this...)

view this post on Zulip 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.𝒪))

view this post on Zulip Scott Morrison (Nov 13 2018 at 08:19):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 13 2018 at 08:22):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 08:22):

Why would you want the bundled presheaves?

view this post on Zulip Johan Commelin (Nov 13 2018 at 08:23):

To define morphisms of ringed spaces?

view this post on Zulip Johan Commelin (Nov 13 2018 at 08:23):

I think I would first do that unbundled.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:03):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 09:46):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:47):

That is one of the 23 possibilities (-;

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:47):

This is math-trivial, of course

view this post on Zulip Harry Gindi (Nov 13 2018 at 09:48):

A lot of them aren't true for sheafy rings

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:48):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:48):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 09:49):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 09:50):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:52):

What exactly do you mean?

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:52):

Working internally in some topos?

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:53):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:53):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 09:55):

Yeah, I agree

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Nov 13 2018 at 09:57):

Why not just use a sigma type?

view this post on Zulip Scott Morrison (Nov 13 2018 at 09:57):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:57):

I want to use full_subcategory

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:57):

But maybe I shouldn't?

view this post on Zulip Scott Morrison (Nov 13 2018 at 09:57):

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

view this post on Zulip Scott Morrison (Nov 13 2018 at 09:57):

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

view this post on Zulip Scott Morrison (Nov 13 2018 at 09:58):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:58):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:58):

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

view this post on Zulip 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 ...

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:58):

/me is lazy...

view this post on Zulip Scott Morrison (Nov 13 2018 at 09:58):

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

view this post on Zulip Scott Morrison (Nov 13 2018 at 09:59):

so it's not just merging a branch

view this post on Zulip Johan Commelin (Nov 13 2018 at 09:59):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 09:59):

Is there documentation for what a sigma-category is?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Nov 13 2018 at 10:00):

into full_subcategory.lean?

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:00):

does it have a non-type-theoretic analogue?

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:01):

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

view this post on Zulip 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'.

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:02):

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

view this post on Zulip Scott Morrison (Nov 13 2018 at 10:02):

Does it have a name?

view this post on Zulip Scott Morrison (Nov 13 2018 at 10:02):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:04):

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

view this post on Zulip 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 XX with values in a category CC?
What assumptions do I need to make on XX and/or CC? Is there some grand theory that unifies everything?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:07):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:08):

yes, but it is usually the wrong thing

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:08):

Ok, so it works but is useless.

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:09):

I think so, yes

view this post on Zulip 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.

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:12):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:12):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:13):

probably the easiest way is as you said

view this post on Zulip 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

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:15):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:16):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Nov 13 2018 at 10:19):

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

view this post on Zulip 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

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:19):

then you could try to follow Hakim's thesis

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:21):

I challenge you to try it :smiley:

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:22):

What do you mean?

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:22):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:23):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:23):

Sure. And Type is equivalent to sheaves on unit

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:23):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:24):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:24):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:25):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:25):

exactly, it looks daunting

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:25):

Very daunting

view this post on Zulip Johan Commelin (Nov 13 2018 at 10:25):

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

view this post on Zulip 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?

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:27):

it's not easy

view this post on Zulip Harry Gindi (Nov 13 2018 at 10:29):

It would probably be highly rewarding in terms of work saved

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 10:51):

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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 10:51):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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)

view this post on Zulip Harry Gindi (Nov 13 2018 at 11:46):

oh yeah, he's here, Jonas

view this post on Zulip Harry Gindi (Nov 13 2018 at 11:47):

@Jonas Frey

view this post on Zulip Johan Commelin (Nov 13 2018 at 12:01):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:00):

so what does "algebraic" mean here?

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:01):

admits a finite limit sketch over set, I believe

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:01):

like what are some simple examples?

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:01):

sheaves of categories are bad, for example

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:01):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:02):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:02):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:03):

yeah, basically

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:04):

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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:04):

or does pullbacks suffice?

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:05):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:05):

(deleted)

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:06):

sorry, all products

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:07):

because you can have infinite covering families

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:08):

Scott's version works better than that

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:08):

it hits all of the ones we care about

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:09):

Scott can say better than me

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:13):

In the perfectoid project we need sheaves of topological rings

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:13):

hmm, how are those even defined?

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:14):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:14):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:15):

Are they pro-rings like completions?

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:17):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:17):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:18):

https://www2.math.uni-paderborn.de/fileadmin/Mathematik/People/wedhorn/Lehre/AdicSpaces.pdf remark 8.19 on p80

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:20):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:20):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:20):

I am not sure this has anything to do with it

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:21):

there is epsilon more to it than this.

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:21):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:22):

These rings are not adic rings in general

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:22):

ah

view this post on Zulip 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 + ..."

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:22):

mhm

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:23):

They're now called Huber rings

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 13:23):

(terminology due to Scholze)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:24):

in which case the forgetful functor is implicit

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:24):

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

view this post on Zulip 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.

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:26):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:27):

but that way lies madness

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 13 2018 at 13:51):

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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:52):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:52):

Can sieves make life easier?

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:54):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 13 2018 at 13:56):

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

I am already using sieves.

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:57):

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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Nov 13 2018 at 13:59):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 13:59):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:00):

@Mario Carneiro Hence my more precise question...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:01):

So it is not as general as your test case.

view this post on Zulip Harry Gindi (Nov 13 2018 at 14:02):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:03):

Feel free to join in :joy_cat:

view this post on Zulip Harry Gindi (Nov 13 2018 at 14:03):

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

view this post on Zulip Kenny Lau (Nov 13 2018 at 14:04):

let's just define the spectrum of a ring fist

view this post on Zulip Kenny Lau (Nov 13 2018 at 14:04):

(sorry, I'm a more concrete guy)

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:05):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 14:06):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Harry Gindi (Nov 13 2018 at 14:18):

especially if you decide to go down the internal logic route

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:28):

Ok, thanks for the tips.

view this post on Zulip Reid Barton (Nov 13 2018 at 14:28):

Step 1 will require choice

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:28):

I'm currently trying to build a function.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 13 2018 at 14:28):

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

view this post on Zulip Patrick Massot (Nov 13 2018 at 14:31):

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

view this post on Zulip 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]

view this post on Zulip Patrick Massot (Nov 13 2018 at 14:32):

exactly

view this post on Zulip Patrick Massot (Nov 13 2018 at 14:32):

hopefully this is what I linked to

view this post on Zulip Harry Gindi (Nov 13 2018 at 14:32):

I can't get that link to work on mobile

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:34):

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

view this post on Zulip 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 A0A_0, A1A_1 closed subsets of a space X, there is a pushout square in Top involving A0A1A_0 \cap A_1, A0A_0, A1A_1, A0A1A_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.

view this post on Zulip Harry Gindi (Nov 13 2018 at 14:36):

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

view this post on Zulip Harry Gindi (Nov 13 2018 at 14:36):

that's surprising to me

view this post on Zulip Harry Gindi (Nov 13 2018 at 14:37):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 13 2018 at 14:38):

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

view this post on Zulip Reid Barton (Nov 13 2018 at 14:38):

In Lean, basically, choice = nonconstructive

view this post on Zulip Harry Gindi (Nov 13 2018 at 14:38):

so how do intuitionists glue maps?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 13 2018 at 14:43):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 13 2018 at 14:45):

where by "choice" I mean unique choice

view this post on Zulip Mario Carneiro (Nov 13 2018 at 14:46):

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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 14:46):

they all follow from the same axiom

view this post on Zulip Harry Gindi (Nov 13 2018 at 14:49):

Can you glue maps of locales without choice?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:55):

@Ramon Fernandez Mir Good to see you!

view this post on Zulip Mario Carneiro (Nov 13 2018 at 14:55):

There is a rewrite rule for this

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:55):

I want rewrite_search...

view this post on Zulip Mario Carneiro (Nov 13 2018 at 14:57):

supr_subtype

view this post on Zulip 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 V, U (where U,VU, V cover the overall domain XX) agreeing on their intersection UV U \cap V and I needed to construct a continuous function XY 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.

view this post on Zulip Kenny Lau (Nov 13 2018 at 14:58):

@Luca Gerolla wrong thread?

view this post on Zulip Mario Carneiro (Nov 13 2018 at 14:58):

I don't think so

view this post on Zulip Kenny Lau (Nov 13 2018 at 14:59):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:59):

He's on a thread about gluing functions.

view this post on Zulip Kenny Lau (Nov 13 2018 at 14:59):

\cap \cap

view this post on Zulip Johan Commelin (Nov 13 2018 at 14:59):

His post is about gluing functions.

view this post on Zulip 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 :)

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 13 2018 at 15:42):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 15:43):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Reid Barton (Nov 13 2018 at 15:49):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 13 2018 at 15:50):

But your suggested lemma would also fix this problem.

view this post on Zulip 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)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).

view this post on Zulip 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".

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 16:55):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 13 2018 at 17:38):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 17:38):

I convinced myself this afternoon that they all existed

view this post on Zulip 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 (-;

view this post on Zulip Reid Barton (Nov 13 2018 at 17:39):

They do all exist

view this post on Zulip Johan Commelin (Nov 13 2018 at 17:39):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 17:40):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 17:42):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 17:45):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 13 2018 at 17:49):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:06):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 18:06):

@Mario Carneiro Do you want schemes in mathlib?

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:06):

I want polished code in mathlib

view this post on Zulip Johan Commelin (Nov 13 2018 at 18:06):

Do you want polished schemes in mathlib?

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:07):

sure, if that interests yous

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:07):

there seem to be a lot of intermediate steps though

view this post on Zulip Johan Commelin (Nov 13 2018 at 18:07):

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

view this post on Zulip Johan Commelin (Nov 13 2018 at 18:09):

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

view this post on Zulip Reid Barton (Nov 13 2018 at 18:14):

I'm not sure which construction Mario is referring to

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Scott Morrison (Nov 13 2018 at 20:49):

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

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:33):

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

view this post on Zulip 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.)

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:35):

And Kenny did them already :P

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:37):

but colimits in Set are completely different to colimits in CommRing

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:37):

or am I misunderstanding? (presumably)

view this post on Zulip Reid Barton (Nov 13 2018 at 22:37):

General ones are, but filtered ones are not

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:38):

Oh I see!

view this post on Zulip 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!)

view this post on Zulip Scott Morrison (Nov 13 2018 at 22:40):

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

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Nov 13 2018 at 22:40):

Yes

view this post on Zulip Scott Morrison (Nov 13 2018 at 22:40):

That isn't wise. :-)

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:41):

and instead of stalk_at one should use something else?

view this post on Zulip Scott Morrison (Nov 13 2018 at 22:41):

I think stalk_at will be exactly the same

view this post on Zulip Scott Morrison (Nov 13 2018 at 22:42):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:42):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:42):

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

view this post on Zulip 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,

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:42):

at the minute cloning it would lead me astray

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:43):

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

view this post on Zulip Scott Morrison (Nov 13 2018 at 22:43):

That I don't know.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:44):

and then quotiented

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:44):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:44):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Nov 13 2018 at 22:45):

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

view this post on Zulip 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. :-)

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 13 2018 at 22:46):

and filtered colimits are easy

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:46):

Is there a general story?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:47):

Reducing a general colimit to a filtered colimit?

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:49):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:49):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:49):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:50):

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

view this post on Zulip Reid Barton (Nov 13 2018 at 22:50):

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

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 22:51):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Harry Gindi (Nov 14 2018 at 02:08):

the general statement comes from the theory of locally presentable categories

view this post on Zulip 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

view this post on Zulip Harry Gindi (Nov 14 2018 at 02:12):

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

view this post on Zulip 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

view this post on Zulip Harry Gindi (Nov 14 2018 at 02:15):

standard reference is Adamek-Rosicky

view this post on Zulip Harry Gindi (Nov 14 2018 at 02:17):

It seems a lot less complicated than doing Lawvere theories generally

view this post on Zulip 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

view this post on Zulip Harry Gindi (Nov 14 2018 at 02:22):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 }

view this post on Zulip Reid Barton (Nov 15 2018 at 13:24):

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

view this post on Zulip Reid Barton (Nov 15 2018 at 13:25):

what goal is the last line solving?

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 15 2018 at 13:39):

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:44):

Not yet, still working on it.

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:45):

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:46):

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

view this post on Zulip Reid Barton (Nov 15 2018 at 13:52):

Oh, I see

view this post on Zulip Reid Barton (Nov 15 2018 at 13:55):

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

view this post on Zulip Reid Barton (Nov 15 2018 at 13:55):

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:56):

Hmmm... I think so.

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:56):

If you want to help, please do so.

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:56):

Lean is fighting back hard (-;

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:57):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 15 2018 at 13:58):

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

view this post on Zulip Reid Barton (Nov 15 2018 at 13:59):

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:00):

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:00):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 15 2018 at 14:06):

I think you will want to apply it twice

view this post on Zulip Reid Barton (Nov 15 2018 at 14:06):

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:07):

What do you mean?

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:08):

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:08):

I have a presheaf on B

view this post on Zulip Reid Barton (Nov 15 2018 at 14:08):

Okay so let's call opens X C for now

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:09):

Aaah, C was my category of coefficients so far

view this post on Zulip Reid Barton (Nov 15 2018 at 14:09):

ah

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:09):

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

view this post on Zulip Reid Barton (Nov 15 2018 at 14:09):

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:10):

Right, so I should forget about C

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:10):

And sheaves of rings will require some extra thought

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 15 2018 at 14:11):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 15 2018 at 14:11):

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

view this post on Zulip Reid Barton (Nov 15 2018 at 14:17):

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:17):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 15 2018 at 15:04):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Nov 15 2018 at 16:16):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Nov 15 2018 at 19:42):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 20 2018 at 08:26):

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

view this post on Zulip Kevin Buzzard (Nov 20 2018 at 08:26):

I'm explicitly talking about typeclasses

view this post on Zulip Chris Hughes (Nov 20 2018 at 08:26):

What universe is ?m_1 expected to be in?

view this post on Zulip Johan Commelin (Nov 20 2018 at 08:26):

Type u

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 20 2018 at 08:28):

Can I rewrite along equivs?

view this post on Zulip Mario Carneiro (Nov 20 2018 at 08:28):

I think? calc for sure

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Nov 20 2018 at 08:28):

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

view this post on Zulip Mario Carneiro (Nov 20 2018 at 08:29):

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

view this post on Zulip Mario Carneiro (Nov 20 2018 at 08:30):

obviously it's not high on the list of priorities

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 20 2018 at 08:30):

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

view this post on Zulip Mario Carneiro (Nov 20 2018 at 08:31):

that sounds fine

view this post on Zulip Mario Carneiro (Nov 20 2018 at 08:31):

you can just check, of course

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Nov 20 2018 at 08:32):

No it isn't

view this post on Zulip Mario Carneiro (Nov 20 2018 at 08:34):

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

view this post on Zulip Mario Carneiro (Nov 20 2018 at 08:34):

it should home in on the mismatched part

view this post on Zulip Johan Commelin (Nov 20 2018 at 08:35):

How exactly should I do that?

view this post on Zulip 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

view this post on Zulip 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}

view this post on Zulip Johan Commelin (Nov 20 2018 at 08:38):

That's progress at least.

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 20 2018 at 09:49):

Right. That is about what I expected.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johannes Hölzl (Nov 20 2018 at 09:55):

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

view this post on Zulip Johannes Hölzl (Nov 20 2018 at 09:55):

and param provides us with the necessary relations

view this post on Zulip Johan Commelin (Nov 20 2018 at 09:58):

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

view this post on Zulip Patrick Massot (Nov 20 2018 at 10:01):

You need to ask @Cyril Cohen about this

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Nov 20 2018 at 14:05):

What's up, @Kenny Lau?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 20 2018 at 15:26):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 20 2018 at 15:28):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Nov 20 2018 at 15:28):

No, they aren't equal by tidy either

view this post on Zulip Reid Barton (Nov 20 2018 at 15:29):

Or rather, what did you change that instance to?

view this post on Zulip Reid Barton (Nov 20 2018 at 15:30):

well, the right hand side of that goal I guess

view this post on Zulip Johan Commelin (Nov 20 2018 at 15:30):

Exactly

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 20 2018 at 15:32):

... I'm really confused now

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 20 2018 at 15:36):

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

view this post on Zulip Reid Barton (Nov 20 2018 at 15:36):

But I still think the duplication is silly anyways

view this post on Zulip Johan Commelin (Nov 20 2018 at 15:37):

Which duplication do you mean exactly?

view this post on Zulip Reid Barton (Nov 20 2018 at 15:38):

Good question

view this post on Zulip Reid Barton (Nov 20 2018 at 15:38):

I was thinking of has_colimits_of_shape and has_colimits being unrelated

view this post on Zulip Reid Barton (Nov 20 2018 at 15:39):

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

view this post on Zulip Reid Barton (Nov 20 2018 at 15:39):

Gah, has_coproducts

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 20 2018 at 15:44):

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

view this post on Zulip Reid Barton (Nov 20 2018 at 15:45):

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

view this post on Zulip 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:

view this post on Zulip Reid Barton (Nov 20 2018 at 15:46):

by convert x should be the same as by exact x

view this post on Zulip Johan Commelin (Nov 20 2018 at 15:46):

which apparently is not the same as x

view this post on Zulip Reid Barton (Nov 20 2018 at 17:56):

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

view this post on Zulip 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...

view this post on Zulip Reid Barton (Nov 20 2018 at 18:00):

I wish you could jump from names in the goal window to their definitions...

view this post on Zulip Johan Commelin (Nov 20 2018 at 18:11):

Right, we should but the "interactive" back in the goal window :grinning:

view this post on Zulip 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)

view this post on Zulip Reid Barton (Nov 20 2018 at 18:17):

Apparently your instances which were not the same reduce to something like the following

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 20 2018 at 18:19):

both of these constructions being nontrivial

view this post on Zulip Reid Barton (Nov 20 2018 at 18:20):

so that they don't just cancel out

view this post on Zulip Reid Barton (Nov 20 2018 at 18:21):

I haven't even seen this file limits/products.lean before

view this post on Zulip Johan Commelin (Nov 20 2018 at 20:25):

Thanks for looking into this! Apparently it's trickier than I thought...

view this post on Zulip Reid Barton (Nov 20 2018 at 20:25):

There are so many instances and it's hard to tell which ones are used where.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 27 2018 at 14:23):

This is what I implemented in the adjunctions branch, I think?

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:23):

This is what will give us the pullback of (pre)sheaves.

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:24):

Aaah, did you?

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:24):

I didn't look far enough, I'm afraid.

view this post on Zulip Reid Barton (Nov 27 2018 at 14:24):

I think it is yoneda_extension (F.comp yoneda)?

view this post on Zulip Reid Barton (Nov 27 2018 at 14:24):

at least, it seems to involve many of the same ingredients :)

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:25):

In which file?

view this post on Zulip Reid Barton (Nov 27 2018 at 14:25):

another construction which I am not very happy about, though...

view this post on Zulip Reid Barton (Nov 27 2018 at 14:25):

presheaf.lean

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:27):

Aaah, I see. Seems pretty non-trivial...

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:27):

Also, why do you work with instead of . Isn't that just as "bad"?

view this post on Zulip Reid Barton (Nov 27 2018 at 14:27):

Yeah, I did it in a round-about way, in retrospect

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 27 2018 at 14:28):

though I added a couple more lemmas for iso in the limits PR

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:53):

I see. That's what I've been trying to do. But I also got stuck.

view this post on Zulip 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...

view this post on Zulip Reid Barton (Nov 27 2018 at 14:56):

it's true

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 27 2018 at 15:07):

and that's where my current version of presheaf.lean sort of fell apart

view this post on Zulip Reid Barton (Nov 27 2018 at 15:08):

https://github.com/leanprover-community/mathlib/blob/adjunctions/category_theory/presheaf.lean#L310

view this post on Zulip Johan Commelin (Nov 27 2018 at 15:25):

@Reid Barton Does this mean that you think we should avoid adjunction.left_adjoint_of_equiv?

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Nov 29 2018 at 05:49):

I see. (I've stopped using rw, because erw has more powerful magic (-;)

view this post on Zulip Johan Commelin (Nov 29 2018 at 05:49):

Is dsimp faster than erw?

view this post on Zulip Scott Morrison (Nov 29 2018 at 05:49):

Yes.

view this post on Zulip Scott Morrison (Nov 29 2018 at 05:50):

And erw can be slower than rw, in places where either work. (I think?)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 29 2018 at 05:56):

@Scott Morrison Do you think we could have a [derive rfl-lemmas]?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 29 2018 at 10:24):

You know how to use rewrite_search, don't you? :-)

view this post on Zulip 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

view this post on Zulip Keeley Hoek (Nov 29 2018 at 10:41):

It only worked for structures though

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Nov 29 2018 at 12:23):

Thanks for the explanation!

view this post on Zulip Scott Morrison (Nov 29 2018 at 12:34):

I've actually never used it inside mathlib, I'm very curious if it works.

view this post on Zulip Keeley Hoek (Nov 29 2018 at 12:34):

ooh
Maybe it won't then

view this post on Zulip Keeley Hoek (Nov 29 2018 at 12:35):

something about "ambiguous import xxxx"

view this post on Zulip Johan Commelin (Nov 29 2018 at 12:59):

How far are we from a merge request of a (preliminary) version of rewrite_search?

view this post on Zulip 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:

view this post on Zulip Keeley Hoek (Nov 29 2018 at 13:14):

:D

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Dec 28 2018 at 06:14):

Are you going to need to prove the resulting construction is independent of the choice?

view this post on Zulip Reid Barton (Dec 28 2018 at 06:15):

The simple answer is to use choice again, in the form of classical.choice

view this post on Zulip Reid Barton (Dec 28 2018 at 06:16):

maybe the choose tactic could do this when the final Prop is a nonempty

view this post on Zulip Reid Barton (Dec 28 2018 at 06:16):

or you could use that \exists blah, blah, blah, true encoding

view this post on Zulip Johan Commelin (Dec 28 2018 at 06:18):

So nonempty blah is not Lean-equivalent to the \exists blah, blah, blah, true encoding?

view this post on Zulip Johan Commelin (Dec 28 2018 at 06:19):

The choose tactic doesn't help... :sad:

view this post on Zulip Reid Barton (Dec 28 2018 at 06:19):

it's not definitionally equivalent, much as p /\ true isn't definitionally equivalent to p

view this post on Zulip Johan Commelin (Dec 28 2018 at 06:21):

nonempty_of_exists is not an iff...

view this post on Zulip Reid Barton (Dec 28 2018 at 06:22):

You can just use choice f

view this post on Zulip Johan Commelin (Dec 28 2018 at 06:23):

Ok, I'll try that. Too bad that choose f does not work.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 := _ }

view this post on Zulip Kenny Lau (Dec 28 2018 at 08:25):

because choose is skolemization?

view this post on Zulip Johan Commelin (Dec 28 2018 at 08:32):

I don't know what that means.

view this post on Zulip 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 }

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 FF on a basis we can define the stalk FxF_x at a point xx via a direct limit construction, and then we define a presheaf F+F^+ on the space by saying that its values on an open UU are a subtype of a big Pi type sending xUx\in U to an element of the stalk FxF_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 FF is a sheaf on a basis then this extension is a sheaf. This gets really hairy. Say I have a bunch of local sections sis_i on opens UiU_i, which agree on overlaps. I want to glue them together to get a section SS of F+F^+. Well, a section of F+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 SS we want to say S(x)=si(x)S(x)=s_i(x) where we choose some ii such that xUix\in U_i. As mathematicians we know that S(x)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 SS restricted to sis_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 UU, 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+F^+ is a presheaf coming from a presheaf-on-a-basis then for xUXx\in U\subseteq X and sF+(X)s\in F^+(X) a function, the fact that (resUs)(x)=s(x)(res_U s)(x)=s(x) seemed to be true by definition, but Lean would not definitionally unfold the restriction map from F+(X)F^+(X) to F+(U)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 FF a presheaf on a basis, and an open set $$U$ (not necc in the basis), define the space of functions sending an element xx of UU to an element of the stalk FxF_x, and have some coercion from F+(U)F^+(U) to this space of functions.
3) Crucially, prove (by rfl) that the restriction map on F+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 SF+(U)S\in F^+(U) and VUV\subseteq U and xVx\in V then S(x)=res(S)(x)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 sis_i which agree on overlaps, there's a non-computable function on UU which agrees with each sis_i, but to define it at xx you have to choose
ii with xUix\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.

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 18:45):

How do you extend the presheaf on a basis in your generality?

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 18:45):

Is it still a stalk-valued function?

view this post on Zulip Johan Commelin (Jan 29 2019 at 18:47):

You can take a limit over all basic opens contained in U.

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 18:47):

Does that work for sites?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 18:49):

But your limit is different. You're taking a subset of a product perhaps.

view this post on Zulip 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(Ui)F(U_i) where the UiU_i range over the basis elements that are part of a cover. Then prove that if VV is a subset of UU then the restriction map is something like "restrict to the UiU_i which map to VV". Or something.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 20:13):

https://github.com/ramonfmir/lean-scheme

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 20:13):

We've only just started really, but we're moving along nicely.

view this post on Zulip Kenny Lau (Jun 23 2019 at 09:44):

do we have sheaves on sites yet? how far are we away from it?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 23 2019 at 23:32):

@Johan Commelin Am I duplicating effort?

view this post on Zulip 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 (-;

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

Regarding is_univalent --- usually this is called skeletal.

view this post on Zulip Kenny Lau (Jun 24 2019 at 08:09):

@Johan Commelin didn't I formalize sites in terms of coverages?

view this post on Zulip Johan Commelin (Jun 24 2019 at 08:25):

You use pullbacks

view this post on Zulip Johan Commelin (Jun 24 2019 at 08:25):

Coverages allow you to define sites on categories that don't have pullbacks

view this post on Zulip Johan Commelin (Jun 24 2019 at 08:25):

E.g. lattices without infs

view this post on Zulip Johan Commelin (Jun 24 2019 at 08:25):

E.g. bases of topologies

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 08:26):

D(f)D(g)=D(fg)D(f)\cap D(g)=D(fg).

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 08:27):

Without that, the construction of the sheaf of rings on Spec(A)\mathrm{Spec}(A) would have been harder.

view this post on Zulip Kenny Lau (Jun 24 2019 at 08:29):

I just followed Stacks project

view this post on Zulip Johan Commelin (Jun 24 2019 at 08:31):

https://ncatlab.org/nlab/show/coverage

view this post on Zulip Kenny Lau (Jun 24 2019 at 08:31):

so I should use that definition instead?

view this post on Zulip Kenny Lau (Jun 24 2019 at 08:34):

also where did the first two axioms go?

view this post on Zulip Johan Commelin (Jun 24 2019 at 08:59):

@Kenny Lau You don't need the first two axioms.

view this post on Zulip Kenny Lau (Jun 24 2019 at 08:59):

then why did Stacks include them?

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:00):

See also https://ncatlab.org/nlab/show/Grothendieck+topology#Saturation

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:01):

SGA 4 you mean? Or not

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:01):

Fixed :smiley:

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:02):

how about no

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:02):

SGA4 is not hard to read

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:02):

It's much easier than EGA4

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:03):

is there an English translation?

view this post on Zulip 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}.

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:04):

so espace etale = spac tal?

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:05):

change e-acute to s

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:05):

that sometimes work.

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:05):

fenetre -> fenester

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:05):

surely fenetre -> fnstr

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:05):

Oh it's e-hat goes to s

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:05):

Come on Kenny, your French is better than mine... and I can read that...

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:06):

You're missing off the accents. They're not all e's.

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:09):

how did Grothendieck call Grothendieck topos/topology/etc?

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:12):

Probably just topos / topology on a category.

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:12):

et d'ailleurs, quelles pages dois-je lire?

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 09:12):

The definitions are probably only a few pages in.

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:15):

il ne definit faisceaux que dans page 223

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:18):

ok tous ce que j'ai besoin de est dans expose II

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:24):

seems complicated

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:26):

Right... another option is to forget about sites for the moment.

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:26):

And focus on sheaves on distrib_inf_lattices or whatever the variant you need.

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:27):

can't I just use some variants of my current definition

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:27):

Sure, you can

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:28):

Yup, if you want to do that using the general framework

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:28):

how do I do that if I have coverages?

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:28):

We could of course do a hands-on extension

view this post on Zulip 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 sitebasissite_{basis} comes with a geometric morphism (aka morphism of sites/topoi) to sitetopologysite_{topology}.

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:29):

You pushforward along this morphism.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:30):

That's a theorem. I'm not saying it's easy.

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:30):

(It's math easy, of course)

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:31):

how do you do it in maths?

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:32):

"Proof. Follows from the sheaf property. QED" (I guess this is what most people would do...)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:33):

I don't know if we want to care about sheaves on bases...

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:40):

Well, you will still need to use the sheaf property for coverages

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:41):

But anyway... do you have a good reason to pursue this?

view this post on Zulip Johan Commelin (Jun 24 2019 at 09:41):

Or should we first try to do the push-pull adjunction for sheaves on topological spaces?

view this post on Zulip Kenny Lau (Jun 24 2019 at 09:44):

I don't know

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 24 2019 at 10:07):

@Johan Commelin how does this look?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 24 2019 at 10:19):

I'm just using https://ncatlab.org/nlab/show/coverage#Definition

view this post on Zulip Kenny Lau (Jun 24 2019 at 10:19):

I believe it's like how you can generate an equivalence relation given just any relation

view this post on Zulip Kenny Lau (Jun 24 2019 at 10:20):

and it's also to allow for a basis to be a site

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 24 2019 at 10:37):

looks like it's working

view this post on Zulip Johan Commelin (Jun 24 2019 at 10:57):

@Kenny Lau Cool!

view this post on Zulip Johan Commelin (Jun 24 2019 at 11:17):

So now you can probably also write down the sheaf axiom(s) in this language.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 24 2019 at 11:19):

Galois connections are adjunctions one level down, yes.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 24 2019 at 11:20):

Is it a Galois insertion I'm talking about then?

view this post on Zulip Johan Commelin (Jun 24 2019 at 11:20):

A Galois insertion is like an adjunction where the left(?) adjoint is fully faithful.

view this post on Zulip Johan Commelin (Jun 24 2019 at 11:21):

Ad coverage and axioms, see https://ncatlab.org/nlab/show/coverage#saturation_conditions

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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