## Stream: maths

### Topic: function extension

#### Patrick Massot (Jul 01 2019 at 12:57):

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 (Jul 01 2019 at 15:17):

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 (Jul 01 2019 at 20:00):

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 (Jul 02 2019 at 13:19):

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 (Jul 03 2019 at 11:36):

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 (Jul 03 2019 at 11:45):

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 (Jul 03 2019 at 12:03):

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

#### Patrick Massot (Jul 03 2019 at 12:04):

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 (Jul 03 2019 at 12:05):

I think the magic doesn't go that far

#### Patrick Massot (Jul 03 2019 at 12:05):

and probably using old_structure would solve that

#### Mario Carneiro (Jul 03 2019 at 12:07):

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

#### Patrick Massot (Jul 03 2019 at 12:08):

So what do you think about my global question?

#### Mario Carneiro (Jul 03 2019 at 12:09):

I'm fine with changing this to a structure

New or old?

#### Mario Carneiro (Jul 03 2019 at 12:10):

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

#### Mario Carneiro (Jul 03 2019 at 12:30):

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 (Jul 03 2019 at 12:31):

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 (Jul 03 2019 at 12:32):

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

Thanks

#### Patrick Massot (Jul 08 2019 at 13:49):

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.

Congrats!

#### Patrick Massot (Jul 08 2019 at 16:04):

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

Last updated: May 10 2021 at 07:15 UTC