Stream: triage

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

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?

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.

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.

Rob Lewis (Nov 16 2020 at 14:59):

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

Simon Hudon (Nov 16 2020 at 15:51):

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

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

Rob Lewis (Nov 16 2020 at 15:59):

If there are none the script presumably crashes

Rob Lewis (Nov 16 2020 at 15:59):

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

Eric Wieser (Nov 16 2020 at 16:04):

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

Eric Wieser (Nov 16 2020 at 16:04):

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

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 :(

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

Adam Topaz (Nov 16 2020 at 16:35):

Yeah, exactly, it depends on the signature right?

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)

Reid Barton (Nov 16 2020 at 16:37):

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

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"

Adam Topaz (Nov 16 2020 at 18:58):

Would there be a different transportableflag for each algebraic structure?

Adam Topaz (Nov 16 2020 at 18:58):

E.g. ring_transportable monoid_transportable, etc.?

I...guess?

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.

Adam Topaz (Nov 16 2020 at 19:03):

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

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

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 :)

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

Reid Barton (Nov 16 2020 at 19:17):

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

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

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.

Adam Topaz (Nov 16 2020 at 19:28):

Sounds like this is converging towards univalence...

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

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

Reid Barton (Nov 16 2020 at 19:33):

It's definitely related though

Reid Barton (Nov 16 2020 at 19:33):

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

Eric Wieser (Nov 16 2020 at 22:31):

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

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?

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).

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