Co-analytic spaces, K-analytic spaces, and definable versions of Menger's conjecture

Abstract Menger's conjecture that Menger spaces are σ-compact is false; it is true for analytic subspaces of Polish spaces and undecidable for more complex definable subspaces of Polish spaces. We define co-analytic and co-K-analytic spaces. For non-metrizable spaces, analytic Menger spaces are σ-compact, but Menger continuous images of co-analytic spaces need not be. The general co-analytic case is still open, but many special cases are undecidable, in particular, Menger co-analytic topological groups. We also give numerous characterizations of proper K-Lusin spaces, suggesting such spaces are a good answer to the question of “what is a suitable class of ‘definable’ spaces in the non-metrizable context?”. Our methods include the Axiom of Co-analytic Determinacy, non-metrizable Descriptive Set Theory, and Arhangel'skiĭ's work on generalized metric spaces.