Mathlib.Topology.Coherent

Module docstring

{"# Topology generated by its restrictions to subsets

We say that restrictions of the topology on X to sets from a family S generates the original topology, if either of the following equivalent conditions hold:

a set which is relatively open in each s ∈ S is open;
a set which is relatively closed in each s ∈ S is closed;
for any topological space Y, a function f : X → Y is continuous provided that it is continuous on each s ∈ S.

We use the first condition as the definition (see IsCoherentWith in Mathlib/Topology/Defs/Induced.lean), and provide the others as corollaries.

Main results

IsCoherentWith.of_seq: if X is a sequential space and S contains all sets of the form insert x (Set.range u), where u : ℕ → X is a sequence that converges to x, then we have IsCoherentWith S;
IsCoherentWith.isCompact_of_seq: specialization of the previous lemma to the case S = {K | IsCompact K}. "}

Topology.IsCoherentWith.isOpen_iff theorem

(hS : IsCoherentWith S) : IsOpen t ↔ ∀ s ∈ S, IsOpen ((↑) ⁻¹' t : Set s)

Full source

protected theorem isOpen_iff (hS : IsCoherentWith S) :
    IsOpenIsOpen t ↔ ∀ s ∈ S, IsOpen ((↑) ⁻¹' t : Set s) :=
  ⟨fun ht _ _ ↦ ht.preimage continuous_subtype_val, hS.1 t⟩

Characterization of Open Sets in Coherent Topology

Informal description

Let $X$ be a topological space and $S$ be a family of subsets of $X$. If the topology on $X$ is coherent with $S$ (i.e., generated by its restrictions to subsets in $S$), then a subset $t \subseteq X$ is open if and only if for every $s \in S$, the preimage of $t$ under the inclusion map $s \hookrightarrow X$ is open in $s$.

Topology.IsCoherentWith.isClosed_iff theorem

(hS : IsCoherentWith S) : IsClosed t ↔ ∀ s ∈ S, IsClosed ((↑) ⁻¹' t : Set s)

Full source

protected theorem isClosed_iff (hS : IsCoherentWith S) :
    IsClosedIsClosed t ↔ ∀ s ∈ S, IsClosed ((↑) ⁻¹' t : Set s) := by
  simp only [← isOpen_compl_iff, hS.isOpen_iff, preimage_compl]

Characterization of Closed Sets in Coherent Topology

Informal description

Let $X$ be a topological space and $S$ be a family of subsets of $X$. If the topology on $X$ is coherent with $S$, then a subset $t \subseteq X$ is closed if and only if for every $s \in S$, the preimage of $t$ under the inclusion map $s \hookrightarrow X$ is closed in $s$.

Topology.IsCoherentWith.continuous_iff theorem

{Y : Type*} [TopologicalSpace Y] {f : X → Y} (hS : IsCoherentWith S) : Continuous f ↔ ∀ s ∈ S, ContinuousOn f s

Full source

protected theorem continuous_iff {Y : Type*} [TopologicalSpace Y] {f : X → Y}
    (hS : IsCoherentWith S) :
    ContinuousContinuous f ↔ ∀ s ∈ S, ContinuousOn f s :=
  ⟨fun h _ _ ↦ h.continuousOn, fun h ↦ continuous_def.2 fun _u hu ↦ hS.isOpen_iff.2 fun s hs ↦
    hu.preimage <| (h s hs).restrict⟩

Characterization of Continuity in Coherent Topology

Informal description

Let $X$ be a topological space with topology coherent with a family of subsets $S$ (i.e., the topology is generated by its restrictions to subsets in $S$). For any topological space $Y$ and function $f \colon X \to Y$, $f$ is continuous if and only if for every $s \in S$, the restriction of $f$ to $s$ is continuous.

Topology.IsCoherentWith.of_continuous_prop theorem

(h : ∀ f : X → Prop, (∀ s ∈ S, ContinuousOn f s) → Continuous f) : IsCoherentWith S

Full source

theorem of_continuous_prop (h : ∀ f : X → Prop, (∀ s ∈ S, ContinuousOn f s) → Continuous f) :
    IsCoherentWith S where
  isOpen_of_forall_induced u hu := by
    simp only [continuousOn_iff_continuous_restrict, continuous_Prop] at *
    exact h _ hu

Characterization of Coherent Topology via Continuous Prop-Valued Functions

Informal description

Let $X$ be a topological space and $S$ a family of subsets of $X$. If for every function $f : X \to \text{Prop}$, the continuity of $f$ on each subset $s \in S$ implies the continuity of $f$ on $X$, then the topology on $X$ is coherent with $S$.

Topology.IsCoherentWith.of_isClosed theorem

(h : ∀ t : Set X, (∀ s ∈ S, IsClosed ((↑) ⁻¹' t : Set s)) → IsClosed t) : IsCoherentWith S

Full source

theorem of_isClosed (h : ∀ t : Set X, (∀ s ∈ S, IsClosed ((↑) ⁻¹' t : Set s)) → IsClosed t) :
    IsCoherentWith S :=
  ⟨fun _t ht ↦ isClosed_compl_iff.1 <| h _ fun s hs ↦ (ht s hs).isClosed_compl⟩

Closedness condition for coherence of topology with respect to a family of subsets

Informal description

Let $X$ be a topological space and $S$ a family of subsets of $X$. If for every subset $t \subseteq X$, the condition that $t \cap s$ is closed in $s$ for all $s \in S$ implies that $t$ is closed in $X$, then the topology on $X$ is coherent with $S$.

Topology.IsCoherentWith.enlarge theorem

{T} (hS : IsCoherentWith S) (hT : ∀ s ∈ S, ∃ t ∈ T, s ⊆ t) : IsCoherentWith T

Full source

protected theorem enlarge {T} (hS : IsCoherentWith S) (hT : ∀ s ∈ S, ∃ t ∈ T, s ⊆ t) :
    IsCoherentWith T :=
  of_continuous_prop fun _f hf ↦ hS.continuous_iff.2 fun s hs ↦
    let ⟨t, htT, hst⟩ := hT s hs; (hf t htT).mono hst

Enlargement of Coherent Topology Family

Informal description

Let $X$ be a topological space with topology coherent with a family of subsets $S$. If for every $s \in S$, there exists a subset $t \in T$ such that $s \subseteq t$, then the topology on $X$ is also coherent with the family $T$.

Topology.IsCoherentWith.mono theorem

{T} (hS : IsCoherentWith S) (hT : S ⊆ T) : IsCoherentWith T

Full source

protected theorem mono {T} (hS : IsCoherentWith S) (hT : S ⊆ T) : IsCoherentWith T :=
  hS.enlarge fun s hs ↦ ⟨s, hT hs, Subset.rfl⟩

Monotonicity of Coherent Topology Family

Informal description

Let $X$ be a topological space with topology coherent with a family of subsets $S$. If $S$ is a subset of another family $T$, then the topology on $X$ is also coherent with $T$.

Topology.IsCoherentWith.of_seq theorem

 [SequentialSpace X] (h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S) : IsCoherentWith S

Full source

/-- If `X` is a sequential space
and `S` contains each set of the form `insert x (Set.range u)`
where `u : ℕ → X` is a sequence and `x` is its limit,
then topology on `X` is generated by its restrictions to the sets of `S`. -/
lemma of_seq [SequentialSpace X]
    (h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insertinsert x (range u) ∈ S) :
    IsCoherentWith S := by
  refine of_isClosed fun t ht ↦ IsSeqClosed.isClosed fun u x hut hux ↦ ?_
  rcases isClosed_induced_iff.1 (ht _ (h hux)) with ⟨s, hsc, hst⟩
  rw [Subtype.preimage_val_eq_preimage_val_iff, Set.ext_iff] at hst
  suffices x ∈ s by specialize hst x; simp_all
  refine hsc.mem_of_tendsto hux <| Eventually.of_forall fun k ↦ ?_
  specialize hst (u k)
  simp_all

Coherence of Topology with Sequential Limits

Informal description

Let $X$ be a sequential topological space and $S$ a family of subsets of $X$. If for every sequence $u : \mathbb{N} \to X$ converging to a point $x \in X$, the set $\{x\} \cup \text{range}(u)$ belongs to $S$, then the topology on $X$ is generated by its restrictions to the subsets in $S$.

Topology.IsCoherentWith.isCompact_of_seq theorem

[SequentialSpace X] : IsCoherentWith {K : Set X | IsCompact K}

Full source

/-- A sequential space is compactly generated. -/
lemma isCompact_of_seq [SequentialSpace X] : IsCoherentWith {K : Set X | IsCompact K} :=
  of_seq fun _u _x hux ↦ hux.isCompact_insert_range

Topology Generated by Compact Subsets in Sequential Spaces

Informal description

Let $X$ be a sequential topological space. Then the topology on $X$ is generated by its restrictions to all compact subsets of $X$, i.e., a set is open in $X$ if and only if its intersection with every compact subset of $X$ is relatively open in that subset.

Topology.IsCoherentWith.of_nhds theorem

(h : ∀ x, ∃ s ∈ S, s ∈ 𝓝 x) : IsCoherentWith S

Full source

/-- If each point of the space has a neighborhood from the family `S`,
then the topology is generated by its restrictions to the sets of `S`. -/
lemma of_nhds (h : ∀ x, ∃ s ∈ S, s ∈ 𝓝 x) : IsCoherentWith S :=
  of_continuous_prop fun _f hf ↦ continuous_iff_continuousAt.2 fun x ↦
    let ⟨s, hsS, hsx⟩ := h x
    (hf s hsS).continuousAt hsx

Neighborhood Condition for Coherent Topology Generation

Informal description

Let $X$ be a topological space and $S$ a family of subsets of $X$. If every point $x \in X$ has a neighborhood in $S$ (i.e., for each $x$, there exists $s \in S$ such that $s$ is a neighborhood of $x$), then the topology on $X$ is generated by its restrictions to the sets in $S$.

Topology.IsCoherentWith.isCompact_of_weaklyLocallyCompact theorem

[WeaklyLocallyCompactSpace X] : IsCoherentWith {K : Set X | IsCompact K}

Full source

/-- A weakly locally compact space is compactly generated. -/
lemma isCompact_of_weaklyLocallyCompact [WeaklyLocallyCompactSpace X] :
    IsCoherentWith {K : Set X | IsCompact K} :=
  of_nhds exists_compact_mem_nhds

Topology Generation by Compact Subsets in Weakly Locally Compact Spaces

Informal description

For any weakly locally compact topological space $X$, the topology on $X$ is generated by its restrictions to all compact subsets of $X$. In other words, a set is open in $X$ if and only if its intersection with every compact subset of $X$ is relatively open in that subset.