Zulip Chat Archive

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

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

Reid Barton (Dec 10 2020 at 13:44):

I think again an inductive proposition will be more convenient

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

Bhavik Mehta (Dec 10 2020 at 13:47):

I'll try that next, thanks

Reid Barton (Dec 10 2020 at 13:47):

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

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

Bhavik Mehta (Dec 10 2020 at 13:53):

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

Reid Barton (Dec 10 2020 at 13:54):

Right

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

Bhavik Mehta (Dec 10 2020 at 13:55):

Perhaps the fintype way would be cleaner for transitivity

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

Reid Barton (Dec 10 2020 at 13:57):

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

Reid Barton (Dec 10 2020 at 13:58):

You do care about the sizes of the individual covering families

Reid Barton (Dec 10 2020 at 13:58):

but that doesn't change between fin and fintype

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

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?

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

Adam Topaz (Dec 10 2020 at 14:51):

Or on Kleisli ultrafilter

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?

Kevin Buzzard (Dec 13 2020 at 20:39):

Are you a maths undergrad?

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: Dec 20 2023 at 11:08 UTC