Vector space over continuous real functions

Stream: new members

[Nicolò Cavalleri]

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]

It should be in https://leanprover-community.github.io/mathlib_docs/topology/algebra/continuous_functions.html

[Patrick Massot]

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

[Patrick Massot]

You can also use library_search of course

[Johan Commelin]

This would need bundled ctu functions, right?

[Johan Commelin]

I thought we didn't have those yet.

[Patrick Massot]

No, look at the link I posted

[Heather Macbeth]

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

[Nicolò Cavalleri]

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]

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]

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

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

[Patrick Massot]

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

[Scott Morrison]

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]

We have bundled continuous functions in topology/compact_open.

[Yury G. Kudryashov]

Probably they should be redefined using structure.

[Yury G. Kudryashov]

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

[Nicolò Cavalleri]

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,

@[to_additive continuous_add_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]

You're missing a hypothesis on M

[Reid Barton]

it needs to be a topological_module or whatever

[Reid Barton]

at the very least a topological_add_group

[Nicolò Cavalleri]

Right I forgot

[Nicolò Cavalleri]

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]

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]

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

[Nicolò Cavalleri]

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 } :=
{ add_smul := sorry,
  zero_smul := sorry,
  ..continuous_add_comm_group, }

[Reid Barton]

This has_coe business is wishful thinking

[Reid Barton]

It's also not true

[Reid Barton]

You need both hypotheses.

[Nicolò Cavalleri]

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]

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 } :=
{ add_smul := sorry,
  zero_smul := sorry,
  ..continuous_add_comm_group, }

[Reid Barton]

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]

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]

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]

In any case why does there not exist is_submodule?

[Reid Barton]

Are we talking about

instance : semimodule 𝕜 (α →ᵇ β) :=
semimodule.of_core $ [...]

?

[Nicolò Cavalleri]

Reid Barton said:

Are we talking about

instance : semimodule 𝕜 (α →ᵇ β) :=
semimodule.of_core $ [...]

?

Yes

[Reid Barton]

Well, look at the types and the definitions involved.

[Reid Barton]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

You know about jump to definition, right?

[Reid Barton]

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

[Reid Barton]

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

[Nicolò Cavalleri]

Reid Barton said:

You know about jump to definition, right?

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]

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]

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]

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

[Nicolò Cavalleri]

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

[Alex J. Best]

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]

Why is this better then is_subgroup?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Yury G. Kudryashov]

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