Constructions of new topological spaces from old ones
This file constructs products, sums, subtypes and quotients of topological spaces and sets up their basic theory, such as criteria for maps into or out of these constructions to be continuous; descriptions of the open sets, neighborhood filters, and generators of these constructions; and their behavior with respect to embeddings and other specific classes of maps.
Implementation note
The constructed topologies are defined using induced and coinduced topologies
along with the complete lattice structure on topologies. Their universal properties
(for example, a map X → Y × Z is continuous if and only if both projections
X → Y, X → Z are) follow easily using order-theoretic descriptions of
continuity. With more work we can also extract descriptions of the open sets,
neighborhood filters and so on.
Tags
product, sum, disjoint union, subspace, quotient space
@[instance]
Equations
@[instance]
def
quot.topological_space
{α : Type u}
{r : α → α → Prop}
[t : topological_space α] :
topological_space (quot r)
Equations
- quot.topological_space = topological_space.coinduced (quot.mk r) t
@[instance]
@[instance]
def
prod.topological_space
{α : Type u}
{β : Type v}
[t₁ : topological_space α]
[t₂ : topological_space β] :
topological_space (α × β)
@[instance]
def
sum.topological_space
{α : Type u}
{β : Type v}
[t₁ : topological_space α]
[t₂ : topological_space β] :
topological_space (α ⊕ β)
@[instance]
def
sigma.topological_space
{α : Type u}
{β : α → Type v}
[t₂ : Π (a : α), topological_space (β a)] :
Equations
- sigma.topological_space = ⨆ (a : α), topological_space.coinduced (sigma.mk a) (t₂ a)
@[instance]
def
Pi.topological_space
{α : Type u}
{β : α → Type v}
[t₂ : Π (a : α), topological_space (β a)] :
topological_space (Π (a : α), β a)
Equations
- Pi.topological_space = ⨅ (a : α), topological_space.induced (λ (f : Π (a : α), β a), f a) (t₂ a)
@[instance]
Equations
@[instance]
def
subtype.discrete_topology
{α : Type u}
{p : α → Prop}
[topological_space α]
[discrete_topology α] :
Equations
@[instance]
def
sum.discrete_topology
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[hα : discrete_topology α]
[hβ : discrete_topology β] :
discrete_topology (α ⊕ β)
Equations
@[instance]
def
sigma.discrete_topology
{α : Type u}
{β : α → Type v}
[Π (a : α), topological_space (β a)]
[h : ∀ (a : α), discrete_topology (β a)] :
Equations
theorem
continuous_at_fst
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α × β} :
theorem
continuous_at_snd
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α × β} :
theorem
continuous.prod_mk
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : γ → α}
{g : γ → β} :
continuous f → continuous g → continuous (λ (x : γ), (f x, g x))
theorem
continuous.prod_map
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : γ → α}
{g : δ → β} :
continuous f → continuous g → continuous (λ (x : γ × δ), (f x.fst, g x.snd))
theorem
filter.eventually.prod_inl_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α → Prop}
{a : α}
(h : ∀ᶠ (x : α) in nhds a, p x)
(b : β) :
theorem
filter.eventually.prod_inr_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : β → Prop}
{b : β}
(h : ∀ᶠ (x : β) in nhds b, p x)
(a : α) :
theorem
filter.eventually.prod_mk_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{pa : α → Prop}
{a : α}
(ha : ∀ᶠ (x : α) in nhds a, pa x)
{pb : β → Prop}
{b : β} :
theorem
is_open_prod
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set α}
{t : set β} :
theorem
nhds_prod_eq
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{a : α}
{b : β} :
@[instance]
def
prod.discrete_topology
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[discrete_topology α]
[discrete_topology β] :
discrete_topology (α × β)
Equations
- prod.discrete_topology = _
- _ = _
theorem
prod_mem_nhds_sets
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set α}
{t : set β}
{a : α}
{b : β} :
theorem
nhds_swap
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(a : α)
(b : β) :
nhds (a, b) = filter.map prod.swap (nhds (b, a))
theorem
filter.tendsto.prod_mk_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{γ : Type u_1}
{a : α}
{b : β}
{f : filter γ}
{ma : γ → α}
{mb : γ → β} :
filter.tendsto ma f (nhds a) → filter.tendsto mb f (nhds b) → filter.tendsto (λ (c : γ), (ma c, mb c)) f (nhds (a, b))
theorem
filter.eventually.curry_nhds
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α × β → Prop}
{x : α}
{y : β} :
theorem
continuous_at.prod
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β}
{g : α → γ}
{x : α} :
continuous_at f x → continuous_at g x → continuous_at (λ (x : α), (f x, g x)) x
theorem
continuous_at.prod_map
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → γ}
{g : β → δ}
{p : α × β} :
continuous_at f p.fst → continuous_at g p.snd → continuous_at (λ (p : α × β), (f p.fst, g p.snd)) p
theorem
continuous_at.prod_map'
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → γ}
{g : β → δ}
{x : α}
{y : β} :
continuous_at f x → continuous_at g y → continuous_at (λ (p : α × β), (f p.fst, g p.snd)) (x, y)
theorem
prod_eq_generate_from
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β] :
The first projection in a product of topological spaces sends open sets to open sets.
The second projection in a product of topological spaces sends open sets to open sets.
theorem
closure_prod_eq
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set α}
{t : set β} :
theorem
mem_closure2
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{s : set α}
{t : set β}
{u : set γ}
{f : α → β → γ}
{a : α}
{b : β} :
theorem
is_closed_prod
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s₁ : set α}
{s₂ : set β} :
theorem
inducing.prod_mk
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → β}
{g : γ → δ} :
theorem
embedding.prod_mk
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → β}
{g : γ → δ} :
theorem
is_open_map.prod
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → β}
{g : γ → δ} :
is_open_map f → is_open_map g → is_open_map (λ (p : α × γ), (f p.fst, g p.snd))
theorem
open_embedding.prod
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → β}
{g : γ → δ} :
open_embedding f → open_embedding g → open_embedding (λ (x : α × γ), (f x.fst, g x.snd))
theorem
embedding_graph
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β} :
continuous f → embedding (λ (x : α), (x, f x))
theorem
continuous_sum_rec
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → γ}
{g : β → γ} :
continuous f → continuous g → continuous (sum.rec f g)
theorem
is_open_sum_iff
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set (α ⊕ β)} :
theorem
is_open_map_sum
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α ⊕ β → γ} :
is_open_map (λ (a : α), f (sum.inl a)) → is_open_map (λ (b : β), f (sum.inr b)) → is_open_map f
theorem
is_open.open_embedding_subtype_coe
{α : Type u}
[topological_space α]
{s : set α} :
is_open s → open_embedding coe
theorem
is_open.is_open_map_subtype_coe
{α : Type u}
[topological_space α]
{s : set α} :
is_open s → is_open_map coe
theorem
is_open_map.restrict
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β}
(hf : is_open_map f)
{s : set α} :
is_open s → is_open_map (set.restrict f s)
theorem
continuous_subtype_mk
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{p : α → Prop}
{f : β → α}
(hp : ∀ (x : β), p (f x)) :
continuous f → continuous (λ (x : β), ⟨f x, _⟩)
theorem
continuous_at_subtype_coe
{α : Type u}
[topological_space α]
{p : α → Prop}
{a : subtype p} :
theorem
map_nhds_subtype_coe_eq
{α : Type u}
[topological_space α]
{p : α → Prop}
{a : α}
(ha : p a) :
theorem
tendsto_subtype_rng
{α : Type u}
[topological_space α]
{β : Type u_1}
{p : α → Prop}
{b : filter β}
{f : β → subtype p}
{a : subtype p} :
filter.tendsto f b (nhds a) ↔ filter.tendsto (λ (x : β), ↑(f x)) b (nhds ↑a)
theorem
continuous_subtype_nhds_cover
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{ι : Sort u_1}
{f : α → β}
{c : ι → α → Prop} :
(∀ (x : α), ∃ (i : ι), {x : α | c i x} ∈ nhds x) → (∀ (i : ι), continuous (λ (x : subtype (c i)), f ↑x)) → continuous f
theorem
continuous_subtype_is_closed_cover
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{ι : Type u_1}
{f : α → β}
(c : ι → α → Prop) :
locally_finite (λ (i : ι), {x : α | c i x}) → (∀ (i : ι), is_closed {x : α | c i x}) → (∀ (x : α), ∃ (i : ι), c i x) → (∀ (i : ι), continuous (λ (x : subtype (c i)), f ↑x)) → continuous f
theorem
quotient_map_quot_mk
{α : Type u}
[topological_space α]
{r : α → α → Prop} :
quotient_map (quot.mk r)
theorem
continuous_quot_mk
{α : Type u}
[topological_space α]
{r : α → α → Prop} :
continuous (quot.mk r)
theorem
continuous_quot_lift
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{r : α → α → Prop}
{f : α → β}
(hr : ∀ (a b : α), r a b → f a = f b) :
continuous f → continuous (quot.lift f hr)
theorem
continuous_quotient_lift
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : setoid α}
{f : α → β}
(hs : ∀ (a b : α), a ≈ b → f a = f b) :
continuous f → continuous (quotient.lift f hs)
theorem
continuous_pi
{α : Type u}
{ι : Type u_1}
{π : ι → Type u_2}
[topological_space α]
[Π (i : ι), topological_space (π i)]
{f : α → Π (i : ι), π i} :
(∀ (i : ι), continuous (λ (a : α), f a i)) → continuous f
theorem
continuous_apply
{ι : Type u_1}
{π : ι → Type u_2}
[Π (i : ι), topological_space (π i)]
(i : ι) :
continuous (λ (p : Π (i : ι), π i), p i)
theorem
continuous_update
{ι : Type u_1}
{π : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), topological_space (π i)]
{i : ι}
{f : Π (i : ι), π i} :
continuous (λ (x : π i), function.update f i x)
Embedding a factor into a product space (by fixing arbitrarily all the other coordinates) is continuous.
theorem
nhds_pi
{ι : Type u_1}
{π : ι → Type u_2}
[t : Π (i : ι), topological_space (π i)]
{a : Π (i : ι), π i} :
nhds a = ⨅ (i : ι), filter.comap (λ (x : Π (i : ι), π i), x i) (nhds (a i))
theorem
is_open_set_pi
{ι : Type u_1}
{π : ι → Type u_2}
[Π (a : ι), topological_space (π a)]
{i : set ι}
{s : Π (a : ι), set (π a)} :
theorem
pi_eq_generate_from
{ι : Type u_1}
{π : ι → Type u_2}
[Π (a : ι), topological_space (π a)] :
theorem
pi_generate_from_eq_fintype
{ι : Type u_1}
{π : ι → Type u_2}
{g : Π (a : ι), set (set (π a))}
[fintype ι] :
theorem
continuous_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
continuous (sigma.mk i)
theorem
is_open_sigma_iff
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{s : set (sigma σ)} :
theorem
is_closed_sigma_iff
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{s : set (sigma σ)} :
theorem
is_open_map_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
is_open_map (sigma.mk i)
theorem
is_open_range_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
is_closed_map_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
is_closed_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
open_embedding_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
closed_embedding_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
embedding_sigma_mk
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
theorem
continuous_sigma
{β : Type v}
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
[topological_space β]
{f : sigma σ → β} :
(∀ (i : ι), continuous (λ (a : σ i), f ⟨i, a⟩)) → continuous f
A map out of a sum type is continuous if its restriction to each summand is.
theorem
continuous_sigma_map
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{κ : Type u_3}
{τ : κ → Type u_4}
[Π (k : κ), topological_space (τ k)]
{f₁ : ι → κ}
{f₂ : Π (i : ι), σ i → τ (f₁ i)} :
(∀ (i : ι), continuous (f₂ i)) → continuous (sigma.map f₁ f₂)
theorem
is_open_map_sigma
{β : Type v}
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
[topological_space β]
{f : sigma σ → β} :
(∀ (i : ι), is_open_map (λ (a : σ i), f ⟨i, a⟩)) → is_open_map f
theorem
embedding_sigma_map
{ι : Type u_1}
{σ : ι → Type u_2}
[Π (i : ι), topological_space (σ i)]
{τ : ι → Type u_3}
[Π (i : ι), topological_space (τ i)]
{f : Π (i : ι), σ i → τ i} :
The sum of embeddings is an embedding.
theorem
mem_closure_of_continuous
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β}
{a : α}
{s : set α}
{t : set β} :
continuous f → a ∈ closure s → set.maps_to f s (closure t) → f a ∈ closure t
theorem
mem_closure_of_continuous2
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β → γ}
{a : α}
{b : β}
{s : set α}
{t : set β}
{u : set γ} :