Is the quotient of a Polish TVS Polish? The title says it pretty much: Suppose $X$ is a Polish TVS. Let $A$ be a closed subspace of $X$. Is the quotient space $X/A$ Polish with respect to the relative topology?
I know this is true for topological Polish groups from Kechris's paper [Topology and its Applications 58, 195 (1994)]. As silly it may sound, I couldn't find the above statement in the literature. Could anyone let me know of a reference, please?
 A: It is, though I don't have literature reference handy.
$X{/}A$ has a standard quotient linear structure (as $A$ is a linear subspace), and like in the case of groups, the operations on the quotient are still continuous.
As $A$ is closed in the Polish $X$, it's a $G_\delta$ and this implies that $0$ in $X{/}A$ has a countable local base (and $\{0\}$ is closed so the quotient is Hausdorff and regular) and so is metrisable (Birkhoff's theorem). It's separable as $X$ is, and $X{/}A$ is its continuous image.
I think that completeness of the quotient will follow from the closedness of $X$ too.
Maybe others do know of a good reference?
A: Here is a proof of a slightly more general statement about abelian (not necessarily Polish) groups.
If $G$ is an abelian, completely metrisable group and $H\leq G$ is a closed subgroup, then $G/H$ is also completely metrisable (in general, if $H$ is not necessarily closed, it is pseudometrisable). (In particular, if $G$ is Polish, so is $G/H$, since separability trivially passes to the quotient.)
Since $G$ is completely metrisable and abelian, by a variant of the Birkhoff-Kakutani theorem, its topology is induced by a complete invariant metric $d$. Following that observation, the proof is very standard. I suspect a version of the argument for Frechet spaces should be easy to find in analysis textbooks (local convexity is irrelevant here, as far as I can tell).
Namely, we can then define on $G/H$ the function $\bar d(g+H,g'+H)=\inf_{h\in H} d(g,g'+h)$. Now, $\bar d$ is clearly invariant. It also satisfies triangle inequality:
$$\bar d(g_1+H,g_2+H)+\bar d(g_2+H,g_3+H)=\inf_{h_1,h_2} d(g_1,g_2+h_1)+d(g_2+h_1,g_3+h_2)\geq \inf_{h_1,h_2} d(g_1,g_3+h_2)=\bar d(g_1+H,g_3+H),$$
it is also trivially symmetric (by invariance of $d$) and non-negative. It is also easy to see that if $\bar d(g+H,H)=0$, then $g\in \bar H$, so it is a metric if $H$ is closed (and a pseudometric otherwise).
It is fairly easy to show that $\bar d$ generates the quotient topology, but that is straightforward: the preimage of a $\bar d$-ball around $g+H$ is the union of the $d$-balls of the same radius around all elements of $g+H$, and if any $U\subseteq G$ is open and a preimage of a subset of $G/H$, then it is a $H$-invariant union of $d$-balls, so it is a preimage of a union of $\bar d$-balls.
Completeness of $\bar d$ is also quite standard: let $(g_n+H)_n$ be Cauchy. We may assume without loss of generality (passing to a subsequence) that $\bar d(g_n+H,g_m+H)<2^{-n-1}$ when $n<m$. Let $g_0'=g_0$. Then take $g_1'\in g_1+H$ such that $d(g_0',g_1')<2^{-1}$, $g_2'\in g_2+H$ such that $d(g_1',g_2')<2^{-2}$ etc. Then by triangle inequality it is easy to check that $d(g_n',g_m')<2^{-n}$ when $n<m$, so the sequence $(g_n')_n$ is Cauchy, and so it converges to some $g$. Since $g_n'+H=g_n+H$ for each $n$, it easily follows that $g_n+H\to g+H$.
