Ordering on topologies and (co)induced topologies #
Topologies on a fixed type α are ordered, by reverse inclusion.
That is, for topologies t₁ and t₂ on α, we write t₁ ≤ t₂
if every set open in t₂ is also open in t₁.
(One also calls t₁ finer than t₂, and t₂ coarser than t₁.)
Any function f : α → β induces
induced f : topological_space β → topological_space α
and coinduced f : topological_space α → topological_space β.
Continuity, the ordering on topologies and (co)induced topologies are
related as follows:
- The identity map (α, t₁) → (α, t₂) is continuous iff t₁ ≤ t₂.
- A map f : (α, t) → (β, u) is continuous
iff t ≤ induced f u (
continuous_iff_le_induced) iff coinduced f t ≤ u (continuous_iff_coinduced_le).
Topologies on α form a complete lattice, with ⊥ the discrete topology and ⊤ the indiscrete topology.
For a function f : α → β, (coinduced f, induced f) is a Galois connection between topologies on α and topologies on β.
Implementation notes #
There is a Galois insertion between topologies on α (with the inclusion ordering) and all collections of sets in α. The complete lattice structure on topologies on α is defined as the reverse of the one obtained via this Galois insertion.
Tags #
finer, coarser, induced topology, coinduced topology
- basic : ∀ {α : Type u} {g : set (set α)} (s : set α), s ∈ g → topological_space.generate_open g s
- univ : ∀ {α : Type u} {g : set (set α)}, topological_space.generate_open g set.univ
- inter : ∀ {α : Type u} {g : set (set α)} (s t : set α), topological_space.generate_open g s → topological_space.generate_open g t → topological_space.generate_open g (s ∩ t)
- sUnion : ∀ {α : Type u} {g : set (set α)} (k : set (set α)), (∀ (s : set α), s ∈ k → topological_space.generate_open g s) → topological_space.generate_open g (⋃₀k)
The open sets of the least topology containing a collection of basic sets.
The smallest topological space containing the collection g of basic sets
Equations
- topological_space.generate_from g = {is_open := topological_space.generate_open g, is_open_univ := _, is_open_inter := _, is_open_sUnion := _}
@[protected]
Construct a topology on α given the filter of neighborhoods of each point of α.
Equations
- topological_space.mk_of_nhds n = {is_open := λ (s : set α), ∀ (a : α), a ∈ s → s ∈ n a, is_open_univ := _, is_open_inter := _, is_open_sUnion := _}
The inclusion ordering on topologies on α. We use it to get a complete
lattice instance via the Galois insertion method, but the partial order
that we will eventually impose on topological_space α is the reverse one.
Equations
- tmp_order = {le := λ (t s : topological_space α), t.is_open ≤ s.is_open, lt := preorder.lt._default (λ (t s : topological_space α), t.is_open ≤ s.is_open), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected]
def
mk_of_closure
{α : Type u}
(s : set (set α))
(hs : {u : set α | (topological_space.generate_from s).is_open u} = s) :
If s equals the collection of open sets in the topology it generates,
then s defines a topology.
Equations
- mk_of_closure s hs = {is_open := λ (u : set α), u ∈ s, is_open_univ := _, is_open_inter := _, is_open_sUnion := _}
theorem
mk_of_closure_sets
{α : Type u}
{s : set (set α)}
{hs : {u : set α | (topological_space.generate_from s).is_open u} = s} :
def
gi_generate_from
(α : Type u_1) :
galois_insertion topological_space.generate_from (λ (t : topological_space α), {s : set α | t.is_open s})
The Galois insertion between set (set α) and topological_space α whose lower part
sends a collection of subsets of α to the topology they generate, and whose upper part
sends a topology to its collection of open subsets.
Equations
- gi_generate_from α = {choice := λ (g : set (set α)) (hg : {s : set α | (topological_space.generate_from g).is_open s} ≤ g), mk_of_closure g _, gc := _, le_l_u := _, choice_eq := _}
theorem
generate_from_set_of_is_open
{α : Type u}
(t : topological_space α) :
topological_space.generate_from {s : set α | t.is_open s} = t
theorem
left_inverse_generate_from
{α : Type u} :
function.left_inverse topological_space.generate_from (λ (t : topological_space α), {s : set α | t.is_open s})
theorem
set_of_is_open_injective
{α : Type u} :
function.injective (λ (t : topological_space α), {s : set α | t.is_open s})
The "temporary" order tmp_order on topological_space α, i.e. the inclusion order, is a
complete lattice. (Note that later topological_space α will equipped with the dual order to
tmp_order).
Equations
@[protected, instance]
Equations
- topological_space.has_le = {le := λ (t s : topological_space α), s.is_open ≤ t.is_open}
@[protected]
@[protected, instance]
The ordering on topologies on the type α.
t ≤ s if every set open in s is also open in t (t is finer than s).
Equations
- topological_space.partial_order = {le := has_le.le topological_space.has_le, lt := preorder.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
theorem
le_generate_from_iff_subset_is_open
{α : Type u}
{g : set (set α)}
{t : topological_space α} :
@[protected, instance]
Topologies on α form a complete lattice, with ⊥ the discrete topology
and ⊤ the indiscrete topology. The infimum of a collection of topologies
is the topology generated by all their open sets, while the supremum is the
topology whose open sets are those sets open in every member of the collection.
@[class]
A topological space is discrete if every set is open, that is,
its topology equals the discrete topology ⊥.
Instances
- discrete_topology_bot
- subsingleton.discrete_topology
- empty.discrete_topology
- pempty.discrete_topology
- punit.discrete_topology
- bool.discrete_topology
- nat.discrete_topology
- int.discrete_topology
- subtype.discrete_topology
- sum.discrete_topology
- sigma.discrete_topology
- prod.discrete_topology
- Pi.discrete_topology
@[simp]
theorem
is_open_discrete
{α : Type u}
[topological_space α]
[discrete_topology α]
(s : set α) :
is_open s
@[simp]
theorem
continuous_of_discrete_topology
{α : Type u}
{β : Type v}
[topological_space α]
[discrete_topology α]
[topological_space β]
{f : α → β} :
theorem
mem_nhds_discrete
{α : Type u}
[topological_space α]
[discrete_topology α]
{x : α}
{s : set α} :
theorem
le_of_nhds_le_nhds
{α : Type u}
{t₁ t₂ : topological_space α}
(h : ∀ (x : α), 𝓝 x ≤ 𝓝 x) :
t₁ ≤ t₂
theorem
eq_of_nhds_eq_nhds
{α : Type u}
{t₁ t₂ : topological_space α}
(h : ∀ (x : α), 𝓝 x = 𝓝 x) :
t₁ = t₂
theorem
eq_bot_of_singletons_open
{α : Type u}
{t : topological_space α}
(h : ∀ (x : α), t.is_open {x}) :
theorem
forall_open_iff_discrete
{X : Type u_1}
[topological_space X] :
(∀ (s : set X), is_open s) ↔ discrete_topology X
theorem
singletons_open_iff_discrete
{X : Type u_1}
[topological_space X] :
(∀ (a : X), is_open {a}) ↔ discrete_topology X
Given f : α → β and a topology on β, the induced topology on α is the collection of
sets that are preimages of some open set in β. This is the coarsest topology that
makes f continuous.
Equations
- topological_space.induced f t = {is_open := λ (s : set α), ∃ (s' : set β), t.is_open s' ∧ f ⁻¹' s' = s, is_open_univ := _, is_open_inter := _, is_open_sUnion := _}
theorem
is_open_induced_iff'
{α : Type u_1}
{β : Type u_2}
[t : topological_space β]
{s : set α}
{f : α → β} :
Given f : α → β and a topology on α, the coinduced topology on β is defined
such that s:set β is open if the preimage of s is open. This is the finest topology that
makes f continuous.
Equations
- topological_space.coinduced f t = {is_open := λ (s : set β), t.is_open (f ⁻¹' s), is_open_univ := _, is_open_inter := _, is_open_sUnion := _}
theorem
is_open_coinduced
{α : Type u_1}
{β : Type u_2}
{t : topological_space α}
{s : set β}
{f : α → β} :
theorem
preimage_nhds_coinduced
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{π : α → β}
{s : set β}
{a : α}
(hs : s ∈ 𝓝 (π a)) :
theorem
continuous.coinduced_le
{α : Type u_1}
{β : Type u_2}
{t : topological_space α}
{t' : topological_space β}
{f : α → β}
(h : continuous f) :
topological_space.coinduced f t ≤ t'
theorem
coinduced_le_iff_le_induced
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{tα : topological_space α}
{tβ : topological_space β} :
topological_space.coinduced f tα ≤ tβ ↔ tα ≤ topological_space.induced f tβ
theorem
continuous.le_induced
{α : Type u_1}
{β : Type u_2}
{t : topological_space α}
{t' : topological_space β}
{f : α → β}
(h : continuous f) :
t ≤ topological_space.induced f t'
theorem
induced_mono
{α : Type u_1}
{β : Type u_2}
{t₁ t₂ : topological_space α}
{g : β → α}
(h : t₁ ≤ t₂) :
theorem
coinduced_mono
{α : Type u_1}
{β : Type u_2}
{t₁ t₂ : topological_space α}
{f : α → β}
(h : t₁ ≤ t₂) :
@[simp]
@[simp]
theorem
induced_inf
{α : Type u_1}
{β : Type u_2}
{t₁ t₂ : topological_space α}
{g : β → α} :
topological_space.induced g (t₁ ⊓ t₂) = topological_space.induced g t₁ ⊓ topological_space.induced g t₂
@[simp]
theorem
induced_infi
{α : Type u_1}
{β : Type u_2}
{g : β → α}
{ι : Sort w}
{t : ι → topological_space α} :
topological_space.induced g (⨅ (i : ι), t i) = ⨅ (i : ι), topological_space.induced g (t i)
@[simp]
@[simp]
theorem
coinduced_sup
{α : Type u_1}
{β : Type u_2}
{t₁ t₂ : topological_space α}
{f : α → β} :
topological_space.coinduced f (t₁ ⊔ t₂) = topological_space.coinduced f t₁ ⊔ topological_space.coinduced f t₂
@[simp]
theorem
coinduced_supr
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{ι : Sort w}
{t : ι → topological_space α} :
topological_space.coinduced f (⨆ (i : ι), t i) = ⨆ (i : ι), topological_space.coinduced f (t i)
theorem
induced_compose
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[tγ : topological_space γ]
{f : α → β}
{g : β → γ} :
topological_space.induced f (topological_space.induced g tγ) = topological_space.induced (g ∘ f) tγ
theorem
induced_const
{α : Type u_1}
{β : Type u_2}
[t : topological_space α]
{x : α} :
topological_space.induced (λ (y : β), x) t = ⊤
theorem
coinduced_compose
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[tα : topological_space α]
{f : α → β}
{g : β → γ} :
topological_space.coinduced g (topological_space.coinduced f tα) = topological_space.coinduced (g ∘ f) tα
@[protected, instance]
Equations
@[protected, instance]
Equations
- subsingleton.unique_topological_space = {to_inhabited := {default := ⊥}, uniq := _}
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem
le_generate_from
{α : Type u}
{t : topological_space α}
{g : set (set α)}
(h : ∀ (s : set α), s ∈ g → is_open s) :
theorem
le_induced_generate_from
{α : Type u_1}
{β : Type u_2}
[t : topological_space α]
{b : set (set β)}
{f : α → β}
(h : ∀ (a : set β), a ∈ b → is_open (f ⁻¹' a)) :
This construction is left adjoint to the operation sending a topology on α
to its neighborhood filter at a fixed point a : α.
Equations
- nhds_adjoint a f = {is_open := λ (s : set α), a ∈ s → s ∈ f, is_open_univ := _, is_open_inter := _, is_open_sUnion := _}
theorem
gc_nhds
{α : Type u}
(a : α) :
galois_connection (nhds_adjoint a) (λ (t : topological_space α), 𝓝 a)
theorem
is_open_singleton_nhds_adjoint
{α : Type u_1}
{a b : α}
(f : filter α)
(hb : b ≠ a) :
is_open {b}
theorem
nhds_Inf
{α : Type u}
{s : set (topological_space α)}
{a : α} :
𝓝 a = ⨅ (t : topological_space α) (H : t ∈ s), 𝓝 a
theorem
continuous_iff_coinduced_le
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : topological_space α}
{t₂ : topological_space β} :
continuous f ↔ topological_space.coinduced f t₁ ≤ t₂
theorem
continuous_iff_le_induced
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : topological_space α}
{t₂ : topological_space β} :
continuous f ↔ t₁ ≤ topological_space.induced f t₂
theorem
continuous_generated_from
{α : Type u}
{β : Type v}
{f : α → β}
{t : topological_space α}
{b : set (set β)}
(h : ∀ (s : set β), s ∈ b → is_open (f ⁻¹' s)) :
@[continuity]
theorem
continuous_induced_rng
{α : Type u}
{β : Type v}
{γ : Type u_1}
{f : α → β}
{g : γ → α}
{t₂ : topological_space β}
{t₁ : topological_space γ}
(h : continuous (f ∘ g)) :
theorem
continuous_induced_rng'
{α : Type u}
{β : Type v}
{γ : Type u_1}
[topological_space α]
[topological_space β]
[topological_space γ]
{g : γ → α}
(f : α → β)
(H : _inst_1 = topological_space.induced f _inst_2)
(h : continuous (f ∘ g)) :
theorem
continuous_coinduced_dom
{α : Type u}
{β : Type v}
{γ : Type u_1}
{f : α → β}
{g : β → γ}
{t₁ : topological_space α}
{t₂ : topological_space γ}
(h : continuous (g ∘ f)) :
theorem
continuous_le_dom
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ t₂ : topological_space α}
{t₃ : topological_space β}
(h₁ : t₂ ≤ t₁)
(h₂ : continuous f) :
theorem
continuous_le_rng
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : topological_space α}
{t₂ t₃ : topological_space β}
(h₁ : t₂ ≤ t₃)
(h₂ : continuous f) :
theorem
continuous_sup_dom
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ t₂ : topological_space α}
{t₃ : topological_space β}
(h₁ : continuous f)
(h₂ : continuous f) :
theorem
continuous_sup_rng_left
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : topological_space α}
{t₃ t₂ : topological_space β} :
continuous f → continuous f
theorem
continuous_sup_rng_right
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : topological_space α}
{t₃ t₂ : topological_space β} :
continuous f → continuous f
theorem
continuous_Sup_dom
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : set (topological_space α)}
{t₂ : topological_space β}
(h : ∀ (t : topological_space α), t ∈ t₁ → continuous f) :
theorem
continuous_Sup_rng
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : topological_space α}
{t₂ : set (topological_space β)}
{t : topological_space β}
(h₁ : t ∈ t₂)
(hf : continuous f) :
theorem
continuous_supr_dom
{α : Type u}
{β : Type v}
{f : α → β}
{ι : Sort u_2}
{t₁ : ι → topological_space α}
{t₂ : topological_space β}
(h : ∀ (i : ι), continuous f) :
theorem
continuous_supr_rng
{α : Type u}
{β : Type v}
{f : α → β}
{ι : Sort u_2}
{t₁ : topological_space α}
{t₂ : ι → topological_space β}
{i : ι}
(h : continuous f) :
theorem
continuous_inf_rng
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : topological_space α}
{t₂ t₃ : topological_space β}
(h₁ : continuous f)
(h₂ : continuous f) :
theorem
continuous_inf_dom_left
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ t₂ : topological_space α}
{t₃ : topological_space β} :
continuous f → continuous f
theorem
continuous_inf_dom_right
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ t₂ : topological_space α}
{t₃ : topological_space β} :
continuous f → continuous f
theorem
continuous_Inf_dom
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : set (topological_space α)}
{t₂ : topological_space β}
{t : topological_space α}
(h₁ : t ∈ t₁) :
continuous f → continuous f
theorem
continuous_Inf_rng
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : topological_space α}
{t₂ : set (topological_space β)}
(h : ∀ (t : topological_space β), t ∈ t₂ → continuous f) :
theorem
continuous_infi_dom
{α : Type u}
{β : Type v}
{f : α → β}
{ι : Sort u_2}
{t₁ : ι → topological_space α}
{t₂ : topological_space β}
{i : ι} :
continuous f → continuous f
theorem
continuous_infi_rng
{α : Type u}
{β : Type v}
{f : α → β}
{ι : Sort u_2}
{t₁ : topological_space α}
{t₂ : ι → topological_space β}
(h : ∀ (i : ι), continuous f) :
@[continuity]
@[continuity]
theorem
nhds_induced
{α : Type u}
{β : Type v}
[T : topological_space α]
(f : β → α)
(a : β) :
𝓝 a = filter.comap f (𝓝 (f a))
theorem
induced_iff_nhds_eq
{α : Type u}
{β : Type v}
[tα : topological_space α]
[tβ : topological_space β]
(f : β → α) :
tβ = topological_space.induced f tα ↔ ∀ (b : β), 𝓝 b = filter.comap f (𝓝 (f b))
theorem
map_nhds_induced_of_surjective
{α : Type u}
{β : Type v}
[T : topological_space α]
{f : β → α}
(hf : function.surjective f)
(a : β) :
filter.map f (𝓝 a) = 𝓝 (f a)
theorem
is_open_induced_eq
{α : Type u_1}
{β : Type u_2}
[t : topological_space β]
{f : α → β}
{s : set α} :
theorem
is_open_induced
{α : Type u_1}
{β : Type u_2}
[t : topological_space β]
{f : α → β}
{s : set β}
(h : is_open s) :
(topological_space.induced f t).is_open (f ⁻¹' s)
theorem
map_nhds_induced_eq
{α : Type u_1}
{β : Type u_2}
[t : topological_space β]
{f : α → β}
(a : α) :
theorem
map_nhds_induced_of_mem
{α : Type u_1}
{β : Type u_2}
[t : topological_space β]
{f : α → β}
{a : α}
(h : set.range f ∈ 𝓝 (f a)) :
filter.map f (𝓝 a) = 𝓝 (f a)
theorem
closure_induced
{α : Type u_1}
{β : Type u_2}
[t : topological_space β]
{f : α → β}
{a : α}
{s : set α} :
theorem
continuous_Prop
{α : Type u_1}
[topological_space α]
{p : α → Prop} :
continuous p ↔ is_open {x : α | p x}
theorem
is_open_iff_continuous_mem
{α : Type u_1}
[topological_space α]
{s : set α} :
is_open s ↔ continuous (λ (x : α), x ∈ s)
theorem
generate_from_Union
{α : Type u}
{ι : Sort v}
{f : ι → set (set α)} :
topological_space.generate_from (⋃ (i : ι), f i) = ⨅ (i : ι), topological_space.generate_from (f i)
theorem
generate_from_sUnion
{α : Type u}
{S : set (set (set α))} :
topological_space.generate_from (⋃₀S) = ⨅ (s : set (set α)) (H : s ∈ S), topological_space.generate_from s
theorem
generate_from_Union_is_open
{α : Type u}
{ι : Sort v}
(f : ι → topological_space α) :
topological_space.generate_from (⋃ (i : ι), {s : set α | (f i).is_open s}) = ⨅ (i : ι), f i
theorem
generate_from_Inter
{α : Type u}
{ι : Sort v}
(f : ι → topological_space α) :
topological_space.generate_from (⋂ (i : ι), {s : set α | (f i).is_open s}) = ⨆ (i : ι), f i
theorem
generate_from_Inter_of_generate_from_eq_self
{α : Type u}
{ι : Sort v}
(f : ι → set (set α))
(hf : ∀ (i : ι), {s : set α | (topological_space.generate_from (f i)).is_open s} = f i) :
topological_space.generate_from (⋂ (i : ι), f i) = ⨆ (i : ι), topological_space.generate_from (f i)