Locally convex spaces

Stream: maths

[Moritz]

Hi, I looked a bit at the seminorm stuff and it seems to me that there should be all the ingredients needed to define lcs and prove that the geometric definition is equivalent to the analytic (seminorms) one. Is there anyone actively working on this or are there any known issues with implementing this?

[Yaël Dillies]

This is on my todo list. @Bhavik Mehta and I defined the Minkowski functional recently, I'm currently defining several kinds of convexity (star, strict), I'll be refactoring affine spaces over December, and at some point between all this I was planning to do locally convex spaces.

[Yaël Dillies]

But you're welcome to try it if you want. There's no obstruction in view.

[Moritz]

I would like to implement the seminorms -> locally convex space direction, this should be quite easy (mathematically its trivial), but I have to find my way around the topology part of mathlib, so it might take me some time.

[Yaël Dillies]

Okay! I will let you do it then. Please tell me which branch you're working on and feel free to ask for help.

[Moritz]

Should I create a new structure for spaces with a family of seminorms? It looks a bit weird, because I have only one field seminorms : ι → seminorm 𝕜 E.

[Moritz]

I haven't pushed my branch to github yet, because it is extremely messy and probably nothing in it is of any use (except for me learning lean)

[Yaël Dillies]

This is a bad definition because several indexed families can correspond to the same space.

[Yaël Dillies]

This characterization as a family of seminorms should rather be a constructor + eventually a definition (a destructor)

[Moritz]

I know the choice of seminorms is not unique, the issue I have is that I have no idea for what I have to write the instance of has_continuous_add. I have

def seminorm_subbasis (P : ι → seminorm 𝕜 E) : set (set E)
  := Union $ λ x, Union $ λ i, Union $ λ r, set_of (λ y, y = ball (P i) x r)

def seminorm_topology (P : ι → seminorm 𝕜 E) : topological_space E
  := topological_space.generate_from (seminorm_subbasis P)

and I wanted to write something like

instance : has_continuous_add (seminorm_topology P) := sorry

but that does not work.

[Adam Topaz]

What's the error?

[Moritz]

type mismatch at application
  has_continuous_add (seminorm_topology P)
term
  seminorm_topology P
has type
  topological_space E : Type u_2
but is expected to have type
  Type ? : Type (?+1)

and something about failing to synthesizing topological_space ?m_1

[Adam Topaz]

Right, so that's telling you that has_cpntinuous_add is expecting a type, which probably needs to have a topological space and has_add instance, and instead you have it a term of type topological_space E

[Moritz]

So should I do this?

instance : topological_space (E) := seminorm_topology P
instance : has_continuous_add (E) := sorry

This type-checks, but I am not sure whether it is the right thing

[Adam Topaz]

I think you probably would need an alias for E which has P as a variable. Otherwise typeclass search wouldn't be able to know about P just from E

[Adam Topaz]

Also I would recommend using the Inf of topological spaces in your def

[Adam Topaz]

Let me sketch some code for you...

[Adam Topaz]

import analysis.seminorm

variables {k E : Type*} [normed_field k] [add_comm_group E] [module k E]

def seminorm.topological_space (e : seminorm k E) : topological_space E := sorry

@[derive [add_comm_group]]
def name_me {ι} (P : ι → seminorm k E) : Type* := E

instance {ι} (P : ι → seminorm k E) : module k (name_me P) := by { delta name_me, apply_instance }

instance {ι} {P : ι → seminorm k E} : topological_space (name_me P) :=
⨅ i, (P i).topological_space

instance {ι} {P : ι → seminorm k E} : has_continuous_add (name_me P) := sorry

[Adam Topaz]

We may even have seminorm.topological_space in mathlib, I'm not sure.

[Reid Barton]

It might be confusing that the thing mathlib calls a topological_space is actually a topology (and likewise what it calls a group is actually a group structure, etc.)

[Adam Topaz]

(I am assuming that the infimum of the topologies is what you intend in your definition, but I'm not completely sure.)

[Adam Topaz]

Actually, I think it should be okay, given what you wrote for seminorm_subbasis above.

[Yaël Dillies]

I think locally_convex_space should carry a topology and a proof it agrees with the seminorms-induced one, simiar to how metric_space works.

[Adam Topaz]

Yeah, that's probably the best approach

[Yury G. Kudryashov]

I think that locally_convex_space E should be either a Prop-valued mixin nhds_basis_convex : ∀ (x : E), (𝓝 x).has_basis (λ s, s ∈ 𝓝 x ∧ convex ℝ s), or extend topological_space E, module ℝ E, topological_group E, has_continuous_smul ℝ E, and add nhds_basis_convex to the list of axioms.

[Yury G. Kudryashov]

There should be a type tag as proposed by @Adam Topaz above for a space with topology generated by a family of seminorms.

[Yury G. Kudryashov]

But the main definition should be "geometric" and should not carry additional data.

[Moritz]

Is there a way to do Adam's approach, but using the seminormed spaces from analysis/normed_space in a way that we get the tvs structure for free? It seems to me that all the abstract topological stuff is already in there.

[Yury G. Kudryashov]

Currently we have 2 unrelated formalizations of a seminorm: docs#semi_normed_space and docs#seminorm.

[Yury G. Kudryashov]

The former version assumes that the topological space structure is exactly the one generated by the seminorm.

[Yury G. Kudryashov]

There is docs#semi_normed_group.of_core that constructs a semi_normed_group from semi_normed_group.core.

[Yury G. Kudryashov]

Given a family of seminorms, you can define a toplogical_space structure for each seminorm using something like by letI := seminormed_group.of_core S.to_core; apply_instance, where seminorm.to_core converts a seminorm to a semi_normed_group.core.

[Yury G. Kudryashov]

This way you get seminorm.topological_space in Adam's code above.

[Yury G. Kudryashov]

I think that we should have 2 type tags:

def seminorm.domain {X : Type*} (s : seminorm 𝕜 X) := X

instance (s : seminorm 𝕜 X) : semi_normed_group s.domain :=
semi_normed_group.of_core s.to_core

protected def seminorm.uniform_space (s : seminorm 𝕜 X) :
  uniform_space X :=
(by apply_instance : uniform_space s.domain)

instance (s : seminorm 𝕜 X) : semi_normed_space 𝕜 s.domain :=
sorry

[Yury G. Kudryashov]

Then we should have another type tag for a group with a family of seminorms.

[Yury G. Kudryashov]

def with_seminorms (s : ι → seminorm 𝕜 X) := X

instance (s : ι → seminorm 𝕜 X) : uniform_space (with_seminorms s) :=
⨅ i, (s i).uniform_space

[Yury G. Kudryashov]

Due to docs#uniform_space.to_topological_space_infi, you'll get (with_seminorms.uniform_space s).to_topological_space = ⨅ i, (s i).uniform_space.to_topological_space.

[Yaël Dillies]

with_seminorms s, you mean?

[Moritz]

I have lots of other (math) stuff to do, so I cannot do any lean until christmas. so if anyone wants to do what Yury has written, feel free.

[Yaël Dillies]

I'll tell you if ever I take over

[Moritz]

(deleted, I am too stupid to tell {} from () )

[Moritz]

Does this look sensible? https://github.com/leanprover-community/mathlib/blob/mcdoll/lcspaces/src/analysis/locally_convex.lean

[Moritz]

oh I don't need the instance for module

[Heather Macbeth]

You can also cut the add_comm_group instance by using derive:

@[derive add_comm_group] def seminorm.domain (s : seminorm 𝕜 E) := E

[Heather Macbeth]

In fact, you can equip it with the module instance at the same time:

@[derive [add_comm_group, module 𝕜]] def seminorm.domain (s : seminorm 𝕜 E) := E

and then when the time comes to put the seminormed space instance on, you don't need to mention the module structure at all:

instance (s : seminorm 𝕜 E) : semi_normed_space 𝕜 s.domain :=
{ norm_smul_le := s.smul_le }

[Moritz]

Yury G. Kudryashov said:

Due to docs#uniform_space.to_topological_space_infi, you'll get (with_seminorms.uniform_space s).to_topological_space = ⨅ i, (s i).uniform_space.to_topological_space.

The link is dead and I could not find the correct lemma.

[Moritz]

ah it is this https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/basic.html#to_topological_space_infi

[Yury G. Kudryashov]

We should move this lemma to the uniform_space namespace.

[Moritz]

I made a little bit of progress: I got everything from the discussion above to work, but now I am failing at showing that addition is continuous. I guess that I am not supposed to prove this by hand, but use some very general statement using the infinimum of the topologies. The only helpful thing I found was the stuff in topology.algebra.filter_basis, but I guess this would create a second topology which is not defeq to the one we already have.

[Moritz]

I managed to define the topological group structure for with_seminorms s: https://github.com/leanprover-community/mathlib/blob/mcdoll/lcspaces/src/analysis/locally_convex.lean maybe someone can take a look and tell me whether this is reasonable.

[Yaël Dillies]

@Moritz Doll, do have a look at #7288 so that we don't duplicate work.