Topology on a finite dimensional vector space

Stream: Is there code for X?

[Yaël Dillies]

Say I have a real finite dimensional vector space E and Bhavik insistently wants to apply the Krein-Milman lemma (docs#IsCompact.extremePoints_nonempty) in it, how do I give any topology on E so that [TopologicalSpace E] [T2Space E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] and Bhavik leaves me alone?

[Johan Commelin]

Are those the only conditions? I think the discrete topology would work, in that case...

[Johan Commelin]

Aah wait, that isn't ContinuousSMul

[Johan Commelin]

Well, then you'll need the famous theorem that a findim vect space over a complete normed field has a unique vector space topology

[Johan Commelin]

And I think this has been discussed many times on zulip, but I'm not sure it was every formalized.

[Yaël Dillies]

Johan Commelin said:

Aah wait, that isn't ContinuousSMul

Hmm, is it not?

[Yaël Dillies]

Oh, it's only docs#ContinuousConstSMul, or something?

[Yaël Dillies]

I will try to see whether Krein-Milman can be weakened to ContinuousConstSMul...

[Yaël Dillies]

Here is my best attempt so far:

1. Notice that basically any reasonable topology will do
2. Remember from my functional analysis lectures that the weak*-topology is such a reasonable topology
3. Find docs#WeakBilin
4. Find docs#LinearMap.applyₗ
5. Write the following where needed:

let _ : TopologicalSpace E := inferInstanceAs (TopologicalSpace (WeakBilin (LinearMap.applyₗ (R := ℝ))))
let _ : TopologicalAddGroup E := inferInstanceAs (TopologicalAddGroup (WeakBilin (LinearMap.applyₗ (R := ℝ))))
let _ : ContinuousSMul ℝ E := inferInstanceAs (ContinuousSMul ℝ (WeakBilin (LinearMap.applyₗ (R := ℝ))))
let _ : LocallyConvexSpace ℝ E := inferInstanceAs (LocallyConvexSpace ℝ (WeakBilin (LinearMap.applyₗ (R := ℝ))))
let _ : T2Space E := inferInstanceAs (T2Space (WeakBilin (LinearMap.applyₗ (R := ℝ))))

6. Be sad that the last line doesn't work :sad:

[Oliver Nash]

Are you looking for docs#ContinuousLinearEquiv.ofFinrankEq ?

[Oliver Nash]

As in:

import Mathlib

variable {E : Type*} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E]
  [TopologicalSpace E] [T2Space E] [TopologicalAddGroup E] [ContinuousSMul ℝ E]

open FiniteDimensional

noncomputable example : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ :=
  ContinuousLinearEquiv.ofFinrankEq (by simp)

[Sébastien Gouëzel]

Can you take a basis, and then pull back the topology from the corresponding product space (which has the sup norm and everything)?

[Yaël Dillies]

Oliver Nash said:

Are you looking for docs#ContinuousLinearEquiv.ofFinrankEq ?

No! I don't have a topology on E yet

[Yaël Dillies]

As Sébastien says, I could use the LinearEquiv version of this and transfer the topology along, but I would like (understand: Bhavik would like) there to be no explicit identification needed. The dream would be to have a (semi)automatic procedure (a tactic?) to endow E with the right topology

[Kevin Buzzard]

You could use this (from the FLT project). I haven't PRed it yet because I wanted to check it was OK in my use case, but most of the theorems are there. The idea is that you either do let _ : TopologicalSpace E := actionTopology \R E and then have _ : IsActionTopology \R E := \<rfl\> and typeclass inference should do everything for you. Alternatively you do [TopologicalSpace E] [IsActionTopology \R E] because the predicate typeclass uniquely determines the top space.

[Yaël Dillies]

Johan Commelin said:

Are those the only conditions? I think the discrete topology would work, in that case...

Just to confirm: this approach can't work since the proof of KM requires neighborhoods of the origin being absorbent

[Bhavik Mehta]

Yes, this came up in a teaching context, and among other things I was trying to make the point that "for any finite dimensional real vector space" is a better way of phrasing a theorem than "for R^d". But then having the library only help me if I do pick a basis makes this super awkward, especially since the topology is invariant (admittedly not definitionally) under basis change. If the identification is hidden under something else, like a good API or a tactic, then I'd be happy too.

[Bhavik Mehta]

Kevin Buzzard said:

You could use this (from the FLT project). I haven't PRed it yet because I wanted to check it was OK in my use case, but most of the theorems are there. The idea is that you either do let _ : TopologicalSpace E := actionTopology \R E and then have _ : IsActionTopology \R E := \<rfl\> and typeclass inference should do everything for you. Alternatively you do [TopologicalSpace E] [IsActionTopology \R E] because the predicate typeclass uniquely determines the top space.

Unfortunately it doesn't look like it has all the typeclasses I need - ContinuousSMul and T2Space are missing

[Bhavik Mehta]

Johan Commelin said:

Are those the only conditions? I think the discrete topology would work, in that case...

This was exactly my thought too, although you were much faster at noticing ContinuousSMul breaks than I was!

[Kevin Buzzard]

ContinuousSMul should be there and T2Space will be easy to add if typeclass inference can find Module.Finite, Module.Free and T2Space R.

[Notification Bot]

3 messages were moved from this topic to #junk > Topology on a finite dimensional vector space by Kevin Buzzard.

[Kevin Buzzard]

#16895 for the definition of the topology.

[Ruben Van de Velde]

You'll want a copyright header

[Kevin Buzzard]

Can you remind me of the keyboard shortcut?

Ruben Van de Velde said:

You'll want a copyright header

I'm surprised the PR passed CI! I've added one.

[Ruben Van de Velde]

Uh, that's no good. Will try to look later if I can find out why it didn't fail

[Damiano Testa]

I suspect this is something that might already have been fixed: the text-based linters have changed recently and there was some later fix that was merged and is maybe not part of the commit of master from which this PR originated.

CC @Michael Rothgang @Bryan Gin-ge Chen

[Ruben Van de Velde]

This was based on b755dda4cc224e363581d92a4d0b470d28742d4c from this morning

[Ruben Van de Velde]

Seems like the linter didn't even run on the new file

[Ruben Van de Velde]

Oh, that's because it also wasn't added to Mathlib.lean

[Ruben Van de Velde]

Incidentally, that's also not being caught in CI

[Ruben Van de Velde]

(#16896)