Let $E$ be a topological vector space locally convex, defined by the family of seminorms $\mathcal{F}=(p_j)_{j\in J}$.

I can't prove that $\underset{j\in J}\bigcap Ker(p_j)=\overline{\{0\}}$

  • $\begingroup$ This condition is equivalent to your topology being Hausdorff. If you didn't start with enough seminorms, then your TVS won't have this property. However, if you require your TVS to be Hausdorff, distinct points can be separated by seminorms. What would that tell you about the intersection of the kernels of the seminorms? $\endgroup$ – Ashwin Trisal Dec 16 '18 at 8:13
  • 1
    $\begingroup$ @AshwinTrisal No, this is not true, this identity always holds. If $X$ is $T_1$ we get that the right hand closure is just $\{0\}$ and we do get the separation property. $\endgroup$ – Henno Brandsma Dec 16 '18 at 9:29

Suppose $x \in \overline{\{0\}}$.

We know that all $p_j$ are by definition continuous in the topology generated by the semininorms, so for any $j \in J$: $$p_j(x) \in p_j[\overline{\{0\}}] \subseteq \overline{p_j[\{0\}]} = \overline{\{0\}} = \{0\}$$ as the last closure is taken in the reals (or complex numbers) where singletons are closed, and so $x \in \operatorname{Ker}(p_j)$ for all $j$, also using that $p_j(0)=0$ of course.

This shows $$\overline{\{0\}} \subseteq \bigcap_{j \in J} \operatorname{Ker}(p_j)$$

To see the other inclusion, let $x$ be in $\bigcap_{j \in J} \operatorname{Ker}(p_j)$ and let $O$ be a basic neighbourhood of $x$. This means that there are finitely many $p_{j_1},\ldots,p_{j_n}$ and an $\epsilon >0$ such that $O = \bigcap_{i=1}^n B_{j_i}(x,\varepsilon)$, where $B_{j_i}(x,\varepsilon)= \{y \in X: p_{j_i}(x - y) < \varepsilon\}$ is the open ball around $x$ induced by the seminorm $p_{j_i}$.

The fact that $x \in \operatorname{Ker}(p_{j_i})$ implies that $0 \in B_{j_i}(x,\varepsilon)$, and so $0 \in O$. As $O$ is an arbitary base element containing $x$ we have shown that $x \in \overline{\{0\}}$ as required.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.