Zulip Chat Archive

Stream: maths

Topic: transport forever


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 10 2018 at 18:58):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:07):

yes

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:08):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:09):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:09):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:11):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:11):

what?

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:12):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:12):

I wrote very precisely what immediate application I have

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:12):

In this thread, right before Johan's message

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:13):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:13):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:15):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:16):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:16):

any uniform space structure on any type

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:17):

so where are the rings coming from

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:20):

Left hand side has the ring

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:20):

Because separation_quotient α is separated

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:21):

This is the content of the second sentence

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:24):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:24):

A posteriori yes

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:25):

completion α is separated, but α isn't

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:25):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:28):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:31):

does injectivity get used somewhere?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:32):

So I didn't think hard about it

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:32):

but again a posteriori it seems like it is actually injective

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:32):

or else you wouldn't have that equiv

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:32):

No

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:32):

it's not injective

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:33):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:33):

separation_quotient α -> completion (separation_quotient α) is injective

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:33):

ah, ok

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:33):

because separation_quotient α is separated

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:34):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:35):

Probably

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:35):

maybe not actually

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:35):

sorry

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:36):

You can define mul

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:36):

the issue is continuity

view this post on Zulip Mario Carneiro (Oct 10 2018 at 19:38):

I'm checking this branch out, 1 sec

view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:40):

In need to transport something along this equiv though

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 10 2018 at 19:45):

maths on a computer are so complicated...

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:15):

Oh, this is evil: https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L263-L273

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:15):

I'm starting to see why you get heq goals

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:16):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:16):

I already confessed

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:18):

And I blame Danish thefts

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:18):

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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Oct 10 2018 at 20:19):

What's evil about it?

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:19):

constructive is evil

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:19):

Type equality is evil

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:20):

Actually I tried to redeem with the next lemma

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:20):

eq_mpr_heq?

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:20):

or previous lemma

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:20):

the instance?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:22):

I mean https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/completion.lean#L255-L261

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:22):

right

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:44):

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

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:45):

indeed it's been refactored again

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:45):

(module refactor touched this too)

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:45):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 20:50):

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

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 20:50):

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

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:50):

Yes, this is exactly what I was thinking

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 20:50):

I'm not that busy in January...

view this post on Zulip Patrick Massot (Oct 10 2018 at 20:51):

Yeah, too bad we have orthogonal teaching schedules this year

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rudi Grinberg (Oct 20 2018 at 00:18):

Where is this thread? The search is failing me.

view this post on Zulip Bryan Gin-ge Chen (Oct 20 2018 at 00:20):

It's here.

view this post on Zulip 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.

view this post on Zulip 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