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.

Totally disconnected LCA groups have bases of compact open subgroups

Statement

Let $G$ be a totally disconnected (Totally disconnected spaces and totally separated spaces) locally compact Hausdorff abelian topological group (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not, Topological group: multiplication and inversion are continuous). Then every neighbourhood of $0$ contains a compact open subgroup of $G$ . More precisely:

(i) if $E \subseteq G$ is compact and open then there is a neighbourhood $W$ of $0$ with $W = - W$ and $E + W = E$ ;

(ii) if in addition $0 \in E$ , then $E$ contains a compact open subgroup of $G$ ;

(iii) such an $E$ is a finite union of open cosets of that subgroup.

No choice principle is used.

Facts & Assumptions

Given: A totally disconnected locally compact Hausdorff abelian group $G$ with identity $0$ .

[F1]

$G$ is totally disconnected: every connected component of $G$ is a singleton, and for $x \in G$ the component $C (x)$ is the largest connected subset of $G$ containing $x$ . Subsets carry the subspace topology, and connectedness of a subset is intrinsic: a subset $A$ of a subspace $Y \subseteq X$ is connected in $Y$ exactly when it is connected in $X$ . (Totally disconnected spaces and totally separated spaces, Connected components, quasicomponents, and totally disconnected spaces, 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)

[F2]

In a compact Hausdorff space, total disconnectedness and total separatedness agree: distinct points are separated by a clopen set. (For compact Hausdorff spaces, total disconnectedness and total separatedness are equivalent, Totally disconnected spaces and totally separated spaces)

[F3]

A compact Hausdorff space $X$ is compact if and only if every family of closed subsets of $X$ with the finite intersection property has nonempty total intersection. A set is clopen when it is both open and closed; finite unions and finite intersections of clopen sets are clopen, and arbitrary intersections of closed sets are closed. (A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection, Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison)

[F4]

In a locally compact Hausdorff space each neighbourhood contains a compact neighbourhood of its point (In a locally compact Hausdorff space every open set containing a point contains an open set containing it whose closure is compact and still inside; such a space is regular); and a compact subset of a Hausdorff space is closed. A closed subset of a compact space is compact; compactness of a subset is a property of the ambient space. (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space, Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open, 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, A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact, 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)

[F5]

Addition $G \times G \to G$ and inversion $G \to G$ are continuous, and for fixed $a \in G$ the translations $x \mapsto a + x$ and $x \mapsto x + a$ are homeomorphisms carrying open sets to open sets. (Topological group: multiplication and inversion are continuous, Left and right translations and inversion in a topological group are homeomorphisms, 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, Continuity of a map of topological spaces at a point and globally)

[F6]

The cosets of a subgroup $F \leq G$ partition $G$ ; a subset $E \subseteq G$ satisfying $f + E = E$ for every $f \in F$ is a union of cosets of $F$ . A subgroup containing a neighbourhood of $0$ is open in $G$ . (Subgroup, Topological group: multiplication and inversion are continuous)

[F7]

A preimage of a closed set under a continuous map is closed; the interior of a subset is open; a set open in the subspace $N$ has the form $N \cap O$ with $O$ open in $G$ . (Continuity of a map of topological spaces at a point and globally, For $A \subseteq S \subseteq X$ the closure of $A$ in $S$ is ${\overline{A}}^{X} \cap S$ , while the interior only contains ${int}^{X} (A) \cap S$ , with equality when $S$ is open; and a dense subset of $X$ traces to a dense subset of every open $S$ , 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)

[F8]

If $U_{1}$ is open in $G$ and $U_{1} \subseteq N$ , a set open in $N$ and contained in $U_{1}$ is open in $G$ : if $V \subseteq N$ is open in $N$ and $V \subseteq U_{1}$ , say $V = N \cap O$ with $O$ open in $G$ , then $V = U_{1} \cap O$ is open in $G$ . (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, For $A \subseteq S \subseteq X$ the closure of $A$ in $S$ is ${\overline{A}}^{X} \cap S$ , while the interior only contains ${int}^{X} (A) \cap S$ , with equality when $S$ is open; and a dense subset of $X$ traces to a dense subset of every open $S$ )

Proof

1.1F2F3

In a compact Hausdorff totally disconnected space $X$ , let $U$ be an open neighbourhood of $x$ . Let $C$ be the family of all clopen sets containing $x$ . Total separatedness implies the open sets $X ∖ C$ , $C \in C$ , cover the compact set $X ∖ U$ : each $y \notin U$ is excluded by at least one such $C$ . A finite subcover gives $C_{1}, \dots, C_{n} \in C$ with $X ∖ U \subseteq ⋃_{j} (X ∖ C_{j})$ . Thus $V = ⋂_{j} C_{j}$ is clopen and $x \in V \subseteq U$ . If the complement is empty take $V = X$ . The family includes all separators, so no point-indexed choice is made.

1.2F5F7

Let $E \subseteq G$ be compact and open; if $E = \emptyset$ take $W : = G$ , which is symmetric and satisfies $E + W = \emptyset = E$ . Assume $E \neq \emptyset$ . The set $D : = {(x, y) \in E \times G : x + y \notin E}$ is closed in $E \times G$ : it is the trace on $E \times G$ of the preimage of the closed set $G ∖ E$ under the continuous addition map $G \times G \to G$ . It misses $E \times {0}$ because $x + 0 = x \in E$ for $x \in E$ . Consider the family $R$ of all pairs $(U, V)$ with $U$ open in $E$ , $V$ open in $G$ containing $0$ , and $U \times V$ disjoint from $D$ . The product topology and continuity ensure their first coordinates cover $E$ , without choosing one rectangle for each point.

2.1F5step 1.2

Compactness gives finitely many pairs $(U_{j}, V_{j}) \in R$ whose first coordinates cover $E$ . Put $W_{0} = ⋂_{j} V_{j}$ and $W = W_{0} \cap (- W_{0})$ . Then $W$ is a symmetric open neighbourhood of $0$ , and each $x \in E$ , $w \in W$ belongs to some admissible rectangle, giving $x + w \in E$ . Since $0 \in W$ , $E + W = E$ , proving (i). Only a finite subfamily of the specified family was selected.

2.2F1F4F8step 1.1

Let $U$ be a neighbourhood of $0$ in $G$ . Choose an open neighbourhood $U_{0} \subseteq U$ of $0$ and a compact neighbourhood $N$ of $0$ with $N \subseteq U_{0}$ . Then $N$ is a compact Hausdorff space, and it is totally disconnected: for $x \in N$ the component of $x$ in $N$ is a connected subset of $G$ containing $x$ , hence is contained in the component $C (x) = {x}$ of $G$ . Applying step 1.1 in $N$ to the relatively open set $N \cap {i n t}_{G} (N) \cap U_{0}$ , which contains $0$ , we obtain a set $V$ that is clopen in $N$ with $0 \in V \subseteq {i n t}_{G} (N) \cap U_{0}$ .

3.1F6step 2.1

Now let $E$ be compact and open with $0 \in E$ , and let $W$ be as in step 2.1, so that $W = - W$ , $0 \in W$ and $E + W = E$ . Put $F : = {x \in G : x + E = E}$ . Then $F$ is a subgroup: if $x + E = E$ and $y + E = E$ then $(x + y) + E = x + (y + E) = x + E = E$ by associativity, and from $x + E = E$ we get $- x + E = - x + (x + E) = E$ ; certainly $0 \in F$ . Also $F \subseteq E$ , because for $x \in F$ one has $x = x + 0 \in x + E = E$ . Moreover $F \supseteq W$ : for $w \in W$ , both $E + w \subseteq E$ and $E - w \subseteq E$ hold, so $E + w = E$ , so $F$ contains the neighbourhood $W$ of $0$ and is therefore open; and $F$ is closed because ${x : x + E \subseteq E} = ⋂_{e \in E} (E - e)$ and ${x : E \subseteq x + E} = ⋂_{e \in E} (e - E)$ are intersections of translates of the closed set $E$ , hence closed, and $F$ is their intersection. Being a closed subset of the compact set $E$ , the subgroup $F$ is compact. Thus $F$ is a compact open subgroup of $G$ contained in $E$ , proving (ii).

3.2F8step 2.2

The set $V$ of step 2.2 is compact in $G$ : it is closed in $N$ and $N$ is compact. It is open in $G$ : being open in $N$ it has the form $V = N \cap O$ with $O$ open in $G$ , and $V \subseteq {i n t}_{G} (N)$ , so the criterion of [F8] applies with $U_{1} : = {i n t}_{G} (N)$ and $V = U_{1} \cap O$ . Thus $V$ is a compact open subset of $G$ with $0 \in V \subseteq U$ .

4.1F6step 3.1

Since $E$ is a union of cosets of the subgroup $F$ (for $f \in F$ one has $f + E = E$ ) and $F$ is open, each coset is open and the cosets partition $E$ ; compactness of $E$ makes this open cover of $E$ finite, so $E$ is a finite union of open cosets of $F$ . This proves (iii).

5.1step 3.2step 3.1step 2.1step 4.1∎

Applying step 3.1 to the compact open set $E : = V$ of step 3.2, which contains $0$ and is contained in $U$ , produces a compact open subgroup $F_{0} \subseteq V \subseteq U$ . As $U$ was an arbitrary neighbourhood of $0$ , every neighbourhood of $0$ contains a compact open subgroup of $G$ ; together with parts (i), (ii) and (iii) proved in steps 2.1, 3.1 and 4.1 this is the statement.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

61 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

T. W. Koerner, Topological Groups (author lecture notes) (standard reference, not scraped)