Formalasing Alaoglu-Bourbaki theorem

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I'm planning on formalasing Alaoglu-Bourbaki theorem.

As part of the proof I need to prove that for balanced sets the polar of a set with respect to the dual pair math \langle E, E^* \rangle is equal to the polar of the same set but with respect to the dual pair math \langle E, E' \rangle (where math E' is the algebraic dual and math E^* is the topological one).

To do that I've defined

def TVS.polar {E: Type*} (𝕂 : Type*) [RCLike 𝕂]  [AddCommMonoid E] [Module 𝕂 E] [TopologicalSpace E] (A : Set E) : Set (WeakDual 𝕂 E)
 := LinearMap.polar ((topDualPairing 𝕂 E).flip) A

def alg.polar {E: Type*} (𝕂 : Type*) [RCLike 𝕂]  [AddCommMonoid E] [Module 𝕂 E] (A : Set E) : Set (E →ₗ[𝕂] 𝕂) :=
  LinearMap.polar (algDualPairing 𝕂 E) A

I'll I need something like

lemma lemma1 {E 𝕂: Type*} [RCLike 𝕂]  [AddCommMonoid E] [Module 𝕂 E] [TopologicalSpace E] (A : Set E) (h: Balanced 𝕂 A) :
  TVS.polar 𝕂 A = alg.polar 𝕂 A

But, this is obviously wrong as the sets don't have the same type, one is a set in WeakDual 𝕂 E and the other one is a set in E →ₗ[𝕂] 𝕂. How can I relate both?

On the same line, I also need to show that the weak-star topology induced by the algebraic dual pair restricted to the topological dual is equal to the weak-star topology induced by the topological dual pair.

Something like the following (but including the corresponding restriction of the first topology):

theorem lemma2 {𝕂 E: Type*} [RCLike 𝕂] [AddCommMonoid E] [Module 𝕂 E] [TopologicalSpace E]:
 WeakBilin.instTopologicalSpace ((algDualPairing 𝕂 E).flip) = @WeakDual.instTopologicalSpace 𝕂 E _ _ _ _ _ _ _

Is there a simple way of relating these concepts? Or should I try to reformulate the proof to avoid them?

[Esteban Martínez Vañó]

I think I've solved how to state what I want.

In the first case, I've restated the lemma as:

lemma lemma1 {E 𝕂: Type*} [RCLike 𝕂]  [AddCommMonoid E] [Module 𝕂 E] [TopologicalSpace E] (A : Set E) (h: Balanced 𝕂 A) :
  alg.polar 𝕂 A = {f | ∃ g ∈ TVS.polar 𝕂 A, f.toFun = g.toFun}

And, for the second question, I've restated it in terms of the existence of a homeomorphism, which will be enough and I think it is easier to state.

[Etienne Marion]

Is it the same as docs#WeakDual.isCompact_polar? If so you can look it up to see how it is done.

[Esteban Martínez Vañó]

Ups. It's exactly that theorem. I don't know how I overlooked it. Thanks