## Stream: new members

### Topic: Vector space over continuous real functions

#### Nicolò Cavalleri (Jul 04 2020 at 14:56):

Is there anywhere in Mathlib the fact that continuous real functions over a topological space make up a vector space? I would not really know how to find out if something like this existed

#### Patrick Massot (Jul 04 2020 at 14:59):

but it doesn't seem to be, so the next place to look at is the analysis folder

#### Patrick Massot (Jul 04 2020 at 15:00):

You can also use library_search of course

#### Johan Commelin (Jul 04 2020 at 15:00):

This would need bundled ctu functions, right?

#### Johan Commelin (Jul 04 2020 at 15:00):

I thought we didn't have those yet.

#### Patrick Massot (Jul 04 2020 at 15:01):

No, look at the link I posted

#### Heather Macbeth (Jul 04 2020 at 15:23):

There is topology/bounded_continuous_function, but it has the extra assumption of boundedness.

#### Nicolò Cavalleri (Jul 04 2020 at 15:46):

Heather Macbeth said:

There is topology/bounded_continuous_function, but it has the extra assumption of boundedness.

Thanks actually this is great already for my purpose

#### Nicolò Cavalleri (Jul 04 2020 at 15:47):

Patrick Massot said:

You can also use library_search of course

Yeah I could not easily think of a way to use library_search for something of this kind!

#### Patrick Massot (Jul 04 2020 at 17:02):

You can try to have variable including a bunch a type classes and type:

example : submodule R (α → M) :=
by library_search


#### Patrick Massot (Jul 04 2020 at 17:03):

It will tell you whether mathlib knows about a R-submodule of the module of functions from alpha to M

#### Scott Morrison (Jul 05 2020 at 03:59):

I think it would be good to set up bundled continuous functions, with plenty of additional structure (at least as a subalgebra). Variants like continuous functions vanishing at infinity as well?

#### Yury G. Kudryashov (Jul 05 2020 at 04:30):

We have bundled continuous functions in topology/compact_open.

#### Yury G. Kudryashov (Jul 05 2020 at 04:31):

Probably they should be redefined using structure.

#### Yury G. Kudryashov (Jul 05 2020 at 04:32):

It should be easy to define algebraic operations on these functions using continuous.mul etc.

#### Nicolò Cavalleri (Jul 10 2020 at 17:24):

I am trying to define the vector space structure on continuous functions but it does not find the commutative group instance even if I also defined that... Can someone help me to understand what is going on? Maybe something having to do with coercions?

import topology.algebra.module
import topology.algebra.continuous_functions

example {α : Type*} [comm_group α] (β : set α) [is_subgroup β] : comm_group β := by refine subtype.comm_group,

instance continuous_comm_group {α : Type*} {β : Type*} [topological_space α] [topological_space β]
[comm_group β] [topological_group β] : comm_group { f : α → β | continuous f } :=
{ mul_comm := subtype.comm_group.mul_comm,
..continuous_group, }

instance continuous_module {α : Type*} [topological_space α] (R : Type*) (M : Type*)
[ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] :
module R { f : α → M | continuous f } := sorry


#### Reid Barton (Jul 10 2020 at 17:31):

You're missing a hypothesis on M

#### Reid Barton (Jul 10 2020 at 17:32):

it needs to be a topological_module or whatever

#### Reid Barton (Jul 10 2020 at 17:32):

at the very least a topological_add_group

Right I forgot

#### Nicolò Cavalleri (Jul 11 2020 at 11:13):

In any case I guess I cannot imitate the rest of the continuous_functions file as there is not a is_submodulestructure so I guess I will have to go proving things as for continuous_bounded_functions?

#### Nicolò Cavalleri (Jul 11 2020 at 11:14):

I don't really understand the algebra section of the library: I do not understand why for some structures there is both subobject and is_subobject and for other structures there is only one of them

#### Nicolò Cavalleri (Jul 11 2020 at 11:16):

Like for group there is both, for ring there is only is_subring and for module there is only submodule

#### Nicolò Cavalleri (Jul 11 2020 at 11:55):

Reid Barton said:

it needs to be a topological_module or whatever

I cannot really manage to make it find the instance even by adding the hypothesis topological_module by the way

variables {α : Type*} [topological_space α] (R : Type*) (M : Type*)
[ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] [topological_module R M]

instance : has_coe (topological_module R M) (topological_add_group M) := sorry

instance continuous_module :
module R { f : α → M | continuous f } :=
zero_smul := sorry,


#### Reid Barton (Jul 11 2020 at 11:56):

This has_coe business is wishful thinking

#### Reid Barton (Jul 11 2020 at 11:57):

It's also not true

#### Reid Barton (Jul 11 2020 at 11:57):

You need both hypotheses.

#### Nicolò Cavalleri (Jul 11 2020 at 12:02):

Reid Barton said:

It's also not true

If I forget about multiplication with a scalar I do not get a topological commutative group?

#### Nicolò Cavalleri (Jul 11 2020 at 12:04):

Reid Barton said:

You need both hypotheses.

I did try with both hypotheses but then it does not find an instance of distrib_mul_action R ↥{f : α → M | continuous f}. Should I define it manually or am I forgetting something else?

instance continuous_module {α : Type*} [topological_space α] (R : Type*) (M : Type*)
[ring R] [topological_space R] [topological_space M] [add_comm_group M] [module R M] [topological_add_group M] [topological_module R M] :
module R { f : α → M | continuous f } :=
zero_smul := sorry,


#### Reid Barton (Jul 11 2020 at 12:05):

Nicolò Cavalleri said:

Reid Barton said:

It's also not true

If I forget about multiplication with a scalar I do not get a topological commutative group?

Look at the definitions--unless I am missing something the answer is no

#### Reid Barton (Jul 11 2020 at 12:06):

Nicolò Cavalleri said:

it does not find an instance of distrib_mul_action R ↥{f : α → M | continuous f}

This is part of what you need to define a module structure, right? (Not a rhetorical question.)

#### Nicolò Cavalleri (Jul 11 2020 at 13:03):

Reid Barton said:

Nicolò Cavalleri said:

it does not find an instance of distrib_mul_action R ↥{f : α → M | continuous f}

This is part of what you need to define a module structure, right? (Not a rhetorical question.)

It is but I could not find such instance for continuous bounded function, so since everything compiles there I was thinking Lean was able to deduce it from the fact that it is valid for  α → M... I am very confused about why things that work for continuous bounded functions do not work here

#### Nicolò Cavalleri (Jul 11 2020 at 13:04):

In any case why does there not exist is_submodule?

#### Reid Barton (Jul 11 2020 at 13:10):

instance : semimodule 𝕜 (α →ᵇ β) :=
semimodule.of_core $[...]  ? #### Nicolò Cavalleri (Jul 11 2020 at 13:10): Reid Barton said: Are we talking about instance : semimodule 𝕜 (α →ᵇ β) := semimodule.of_core$ [...]


?

Yes

#### Reid Barton (Jul 11 2020 at 13:11):

Well, look at the types and the definitions involved.

#### Reid Barton (Jul 11 2020 at 13:12):

If you have class B extends A then you can write an instance for B and supply the fields for A at the same time.

#### Reid Barton (Jul 11 2020 at 13:13):

If you don't then I guess it looks for an instance of A (I don't really know).

#### Kevin Buzzard (Jul 11 2020 at 13:14):

Nicolò Cavalleri said:

Like for group there is both, for ring there is only is_subring and for module there is only submodule

The is_ classes are deprecated.

#### Nicolò Cavalleri (Jul 11 2020 at 13:16):

Reid Barton said:

If you don't then I guess it looks for an instance of A (I don't really know).

Oh ok thanks that actually solves my confusion I was convinced that it was required as a separate instance: I did not notice module was extending that class, as usually it asks me for missing fields not missing instances

#### Nicolò Cavalleri (Jul 11 2020 at 13:17):

Nicolò Cavalleri said:

Reid Barton said:

If you don't then I guess it looks for an instance of A (I don't really know).

Oh ok thanks that actually solves my confusion I was convinced that it was required as a separate instance: I did not notice module was extending that class, as usually it asks me for missing fields not missing instances

I mean I thought that class was included as a hypothesis as otherwise it would have asked me for missing fields but it's not how these errors work apparently

#### Reid Barton (Jul 11 2020 at 13:17):

actually I don't know either and can't reproduce this

#### Reid Barton (Jul 11 2020 at 13:18):

it might depend on old versus new structure cmd too, possibly

#### Reid Barton (Jul 11 2020 at 13:19):

You can unconvince yourself of such things by looking at the definitions :upside_down:

#### Reid Barton (Jul 11 2020 at 13:20):

I'm confused by your error, but then again I haven't seen your source.

#### Nicolò Cavalleri (Jul 11 2020 at 13:20):

Reid Barton said:

Yeah sure but it did not come to my mind to check because it never occurred to me such error for missing fields, only when an instance required in the hypotheses was missing so I gave it for granted without checking!

#### Nicolò Cavalleri (Jul 11 2020 at 13:21):

Reid Barton said:

I'm confused by your error, but then again I haven't seen your source.

I can try to reproduce it if you want but adding the fields you suggested solved my problem so I am not sure you want to lose more time behind this haha

#### Nicolò Cavalleri (Jul 11 2020 at 13:24):

Kevin Buzzard said:

Nicolò Cavalleri said:

Like for group there is both, for ring there is only is_subring and for module there is only submodule

The is_ classes are deprecated.

It means is_subgroup will be removed or did just people stop using it at some point and it the structures that have it will keep having it?

#### Kevin Buzzard (Jul 11 2020 at 13:43):

It is a gigantic job to remove it, but we hope to remove it someday.

#### Nicolò Cavalleri (Jul 11 2020 at 13:45):

Is it possible to give a brief reason why it was deprecated? I'm curious

#### Alex J. Best (Jul 11 2020 at 13:51):

We've moved over to bundled subgroups instead; rather than having a group G and a set H with the predicate is_subgroup H saying that H is in fact a subgroup, we have a type subgroup G which whose terms are a carrier set H and the proofs that H is closed under addition etc. So its a different repackaging of the same information. We don't really want both concepts around so we're partway through changing everything to refer to the bundled version.

#### Nicolò Cavalleri (Jul 11 2020 at 14:14):

Why is this better then is_subgroup?

#### Kevin Buzzard (Jul 11 2020 at 14:15):

We tried both, we had to choose one, we chose subgroup. The main reason is that dot notation works well for it.

#### Kevin Buzzard (Jul 11 2020 at 14:16):

For example, if H : subgroup G then H.mul_mem is the theorem that if a, b \in H then so is ab. With is_subgroup you have to do is_subgroup.mul_mem H and you also have to hope that type class inference works.

#### Scott Morrison (Jul 12 2020 at 02:01):

Unfortunately these infrastructure changes take time, and enthusiasm, to get done. Kevin and I have been working on removing some more uses of is_subgroup at #3321 --- anyone who wants to jump in and deal with some errors on that branch would be very welcome!

#### Scott Morrison (Jul 12 2020 at 02:01):

A PR creating subring, following the model of the recent PR which created subgroup, would also be a fantastic contribution.

#### Yury G. Kudryashov (Jul 12 2020 at 02:50):

Note that we already have subsemiring. This can be used as an example of mixing * and +.

Last updated: May 18 2021 at 17:44 UTC