function extension

Stream: maths

[Patrick Massot]

Currently we have a hack at https://github.com/leanprover-community/mathlib/blob/master/src/topology/maps.lean#L178-L180 ensuring that we could potentially extend by contuity some functions with values in a space which is not regular. Is there any use to this? The trade-off is we need to assume the dense embedding of the original space into the space we want to extend to is injective. I don't know any case where we want to target to be non-regular whereas there is a clear use case for dropping the injectivity assumption: the completion of uniform spaces.

[Patrick Massot]

Looking at the history of this "feature", I see @Johannes Hölzl made me change that last summer, so it's probably safe to assume nothing will be impacted.

[Johannes Hölzl]

Which properties can you show if the dense embedding is not injective? How do you state universality (is this the right term?). Otherwise, I'm fine with changing it as long as the extensions like the Bochner integral works.

[Patrick Massot]

Johannes, I think I can prove almost everything without injectivity. I don't understand what universality you don't see how to state. I'm not worried about Bochner integration, I don't see any non-separated spaces could show up there

[Patrick Massot]

What would be a good name for a function from a topological space to another one with the property that it pulls back the target topology to the source topology? This is half of what we ask of a topological embedding. The other half is injectivity which is actually completely irrelevant in almost every lemma we prove about topological embedding. So I think we should really have a name for the crucial part.

[Patrick Massot]

Another issue with the definition I linked to is it is stated as an and instead of a structure with two fields. And then we have https://github.com/leanprover-community/mathlib/blob/master/src/topology/maps.lean#L81-L82 which first complains it doesn't use the previous definition, and then is defined as a structure with three fields. @Mario Carneiro, @Johannes Hölzl, @Reid Barton, @Sebastien Gouezel how would you feel if we had a web of structures extending each other here? The bases would be structures with only one axiom, either the induced topology axiom or a density axiom, then structures combining them, with variants adding an injectivity assumption or not. And then variations with uniform structures. Note that I don't suggest making any of these classes, only structures in Prop. One thing that I like with this approach is that proofs can use fields names instead of anonymous and constructors, and using the various parts also goes through meaningful names like hf.inj instead of hf.1. The down-side is you get a bunch of hf.to_something.some_property, unless we restated some_property for every extending structure. Or should we use flat (aka "old") structures?

[Mario Carneiro]

Actually lean does some magic so that hf.some_property means hf.to_something.some_property

[Patrick Massot]

Sorry I was unclear. I'm not only talking about some_property being a field of a parent structure, but also a lemma in the namespace of a parent structure

[Patrick Massot]

I think the magic doesn't go that far

[Patrick Massot]

and probably using old_structure would solve that

[Mario Carneiro]

I don't think it would. You still have to insert a parent coercion before using it in a lemma

[Patrick Massot]

So what do you think about my global question?

[Mario Carneiro]

I'm fine with changing this to a structure

[Patrick Massot]

New or old?

[Mario Carneiro]

It doesn't really matter since it's a proof

[Patrick Massot]

Could you quickly recap when it does matter? I'm very fuzzy about this distinction

[Mario Carneiro]

When the structure is a proposition, all parent coercions and projections are just theorems, so it doesn't really matter how things get packed as long as the statements are the same. The only thing that is affected is the time it takes to compile the structure definition itself

[Mario Carneiro]

When the structure is data, structure instances will need to be unfolded to get at the projections. This is especially true for classes, which do this implicitly all over the place

[Mario Carneiro]

If those structure instances are huge then there is a performance penalty as a result

[Patrick Massot]

Thanks

[Patrick Massot]

I'm done with this refactor. Monster refactor PR at https://github.com/leanprover-community/mathlib/pull/1193 @Sebastien Gouezel @Reid Barton @Johannes Hölzl It would be really really nice to review this as soon as possible, since it will conflict any present or future topology PR as long as it isn't merged. I'm sorry about the size of the PR, but dense embeddings and their useless injectivity assumptions were everywhere, and I needed to go all the way to removing the separation assumption in ring completion to prove my point.

[Johan Commelin]

Congrats!

[Patrick Massot]

GitHub is doing something weird here. Travis is happy but GitHub doesn't notice