LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Basic stability of proper continuous maps

Statement

Let $X$ , $Y$ and $Z$ be topological spaces (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), with properness as in Proper continuous maps of topological spaces.

If $i : Z ↪ X$ is the inclusion of a closed subset, then $i$ is proper.
If $f : X \to Y$ and $g : Y \to Z$ are proper continuous maps, then the composite $g f : X \to Z$ is proper.
If $f : X \to Y$ is proper, $Y$ is Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not) and $u : Y^{'} \to Y$ is continuous, then the pullback $f^{'} : X \times_{Y} Y^{'} ⟶ Y^{'}, X \times_{Y} Y^{'} = {(x, y^{'}) \in X \times Y^{'} : f (x) = u (y^{'})},$ the subset carrying the subspace topology of the product (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace), is proper.
If $f : X \to Y$ is proper, then every fibre $f^{- 1} (y)$ is a compact subset of $X$ .
If $f : X \to Y$ is proper and $S \subseteq X$ is closed, then the restriction $f ∣_{S} : S \to Y$ is proper.
If $f : X \to Y$ is proper and $Y$ is locally compact Hausdorff (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space), then $f$ is a closed map: the image of every closed subset of $X$ is closed in $Y$ .

These are the stability properties consumed by the closed-support functor $f_{!}$ on this page; no choice principle is used in any of them.

Facts & Assumptions

Given: Topological spaces $X$ , $Y$ , $Z$ and $Y^{'}$ , continuous maps as in the Statement, and the intrinsic convention for compactness of subsets.

[F1]

A continuous $f : X \to Y$ is proper exactly when $f^{- 1} (K)$ is a compact subset of $X$ for every compact subset $K \subseteq Y$ (Proper continuous maps of topological spaces).

[F2]

A continuous map carries compact subsets to compact subsets: if $g$ is continuous and $K$ compact, then $g [K]$ is compact (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

[F3]

A closed subset of a compact space is a compact subset of it, and finitely many compact subsets have compact union (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

[F4]

A finite product of compact spaces is compact; in particular the binary product of two compact spaces is compact, and a one-point space is compact (A product of finitely many compact spaces is compact in the product topology).

[F5]

A space is Hausdorff exactly when its diagonal is closed in the product; here $Δ_{Y} \subseteq Y \times Y$ is the diagonal of $Y$ (A space is Hausdorff if and only if its diagonal is closed in the square carrying the product topology, The diagonal $Δ_{X} \subseteq X \times X$ , the diagonal map $δ_{X}$ , and the pairing $⟨ f, g ⟩$ of two maps).

[F6]

Compactness of subsets is intrinsic: a subset of a subspace carries the same subspace topology whether it is viewed inside the subspace or inside the ambient space, and this intrinsic reading agrees with the ambient reading by covers (A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F7]

The product topology is the initial topology for the projections, so a map into a product is continuous exactly when all its components are, and composites of continuous maps are continuous (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, The initial topology of a family of maps into spaces and the final topology of a family of maps out of spaces, and the subspace topology as the model initial topology, Continuity of a map of topological spaces at a point and globally).

[F8]

In a locally compact Hausdorff space every point has an open neighbourhood whose closure is compact, and every compact subset of a Hausdorff space is closed (In a locally compact Hausdorff space every point has a neighbourhood base of compact sets, every open subspace and every closed subspace is locally compact, every open set around a point contains an open set with compact closure inside it, and every compact set sits inside an open set with compact closure, In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones).

Proof

technique · direct

1.1givenF1F3F6

Closed inclusions are proper. Let $i : Z ↪ X$ be the inclusion of a closed subset and let $K \subseteq X$ be compact. Its preimage $K \cap Z$ is closed in the compact space $K$ , hence compact by [F3]. The topology on $K \cap Z$ induced from $Z$ is the same as that induced from $K$ or $X$ , by transitivity of subspace topology [F6]. Thus $i^{- 1} (K)$ is compact in $Z$ , and $i$ is proper by [F1].

1.2givenF1algebra

Composites of proper maps are proper. For $K \subseteq Z$ compact, $(g f)^{- 1} (K) = f^{- 1} (g^{- 1} (K))$ ; the set $g^{- 1} (K)$ is compact by [F1] applied to $g$ , and then its $f$ -preimage is compact by [F1] applied to $f$ . Hence $g f$ is proper.

1.3givenF1F4

Fibres of a proper map are compact. A one-point space is compact by [F4], so for each $y \in Y$ the preimage $f^{- 1} ({y})$ is compact by [F1].

1.4givenF1F3F6

Restrictions to closed subspaces are proper. Let $S \subseteq X$ be closed, and give $S$ its subspace topology. For a compact $K \subseteq Y$ one has $(f ∣_{S})^{- 1} (K) = f^{- 1} (K) \cap S$ . The set $f^{- 1} (K)$ is compact by [F1], and $f^{- 1} (K) \cap S$ is closed in the compact space $f^{- 1} (K)$ because $S$ is closed in $X$ ; hence $f^{- 1} (K) \cap S$ is a compact subset of $f^{- 1} (K)$ by [F3]. Its topology as a subset of $S$ agrees with its topology as a subset of $X$ by [F6], so $(f ∣_{S})^{- 1} (K)$ is a compact subset of $S$ and $f ∣_{S}$ is proper by [F1].

1.5givenF1F2F3F4F5F6F7

Properness is preserved by base change along a map into a Hausdorff space. Let $K \subseteq Y^{'}$ be compact and put $K_{0} = u [K]$ , a compact subset of $Y$ by [F2]. Then $f^{- 1} (K_{0})$ is compact by [F1], so the product $f^{- 1} (K_{0}) \times K$ is a compact subspace of $X \times Y^{'}$ by [F4]. The pairing $(f, u) : X \times Y^{'} \to Y \times Y$ is continuous by [F7], and $Δ_{Y}$ is closed in $Y \times Y$ by [F5]; hence $X \times_{Y} Y^{'} = (f, u)^{- 1} (Δ_{Y})$ is closed in $X \times Y^{'}$ , and its intersection with the subspace $f^{- 1} (K_{0}) \times K$ is closed in that compact space. Moreover this intersection is exactly $(f^{'})^{- 1} (K)$ : a pair $(x, y^{'})$ lies in $X \times_{Y} Y^{'}$ with $y^{'} \in K$ precisely when $f (x) = u (y^{'})$ and $y^{'} \in K$ , and then $u (y^{'}) \in K_{0}$ forces $x \in f^{- 1} (K_{0})$ , so $(f^{'})^{- 1} (K) = X \times_{Y} Y^{'} \cap (f^{- 1} (K_{0}) \times K)$ . By [F3] this is a compact subset of the product $X \times Y^{'}$ , and by [F6] its topology as a subset of $X \times_{Y} Y^{'}$ agrees with that as a subset of $X \times Y^{'}$ ; hence $f^{'}$ is proper by [F1].

1.6givenF1F2F3F8

Proper maps into locally compact Hausdorff spaces are closed. Let $f : X \to Y$ be proper with $Y$ locally compact Hausdorff, let $F \subseteq X$ be closed and let $y \in Y ∖ f [F]$ . By [F8] there is an open neighbourhood $V$ of $y$ whose closure $\overline{V}$ is compact. Then $f^{- 1} (\overline{V})$ is compact by [F1] and $F \cap f^{- 1} (\overline{V})$ is closed in it, hence compact by [F3]; its image under the continuous map $f$ is $f [F] \cap \overline{V}$ , which is compact by [F2] and closed in $Y$ by [F8]. Therefore $V ∖ (f [F] \cap \overline{V})$ is open in $Y$ , contains $y$ because $y \in V$ and $y \notin f [F]$ , and is disjoint from $f [F]$ : a point of it lies in $V$ , hence cannot lie in $f [F] ∖ \overline{V}$ , and it is disjoint from $f [F] \cap \overline{V}$ by construction. Hence $f [F]$ is closed.

2.1givenstep 1.1step 1.2step 1.3step 1.4step 1.5step 1.6∎

The six stability properties are established: claim 1 by step 1.1, claim 2 by step 1.2, claim 4 by step 1.3, claim 5 by step 1.4, claim 3 by step 1.5 and claim 6 by step 1.6. Every argument uses only the preimage form of properness [F1], the preservation of compactness under continuous maps [F2], closed-in-compact compactness [F3], finite products of compact spaces [F4], the closed-diagonal criterion [F5], the intrinsic subspace conventions [F6], the initial product topology [F7] and the locally compact Hausdorff basis of compact neighbourhoods [F8]; none of these selects points or open sets from an infinite family, so no choice principle is used.

Depends on

Used by

Dependency tree · two levels

54 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jean-Louis Verdier, Dualité dans la cohomologie des espaces localement compacts, Séminaire N. Bourbaki 1964–1966, exposé 300, pp. 337–349 (Novembre 1965) (standard reference, not scraped)
The Stacks Project, Cohomology of Sheaves (chapter 20): §16 cohomology on Hausdorff quasi-compact spaces and §18 proper base change in topology (standard reference, not scraped)