Conjectures around homogeneous topological spaces

This file formalizes the notion of a weakly first countable topological space and some conjectures around those.

References:

• [Ar2013] Arhangeliski, Alexandr. "Selected old open problems in general topology." Buletinul Academiei de Ştiinţe a Republicii Moldova. Matematica 73.2-3 (2013): 37-46. https://www.math.md/files/basm/y2013-n2-3/y2013-n2-3-(pp37-46).pdf.pdf

class Homogeneous.HomogeneousSpace (X : Type u_1) [TopologicalSpace X] : Prop

A topological space $X$ is called homogeneous if for all $x, y \in X$ there is homeomorphism $f : X \to X$ with $f(x) = y$.

• exists_equiv (x y : X) : ∃ (f : X ≃ₜ X), f x = y

instance Homogeneous.DiscreteTopology.toHomogeneousSpace (X : Type u_1) [TopologicalSpace X] [DiscreteTopology X] : HomogeneousSpace X

Every discrete space is homogeneous.

theorem Homogeneous.homogeneousSpace_exists_inj_tendsto : True ↔ ∀ (X : Type) (x : TopologicalSpace X), ¬Finite X → T2Space X → CompactSpace X → HomogeneousSpace X → ∃ (s : ℕ → X), Function.Injective s ∧ ∃ (a : X), Filter.Tendsto s Filter.atTop (nhds a)

Problem 13 in [Ar2013]: Is it true that every infinite homogeneous compact hausdorff space contains a non-trivial convergent sequence?

theorem Homogeneous.homogeneousSpace_exists_surjective : True ↔ ∀ (X : Type) (x : TopologicalSpace X), T2Space X → CompactSpace X → ∃ (Y : Type) (x_1 : TopologicalSpace Y), T2Space Y ∧ CompactSpace Y ∧ HomogeneousSpace Y ∧ ∃ (f : Y → X), Continuous f ∧ Function.Surjective f

Problem 14 in [Ar2013]: Is it possible to represent an arbitrary compact hausdorff space as an image of a homogeneous compact space under a continuous mapping?

class Homogeneous.CountablyMonolithicSpace (X : Type u_1) [TopologicalSpace X] : Prop

A topological space is called ω-monolithic if the closure of every countable subspace is metrizable.

• metrizable_of_closure_of_countable ⦃s : Set X⦄ : s.Countable → TopologicalSpace.MetrizableSpace ↑(closure s)

instance Homogeneous.MetrizableSpace.countablyMonolithicSpace (X : Type u_1) [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] : CountablyMonolithicSpace X

Every Metrizable space is ω-monolithic.

theorem Homogeneous.firstCountableTopology_of_countablyMonolithicSpace : True ↔ ∀ (X : Type) (x : TopologicalSpace X), T2Space X → CompactSpace X → HomogeneousSpace X → CountablyMonolithicSpace X → FirstCountableTopology X

Problem 15 in [Ar2013]: Is every homogeneous ω-monolithic compact hausdorff space first countable?

theorem Homogeneous.countablyMonolithicSpace_card_lt : True ↔ ∀ (X : Type) (x : TopologicalSpace X), T2Space X → CompactSpace X → HomogeneousSpace X → CountablyMonolithicSpace X → Cardinal.mk X ≤ Cardinal.continuum

Problem 16 in [Ar2013]: Is the cardinality of every homogeneous ω-monolithic compact hausdorff space not greater than 𝔠?

theorem Homogeneous.countablyMonolithicSpace_exists_nhds_generated_countable : True ↔ ∀ (X : Type) (x : TopologicalSpace X), T2Space X → CompactSpace X → Nonempty X → CountablyMonolithicSpace X → ∃ (x_1 : X), (nhds x_1).IsCountablyGenerated

Problem 17 in [Ar2013]: Is it true that every nonempty ω-monolithic compact hausdorff space contains a point with a first countable neighborhood basis?

Note: Nonempty X is required since the conclusion asserts the existence of a point.