Zulip Chat Archive

Stream: triage

Topic: issue #408: transporting definitions and theorems along i...


view this post on Zulip Random Issue Bot (Nov 16 2020 at 14:19):

Today I chose issue 408 for discussion!

transporting definitions and theorems along isomorphisms.
Created by @Kevin Buzzard (@kbuzzard) on 2018-10-08
Labels: feature-request, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 14:48):

I think it is still relevant. I want to be able to prove that if a mathematical statement is true for one specific localisation of R at S then it's true for all of them. There no recent updates and nobody is making progress because Mario has suggested that the issue is too broad/ill-specified, and right now when I run into these issues I tend to deal with them by hand.

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 14:49):

I guess the issue is that I don't say what a "mathematical statement" is here. I could instead give ten examples.

view this post on Zulip Reid Barton (Nov 16 2020 at 14:54):

This issue was also discussed earlier at https://leanprover.zulipchat.com/#narrow/stream/263328-triage/topic/random.20issue.3A.20transporting.20definitions.20and.20theorems.20along.2E.2E.2E/near/215193597

view this post on Zulip Rob Lewis (Nov 16 2020 at 14:59):

(Random Issue Bot knows not to repeat itself now, that was from before the format change.)

view this post on Zulip Simon Hudon (Nov 16 2020 at 15:51):

@Rob Lewis what happens when all the issues have been posted?

view this post on Zulip Rob Lewis (Nov 16 2020 at 15:58):

I think it avoids reposting any issue where the corresponding Zulip thread has had activity in the past month, or something like that

view this post on Zulip Rob Lewis (Nov 16 2020 at 15:59):

If there are none the script presumably crashes

view this post on Zulip Rob Lewis (Nov 16 2020 at 15:59):

https://github.com/leanprover-community/azure-scripts/blob/master/post_issue_on_zulip.py

view this post on Zulip Eric Wieser (Nov 16 2020 at 16:04):

Yep, that'll give IndexError: Cannot choose from an empty sequence

view this post on Zulip Eric Wieser (Nov 16 2020 at 16:04):

Clearly random.choice should just return 37 rather than being partial...

view this post on Zulip Adam Topaz (Nov 16 2020 at 16:30):

Kevin Buzzard said:

I guess the issue is that I don't say what a "mathematical statement" is here. I could instead give ten examples.

Isn't this a nontrivial question? It seems that "mathematical statement" is "dependent prop which only depends on the R-algebra structure" and I have no idea how to say this precisely. Unfortunately, I can't write "I know it when I see it" in lean :(

view this post on Zulip Reid Barton (Nov 16 2020 at 16:33):

It comes down to something like "definable without using choice or equality between types"--but the second condition is kind of subtle because the statement is likely to involve equality between elements of a ring (say), yet there's nothing preventing you from writing ring Type

view this post on Zulip Adam Topaz (Nov 16 2020 at 16:35):

Yeah, exactly, it depends on the signature right?

view this post on Zulip Adam Topaz (Nov 16 2020 at 16:35):

For example if I name a few elements in the localization, things will break (unless the isomorphism is compatible with those elements)

view this post on Zulip Reid Barton (Nov 16 2020 at 16:37):

right, there might be multiple isomorphisms and/or compatibility conditions involved

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 17:51):

I think the plan was to have a recursively defined transportable tag for, say, data and predicates on rings, meaning "transportable along ring isomorphisms"

view this post on Zulip Adam Topaz (Nov 16 2020 at 18:58):

Would there be a different transportableflag for each algebraic structure?

view this post on Zulip Adam Topaz (Nov 16 2020 at 18:58):

E.g. ring_transportable monoid_transportable, etc.?

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 19:03):

I...guess?

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 19:03):

Scott is the person to talk to about this, I think he actually started throwing something together when I was whingeing about this years ago.

view this post on Zulip Adam Topaz (Nov 16 2020 at 19:03):

I'm asking mostly because of all those discussions about universal algebra -- this would complicate things!

view this post on Zulip Reid Barton (Nov 16 2020 at 19:11):

Ideally you might have something like transportable P where P : \Pi (R : Type*) [ring R], Prop and then it would tell you that if you plug in two rings and a ring isomorphism, you get an iff

view this post on Zulip Adam Topaz (Nov 16 2020 at 19:13):

Right! Or even P : \Pi (R : Type*) [ring R], Sort* so that you can transport data too :)

view this post on Zulip Reid Barton (Nov 16 2020 at 19:17):

I posted this in the last thread as well but my attempt at this is at https://github.com/rwbarton/scone/blob/master/src/scone/t2.lean

view this post on Zulip Reid Barton (Nov 16 2020 at 19:17):

where the "transportable" hypothesis is the guy hF on line 42

view this post on Zulip Reid Barton (Nov 16 2020 at 19:22):

obviously it's not fit for consumption yet, but the idea is to have a tactic automatically produce the proof of transportability by induction on the term

view this post on Zulip Reid Barton (Nov 16 2020 at 19:23):

and then the other question is how to make it as usable as if it was rw... I know how to steal the type theory bits but I don't know if there is any system that really makes working with these transport operations pleasant, that's another matter.

view this post on Zulip Adam Topaz (Nov 16 2020 at 19:28):

Sounds like this is converging towards univalence...

view this post on Zulip Adam Topaz (Nov 16 2020 at 19:31):

By the way, the syntax highlighting seems to be broken here:
https://github.com/rwbarton/scone/blob/master/src/scone/edge.lean

view this post on Zulip Reid Barton (Nov 16 2020 at 19:32):

Sort of, but univalence is an internal axiom... this is more like translating theorems about metatheoretic properties into Lean tactics

view this post on Zulip Reid Barton (Nov 16 2020 at 19:33):

It's definitely related though

view this post on Zulip Reid Barton (Nov 16 2020 at 19:33):

and yeah, the syntax highlighting is a vscode-lean/markdown issue

view this post on Zulip Eric Wieser (Nov 16 2020 at 22:31):

(GitHub uses the vs-code lean plugin's syntax definition)

view this post on Zulip Random Issue Bot (Apr 10 2021 at 14:22):

Today I chose issue 408 for discussion!

transporting definitions and theorems along isomorphisms.
Created by @Kevin Buzzard (@kbuzzard) on 2018-10-08
Labels: feature-request, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 16:01):

Nothing to add since the last discussion. Right now the issue is simply that this is a very broad problem and we haven't ever managed to converge on anything reasonable enough to be a useful target; in practice if someone wants to know that if X is profinite and homeomorphic to Y then Y is profinite then they just prove it themselves (as I believe Adam did the other day).

view this post on Zulip Scott Morrison (Apr 11 2021 at 03:08):

I should have written up roadmap for my plans for equiv_rw before I ran out of energy for tactic writing... :-) I was part way to automating transporting compactness across a homeomorphism.


Last updated: May 09 2021 at 15:11 UTC