Direct limits of topological spaces

DefinitionGenerating relation of a direct limit#✓fully proved

Let \((X_i)_{i \in I}\) be a family of topological spaces indexed by a preorder \(I\), with maps \(f_{ij} : X_i \to X_j\) for \(i \le j\) forming a directed system (\(f_{ii}\) is the identity and \(f_{jk} \circ f_{ij} = f_{ik}\) for \(i \le j \le k\)). This relation on the disjoint union \(\bigsqcup_{i \in I} X_i\) relates \((i, x)\) to \((j, f_{ij}(x))\) for all \(i \le j\) and \(x \in X_i\), and relates no other pairs.

def Rel [DirectedSystem X (fun ⦃i j⦄ (h : i ≤ j) => f i j h)] :
    (Σ i, X i) → (Σ i, X i) → Prop :=
  fun a b => ∃ (i j : ι) (h : i ≤ j) (x : X i),
    a = ⟨i, x⟩ ∧ b = ⟨j, f i j h x⟩

Used by 4

Used byDirect limit equivalence relation · Map out of the direct limit · The induced map out of the direct limit is continuous · Canonical maps commute with the transition maps

DefinitionDirect limit equivalence relation#✓fully proved

Let \((X_i)_{i \in I}\) be a family of topological spaces indexed by a preorder \(I\), with maps \(f_{ij} : X_i \to X_j\) for \(i \le j\) forming a directed system. This is the smallest equivalence relation on the disjoint union \(\bigsqcup_{i \in I} X_i\) that relates \((i, x)\) to \((j, f_{ij}(x))\) for all \(i \le j\) and \(x \in X_i\).

def directLimitSetoid
    [DirectedSystem X (fun ⦃i j⦄ (h : i ≤ j) => f i j h)] :
    Setoid (Σ i, X i) :=
  Relation.EqvGen.setoid (Rel X f)

Uses 1 · Used by 10

Statement usesGenerating relation of a direct limit

Used byMap out of the direct limit · The induced map out of the direct limit is continuous · Canonical map into the direct limit · Canonical maps commute with the transition maps · Canonical maps into the direct limit are continuous · Direct limit of topological spaces · Continuity of the map from the direct limit of the pieces · Continuity of the map to the direct limit of the pieces · The restricted product is the direct limit of its finite-support pieces · The forward map undoes the backward map

AbbreviationDirect limit of topological spaces#✓fully proved

Let \(I\) be a preorder, \((X_i)_{i \in I}\) a family of topological spaces, and \(f_{ij} : X_i \to X_j\) for \(i \le j\) continuous maps forming a directed system (\(f_{ii}\) is the identity and \(f_{jk} \circ f_{ij} = f_{ik}\) for \(i \le j \le k\)). The direct limit \(\varinjlim X_i\) is the quotient of the disjoint union \(\bigsqcup_{i \in I} X_i\) by the equivalence relation generated by \((i, x) \sim (j, f_{ij}(x))\) for \(i \le j\) and \(x \in X_i\), with the quotient topology of the disjoint union topology.

The directed-system laws and the continuity of the transition maps are hypotheses of the construction: the underlying quotient does not use them, but without them it need not be a direct limit of topological spaces.

abbrev Space {ι : Type*} [Preorder ι]
    (X : ι → Type*) [∀ i, TopologicalSpace (X i)]
    (f : ∀ i j, i ≤ j → X i → X j)
    [DirectedSystem X (fun ⦃i j⦄ (h : i ≤ j) => f i j h)]
    (_hf_cont : ∀ i j (h : i ≤ j), Continuous (f i j h)) : Type _ :=
  @Quotient (Σ i, X i) (directLimitSetoid X f)

Uses 1 · Used by 8

Statement usesDirect limit equivalence relation

Used byMap out of the direct limit · The induced map out of the direct limit is continuous · Canonical map into the direct limit · Canonical maps commute with the transition maps · Canonical maps into the direct limit are continuous · Continuity of the map to the direct limit of the pieces · Direct limit of the finite-support pieces · The forward map undoes the backward map

DefinitionCanonical map into the direct limit#✓fully proved

Let \((X_i)_{i \in I}\) be a directed system of topological spaces over a preorder \(I\) with continuous transition maps \(f_{ij} : X_i \to X_j\). For \(i \in I\), the canonical map \(\iota_i : X_i \to \varinjlim X_i\) into the direct limit sends \(x\) to the class of \((i, x)\).

def of [DirectedSystem X (fun ⦃i j⦄ (h : i ≤ j) => f i j h)]
    (hf_cont : ∀ i j (h : i ≤ j), Continuous (f i j h))
    (i : ι) (x : X i) : Space X f hf_cont :=
  @Quotient.mk' _ (directLimitSetoid X f) ⟨i, x⟩

Uses 2 · Used by 5

Statement usesDirect limit of topological spaces · Direct limit equivalence relation

Used byCanonical maps commute with the transition maps · Canonical maps into the direct limit are continuous · Continuity of the map to the direct limit of the pieces · Forward map to the direct limit of the pieces · The forward map undoes the backward map

TheoremCanonical maps into the direct limit are continuous#✓fully proved

Let \((X_i)_{i \in I}\) be a directed system of topological spaces over a preorder \(I\) with continuous transition maps \(f_{ij} : X_i \to X_j\). For every \(i \in I\), the canonical map \(\iota_i : X_i \to \varinjlim X_i\) into the direct limit is continuous.

theorem of_continuous
    [DirectedSystem X (fun ⦃i j⦄ (h : i ≤ j) => f i j h)]
    (hf_cont : ∀ i j (h : i ≤ j), Continuous (f i j h)) (i : ι) :
    Continuous (of X f hf_cont i)

Uses 3 · Used by 1

Statement usesDirect limit of topological spaces · Direct limit equivalence relation · Canonical map into the direct limit

Used byContinuity of the map to the direct limit of the pieces

TheoremCanonical maps commute with the transition maps#✓fully proved

Let \((X_i)_{i \in I}\) be a directed system of topological spaces over a preorder \(I\) with continuous transition maps \(f_{ij} : X_i \to X_j\). The canonical maps \(\iota_i : X_i \to \varinjlim X_i\) into the direct limit satisfy \(\iota_j(f_{ij}(x)) = \iota_i(x)\) for all \(i \le j\) and \(x \in X_i\).

theorem of_comp [DirectedSystem X (fun ⦃i j⦄ (h : i ≤ j) => f i j h)]
    (hf_cont : ∀ i j (h : i ≤ j), Continuous (f i j h))
    {i j : ι} (h : i ≤ j) (x : X i) :
    of X f hf_cont j (f i j h x) = of X f hf_cont i x

Uses 4 · Used by 2

Statement usesDirect limit of topological spaces · Canonical map into the direct limit

Proof usesGenerating relation of a direct limit · Direct limit equivalence relation

Used byContinuity of the map to the direct limit of the pieces · The forward map undoes the backward map

DefinitionMap out of the direct limit#✓fully proved

Let \((X_i)_{i \in I}\) be a directed system of topological spaces over a preorder \(I\) with continuous transition maps \(f_{ij} : X_i \to X_j\), and let \(Y\) be a topological space. A family of maps \(\psi_i : X_i \to Y\) with \(\psi_j(f_{ij}(x)) = \psi_i(x)\) for all \(i \le j\) and \(x \in X_i\) induces the map \(\varinjlim X_i \to Y\) from the direct limit that sends the class of \((i, x)\) to \(\psi_i(x)\).

TopologicalSpace.DirectLimit.lift · 16 lines

noncomputable def lift
    [DirectedSystem X (fun ⦃i j⦄ (h : i ≤ j) => f i j h)]
    (hf_cont : ∀ i j (h : i ≤ j), Continuous (f i j h))
    {Y : Type*} [TopologicalSpace Y]
    (ψ : ∀ i, X i → Y)
    (hψ_comp : ∀ i j (h : i ≤ j) (x : X i), ψ j (f i j h x) = ψ i x) :
    Space X f hf_cont → Y :=
  @Quotient.lift _ _ (directLimitSetoid X f) (fun σ => ψ σ.1 σ.2) <| by
    intro a b hab
    induction hab with
    | rel a b hr =>
      obtain ⟨i, j, h, x, rfl, rfl⟩ := hr
      exact (hψ_comp i j h x).symm
    | refl _ => rfl
    | symm _ _ _ ih => exact ih.symm
    | trans _ _ _ _ _ ih1 ih2 => exact ih1.trans ih2

Uses 3 · Used by 2

Statement usesGenerating relation of a direct limit · Direct limit of topological spaces · Direct limit equivalence relation

Used byThe induced map out of the direct limit is continuous · The map from the direct limit of the pieces to the restricted product

TheoremThe induced map out of the direct limit is continuous#✓fully proved

Let \((X_i)_{i \in I}\) be a directed system of topological spaces over a preorder \(I\) with continuous transition maps \(f_{ij} : X_i \to X_j\), and let \(Y\) be a topological space. If the maps \(\psi_i : X_i \to Y\) are continuous and satisfy \(\psi_j(f_{ij}(x)) = \psi_i(x)\) for all \(i \le j\) and \(x \in X_i\), then the induced map \(\varinjlim X_i \to Y\) from the direct limit, sending the class of \((i, x)\) to \(\psi_i(x)\), is continuous.

theorem lift_continuous
    [DirectedSystem X (fun ⦃i j⦄ (h : i ≤ j) => f i j h)]
    (hf_cont : ∀ i j (h : i ≤ j), Continuous (f i j h))
    {Y : Type*} [TopologicalSpace Y]
    (ψ : ∀ i, X i → Y)
    (hψ_cont : ∀ i, Continuous (ψ i))
    (hψ_comp : ∀ i j (h : i ≤ j) (x : X i), ψ j (f i j h x) = ψ i x) :
    Continuous (lift X f hf_cont ψ hψ_comp)

Uses 4 · Used by 1

Statement usesDirect limit of topological spaces · Direct limit equivalence relation · Map out of the direct limit

Proof usesGenerating relation of a direct limit

Used byContinuity of the map from the direct limit of the pieces

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.