Zulip Chat Archive

Stream: condensed mathematics

Topic: finite jointly surjective map


view this post on Zulip Kenny Lau (Dec 09 2020 at 09:13):

What is the best way to say that a presieve consists of finitely many maps that are jointly surjective?

view this post on Zulip Kenny Lau (Dec 09 2020 at 09:13):

This is the pro-étale site of the point.

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 09:15):

Calle's definition in the Profinite2 branch appeared sensible off the top of my head, do you know how well it works?

view this post on Zulip Kenny Lau (Dec 09 2020 at 09:15):

We are working on that very branch and stuck at that very point.

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 09:16):

I see

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 09:19):

(for others coming across this, conversation moved to the discord stream)

view this post on Zulip Bassem Safieldeen (Dec 10 2020 at 05:56):

Bhavik Mehta said:

(for others coming across this, conversation moved to the discord stream)

If the discord stream is not private could you please provide a link? :)

view this post on Zulip Johan Commelin (Dec 10 2020 at 06:01):

https://discord.gg/cQdcRm8g

view this post on Zulip Bassem Safieldeen (Dec 10 2020 at 06:03):

Johan Commelin said:

https://discord.gg/cQdcRm8g

I'm in, thanks!

view this post on Zulip Kevin Buzzard (Dec 10 2020 at 09:34):

Oh it is private but we're happy to let in interested people

view this post on Zulip Kevin Buzzard (Dec 10 2020 at 10:30):

that invite expires in 7 hours by the way

view this post on Zulip Kevin Buzzard (Dec 10 2020 at 10:35):

The discord is far less serious than this place, it's mostly undergraduates, there's a bunch of other stuff going on (chess, among us, memes), for me the most interesting thing is the live streaming events -- this is the one edge it has over Zulip. A lot of the time when I'm working on Lean I just live stream (often with music on) and people watch and ask questions, and others (Bhavik, Kenny) live stream too. We made it private because we didn't want to have to police the site 24/7, but I'll happily give out invites to people who fit the bill (undergraduate mathematicians with an interest in Lean fit it 100%, and people who don't diverge too radically from that profile are often also welcome).

view this post on Zulip Bhavik Mehta (Dec 10 2020 at 13:42):

I went with

def proetale_pretopology : pretopology Profinite :=
{ coverings := λ X, {S | ( x,  Y (f : Y  X) y, S f  f y = x) 
                         set.finite {Y | nonempty {f : Y  X | S f}} 
                          Y, set.finite {f : Y  X | S f}},

as the definition of the pretopology which is the best way I could think of at the time

view this post on Zulip Reid Barton (Dec 10 2020 at 13:44):

I think again an inductive proposition will be more convenient

view this post on Zulip Reid Barton (Dec 10 2020 at 13:45):

e.g.

inductive finite_cover : pretopology Profinite
| mk (n : \N) (Y) (X : \Pi (i : fin n), Profinite) (f : \Pi (i : fin n), X i \hom Y) (hf : ...) : finite_cover Y

view this post on Zulip Bhavik Mehta (Dec 10 2020 at 13:47):

I'll try that next, thanks

view this post on Zulip Reid Barton (Dec 10 2020 at 13:47):

in general things that generate should be presented in a generating kind of way

view this post on Zulip Reid Barton (Dec 10 2020 at 13:52):

Could also use fintype but there might be some universe awkwardness--but perhaps it doesn't matter for now

view this post on Zulip Bhavik Mehta (Dec 10 2020 at 13:53):

You mean index the set by a type with a fintype instance?

view this post on Zulip Reid Barton (Dec 10 2020 at 13:54):

Right

view this post on Zulip Bhavik Mehta (Dec 10 2020 at 13:55):

I could see that working, I think both of these would work for the iso and pullback axioms

view this post on Zulip Bhavik Mehta (Dec 10 2020 at 13:55):

Perhaps the fintype way would be cleaner for transitivity

view this post on Zulip Reid Barton (Dec 10 2020 at 13:57):

I guess maybe there actually isn't ever a point where you care about the size of the collection of generating covering families

view this post on Zulip Reid Barton (Dec 10 2020 at 13:57):

except that it is bounded by the whole category, which follows from working with sieves

view this post on Zulip Reid Barton (Dec 10 2020 at 13:58):

You do care about the sizes of the individual covering families

view this post on Zulip Reid Barton (Dec 10 2020 at 13:58):

but that doesn't change between fin and fintype

view this post on Zulip Reid Barton (Dec 10 2020 at 13:58):

So maybe there's no harm to just using fintype and having a proper class of covering families

view this post on Zulip Adam Topaz (Dec 10 2020 at 14:48):

Don't you think it makes more sense to define this pretopology on CompHaus and then restrict to Profinitevia the obvious embedding?

view this post on Zulip Adam Topaz (Dec 10 2020 at 14:51):

I feel like we should define condensed sets as sheaves on one of the two extremes: either CompHaus or (the still nonexistent) ExtrDisc

view this post on Zulip Adam Topaz (Dec 10 2020 at 14:51):

Or on Kleisli ultrafilter

view this post on Zulip Ben Lee (Dec 13 2020 at 20:38):

Kevin Buzzard said:

Oh it is private but we're happy to let in interested people

Could I get a discord invite?

view this post on Zulip Kevin Buzzard (Dec 13 2020 at 20:39):

Are you a maths undergrad?

view this post on Zulip Ben Lee (Dec 13 2020 at 22:02):

i have a phd in math.....from 15 years ago. so maybe i'm at undergrad level again!


Last updated: May 09 2021 at 16:20 UTC