Cherry picking structure on substructures

Stream: general

[Tomas Skrivan]

I'm defining what is a smooth map between locally convex spaces. The space of all smooth maps X↠Y is a linear subspace of the space of all functions X→Y and I would like to inherit all the algebraic structure but I get also get all the topology, because X→Y is pi.topological_space if Y is a topological space. I do not want this topology because X↠Y should be equipped with a different topology. This prevents me from defining X↠Y as a submodule ℝ (X→Y).

Is there an easy way to inherit all the algebraic structure? Or do I have to manually write down all the instances ofhas_zero has_add add_comm_group ... ?

[Tomas Skrivan]

I had a look at continuous_linear_map and there all the algebraic structure is spelled out again manually. Isn't there a better way?

[Reid Barton]

You don't need to write instances that will be implied by "later" ones, e.g., if you write an instance for add_comm_group, you can skip has_zero and has_add

[Reid Barton]

(though in some other situations the has_add instance might have more general hypotheses than add_comm_group in which case you would need to write it explicitly)

[Heather Macbeth]

You might like to not write this as a literal subtype of X→Y. Instead, define a new "bundled" object consisting of a map X→Y plus some hypotheses (smoothness).

[Heather Macbeth]

Then you won't have the pesky other topological space structure. (I think.). Have a look at continuous linear maps, for an idea of what I mean: docs#continuous_linear_map

[Heather Macbeth]

and one gets, eg, docs#continuous_linear_map.to_normed_space

[Tomas Skrivan]

Heather Macbeth said:

Then you won't have the pesky other topological space structure. (I think.). Have a look at continuous linear maps, for an idea of what I mean: docs#continuous_linear_map

Ok, I will probably do it similarly as continuous_linear_map.

[Heather Macbeth]

By the way, did you see that mathlib has the notion of a smooth function? docs#times_cont_diff

But this is between normed spaces, I don't know how you define smooth between locally convex spaces?

[Tomas Skrivan]

A smooth map transforms smooth curve to a smooth curve. To define smooth curve you just need topological vector space. Definition of smooth map on wiki

[Heather Macbeth]

@Tomas Skrivan you might be interested to see that @Jean Lo has just updated the old PR on local convexity to a new version #4827 that will hopefully join mathlib soon. Anyone is welcome to make comments on an open PR, and I am sure yours would be useful!