Injective spaces (Scott 1972, §1)

Scott's §1 introduces injective T₀-spaces — those with the extension property for continuous maps along subspace embeddings — and shows the two-point Sierpiński space is injective, that injectivity is preserved by products and by retracts, and (the embedding theorem) that every T₀-space embeds in a power of the Sierpiński space.

Main definitions / results

• IsInjectiveSpace — Scott's Definition 1.1.
• proposition_1_2 … proposition_1_5 — Scott's Propositions 1.2–1.5.
• corollary_1_6, corollary_1_7 — Scott's Corollaries 1.6 and 1.7.

@[reducible, inline]

abbrev Sierpinski : Type

Scott's two-point Sierpiński space 𝕆: Prop with the Sierpiński topology.

Equations

• Sierpinski = Prop

def IsInjectiveSpace (D : Type v) [TopologicalSpace D] : Prop

Scott 1972, Definition 1.1. A topological space D is injective when, for every topological embedding e : X → Y and every continuous f : X → D, there is a continuous g : Y → D extending f along e.

Equations

• One or more equations did not get rendered due to their size.

theorem isInjectiveSpace_sierpinski : IsInjectiveSpace Prop

Scott 1972, Proposition 1.2. The Sierpiński space is injective.

theorem proposition_1_2 : IsInjectiveSpace Sierpinski

theorem IsInjectiveSpace.pi {ι : Type w} (D : ι → Type v) [(i : ι) → TopologicalSpace (D i)] (h : ∀ (i : ι), IsInjectiveSpace (D i)) : IsInjectiveSpace ((i : ι) → D i)

Scott 1972, Proposition 1.3. Products of injective spaces are injective.

theorem proposition_1_3 {ι : Type w} (D : ι → Type v) [(i : ι) → TopologicalSpace (D i)] (h : ∀ (i : ι), IsInjectiveSpace (D i)) : IsInjectiveSpace ((i : ι) → D i)

theorem IsInjectiveSpace.of_retract {D D' : Type v} [TopologicalSpace D] [TopologicalSpace D'] (hD : IsInjectiveSpace D) (s : C(D', D)) (r : C(D, D')) (hrs : ∀ (d : D'), r (s d) = d) : IsInjectiveSpace D'

Scott 1972, Proposition 1.4. Retracts of injective spaces are injective.

theorem proposition_1_4 {D D' : Type v} [TopologicalSpace D] [TopologicalSpace D'] (hD : IsInjectiveSpace D) (s : C(D', D)) (r : C(D, D')) (hrs : ∀ (d : D'), r (s d) = d) : IsInjectiveSpace D'

theorem isInjectiveSpace_sierpinski_power (ι : Type w) : IsInjectiveSpace (ι → Prop)

theorem proposition_1_5 (X : Type u) [TopologicalSpace X] [T0Space X] : IsInjectiveSpace (TopologicalSpace.Opens X → Prop) ∧ Topology.IsEmbedding ⇑(TopologicalSpace.productOfMemOpens X)

Scott 1972, Proposition 1.5. Every T₀-space embeds into a power of 𝕆, and that power is injective.

theorem t0_isEmbedding_into_sierpinski_power (X : Type u) [TopologicalSpace X] [T0Space X] : Topology.IsEmbedding ⇑(TopologicalSpace.productOfMemOpens X)

structure IsRetractSubspace (D' D : Type u) [TopologicalSpace D'] [TopologicalSpace D] : Type u

Scott's notion of retract: a subspace with a continuous retraction.

• section' : C(D', D)

  The embedded section into the ambient space.

• isEmbedding_section : Topology.IsEmbedding ⇑self.section'
• retraction : C(D, D')

  The continuous retraction onto the subspace.

• retraction_section (d : D') : self.retraction (self.section' d) = d

theorem corollary_1_6 (D : Type u) [TopologicalSpace D] [T0Space D] : IsInjectiveSpace D ↔ ∃ (ι : Type u), Nonempty (IsRetractSubspace D (ι → Prop))

Scott 1972, Corollary 1.6. Injective spaces are exactly retracts of powers of 𝕆.

theorem corollary_1_7 (D : Type u) [TopologicalSpace D] [T0Space D] : IsInjectiveSpace D ↔ ∀ {Y : Type u} [inst : TopologicalSpace Y] (e : D → Y), Topology.IsEmbedding e → ∃ (r : C(Y, D)), ∀ (d : D), r (e d) = d

Scott 1972, Corollary 1.7. A space is injective iff it is a retract of every super-space of which it is a subspace.