Zulip Chat Archive

Stream: new members

Topic: Vector space over continuous real functions


view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 04 2020 at 14:59):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 04 2020 at 15:00):

You can also use library_search of course

view this post on Zulip Johan Commelin (Jul 04 2020 at 15:00):

This would need bundled ctu functions, right?

view this post on Zulip Johan Commelin (Jul 04 2020 at 15:00):

I thought we didn't have those yet.

view this post on Zulip Patrick Massot (Jul 04 2020 at 15:01):

No, look at the link I posted

view this post on Zulip Heather Macbeth (Jul 04 2020 at 15:23):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jul 05 2020 at 04:30):

We have bundled continuous functions in topology/compact_open.

view this post on Zulip Yury G. Kudryashov (Jul 05 2020 at 04:31):

Probably they should be redefined using structure.

view this post on Zulip Yury G. Kudryashov (Jul 05 2020 at 04:32):

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

view this post on Zulip 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,

@[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

view this post on Zulip Reid Barton (Jul 10 2020 at 17:31):

You're missing a hypothesis on M

view this post on Zulip Reid Barton (Jul 10 2020 at 17:32):

it needs to be a topological_module or whatever

view this post on Zulip Reid Barton (Jul 10 2020 at 17:32):

at the very least a topological_add_group

view this post on Zulip Nicolò Cavalleri (Jul 11 2020 at 11:11):

Right I forgot

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 } :=
{ add_smul := sorry,
  zero_smul := sorry,
  ..continuous_add_comm_group, }

view this post on Zulip Reid Barton (Jul 11 2020 at 11:56):

This has_coe business is wishful thinking

view this post on Zulip Reid Barton (Jul 11 2020 at 11:57):

It's also not true

view this post on Zulip Reid Barton (Jul 11 2020 at 11:57):

You need both hypotheses.

view this post on Zulip 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?

view this post on Zulip 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 } :=
{ add_smul := sorry,
  zero_smul := sorry,
  ..continuous_add_comm_group, }

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Nicolò Cavalleri (Jul 11 2020 at 13:04):

In any case why does there not exist is_submodule?

view this post on Zulip Reid Barton (Jul 11 2020 at 13:10):

Are we talking about

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

?

view this post on Zulip Nicolò Cavalleri (Jul 11 2020 at 13:10):

Reid Barton said:

Are we talking about

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

?

Yes

view this post on Zulip Reid Barton (Jul 11 2020 at 13:11):

Well, look at the types and the definitions involved.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 11 2020 at 13:17):

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

view this post on Zulip Reid Barton (Jul 11 2020 at 13:18):

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

view this post on Zulip Reid Barton (Jul 11 2020 at 13:18):

You know about jump to definition, right?

view this post on Zulip Reid Barton (Jul 11 2020 at 13:19):

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

view this post on Zulip Reid Barton (Jul 11 2020 at 13:20):

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

view this post on Zulip Nicolò Cavalleri (Jul 11 2020 at 13:20):

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!

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 13:43):

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

view this post on Zulip Nicolò Cavalleri (Jul 11 2020 at 13:45):

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

view this post on Zulip 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.

view this post on Zulip Nicolò Cavalleri (Jul 11 2020 at 14:14):

Why is this better then is_subgroup?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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