equivs of mathematical objects

Stream: maths

[Kevin Buzzard]

So part of the raison d'etre of the perfectoid project is to define a very complex mathematical object to see how Lean will handle it. Lean is handling it very well, but here is something which has come out in the wash.

Mathematicians are very good at treating "canonically isomorphic" (whatever that means) objects as equal. This unlocks all the things we can do with equality, for example reflexivity, symmetry and transitivity, plus the ability to rewrite. In Lean we don't have that luxury, and every time I find objects in the background of the theory of perfectoid spaces which mathematicians are treating in this way I've been making an extension of equiv. So far we have mul_equiv (the bijection respects * on objects in the has_mul class) with notation ≃*, add_equiv with notation ≃+ (these are in mathlib), and then group_equiv and monoid_equiv (which are literally defined to be mul_equiv!). Mathlib also has ring_equiv ≃ᵣ and homeomorph ≃ₜ. In the perfectoid repo we needed equivs of totally ordered monoids so I introduced le_equiv ≃≤ and its extension ≃≤* (or ≃*≤, I can't even remember what I called it).

Today I realised that I needed equivs of topological spaces equipped with a presheaf of types, topological spaces equipped with a presheaf of rings, and topological spaces equipped with a presheaf of topological rings.

My notation does not scale.

Does anyone have any suggestions? Or am I really going to go with presheaf_of_topological_rings_equiv? This is not some artificial problem. A perfectoid space is a topological space with a sheaf of topological rings and some extra structure too, which is locally equiv to a structure coming from a perfectoid ring. The notion of isomorphism of complex objects is central to the definition.

[Scott Morrison]

_If_ you're willing to work with bundled objects, you know that merely defining a category instance gives you \iso as "one equiv to rule them all"?

[Scott Morrison]

One can easily prove in Type that "equiv is equiv to iso" and in Ring that "≃ᵣ is equiv to iso", and so on.

[Scott Morrison]

It would also have the benefit of making transport easier to do, because it won't need struts for every different type of equiv someone dreams up.

[Scott Morrison]

(The short answer: this is what category theory was invented for.)

[Kevin Buzzard]

Did you say "if I am willing to go through the pain of constantly having to specify my universes everywhere then category theory solves this"? Or is this viewpoint too pessimistic? We are about to make design decisions about this so we could even try both.

[Kevin Buzzard]

Of course I could go rogue and just stick to Type! I think one model of ZFC is plenty for most mathematicians. I've never seen a perfectoid space which doesn't live in Type.

[Reid Barton]

You shouldn't need to specify your universes much more than usual. You'd write for example (G : Group.{u}) rather than (g : Type u) [group g]--either way you have a u.

[Patrick Massot]

Scott, I would love to be able to use category theory in this project. I don't quite understand why, but there seems to be a deep reason why it never works out. For instance, Johan spent months trying to do sheaves using the category theory part of mathlib, and gave up.

[Reid Barton]

You can also just use Type which is actually what I did in homotopy theory, since I didn't want to bother transporting the reals into every universe.

[Patrick Massot]

Reid, we don't write u, we write Type* everywhere

[Reid Barton]

You could also use local notation to hide the universe variables of categories you use a lot, this is another thing I did in the homotopy theory library (local notation Top := Top.{0}, I think you should be able to put a universe variable there as well).

[Scott Morrison]

I'm pretty dubious about this "deep reason". I never got to the end of reading Johan's work on sheaves, but there is a lot of good stuff there. He told me he couldn't prove f_* and f^*were adjoints, and then stopped. I would love to see all the earlier parts, of which there is a lot, PR'd, so others (including me) can start to process it, and we'll see what's involved in the adjunction problem.

[Kevin Buzzard]

It's time we got to the bottom of this really.

[Kevin Buzzard]

I am tempted to try all approaches and see which one works best.

[Kevin Buzzard]

I know that at the minute he is very busy with the perfectoid project. The PRs that were holding things up got merged today and now he has a bunch of stuff to do which he knows exactly how to do.

[Kevin Buzzard]

I think I really will try all three approaches. I have an auxiliary category in mind which we need and it won't be much extra work to try with it bundled and unbundled

[Scott Morrison]

Okay --- please please try the bundled approach, and ping me whenever I can help. :-) Life is going to be so much better in the long run if we can make this work.

[Kevin Buzzard]

I remember before Reid saying that for a scheme, the underlying topological space is a thing, but in stark contrast to groups and rings etc, it's not that important a thing; somehow the important thing is the sheaf. I interpreted this as an argument for bundling schemes. The same logic applies, perhaps even more so, for adic spaces. Take a look at example 2.20 in Scholze's original paper (page 11 of the pdf). This is a picture of the closed unit disc over an algebraically closed field. In Tate's model of a rigid space this would literally be the points in the algebraically closed field of norm at most one. In the adic space approach the topological space is vastly more complex -- and this is only in dimension 1.

[Johan Commelin]

I think we can retry the categorical approach.

[Johan Commelin]

Morphisms of LRS should be doable, but of course they are a bit fake if we don't have the adjuction between $f^*$ and $f_*$.

[Johan Commelin]

The reason they are doable, is that we can define the morphisms in terms of $f_*$, and it isn't hard to define $f_*$.

[Scott Morrison]

Johan, sometime could you point me to where you try and fail to setup that adjunction?

[Scott Morrison]

Maybe some explanation of the obstacle?

[Johan Commelin]

Sure... I'll first finish a nasty proof in the perfectoid project though (-;

[Mario Carneiro]

@Kevin Buzzard Why don't you think the proliferating equivs are not sustainable? You are basically noticing that there are lots of categories in the world

[Mario Carneiro]

and using real categories isn't going to make anything easier - you still need one category for each algebraic structure or combination

[Kevin Buzzard]

It was the notation which I was concerned about. That was what prompted the thread.

[Mario Carneiro]

The notation can be whatever

[Mario Carneiro]

or none at all

[Mario Carneiro]

if it gets obnoxious then just forget about notation

[Kevin Buzzard]

Maybe then I'm wondering if there could be some standard convention

[Kevin Buzzard]

The top space homeo is \equiv\_t

[Kevin Buzzard]

the ring one is \equiv\_r

[Mario Carneiro]

those seem reasonable

[Kevin Buzzard]

but this doesn't scale because there are more than 26 things

[Kevin Buzzard]

and I'm not even convinced we have all 26 small letter subscripts anyway

[Mario Carneiro]

you can use multiple letters or symbols?

[Kevin Buzzard]

OK I think you're saying this is not something to worry about

[Mario Carneiro]

with conventions like r = +*

[Kevin Buzzard]

As Scott points out, in maths we use the same notation for every single one of these

[Kevin Buzzard]

mathematicians can infer the structure

[Mario Carneiro]

hm, we can't quite do that in lean because these are applied to types, rather than bundled things

[Kevin Buzzard]

I am going to dip my toe into the category theory world and see what happens.

[Mario Carneiro]

you can always make a local notation but that's no good if you have two or three of them in one statement

[Kevin Buzzard]

In practice $\cong$ in maths means "isomorphism of all the structure"

[Kevin Buzzard]

and $=$ means "canonical isomorphism of all the structure"

[Kevin Buzzard]

we have such a great system, you should fix up your computer languages so they worked better.

[Kevin Buzzard]

:P

[Mario Carneiro]

It's actually a problem of specification

[Kevin Buzzard]

I know it's a problem at our end really, I have only come to understand this through learning formalisation.

[Mario Carneiro]

If I want to write A ~= B where A and B are types, then somehow I have to figure out "all the structure" on the types

[Kevin Buzzard]

that's the bit we're good at doing

[Kevin Buzzard]

99% of the time it's the maximal structure such that the notion is sensible

[Mario Carneiro]

which means if "structure" is provided by typeclasses on A then more typeclasses changes the meaning of A ~= B

[Kevin Buzzard]

and when it's not we say "...(considered as abelian groups only)"

[Kevin Buzzard]

I think the definition of $A\cong B$ can change within a talk

[Kevin Buzzard]

if more structure appears on A and B

[Kevin Buzzard]

we play fast and loose

[Mario Carneiro]

I can conceive of a tactic that does this, with a tad of parser support

[Mario Carneiro]

but you still need to have a whole slew of ready made equivs to select from

[Kevin Buzzard]

Sebastian should get a notification every time someone mentions the parser

[Kevin Buzzard]

Are you interested in an equiv PR?

[Kevin Buzzard]

I'd like to finish perfectoids first but I have a bunch of them piled up in for_mathlib

[Mario Carneiro]

sure... I am aware that mathlib has many more algebraic classes than it has equivs, but in principle it should be about 1-1

[Kevin Buzzard]

(My train's just got to Cambridge)