Why WeakDual assumes TopologicalSpace on the Module?

Stream: mathlib4

[Paradoxy]

In Mathlib.Topology.Algebra.Module.WeakDual the current definition is

variable {α 𝕜 𝕝 E F : Type*}

/-- The weak star topology is the topology coarsest topology on `E →L[𝕜] 𝕜` such that all
functionals `fun v => v x` are continuous. -/
def WeakDual (𝕜 E : Type*) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
    [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
  WeakBilin (topDualPairing 𝕜 E)
deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd, Inhabited,
  FunLike, ContinuousLinearMapClass

What I fail to understand is [TopologicalSpace E] assumption. In particular, I am finding myself in a situation where my vector space is not equipped with a topology but nevertheless I want weak topology on the algebraic duals. It is possible to use WeakBilin API and basically repeat steps taken in WeakDual without [TopologicalSpace E] assumption. But this adds a lot of redundancy. What is the correct way of handling this problem?

[Etienne Marion]

The weak-* topology is a topology over the topological dual, which only exists if E has a topology.

[Paradoxy]

Etienne Marion said:

The weak-* topology is a topology over the topological dual, which only exists if E has a topology.

Sorry, I don't follow. The topology is indeed required on the underlying Field, but not on the vector space itself. https://en.wikipedia.org/wiki/Weak_topology#Weak_topology_with_respect_to_a_pairing

[Yaël Dillies]

WeakDual is the continuous dual, not the algebraic one

[Paradoxy]

Yaël Dillies said:

WeakDual is the continuous dual, not the algebraic one

I understand. But what is the proper way of handling the issue I described in my question? Should I simply repeat the same file, without [TopologicalSpace E] assumption?

[Etienne Marion]

Probably you should use WeakBilin with Module.dualPairing.

[Etienne Marion]

What is your use case?

[Paradoxy]

Etienne Marion said:

Probably you should use WeakBilin with Module.dualPairing.

Yeah, this is what I currently have, but it doesn't look right to me to repeat the same construction all over again. Note if WeakDual was defined for algebraic duals, it would've worked for continuous duals for the most part as well, since continuous dual is a special case of algebraic dual. But the way it is defined currently make repetition necessary.

I am working on tensor product of partially vector spaces. In particular, topology is not assumed in this vector spaces to keep the choice of tensor product unique.

[Kevin Buzzard]

Continuous dual is not a special case of algebraic dual -- it's the other way around. Presumably you could just put the discrete topology on E or something?

[Paradoxy]

Kevin Buzzard said:

Continuous dual is not a special case of algebraic dual -- it's the other way around.

Sorry, I don't understand. Every Continuous dual is an algebraic dual through ContinuousLinearMap.toLinearMap but not every algebraic dual is a Continuous dual .

I am not allowed to put any topology on the vector space.

[Yaël Dillies]

Every element of the continuous dual is an element of the algebraic dual. That means that the continuous dual is a subset of the algebraic dual, not that it is equal to it. And what Kevin is saying is that the algebraic dual is equal to the continuous dual with respect to the discrete topology.

[Paradoxy]

Yaël Dillies said:

That means that the continuous dual is a subset of the algebraic dual, not that it is equal to it.

Yaël Dillies said:

Every element of the continuous dual is an element of the algebraic dual. That means that the continuous dual is a subset of the algebraic dual, not that it is equal to it. And what Kevin is saying is that the algebraic dual is equal to the continuous dual with respect to the discrete topology.

Which I presume it means in a general setting where no discrete topology is available, continuous dual is a special case of algebraic dual, or a subset as you put it. Given this fact, should I repeat the construction or should I weaken the current construction?

[Kevin Buzzard]

My instinct would just be to use WeakBilin and if there is API which is there for WeakDual but not WeakBilin then just add it to WeakBilin.

[Paradoxy]

Kevin Buzzard said:

My instinct would just be to use WeakBilin and if there is API which is there for WeakDual but not WeakBilin then just add it to WeakBilin.

It will be a part of much larger contribution to mathlib4 library itself. Is it acceptable to have these two types of WeakDuals in the library? I genuinely do not know.

[Kevin Buzzard]

Paradoxy said:

continuous dual is a special case of algebraic dual, or a subset as you put it.

This is just a grammar issue. "Construction X is a special case of construction Y" means "if you can do construction Y then you can do construction X using it because it's a special case". "Construction X is a subset of Construction Y" means something else, it means every element of construction X is an element of construction Y. All of us know what is happening mathematically so there is nothing more to say here.

I am not suggesting you make a second WeakDual, I am suggesting you use WeakBilin and do not make any new things. Mathlib maintainers love PRs which add new theorems and API for given definitions. They are far more fussy about PRs which add new definitions and are extremely fussy about PRs which change definitions.

You have never made it clear what is wrong with WeakBilin. Why is it not just the answer to your question?

[Paradoxy]

Kevin Buzzard said:

Paradoxy said:

continuous dual is a special case of algebraic dual, or a subset as you put it.

This is just a grammar issue. "Construction X is a special case of construction Y" means "if you can do construction Y then you can do construction X using it because it's a special case". "Construction X is a subset of Construction Y" means something else, it means every element of construction X is an element of construction Y. All of us know what is happening mathematically so there is nothing more to say here.

I am not suggesting you make a second WeakDual, I am suggesting you use WeakBilin and do not make any new things. Mathlib maintainers love PRs which add new theorems and API for given definitions. They are far more fussy about PRs which add new definitions and are extremely fussy about PRs which change definitions.

You have never made it clear what is wrong with WeakBilin. Why is it not just the answer to your question?

Yes, sorry I am not a native English speaker. Currently, I have

import Mathlib.LinearAlgebra.Dual.Lemmas
import Mathlib.Analysis.LocallyConvex.WeakDual

open Module Submodule WeakBilin Topology

section Dual

variable {R : Type*} [CommRing R] [TopologicalSpace R]
variable {V : Type*} [AddCommGroup V] [Module R V]

instance instAddCommGroup : AddCommGroup (Dual R V) :=
  WeakBilin.instAddCommGroup (dualPairing R V)

instance instModule : Module R (Dual R V) :=
  WeakBilin.instModule' (dualPairing R V)

instance instTopologicalSpace : TopologicalSpace (Dual R V) :=
  WeakBilin.instTopologicalSpace (dualPairing R V)

@[simp] theorem dual_coefn_continuous : Continuous fun (x : Dual R V) y => x y :=
  continuous_induced_dom

@[simp] theorem dual_eval_continuous (y : V) : Continuous fun x : Dual R V => x y :=
  continuous_pi_iff.mp dual_coefn_continuous y

variable [IsTopologicalAddGroup R] [ContinuousSMul R R]

instance instIsTopologicalAddGroup : IsTopologicalAddGroup (Dual R V) :=
  WeakBilin.instIsTopologicalAddGroup (dualPairing R V)

instance instContinuousAdd : ContinuousAdd (Dual R V) :=
  WeakBilin.instContinuousAdd (dualPairing R V)

instance instContinuousSMul : ContinuousSMul R (Dual R V) :=
  ⟨continuous_induced_rng.2 <|
    continuous_fst.smul ((WeakBilin.coeFn_continuous (dualPairing R V)).comp continuous_snd)⟩

instance instT2Space [T2Space R] : T2Space (Dual R V) :=
  (WeakBilin.isEmbedding (fun ⦃_ _⦄ a => a)).t2Space

It works just fine for the later constructions. I can either add this to WeakBilin as you suggested, or maybe keep it as a separate file. Alternatively, there is an option of weakening WeakDual assumptions, making all these lines unnecessary.

[Etienne Marion]

You shouldn't put instances on Dual R V, instead you should manipulate WeakBilin (Module.dualPairing R V) which already has the topological instance you want. And if you want an instance that is missing, then you should add it to WeakBilin.

[Kevin Buzzard]

If you get bored of typing WeakBilin (Module.dualPairing R V) then you can make an abbrev in your file.

[Paradoxy]

Etienne Marion said:

You shouldn't put instances on Dual R V, instead you should manipulate WeakBilin (Module.dualPairing R V) which already has the topological instance you want. And if you want an instance that is missing, then you should add it to WeakBilin.

How should I avoid defining instances? For example, I want to prove a particular set of dual vectors is compact in this topology. Either I have to use the instance shown above, or every time I have to manually type

@IsCompact _ (WeakBilin.instTopologicalSpace (dualPairing R V)) ...

Is there any other option?

[Etienne Marion]

You should never write Dual R V, and always write WeakBilin (Module.dualPairing R V) (or an abbrev you may have created).

[Etienne Marion]

That's the point of having a type synonym: it is the same underlying type, but the name is different so you can endow it with different instances.