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

Stream: triage

[Random Issue Bot]

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]

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]

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

[Reid Barton]

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

[Rob Lewis]

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

[Simon Hudon]

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

[Rob Lewis]

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]

If there are none the script presumably crashes

[Rob Lewis]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Adam Topaz]

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]

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]

Yeah, exactly, it depends on the signature right?

[Adam Topaz]

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

[Reid Barton]

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

[Kevin Buzzard]

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]

Would there be a different transportableflag for each algebraic structure?

[Adam Topaz]

E.g. ring_transportable monoid_transportable, etc.?

[Kevin Buzzard]

I...guess?

[Kevin Buzzard]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

Sounds like this is converging towards univalence...

[Adam Topaz]

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

[Reid Barton]

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

[Reid Barton]

It's definitely related though

[Reid Barton]

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

[Eric Wieser]

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

[Random Issue Bot]

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]

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]

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.

[Random Issue Bot]

Today I chose issue 408 for discussion!

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

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

[Kevin Buzzard]

We still don't seem to have a compelling use case for the tactic I proposed

[Kevin Buzzard]

Shall I make some comments and close the issue? I think that until the question becomes well-defined there's no actual issue here

[Random Issue Bot]

Today I chose issue 408 for discussion!

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

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

[Random Issue Bot]

Today I chose issue 408 for discussion!

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

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

[Random Issue Bot]

Today I chose issue 408 for discussion!

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

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