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 := _}
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 := _}
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 := _}
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 := _}
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
Equations
- topological_space.has_le = {le := λ (t s : topological_space α), s.is_open ≤ t.is_open}
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 := _}
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.
A topological space is discrete if every set is open, that is,
its topology equals the discrete topology ⊥
.
Instances of this typeclass
- discrete_topology_bot
- subsingleton.discrete_topology
- empty.discrete_topology
- pempty.discrete_topology
- punit.discrete_topology
- bool.discrete_topology
- nat.discrete_topology
- int.discrete_topology
- additive.discrete_topology
- multiplicative.discrete_topology
- order_dual.discrete_topology
- subtype.discrete_topology
- sum.discrete_topology
- sigma.discrete_topology
- prod.discrete_topology
- Pi.discrete_topology
- add_subgroup.zmultiples.discrete_topology
- sign_type.discrete_topology
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 := _}
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 := _}
Equations
Equations
- subsingleton.unique_topological_space = {to_inhabited := {default := ⊥}, uniq := _}
Equations
Equations
Equations
Equations
Equations
Equations
Equations
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 := _}