## Stream: condensed mathematics

### Topic: finite jointly surjective map

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

#### Kenny Lau (Dec 09 2020 at 09:13):

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

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

#### Kenny Lau (Dec 09 2020 at 09:15):

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

I see

#### Bhavik Mehta (Dec 09 2020 at 09:19):

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

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

#### Johan Commelin (Dec 10 2020 at 06:01):

https://discord.gg/cQdcRm8g

#### Bassem Safieldeen (Dec 10 2020 at 06:03):

Johan Commelin said:

https://discord.gg/cQdcRm8g

I'm in, thanks!

#### Kevin Buzzard (Dec 10 2020 at 09:34):

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

#### Kevin Buzzard (Dec 10 2020 at 10:30):

that invite expires in 7 hours by the way

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

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

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?