Merge profinite branch to master

Stream: condensed mathematics

[Adam Topaz]

Does anyone have any objections merging profinite_clopen to master?
https://github.com/leanprover-community/lean-liquid/compare/profinite_clopen

[Johan Commelin]

Why not? Feel free to merge it.

[Adam Topaz]

Note that for_mathlib.Fintype.basic contains

instance {A : Fintype} : topological_space A := ⊥

I assume this is okay with everyone...

[Johan Commelin]

In this project, certainly. I'm not sure if mathlib will want it as global instance.

[Adam Topaz]

Sure. But of course this doesn't imply

instance {A : Type*} [fintype A] : topological_space A := ⊥

[Adam Topaz]

For mathlib we could define a DiscreteFintype category, and put such a global instance on those things.

[Peter Scholze]

How many variants of a "fintype" are there in Lean already?

[Adam Topaz]

Only one: Fintype.

[Peter Scholze]

But there's also the fintype predicate on a Type?

[Adam Topaz]

but that's a bundled fintype, and we have a class fintype which, when used like this: variable (X) [fintype X] says that X is finite

[Adam Topaz]

yeah exactly

[Johan Commelin]

Ooh, I see what you did there (-;

[Damiano Testa]

As more of an outsider to Lean than Adam, I would have answered by saying that there is finite, finset, fintype, fin n...

[Adam Topaz]

finiteness is a HUGE mess right now IMO

[Johan Commelin]

So you want to say that bundled fintypes are always discrete. But random types that might be finite can have other topologies.

[Johan Commelin]

I guess that could work :stuck_out_tongue_wink:

[Johan Commelin]

But someone might also discover 1.4 years from now that it's really nasty to have that global instance :grimacing:

[Adam Topaz]

The practical reason for the instance is that I got really annoyed manually telling lean that it should think of a Fintype as a discrete space when I was constructing a bunch of functors to Top or Profinite

[Johan Commelin]

I would just make it a local instance.

[Adam Topaz]

For mathlib, sure, but I'm still inclined to leave it global for LTE

[Johan Commelin]

Yes, in LTE I'm sure we won't consider other topologies on finite types.

[Peter Scholze]

I'm a big fan of those, but they don't surface here

[Adam Topaz]

Yeah I was going to say that someone (Kevin?) was going to yell at me about the topology of $Spec A$ with $A$ a DVR.

[Peter Scholze]

Why only DVR's? A general $\mathrm{Spec} R$ is a cofiltered limit of finite topological spaces

[Adam Topaz]

yes of course.

[Adam Topaz]

In this case these all come from a partial order, right? And we have the category PartialOrder ;)

[Peter Scholze]

Yes

[Adam Topaz]

So my suggestion is that on terms of PartialOrder one would define the topology induced by the partial order

[Peter Scholze]

Topologies on a finite set are just partial orders on a finite set, that's right

[Peter Scholze]

Anyways, I'm off! Keep up the good work! :lift:

[Adam Topaz]

Actually now that Peter mentioned this, I think formalizing Hochster's theorem(s) could be a fun (and very doable) project.

[Kevin Buzzard]

Peter Scholze said:

But there's also the fintype predicate on a Type?

It's not a predicate! It contains data, because it was written by a constructivist. But it is a subsingleton, so if p : fintype X and q : fintype X then p = q.

[Adam Topaz]

Adam Topaz said:

finiteness is a HUGE mess right now IMO

:up:

[Kevin Buzzard]

Adam Topaz said:

Actually now that Peter mentioned this, I think formalizing Hochster's theorem(s) could be a fun (and very doable) project.

I once asked Conrad if he'd read the proof and I was stunned to hear that he hadn't! My perception is that it's used in Huber's work, in the following situation: you want to prove some theorem about spectral spaces, and sometimes you say "well, WLOG they're schemes, so we're done by some obscure lemma in EGA 2". And of course the counter argument is "it's only point set topology, how hard can it be?"

[Peter Scholze]

I don't think that's right. Well, I haven't checked the proof that all spectral spaces arise as the spectrum of a ring, but I've never seen a use of it. To me, this is mostly a coincidence that has an important historical role as it led Hochster to isolate the right class of topological spaces.

[Patrick Massot]

Writing this to you feels incredibly stupid, but I recommend you have a look at Wedhorn's lecture notes on adic spaces. In Section 3.3, every proof starting from Remark 3.21 is as Kevin described.

[Patrick Massot]

Note that I don't say they have to be like this, I only tell you one place where Kevin got that idea.

[Kevin Buzzard]

Right -- my impression is that these arguments as written rely on Hochster but this can be avoided.

[Peter Scholze]

Thanks for the pointer! When I learned this stuff, Wedhorn's notes didn't exist, so I wasn't aware... I assumed these statement were always proved by direct point-set arguments. (I saw the assertions stated without proof in Huber's book, and they all seemed to be easily provable by a direct attack.)

[Peter Scholze]

Actually, recently Akhil Mathew explained an argument about spectral spaces to me by writing it as Spec of a ring, but again I think this was only for linguistic reasons.

[Kevin Buzzard]

it's analogous to all those people in the 40s proving lemmas in homological algebra by chasing elements :-)