Inverse limits of topological spaces

DefinitionInverse limit as compatible tuples#✓fully proved

Let \(I\) be a preordered set, let \((X_i)_{i \in I}\) be a family of sets, and for every \(i \le j\) let \(f_{ij} \colon X_j \to X_i\) be a map. The inverse limit is the set of tuples \(x = (x_i)_{i \in I}\) in the product \(\prod_{i \in I} X_i\) such that \(f_{ij}(x_j) = x_i\) whenever \(i \le j\).

def carrier (f : ∀ ⦃i j : ι⦄, i ≤ j → X j → X i) : Set (∀ i, X i) :=
  { x | ∀ ⦃i j : ι⦄ (h : i ≤ j), f h (x j) = x i }

Sources

ATLAS NumberTheoryI, Definition 8.9.

Used by 4

Used byThe inverse limit is closed · The inverse limit of compact Hausdorff spaces is compact · Membership in the inverse limit · Elements of the inverse limit are compatible

TheoremMembership in the inverse limit#✓fully proved

Let \(I\) be a preordered set, let \((X_i)_{i \in I}\) be a family of sets, and for every \(i \le j\) let \(f_{ij} \colon X_j \to X_i\) be a map. A tuple \(x \in \prod_{i \in I} X_i\) lies in the inverse limit if and only if \(f_{ij}(x_j) = x_i\) for all \(i \le j\).

@[simp]
theorem mem_carrier_iff {f : ∀ ⦃i j : ι⦄, i ≤ j → X j → X i}
    {x : ∀ i, X i} :
    x ∈ carrier f ↔ ∀ ⦃i j : ι⦄ (h : i ≤ j), f h (x j) = x i

Uses 1

Statement usesInverse limit as compatible tuples

TheoremElements of the inverse limit are compatible#✓fully proved

Let \(I\) be a preordered set, let \((X_i)_{i \in I}\) be a family of sets, and for every \(i \le j\) let \(f_{ij} \colon X_j \to X_i\) be a map. If \(x = (x_i)_{i \in I}\) lies in the inverse limit, then \(f_{ij}(x_j) = x_i\) for all \(i \le j\).

theorem proj_compat {f : ∀ ⦃i j : ι⦄, i ≤ j → X j → X i}
    {x : ∀ i, X i} (hx : x ∈ carrier f) ⦃i j : ι⦄ (h : i ≤ j) :
    f h (x j) = x i

Uses 1

Statement usesInverse limit as compatible tuples

TheoremThe inverse limit is closed#✓fully proved

Let \(I\) be a preordered set, let \((X_i)_{i \in I}\) be a family of Hausdorff topological spaces, and for every \(i \le j\) let \(f_{ij} \colon X_j \to X_i\) be a continuous map. Then the inverse limit \(\{x \in \prod_{i \in I} X_i : f_{ij}(x_j) = x_i \text{ for all } i \le j\}\) is closed in the product \(\prod_{i \in I} X_i\).

Each equation \(f_{ij}(x_j) = x_i\) cuts out a closed set because \(X_i\) is Hausdorff, and the limit is the intersection of all of them.

theorem isClosed_carrier [∀ i, T2Space (X i)]
    {f : ∀ ⦃i j : ι⦄, i ≤ j → X j → X i}
    (hf : ∀ ⦃i j : ι⦄ (h : i ≤ j), Continuous (f h)) :
    IsClosed (carrier f)

Uses 1 · Used by 1

Statement usesInverse limit as compatible tuples

Used byThe inverse limit of compact Hausdorff spaces is compact

TheoremThe inverse limit of compact Hausdorff spaces is compact#✓fully proved

Let \(I\) be a preordered set, let \((X_i)_{i \in I}\) be a family of compact Hausdorff topological spaces, and for every \(i \le j\) let \(f_{ij} \colon X_j \to X_i\) be a continuous map. Then the inverse limit \(\{x \in \prod_{i \in I} X_i : f_{ij}(x_j) = x_i \text{ for all } i \le j\}\) is compact in the product \(\prod_{i \in I} X_i\).

It is a closed subset of a compact product.

theorem isCompact_carrier [∀ i, CompactSpace (X i)] [∀ i, T2Space (X i)]
    {f : ∀ ⦃i j : ι⦄, i ≤ j → X j → X i}
    (hf : ∀ ⦃i j : ι⦄ (h : i ≤ j), Continuous (f h)) :
    IsCompact (carrier f)

Uses 2

Statement usesInverse limit as compatible tuples

Proof usesThe inverse limit is closed

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.