# Zulip Chat Archive

## Stream: maths

### Topic: equivs of mathematical objects

#### Kevin Buzzard (Apr 03 2019 at 19:01):

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 (Apr 03 2019 at 19:27):

_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 (Apr 03 2019 at 19:28):

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 (Apr 03 2019 at 19:29):

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 (Apr 03 2019 at 19:29):

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

#### Kevin Buzzard (Apr 03 2019 at 19:40):

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 (Apr 03 2019 at 19:46):

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 (Apr 03 2019 at 19:51):

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 (Apr 03 2019 at 19:52):

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 (Apr 03 2019 at 19:52):

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 (Apr 03 2019 at 19:52):

Reid, we don't write `u`

, we write `Type*`

everywhere

#### Reid Barton (Apr 03 2019 at 19:55):

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 (Apr 03 2019 at 20:53):

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 (Apr 03 2019 at 20:57):

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

#### Kevin Buzzard (Apr 03 2019 at 20:57):

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

#### Kevin Buzzard (Apr 03 2019 at 21:04):

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 (Apr 03 2019 at 21:05):

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 (Apr 03 2019 at 21:07):

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 (Apr 03 2019 at 21:20):

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 (Apr 04 2019 at 06:27):

I think we can retry the categorical approach.

#### Johan Commelin (Apr 04 2019 at 06:28):

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 (Apr 04 2019 at 06:28):

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 (Apr 04 2019 at 06:31):

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

#### Scott Morrison (Apr 04 2019 at 06:32):

Maybe some explanation of the obstacle?

#### Johan Commelin (Apr 04 2019 at 06:33):

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

#### Mario Carneiro (Apr 04 2019 at 07:48):

@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 (Apr 04 2019 at 07:49):

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

#### Kevin Buzzard (Apr 04 2019 at 07:50):

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

#### Mario Carneiro (Apr 04 2019 at 07:50):

The notation can be whatever

#### Mario Carneiro (Apr 04 2019 at 07:50):

or none at all

#### Mario Carneiro (Apr 04 2019 at 07:51):

if it gets obnoxious then just forget about notation

#### Kevin Buzzard (Apr 04 2019 at 07:51):

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

#### Kevin Buzzard (Apr 04 2019 at 07:51):

The top space homeo is \equiv\_t

#### Kevin Buzzard (Apr 04 2019 at 07:51):

the ring one is \equiv\_r

#### Mario Carneiro (Apr 04 2019 at 07:51):

those seem reasonable

#### Kevin Buzzard (Apr 04 2019 at 07:51):

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

#### Kevin Buzzard (Apr 04 2019 at 07:52):

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

#### Mario Carneiro (Apr 04 2019 at 07:52):

you can use multiple letters or symbols?

#### Kevin Buzzard (Apr 04 2019 at 07:52):

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

#### Mario Carneiro (Apr 04 2019 at 07:52):

with conventions like `r = +*`

#### Kevin Buzzard (Apr 04 2019 at 07:53):

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

#### Kevin Buzzard (Apr 04 2019 at 07:53):

mathematicians can infer the structure

#### Mario Carneiro (Apr 04 2019 at 07:54):

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

#### Kevin Buzzard (Apr 04 2019 at 07:54):

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

#### Mario Carneiro (Apr 04 2019 at 07:54):

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 (Apr 04 2019 at 07:55):

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

#### Kevin Buzzard (Apr 04 2019 at 07:55):

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

#### Kevin Buzzard (Apr 04 2019 at 07:55):

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

#### Kevin Buzzard (Apr 04 2019 at 07:55):

:P

#### Mario Carneiro (Apr 04 2019 at 07:56):

It's actually a problem of specification

#### Kevin Buzzard (Apr 04 2019 at 07:56):

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

#### Mario Carneiro (Apr 04 2019 at 07:56):

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 (Apr 04 2019 at 07:56):

that's the bit we're good at doing

#### Kevin Buzzard (Apr 04 2019 at 07:57):

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

#### Mario Carneiro (Apr 04 2019 at 07:57):

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

#### Kevin Buzzard (Apr 04 2019 at 07:57):

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

#### Kevin Buzzard (Apr 04 2019 at 07:57):

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

#### Kevin Buzzard (Apr 04 2019 at 07:58):

if more structure appears on A and B

#### Kevin Buzzard (Apr 04 2019 at 07:58):

we play fast and loose

#### Mario Carneiro (Apr 04 2019 at 07:58):

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

#### Mario Carneiro (Apr 04 2019 at 07:59):

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

#### Kevin Buzzard (Apr 04 2019 at 07:59):

Sebastian should get a notification every time someone mentions the parser

#### Kevin Buzzard (Apr 04 2019 at 07:59):

Are you interested in an equiv PR?

#### Kevin Buzzard (Apr 04 2019 at 08:00):

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

#### Mario Carneiro (Apr 04 2019 at 08:00):

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 (Apr 04 2019 at 08:00):

(My train's just got to Cambridge)

Last updated: May 14 2021 at 20:13 UTC