Delta-generated topological spaces

This file defines delta-generated spaces, as topological spaces whose topology is coinduced by all maps from Euclidean spaces into them. This is the strongest topological property that holds for all CW-complexes and is closed under quotients and disjoint unions; every delta-generated space is locally path-connected, sequential and in particular compactly generated.

See https://ncatlab.org/nlab/show/Delta-generated+topological+space.

Adapted from Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean.

TODO

• All locally path-connected first-countable spaces are delta-generated - in particular, all normed spaces and convex subsets thereof, like the standard simplices and the unit interval.
• Delta-generated spaces are equivalently generated by the simplices Δⁿ.
• Delta-generated spaces are equivalently generated by the unit interval I.

def TopologicalSpace.deltaGenerated (X : Type u_3) [TopologicalSpace X] : TopologicalSpace X

The topology coinduced by all maps from ℝⁿ into a space.

theorem deltaGenerated_eq_coinduced {X : Type u_1} [tX : TopologicalSpace X] : TopologicalSpace.deltaGenerated X = TopologicalSpace.coinduced (fun (x : (f : (n : ℕ) × C(Fin n → ℝ, X)) × (Fin f.fst → ℝ)) => x.fst.snd x.snd) inferInstance

The delta-generated topology is also coinduced by a single map out of a sigma type.

theorem deltaGenerated_le {X : Type u_1} [tX : TopologicalSpace X] : TopologicalSpace.deltaGenerated X ≤ tX

The delta-generated topology is at least as fine as the original one.

theorem isOpen_deltaGenerated_iff {X : Type u_1} [tX : TopologicalSpace X] {u : Set X} : IsOpen u ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)

A set is open in deltaGenerated X iff all its preimages under continuous functions ℝⁿ → X are open.

theorem deltaGenerated_deltaGenerated_eq {X : Type u_1} [tX : TopologicalSpace X] : TopologicalSpace.deltaGenerated X = TopologicalSpace.deltaGenerated X

deltaGenerated is idempotent as a function TopologicalSpace X → TopologicalSpace X.

class DeltaGeneratedSpace (X : Type u_3) [t : TopologicalSpace X] : Prop

A space is delta-generated if its topology is equal to the delta-generated topology, i.e. coinduced by all continuous maps ℝⁿ → X. Since the delta-generated topology is always finer than the original one, it suffices to show that it is also coarser.

• le_deltaGenerated : t ≤ TopologicalSpace.deltaGenerated X

theorem eq_deltaGenerated {X : Type u_1} [tX : TopologicalSpace X] [DeltaGeneratedSpace X] : tX = TopologicalSpace.deltaGenerated X

theorem DeltaGeneratedSpace.isOpen_iff {X : Type u_1} [tX : TopologicalSpace X] [DeltaGeneratedSpace X] {u : Set X} : IsOpen u ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)

A subset of a delta-generated space is open iff its preimage is open for every continuous map from ℝⁿ to X.

theorem DeltaGeneratedSpace.continuous_iff {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [DeltaGeneratedSpace X] {f : X → Y} : Continuous f ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), Continuous (f ∘ ⇑p)

A map out of a delta-generated space is continuous iff it preserves continuity of maps from ℝⁿ into X.

theorem continuous_to_deltaGenerated {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [DeltaGeneratedSpace X] {f : X → Y} : Continuous f ↔ Continuous f

A map out of a delta-generated space is continuous iff it is continuous with respect to the delta-generated topology on the codomain.

theorem deltaGeneratedSpace_deltaGenerated {X : Type u_3} {t : TopologicalSpace X} : DeltaGeneratedSpace X

The delta-generated topology on X does in fact turn X into a delta-generated space.

theorem deltaGenerated_mono {X : Type u_3} {t₁ t₂ : TopologicalSpace X} (h : t₁ ≤ t₂) : TopologicalSpace.deltaGenerated X ≤ TopologicalSpace.deltaGenerated X

def DeltaGeneratedSpace.of (X : Type u_3) : Type u_3

Type synonym to be equipped with the delta-generated topology.

instance DeltaGeneratedSpace.instTopologicalSpaceOf {X : Type u_1} [tX : TopologicalSpace X] : TopologicalSpace (of X)

instance DeltaGeneratedSpace.instOf {X : Type u_1} [tX : TopologicalSpace X] : DeltaGeneratedSpace (of X)

def DeltaGeneratedSpace.counit {X : Type u_1} : of X → X

The natural map from DeltaGeneratedSpace.of X to X.

theorem DeltaGeneratedSpace.continuous_counit {X : Type u_1} [tX : TopologicalSpace X] : Continuous counit

instance DeltaGeneratedSpace.instLocPathConnectedSpace {X : Type u_1} [tX : TopologicalSpace X] [DeltaGeneratedSpace X] : LocPathConnectedSpace X

Delta-generated spaces are locally path-connected.

instance DeltaGeneratedSpace.instSequentialSpace {X : Type u_1} [tX : TopologicalSpace X] [DeltaGeneratedSpace X] : SequentialSpace X

Delta-generated spaces are sequential.

theorem DeltaGeneratedSpace.coinduced {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [DeltaGeneratedSpace X] (f : X → Y) : DeltaGeneratedSpace Y

Any topology coinduced by a delta-generated topology is delta-generated.

theorem DeltaGeneratedSpace.iSup {X : Type u_3} {ι : Sort u_4} {t : ι → TopologicalSpace X} (h : ∀ (i : ι), DeltaGeneratedSpace X) : DeltaGeneratedSpace X

Suprema of delta-generated topologies are delta-generated.

theorem DeltaGeneratedSpace.sup {X : Type u_3} {t₁ t₂ : TopologicalSpace X} (h₁ : DeltaGeneratedSpace X) (h₂ : DeltaGeneratedSpace X) : DeltaGeneratedSpace X

Suprema of delta-generated topologies are delta-generated.

theorem Topology.IsQuotientMap.deltaGeneratedSpace {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [DeltaGeneratedSpace X] {f : X → Y} (h : IsQuotientMap f) : DeltaGeneratedSpace Y

Quotients of delta-generated spaces are delta-generated.

instance Quot.deltaGeneratedSpace {X : Type u_1} [tX : TopologicalSpace X] [DeltaGeneratedSpace X] {r : X → X → Prop} : DeltaGeneratedSpace (Quot r)

Quotients of delta-generated spaces are delta-generated.

instance Quotient.deltaGeneratedSpace {X : Type u_1} [tX : TopologicalSpace X] [DeltaGeneratedSpace X] {s : Setoid X} : DeltaGeneratedSpace (Quotient s)

Quotients of delta-generated spaces are delta-generated.

instance Sum.deltaGeneratedSpace {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [DeltaGeneratedSpace X] [DeltaGeneratedSpace Y] : DeltaGeneratedSpace (X ⊕ Y)

Disjoint unions of delta-generated spaces are delta-generated.

instance Sigma.deltaGeneratedSpace {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), DeltaGeneratedSpace (X i)] : DeltaGeneratedSpace ((i : ι) × X i)

Disjoint unions of delta-generated spaces are delta-generated.