Skip to content

Restricted products of topological spaces

23 fully proved

Pieces of a restricted product

DefinitionPiece of a restricted product supported in a finite set#✓fully proved

Let \((X_i)_{i \in \iota}\) be a family of types with subsets \(U_i \subseteq X_i\). For a finite set \(S\) of indices, the piece \(X_S\) is the set of tuples \(x \in \prod_{i \in \iota} X_i\) such that \(x_i \in U_i\) for every \(i \notin S\).

def XS (S : Finset ι) : Set ((i : ι) → X i) :=
  {x | ∀ i, i ∉ S → x i ∈ U i}
Used by 19
Used byContinuity of the map from the direct limit of the pieces · Continuity of the inclusion of pieces · Continuity of the chunk map · Continuity of the map to the direct limit of the pieces · Continuity of the transition maps of the pieces · Direct limit of the finite-support pieces · The map from the direct limit of the pieces to the restricted product · The restricted product is the direct limit of its finite-support pieces · Inclusion of pieces · Tuples restricted on a cofinite set lie in a piece · Every element of the restricted product lies in a piece · An element lies in the piece indexed by its support · The support lies in the index set of every piece containing the element · Chunk map of a piece · Forward map to the direct limit of the pieces · The forward map undoes the backward map · Transition maps of the pieces · Tuples in a piece are eventually in the \(U_i\) · The pieces grow with the finite set

TheoremThe pieces grow with the finite set#✓fully proved

Let \((X_i)_{i \in \iota}\) be a family of types with subsets \(U_i \subseteq X_i\), and for a finite set \(S\) of indices let \(X_S\) be the set of tuples \(x \in \prod_{i \in \iota} X_i\) with \(x_i \in U_i\) for every \(i \notin S\). If \(S \subseteq T\) are finite sets of indices, then \(X_S \subseteq X_T\).

theorem XS_mono {S T : Finset ι} (hST : S ⊆ T) : XS X U S ⊆ XS X U T
Uses 1 · Used by 2
Statement usesPiece of a restricted product supported in a finite set
Used byContinuity of the inclusion of pieces · Inclusion of pieces

TheoremEvery element of the restricted product lies in a piece#✓fully proved

Let \((X_i)_{i \in \iota}\) be sets with subsets \(U_i \subseteq X_i\), and let \(x\) be an element of the restricted product of the \(X_i\) with respect to the \(U_i\), that is, a tuple \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all but finitely many \(i\). Then there is a finite set \(S \subseteq \iota\) such that \(x_i \in U_i\) for all \(i \notin S\), that is, \(x\) lies in the piece \(X_S\).

theorem mem_XS_of_restricted (x : Πʳ i, [X i, U i]) :
    ∃ S : Finset ι, (x : (i : ι) → X i) ∈ XS X U S
Uses 1
Statement usesPiece of a restricted product supported in a finite set

DefinitionSupport of an element of a restricted product#✓fully proved

Let \((X_i)_{i \in \iota}\) be sets with subsets \(U_i \subseteq X_i\). The support of an element \(x\) of the restricted product of the \(X_i\) with respect to the \(U_i\) (a tuple with \(x_i \in U_i\) for all but finitely many \(i\)) is the finite set of indices \(i\) with \(x_i \notin U_i\).

noncomputable def supportFinset (x : Πʳ i, [X i, U i]) : Finset ι :=
  (eventually_cofinite.mp x.2).toFinset
Used by 5
Used byContinuity of the map to the direct limit of the pieces · An element lies in the piece indexed by its support · The support lies in the index set of every piece containing the element · Forward map to the direct limit of the pieces · The forward map undoes the backward map

TheoremAn element lies in the piece indexed by its support#✓fully proved

Let \((X_i)_{i \in \iota}\) be sets with subsets \(U_i \subseteq X_i\), let \(x\) be an element of the restricted product of the \(X_i\) with respect to the \(U_i\) (a tuple with \(x_i \in U_i\) for all but finitely many \(i\)), and let \(\operatorname{supp}(x)\) be the finite set of indices \(i\) with \(x_i \notin U_i\). Then \(x_i \in U_i\) for every \(i \notin \operatorname{supp}(x)\), that is, \(x\) lies in the piece \(X_{\operatorname{supp}(x)}\).

theorem mem_XS_support (x : Πʳ i, [X i, U i]) :
    (x : (i : ι) → X i) ∈ XS X U (supportFinset X U x)
Uses 2 · Used by 3
Statement usesPiece of a restricted product supported in a finite set · Support of an element of a restricted product
Used byContinuity 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

TheoremTuples in a piece are eventually in the \(U_i\)#✓fully proved

Let \((X_i)_{i \in \iota}\) be a family of types with subsets \(U_i \subseteq X_i\), and let \(S\) be a finite set of indices. If a tuple \(x \in \prod_{i \in \iota} X_i\) lies in the piece \(X_S\), that is, \(x_i \in U_i\) for every \(i \notin S\), then \(x_i \in U_i\) for all but finitely many indices \(i\).

In other words, \(x\) defines an element of the restricted product of the \(X_i\) with respect to the \(U_i\).

theorem XS_mem_restricted {S : Finset ι} {x : (i : ι) → X i}
    (hx : x ∈ XS X U S) : ∀ᶠ i in cofinite, x i ∈ U i
Uses 1 · Used by 3
Statement usesPiece of a restricted product supported in a finite set
Used byContinuity of the map from the direct limit of the pieces · The map from the direct limit of the pieces to the restricted product · The forward map undoes the backward map

TheoremThe support lies in the index set of every piece containing the element#✓fully proved

Let \((X_i)_{i \in \iota}\) be sets with subsets \(U_i \subseteq X_i\), and let \(x\) be an element of the restricted product of the \(X_i\) with respect to the \(U_i\) (a tuple with \(x_i \in U_i\) for all but finitely many \(i\)), with support \(\operatorname{supp}(x) = \{i : x_i \notin U_i\}\). If \(T \subseteq \iota\) is a finite set with \(x_i \in U_i\) for all \(i \notin T\), then \(\operatorname{supp}(x) \subseteq T\).

theorem supportFinset_le {T : Finset ι} {x : Πʳ i, [X i, U i]}
    (hx : (x : (i : ι) → X i) ∈ XS X U T) :
    supportFinset X U x ⊆ T
Uses 2 · Used by 2
Statement usesPiece of a restricted product supported in a finite set · Support of an element of a restricted product
Used byContinuity of the map to the direct limit of the pieces · The forward map undoes the backward map

Direct Limit Construction

DefinitionInclusion of pieces#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and for a finite set \(S \subseteq \iota\) let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\). For finite sets \(S \subseteq T\), the inclusion of pieces is the map \(X_S \to X_T\) sending each tuple \(x\) to itself.

def inclusionMap {S T : Finset ι} (h : S ⊆ T) :
    XS X U S → XS X U T :=
  fun ⟨x, hx⟩ => ⟨x, XS_mono X U h hx⟩
Uses 2 · Used by 2
Statement usesPiece of a restricted product supported in a finite set · The pieces grow with the finite set
Used byContinuity of the inclusion of pieces · Transition maps of the pieces

TheoremContinuity of the inclusion of pieces#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and for a finite set \(S \subseteq \iota\) let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\), with the subspace topology of the product topology. For finite sets \(S \subseteq T \subseteq \iota\), the inclusion map \(X_S \to X_T\) is continuous.

theorem continuous_inclusionMap {S T : Finset ι} (h : S ⊆ T) :
    Continuous (inclusionMap X U h)
Uses 3 · Used by 1
Statement usesPiece of a restricted product supported in a finite set · Inclusion of pieces
Proof usesThe pieces grow with the finite set
Used byContinuity of the transition maps of the pieces

DefinitionTransition maps of the pieces#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and for a finite set \(S \subseteq \iota\) let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\). For finite sets \(S \subseteq T\), the transition map \(X_S \to X_T\) of the direct system of pieces sends each tuple \(x\) to itself.

def transitionMaps :
    ∀ (S T : Finset ι), S ≤ T → XS X U S → XS X U T :=
  fun _ _ h => inclusionMap X U h
Uses 2 · Used by 8
Statement usesPiece of a restricted product supported in a finite set · Inclusion of pieces
Used byContinuity of the map from the direct limit of the pieces · Continuity of the map to the direct limit of the pieces · Continuity of the transition maps of the pieces · Direct limit of the finite-support pieces · The map from the direct limit of the pieces to the restricted product · The restricted product is the direct limit of its finite-support pieces · Forward map to the direct limit of the pieces · The forward map undoes the backward map

TheoremContinuity of the transition maps of the pieces#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and for a finite set \(S \subseteq \iota\) let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\), with the subspace topology of the product topology. For all finite sets \(S \subseteq T \subseteq \iota\), the transition map \(X_S \to X_T\) of the direct system of the pieces, which is the inclusion, is continuous.

theorem continuous_transitionMaps (S T : Finset ι) (h : S ≤ T) :
    Continuous (transitionMaps X U S T h)
Uses 3 · Used by 6
Statement usesPiece of a restricted product supported in a finite set · Transition maps of the pieces
Proof usesContinuity of the inclusion of pieces
Used byContinuity of the map from the direct limit of the pieces · Continuity of the map to the direct limit of the pieces · Direct limit of the finite-support pieces · The map from the direct limit of the pieces to the restricted product · Forward map to the direct limit of the pieces · The forward map undoes the backward map

AbbreviationDirect limit of the finite-support pieces#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and for a finite set \(S \subseteq \iota\) let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\), with the subspace topology of the product topology. The space \(\varinjlim_S X_S\) is the direct limit of the \(X_S\) over the finite subsets \(S\) of \(\iota\) ordered by inclusion, with the inclusions \(X_S \to X_T\) for \(S \subseteq T\) as transition maps: the quotient of the disjoint union of the \(X_S\) by the equivalence relation generated by identifying each \(x \in X_S\) with its image in \(X_T\), with the quotient topology.

abbrev DirectLimitXS :=
  TopologicalSpace.DirectLimit.Space
    (fun S : Finset ι => XS X U S)
    (transitionMaps X U)
    (continuous_transitionMaps X U)
Uses 4 · Used by 6
Statement usesPiece of a restricted product supported in a finite set · Continuity of the transition maps of the pieces · Transition maps of the pieces · Direct limit of topological spaces
Used byContinuity of the map from the direct limit of the pieces · Continuity of the map to the direct limit of the pieces · The map from the direct limit of the pieces to the restricted product · The restricted product is the direct limit of its finite-support pieces · Forward map to the direct limit of the pieces · The forward map undoes the backward map

TheoremThe cofinite filter lies below the principal filter of the complement of a finite set#✓fully proved

For every finite set \(S\) of indices in \(\iota\), the cofinite filter on \(\iota\) is less than or equal to the principal filter of the complement \(\iota \setminus S\); that is, \(\iota \setminus S\) belongs to the cofinite filter.

theorem cofinite_le_principal_compl (S : Finset ι) :
    cofinite ≤ principal ((↑S : Set ι)ᶜ)
Used by 1
Used byContinuity of the map from the direct limit of the pieces

Principal Pieces

TheoremTuples restricted on a cofinite set lie in a piece#✓fully proved

Let \((X_i)_{i \in \iota}\) be sets with subsets \(U_i \subseteq X_i\), and for a finite set \(F \subseteq \iota\) let \(X_F\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin F\). Let \(S \subseteq \iota\) have finite complement. Then every tuple \(y \in \prod_i X_i\) with \(y_i \in U_i\) for all \(i \in S\) lies in \(X_{\iota \setminus S}\).

theorem inclusion_mem_XS_of_principal {S : Set ι}
    (hS : Filter.cofinite ≤ Filter.principal S)
    (y : Πʳ i, [X i, U i]_[Filter.principal S]) :
    (RestrictedProduct.inclusion X U hS y : (i : ι) → X i) ∈
      XS X U (Set.Finite.toFinset
        (Filter.eventually_cofinite.mp
          (hS (Filter.mem_principal.mpr (Set.Subset.refl S)))))
Uses 1 · Used by 1
Statement usesPiece of a restricted product supported in a finite set
Used byContinuity of the map to the direct limit of the pieces

Homeomorphism

DefinitionForward map to the direct limit of the pieces#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and let \(L\) be the direct limit, over finite sets \(S \subseteq \iota\), of the pieces \(X_S\) of tuples with \(x_i \in U_i\) for all \(i \notin S\). The forward map sends an element \(x\) of the restricted product of the \(X_i\) with respect to the \(U_i\) (a tuple with \(x_i \in U_i\) for all but finitely many \(i\)) to the class in \(L\) of \(x\), viewed in the piece \(X_{\operatorname{supp}(x)}\) indexed by its support \(\operatorname{supp}(x) = \{i : x_i \notin U_i\}\).

noncomputable def toDirectLimit (x : Πʳ i, [X i, U i]) : DirectLimitXS X U :=
  TopologicalSpace.DirectLimit.of (fun S : Finset ι => XS X U S)
    (transitionMaps X U) (continuous_transitionMaps X U)
    (supportFinset X U x)
    ⟨(x : (i : ι) → X i), mem_XS_support X U x⟩
Uses 7 · Used by 4
Statement usesDirect limit of the finite-support pieces · Piece of a restricted product supported in a finite set · Continuity of the transition maps of the pieces · An element lies in the piece indexed by its support · Support of an element of a restricted product · Transition maps of the pieces · Canonical map into the direct limit
Used byContinuity of the map to the direct limit of the pieces · The backward map undoes the forward map · The restricted product is the direct limit of its finite-support pieces · The forward map undoes the backward map

DefinitionThe map from the direct limit of the pieces to the restricted product#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and for a finite set \(S \subseteq \iota\) let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\), with the subspace topology of the product topology. The backward map sends the class in the direct limit \(\varinjlim_S X_S\) (over the finite subsets of \(\iota\)) of a tuple \(x \in X_S\) to \(x\), regarded as an element of the restricted product \(\prod'_i (X_i, U_i)\) with respect to the cofinite filter; the result does not depend on the representative.

noncomputable def fromDirectLimit : DirectLimitXS X U → Πʳ i, [X i, U i] :=
  TopologicalSpace.DirectLimit.lift (fun S : Finset ι => XS X U S)
    (transitionMaps X U) (continuous_transitionMaps X U)
    (fun S (x : ↥(XS X U S)) => ⟨x.val, XS_mem_restricted X U x.prop⟩)
    (fun _S _T _h _x => rfl)
Uses 6 · Used by 4
Statement usesDirect limit of the finite-support pieces · Piece of a restricted product supported in a finite set · Tuples in a piece are eventually in the \(U_i\) · Continuity of the transition maps of the pieces · Transition maps of the pieces · Map out of the direct limit
Used byContinuity of the map from the direct limit of the pieces · The backward map undoes the forward map · The restricted product is the direct limit of its finite-support pieces · The forward map undoes the backward map

TheoremThe backward map undoes the forward map#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and for a finite set \(S \subseteq \iota\) let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\). For every \(x\) in the restricted product \(\prod'_i (X_i, U_i)\) with respect to the cofinite filter, let \(S(x)\) be the finite set of indices \(i\) with \(x_i \notin U_i\). Sending \(x\) to its class in \(X_{S(x)}\) in the direct limit \(\varinjlim_S X_S\), and then sending that class to the tuple carried by its representative, returns \(x\).

This holds definitionally: unfolding both maps, the quotient lift applied to the canonical representative returns the representative itself.

theorem fromDirectLimit_toDirectLimit (x : Πʳ i, [X i, U i]) :
    fromDirectLimit X U (toDirectLimit X U x) = x
Uses 2 · Used by 1
Statement usesThe map from the direct limit of the pieces to the restricted product · Forward map to the direct limit of the pieces
Used byThe restricted product is the direct limit of its finite-support pieces

TheoremThe forward map undoes the backward map#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), let \(P\) be their restricted product (the tuples with \(x_i \in U_i\) for all but finitely many \(i\)), and let \(L\) be the direct limit, over finite sets \(S \subseteq \iota\), of the pieces \(X_S\) of tuples with \(x_i \in U_i\) for all \(i \notin S\). Let \(f : P \to L\) be the forward map, sending \(x\) to its class in the piece indexed by its support \(\{i : x_i \notin U_i\}\), and let \(g : L \to P\) be the backward map, sending a class to the tuple carried by any of its representatives. Then \(f(g(q)) = q\) for every \(q \in L\).

theorem toDirectLimit_fromDirectLimit (q : DirectLimitXS X U) :
    toDirectLimit X U (fromDirectLimit X U q) = q
Uses 14 · Used by 1
Statement usesDirect limit of the finite-support pieces · The map from the direct limit of the pieces to the restricted product · Forward map to the direct limit of the pieces
Proof usesPiece of a restricted product supported in a finite set · Tuples in a piece are eventually in the \(U_i\) · Continuity of the transition maps of the pieces · An element lies in the piece indexed by its support · Support of an element of a restricted product · The support lies in the index set of every piece containing the element · Transition maps of the pieces · Direct limit of topological spaces · Direct limit equivalence relation · Canonical map into the direct limit · Canonical maps commute with the transition maps
Used byThe restricted product is the direct limit of its finite-support pieces

DefinitionChunk map of a piece#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), let \(S \subseteq \iota\) be finite, and let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\). The chunk map sends each \(x \in X_S\) to the same tuple \(x\), viewed as an element of the restricted product of the \(X_i\) with respect to the \(U_i\) and the principal filter of \(\iota \setminus S\); this restricted product consists of the tuples whose \(i\)-th entry lies in \(U_i\) for every \(i \notin S\).

def toChunk (S : Finset ι) (x : ↥(XS X U S)) :
    Πʳ i, [X i, U i]_[Filter.principal ((↑S : Set ι)ᶜ)] :=
  RestrictedProduct.mk x.val (by
    rw [Filter.eventually_principal]
    intro i hi
    exact x.prop i (by simpa using hi))
Uses 1 · Used by 2
Statement usesPiece of a restricted product supported in a finite set
Used byContinuity of the map from the direct limit of the pieces · Continuity of the chunk map

TheoremContinuity of the chunk map#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), let \(S \subseteq \iota\) be finite, and let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\), with the subspace topology of the product topology. The map that sends \(x \in X_S\) to \(x\), viewed in the restricted product of the \((X_i, U_i)\) with respect to the principal filter of \(\iota \setminus S\) with its restricted product topology, is continuous.

theorem continuous_toChunk (S : Finset ι) : Continuous (toChunk X U S)
Uses 2 · Used by 1
Statement usesPiece of a restricted product supported in a finite set · Chunk map of a piece
Used byContinuity of the map from the direct limit of the pieces

TheoremContinuity of the map from the direct limit of the pieces#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and for a finite set \(S \subseteq \iota\) let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\), with the subspace topology of the product topology. The map from the direct limit \(\varinjlim_S X_S\) over the finite subsets of \(\iota\) to the restricted product \(\prod'_i (X_i, U_i)\) (with respect to the cofinite filter, with its restricted product topology) that sends the class of \(x \in X_S\) to \(x\) is continuous.

This follows from the universal property of the direct limit.

theorem continuous_fromDirectLimit : Continuous (fromDirectLimit X U)
Uses 11 · Used by 1
Statement usesDirect limit of the finite-support pieces · Piece of a restricted product supported in a finite set · The map from the direct limit of the pieces to the restricted product · Transition maps of the pieces · Direct limit equivalence relation
Proof usesTuples in a piece are eventually in the \(U_i\) · The cofinite filter lies below the principal filter of the complement of a finite set · Continuity of the chunk map · Continuity of the transition maps of the pieces · Chunk map of a piece · The induced map out of the direct limit is continuous
Used byThe restricted product is the direct limit of its finite-support pieces

TheoremContinuity of the map to the direct limit of the pieces#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and for a finite set \(S \subseteq \iota\) let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\), with the subspace topology of the product topology. The map from the restricted product \(\prod'_i (X_i, U_i)\) (with respect to the cofinite filter, with its restricted product topology) to the direct limit \(\varinjlim_S X_S\) over the finite subsets of \(\iota\) that sends \(x\) to its class in \(X_{S(x)}\), where \(S(x)\) is the finite set of indices \(i\) with \(x_i \notin U_i\), is continuous.

This follows from the universal property of the restricted product topology.

theorem continuous_toDirectLimit : Continuous (toDirectLimit X U)
Uses 14 · Used by 1
Statement usesDirect limit of the finite-support pieces · Piece of a restricted product supported in a finite set · Forward map to the direct limit of the pieces · Transition maps of the pieces · Direct limit equivalence relation
Proof usesContinuity of the transition maps of the pieces · Tuples restricted on a cofinite set lie in a piece · An element lies in the piece indexed by its support · Support of an element of a restricted product · The support lies in the index set of every piece containing the element · Direct limit of topological spaces · Canonical map into the direct limit · Canonical maps commute with the transition maps · Canonical maps into the direct limit are continuous
Used byThe restricted product is the direct limit of its finite-support pieces

DefinitionThe restricted product is the direct limit of its finite-support pieces#✓fully proved

Let \((X_i)_{i \in \iota}\) be topological spaces with subsets \(U_i \subseteq X_i\), and for a finite set \(S \subseteq \iota\) let \(X_S\) be the set of tuples \(x \in \prod_i X_i\) with \(x_i \in U_i\) for all \(i \notin S\), with the subspace topology of the product topology. Let \(\prod'_i (X_i, U_i)\) be the restricted product with respect to the cofinite filter, with its restricted product topology, and for \(x\) in it let \(S(x)\) be the finite set of indices \(i\) with \(x_i \notin U_i\). The map sending \(x\) to its class in \(X_{S(x)}\) is a homeomorphism from \(\prod'_i (X_i, U_i)\) to the direct limit \(\varinjlim_S X_S\) over the finite subsets of \(\iota\) ordered by inclusion; its inverse sends the class of \(x \in X_S\) to \(x\).

noncomputable def homeomorph_directLimit :
    (Πʳ i, [X i, U i]) ≃ₜ DirectLimitXS X U where
  toFun := toDirectLimit X U
  invFun := fromDirectLimit X U
  left_inv := fromDirectLimit_toDirectLimit X U
  right_inv := toDirectLimit_fromDirectLimit X U
  continuous_toFun := continuous_toDirectLimit X U
  continuous_invFun := continuous_fromDirectLimit X U
Sources
  • ATLAS NumberTheoryI, Proposition 25.5.
Uses 10
Statement usesDirect limit of the finite-support pieces · Piece of a restricted product supported in a finite set · Continuity of the map from the direct limit of the pieces · Continuity of the map to the direct limit of the pieces · The map from the direct limit of the pieces to the restricted product · The backward map undoes the forward map · Forward map to the direct limit of the pieces · The forward map undoes the backward map · Transition maps of the pieces · Direct limit equivalence relation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.