## Stream: maths

### Topic: transport forever

#### Patrick Massot (Oct 10 2018 at 15:10):

Today I tried to setup transport of structure along equiv, since @Mario Carneiro wanted to see (part of) what we would like to be automated. It can be seen at https://gist.github.com/PatrickMassot/9c5246efe8d1fd4f26c21cbf2ac99ff8 First I'd like to know if the beginning looks reasonnable. The answer is almost certainly not since I'm stuck when I try to go to rings at the bottom. This file is autonomous, it should fail reliably with any recentish version of mathlib.

#### Patrick Massot (Oct 10 2018 at 15:11):

Of course this is needed for the ring completions project, which is needed for the perfectoid project

#### Patrick Massot (Oct 10 2018 at 15:16):

I should say why this is only part of what Kevin always asks for. Here we start with some structure on a type and want to transport it along a given equiv, so that the equiv becomes an isomorphism in the relevant category. The next step is to assume we have an isomorphism in a category and transport various statements (like Kevin's exact sequences).

#### Patrick Massot (Oct 10 2018 at 15:24):

Let me recall the context of the ring completion project. We start with a topological ring α. We get a topological ring structure on separation_quotient α in https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L279. We get a topological ring structure on the completion of a separated topological ring at https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L1205 (oops, this is only a comm_ring instance, but the topological axioms should be easy). And we have https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L747 : completion (separation_quotient α) ≃ completion α along which we want to transport the topological ring structure.

#### Johan Commelin (Oct 10 2018 at 17:34):

Nice start @Patrick Massot! It's also a bit sad that it is breaking down for rings.

#### Patrick Massot (Oct 10 2018 at 18:58):

Don't loose hope Johan, Mario will save us.

#### Mario Carneiro (Oct 10 2018 at 19:07):

As you point out, there are two slightly different senses of "transport of structure" being used here. One, which seemed to be Kevin's main point, is a theorem such as "if R ~= S are isomorphic rings and R is artinian then S is artinian", and this has a possibility of being addressed by transfer. The other has the form "Given an equiv A ~= B of sets, and a ring structure on A, there is an induced ring structure on B" which is what you seem to be demonstrating in the gist.

yes

#### Patrick Massot (Oct 10 2018 at 19:08):

In my use case I first want to transport the structure over an equiv and then transport properties

#### Mario Carneiro (Oct 10 2018 at 19:08):

One reason I wouldn't want to just jump in with that kind of tactic is that most of those theorems generalize to a weaker structure than equiv

#### Patrick Massot (Oct 10 2018 at 19:08):

And my equiv is actually a uniform space equiv so completeness would be transported for instance

#### Mario Carneiro (Oct 10 2018 at 19:09):

For example you might just have an injection into a subring of a ring

#### Mario Carneiro (Oct 10 2018 at 19:09):

or it might not even be an injection but there is a coherence property

#### Patrick Massot (Oct 10 2018 at 19:09):

Maybe it's too early for a tactic here. As you wrote, we first need to see a couple of handcrafted examples in order to understand what we want

#### Patrick Massot (Oct 10 2018 at 19:10):

Do you think the ring thing can be done with that starting point? I'm not sure whether I should try to have local instances, or maybe use haveI in the constructions...

#### Mario Carneiro (Oct 10 2018 at 19:11):

I also have no applications of your kind of transport of structure

what?

#### Mario Carneiro (Oct 10 2018 at 19:12):

the "A is a ring so B is a ring" kind

#### Patrick Massot (Oct 10 2018 at 19:12):

I wrote very precisely what immediate application I have

#### Patrick Massot (Oct 10 2018 at 19:12):

In this thread, right before Johan's message

#### Mario Carneiro (Oct 10 2018 at 19:13):

the problem is that just transporting the whole structure won't work

#### Mario Carneiro (Oct 10 2018 at 19:13):

you will end up with yet another copy of the uniform structure

#### Patrick Massot (Oct 10 2018 at 19:14):

A uniform structure and a compatible ring structure, and a universal property, that's exactly what I want

#### Mario Carneiro (Oct 10 2018 at 19:15):

So what is the setting exactly for this theorem? completion (separation_quotient α) ≃ completion α

#### Patrick Massot (Oct 10 2018 at 19:16):

https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L747

#### Patrick Massot (Oct 10 2018 at 19:16):

any uniform space structure on any type

#### Mario Carneiro (Oct 10 2018 at 19:17):

so where are the rings coming from

#### Patrick Massot (Oct 10 2018 at 19:18):

I don't know what to write that is not copy-pasting my message before Johan's message

#### Johan Commelin (Oct 10 2018 at 19:19):

Let me recall the context of the ring completion project. We start with a topological ring α. We get a topological ring structure on separation_quotient α in https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L279. We get a topological ring structure on the completion of a separated topological ring at https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L1205 (oops, this is only a comm_ring instance, but the topological axioms should be easy). And we have https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L747 : completion (separation_quotient α) ≃ completion α along which we want to transport the topological ring structure.

Voila. I did it.

#### Mario Carneiro (Oct 10 2018 at 19:20):

explain the last sentence. Which side has the ring, and why doesn't the other side have one?

#### Patrick Massot (Oct 10 2018 at 19:20):

Left hand side has the ring

#### Patrick Massot (Oct 10 2018 at 19:20):

Because separation_quotient α is separated

#### Patrick Massot (Oct 10 2018 at 19:21):

This is the content of the second sentence

#### Mario Carneiro (Oct 10 2018 at 19:24):

I don't get it. Is this completion (separation_quotient α) ≃ completion α in fact (in math) a uniform ring isomorphism?

#### Mario Carneiro (Oct 10 2018 at 19:24):

If so, why isn't completion α already separated?

A posteriori yes

#### Patrick Massot (Oct 10 2018 at 19:25):

completion α is separated, but α isn't

#### Mario Carneiro (Oct 10 2018 at 19:25):

what goes wrong in the ring (completion α) instance if you drop the separated α property?

#### Patrick Massot (Oct 10 2018 at 19:28):

The map coe : α -> completion α is no longer injective

#### Mario Carneiro (Oct 10 2018 at 19:31):

does injectivity get used somewhere?

#### Patrick Massot (Oct 10 2018 at 19:31):

It is currently used in the proof everywhere, but maybe there is another proof. Johannes wrote that proof.

#### Patrick Massot (Oct 10 2018 at 19:32):

So I didn't think hard about it

#### Mario Carneiro (Oct 10 2018 at 19:32):

but again a posteriori it seems like it is actually injective

#### Mario Carneiro (Oct 10 2018 at 19:32):

or else you wouldn't have that equiv

No

#### Patrick Massot (Oct 10 2018 at 19:32):

it's not injective

#### Patrick Massot (Oct 10 2018 at 19:33):

coe : α -> completion α is injective if and only if α is separated

#### Patrick Massot (Oct 10 2018 at 19:33):

separation_quotient α -> completion (separation_quotient α) is injective

ah, ok

#### Patrick Massot (Oct 10 2018 at 19:33):

because separation_quotient α is separated

#### Mario Carneiro (Oct 10 2018 at 19:34):

Do the definitions of has_one and has_mul at least work without separated?

Probably

#### Patrick Massot (Oct 10 2018 at 19:35):

maybe not actually

sorry

#### Patrick Massot (Oct 10 2018 at 19:36):

You can define mul

#### Patrick Massot (Oct 10 2018 at 19:36):

the issue is continuity

#### Mario Carneiro (Oct 10 2018 at 19:38):

I'm checking this branch out, 1 sec

#### Mario Carneiro (Oct 10 2018 at 19:39):

anyway, my intuition is that you don't want to use transfer of structure like this. You should already be able to define the structure a priori, and you want to show that the equivalence respects the structure that is already there

#### Patrick Massot (Oct 10 2018 at 19:40):

In need to transport something along this equiv though

#### Mario Carneiro (Oct 10 2018 at 19:41):

In particular, if we did transfer of structure your way, we would end up with two ring structures on completion (separation_quotient A)

#### Patrick Massot (Oct 10 2018 at 19:41):

I'm ready to trow away any ring structure which is not compatible with the uniform structure

#### Mario Carneiro (Oct 10 2018 at 19:42):

I would guess the two ring structures are equal, but as we know that's not good enough for lean

#### Patrick Massot (Oct 10 2018 at 19:45):

maths on a computer are so complicated...

#### Mario Carneiro (Oct 10 2018 at 20:15):

I'm starting to see why you get heq goals

#### Patrick Massot (Oct 10 2018 at 20:16):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/heq.20hell.20again/near/135479776

#### Patrick Massot (Oct 10 2018 at 20:18):

And I blame Danish thefts

#### Mario Carneiro (Oct 10 2018 at 20:18):

I think we need to be less constructive with our quotient constructions

#### Mario Carneiro (Oct 10 2018 at 20:19):

the quotient ring construction for example should apply to any quotient map, not just the canonical one

#### Patrick Massot (Oct 10 2018 at 20:19):

constructive is evil

#### Mario Carneiro (Oct 10 2018 at 20:19):

Type equality is evil

#### Patrick Massot (Oct 10 2018 at 20:20):

Actually I tried to redeem with the next lemma

#### Mario Carneiro (Oct 10 2018 at 20:20):

eq_mpr_heq?

#### Patrick Massot (Oct 10 2018 at 20:20):

or previous lemma

the instance?

#### Patrick Massot (Oct 10 2018 at 20:21):

I have one lemma saying the quotients are equal but the other one says the setoids are equal

#### Chris Hughes (Oct 10 2018 at 20:21):

the quotient ring construction for example should apply to any quotient map, not just the canonical one

Do you mean so it would be easy to prove things about quotient rings that aren't constructed using quotient, like zmod, or complex using theorems about quotient rings?

right

#### Mario Carneiro (Oct 10 2018 at 20:23):

as long as it acts like a quotient you should have quotient ring construction, quotient topology, etc

#### Patrick Massot (Oct 10 2018 at 20:43):

as long as it acts like a quotient you should have quotient ring construction, quotient topology, etc

Is this something I'm meant to understand and convert into action, or was this you thinking aloud?

#### Mario Carneiro (Oct 10 2018 at 20:43):

I don't really expect you to do anything on that front, it's mostly the fault of quotient_ring and such

#### Mario Carneiro (Oct 10 2018 at 20:44):

in the short term you might try to avoid casting between types but still unfold the fact that it is a quotient

#### Patrick Massot (Oct 10 2018 at 20:44):

This quotient ring stuff seems tricky to get right. I was already refactored once

#### Mario Carneiro (Oct 10 2018 at 20:45):

indeed it's been refactored again

#### Mario Carneiro (Oct 10 2018 at 20:45):

(module refactor touched this too)

#### Patrick Massot (Oct 10 2018 at 20:45):

I hope this completion stuff will help you get the refactor right

#### Patrick Massot (Oct 10 2018 at 20:49):

@Kevin Buzzard this conversation suggests that the perfectoid project is waiting for module refactor also on the ring completion side

#### Patrick Massot (Oct 10 2018 at 20:49):

unless we find a way to finish that ring completion thing using evil lemmas and fake transport of structure

#### Kevin Buzzard (Oct 10 2018 at 20:49):

One thing that really spurs me on with this whole thing is that as we try to do a different kind of mathematics to the kind that is typically done in a theorem prover, we run into issues which computer scientists seem to be able to solve. I am constantly feeling like both sides somehow benefit.

#### Kevin Buzzard (Oct 10 2018 at 20:50):

I did this once (cutting corners) with schemes, and now look at that project.

#### Kevin Buzzard (Oct 10 2018 at 20:50):

I say we do it right this time, however long it takes.

#### Patrick Massot (Oct 10 2018 at 20:50):

Yes, this is exactly what I was thinking

#### Kevin Buzzard (Oct 10 2018 at 20:50):

I'm not that busy in January...

#### Patrick Massot (Oct 10 2018 at 20:51):

Yeah, too bad we have orthogonal teaching schedules this year

#### Patrick Massot (Oct 10 2018 at 20:53):

Mario, could we still have congr' trying to discharge goals using proof_irrel and proof_irrel_heq in order to cover my evil actions?

#### Patrick Massot (Oct 19 2018 at 20:44):

About transport of structure, Assia pointed out to me https://hal.inria.fr/hal-01559073 It seems it's actually relevant, despite the univalent stuff

#### Patrick Massot (Oct 19 2018 at 20:45):

I notice that it helps publishing CS papers to promise stuff for free. It seems most papers titles in this area contain this promise.

#### Andrew Ashworth (Oct 19 2018 at 21:04):

Everybody loves free things! This is a good paper, I linked it previously in the "hott for newbies" thread, and Mario made a few comments.

#### Rudi Grinberg (Oct 20 2018 at 00:18):

Where is this thread? The search is failing me.

It's here.

#### Bryan Gin-ge Chen (Oct 20 2018 at 00:22):

As a side note, I've found that by default, searching Zulip doesn't turn up results from before I joined the server. However, it does if I additionally include "stream:general" or "stream:maths", etc.

#### Patrick Massot (Oct 20 2018 at 09:47):

Everybody loves free things! This is a good paper, I linked it previously in the "hott for newbies" thread, and Mario made a few comments.

Thanks! I was sure it had been mentioned, I even told @Assia Mahboubi but I couldn't find it.

Last updated: May 12 2021 at 07:17 UTC