TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

Amenability is stable under closed subgroups, quotients and extensions

Statement

Assume AC. Let $G$ be a locally compact Hausdorff group. (i) If $G$ is amenable, every closed subgroup $H \leq G$ is amenable. (ii) If $G$ is amenable and $N ⊴ G$ is closed normal, the Hausdorff quotient $G / N$ is amenable. (iii) If $N ⊴ G$ is closed normal and both $N$ and $G / N$ are amenable, then $G$ is amenable.

Facts & Assumptions

Given: AC, an LCH group $G$ , and the closed subgroup $H$ or closed normal subgroup $N$ appearing in each clause.

[A1]

AC is the choice-function principle (The Axiom of Choice).

[F1]

Every LCH group has a left Haar measure under AC; this applies to $G$ , a closed subgroup, and the closed-normal quotient once its LCH property is established (Existence of left and right Haar measures).

[F2]

A closed subspace of an LCH space is locally compact, and a subspace of a Hausdorff space is Hausdorff; subgroup operations inherit continuity from the ambient topological group, and the inclusion of a subspace is continuous (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, 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, Continuity of a map of topological spaces at a point and globally, Topological group: multiplication and inversion are continuous).

[F3]

For closed $N ⊴ G$ , the canonical projection $p : G \to G / N$ is open and the quotient is locally compact Hausdorff; every compact quotient subset has a compact lift (Compact lifts and averaging onto C_c(G/H)).

[F4]

The set of left cosets $G / N$ has the quotient group law and $p$ is a surjective homomorphism (Normal subgroup: invariance under conjugation, The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ , For $N ⊴ G$ , the cosets form a group with identity $N$ and inverse $(g N)^{- 1} = g^{- 1} N$ ).

[F5]

In a topological group multiplication and inversion are continuous, with the product topology on the square (Topological group: multiplication and inversion 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).

[F6]

$U C B (G)$ consists of actual bounded continuous functions, is translation invariant, and embeds isometrically into complex $L^{\infty}$ by the class map (Left-uniformly continuous bounded functions (UCB)).

[F7]

Amenability gives a positive complex-linear unital invariant mean on $L^{\infty}$ ; such a mean has norm one. Restricting along the isometric UCB class map gives a positive unital invariant mean on UCB, bounded by the sup norm (Amenable locally compact group, Left-invariant means on $L^{\infty}$ of a locally compact group, [F6]).

[F8]

Under AC, a left-invariant mean on UCB gives Reiter (P1), and Reiter (P1) implies amenability (An invariant mean produces a Reiter net, Amenability is equivalent to Reiter's condition (P1)).

[F9]

Under AC and for a fixed left Haar measure, amenability of an LCH group $K$ is equivalent to $1_{K} ≺ λ_{K}$ (The Hulanicki–Reiter weak containment criterion for amenability).

[F10]

Weak containment means uniform approximation of each diagonal coefficient on compact sets by finite sums of diagonal coefficients; this relation is transitive by approximating each of finitely many intermediate coefficients with error divided by their number (Weak containment of unitary representations).

[F11]

If $H$ is closed in $G$ , then the restriction of the left regular representation of $G$ to $H$ is weakly contained in the left regular representation of $H$ (Restriction of the regular representation to a closed subgroup).

[F12]

Under AC the left regular representation is a strongly continuous unitary representation; restricting its parameter to a subgroup with the subspace topology preserves these properties by composition with the continuous inclusion (Left and right regular unitary representations of an LCH group, The regular representations are unitary, strongly continuous, and the left one is faithful, 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, Continuity of a map of topological spaces at a point and globally).

[F13]

A continuous image of a compact space 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).

[F14]

A quotient map is continuous and surjective, and a map out of its target is continuous exactly when its composite with the quotient map is. A continuous open surjection is a quotient map (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection, A continuous open surjection, a continuous closed surjection, and a continuous surjection admitting a continuous section are all quotient maps, For a quotient map $q : X \to Y$ , a map out of $Y$ is continuous iff its composite with $q$ is; a continuous map on $X$ constant on the fibres of $q$ factors uniquely through $q$ ; and a composite of quotient maps is a quotient map).

[F15]

The product topology has a basis of open rectangles; a map into a product is continuous when its coordinate 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).

Proof

technique · direct

1.1F3F4F5F14F15construct

Fix a closed normal $N ⊴ G$ and let $p : G \to K : = G / N$ be the canonical projection with quotient topology. By [F3], $K$ is LCH Hausdorff and $p$ is open. The map $p$ is continuous and surjective by [F14]. The product map $p \times p : G \times G \to K \times K$ is continuous by the rectangle basis in [F15], is surjective since each of two cosets has a representative, and is open: every open subset of $G \times G$ is a union of open rectangles $U \times V$ , whose images are $p (U) \times p (V)$ and are open. Thus $p \times p$ is a quotient map by [F14]. The quotient group law [F4] gives $p \circ ι_{G} = ι_{K} \circ p$ and $p \circ m_{G} = m_{K} \circ (p \times p)$ . Since $G$ is a topological group [F5], both left-hand composites are continuous. The quotient-map continuity test [F14] therefore makes inversion $ι_{K}$ and multiplication $m_{K}$ continuous. Hence $K$ is a topological group.

1.2A1F1F2F9F10F11F12F13construct

Assume $G$ is amenable and let $H \leq G$ be closed. By [F2], $H$ is LCH Hausdorff with its inherited topological-group structure; fix left Haar measures on $G$ and $H$ using [A1, F1]. Hulanicki's criterion [F9] gives $1_{G} ≺ λ_{G}$ . If $Q \subseteq H$ is compact, its image under the continuous inclusion $H ↪ G$ is compact by [F13]. Restricting the coefficient approximations on that compact subset to $H$ shows $1_{H} ≺ λ_{G} ∣_{H}$ : for a scalar $z \in C$ , multiply the approximating vectors for the unit scalar by $z$ to approximate the constant coefficient $∣ z ∣^{2}$ . The restricted-regular-representation lemma [F11] and [F12] show that the restricted unitary representation is strongly continuous and give $λ_{G} ∣_{H} ≺ λ_{H}$ ; transitivity [F10] yields $1_{H} ≺ λ_{H}$ . A second application of [F9] to $H$ proves that $H$ is amenable.

1.3A1F1F3F6F7F8F14construct

Assume $G$ is amenable and $N ⊴ G$ is closed normal. Let $K = G / N$ and $p : G \to K$ . The quotient is LCH Hausdorff by [F3], and has a left Haar measure by [A1, F1]. Let $ν$ be an invariant mean on $L^{\infty} (G)$ and define $m_{K} (ψ) : = ν ([ψ \circ p])$ for $ψ \in U C B (K)$ . Pullback is an actual bounded continuous function. Surjectivity of $p$ gives $∥ ψ \circ p ∥_{\sup} = ∥ ψ ∥_{\sup}$ , and for $g \in G$ , $∥ L_{g} (ψ \circ p) - ψ \circ p ∥_{\sup} = ∥ L_{p (g)} ψ - ψ ∥_{\sup} .$ As $p$ is continuous, the right side tends to zero as $g \to e$ , so pullback maps UCB $(K)$ into UCB $(G)$ . It preserves complex linearity, positivity and the constant one. Thus [F7] and invariance of $ν$ make $m_{K}$ a mean on UCB $(K)$ ; for $k \in K$ choose $g$ with $p (g) = k$ , and the same identity shows $m_{K} (L_{k} ψ) = m_{K} (ψ)$ . By [F8], $K$ satisfies (P1) and is amenable.

1.4A1F1F6F7construct

Assume $N$ and $K = G / N$ are amenable. By [F1] fix left Haar measures, and by [F7] restrict their invariant $L^{\infty}$ means to obtain invariant means $m_{N}$ on UCB $(N)$ and $m_{K}$ on UCB $(K)$ , each with norm one. For $ϕ \in U C B (G)$ and $g \in G$ , define $ϕ_{g} (h) : = ϕ (g h)$ for $h \in N$ . For $n \in N$ and $h \in N$ , $L_{n} ϕ_{g} (h) = ϕ (g n^{- 1} h) = (L_{g n g^{- 1}} ϕ) (g h),$ so $∥ L_{n} ϕ_{g} - ϕ_{g} ∥_{\sup, N} \leq ∥ L_{g n g^{- 1}} ϕ - ϕ ∥_{\sup, G} \to 0$ as $n \to e$ in $N$ . Thus $ϕ_{g} \in U C B (N)$ . Set $F_{ϕ} (g) : = m_{N} (ϕ_{g})$ . For $γ \in G$ and $g \in G$ , $F_{ϕ} (γ^{- 1} g) = m_{N} ((L_{γ} ϕ)_{g})$ ; hence [F7] gives $∥ L_{γ} F_{ϕ} - F_{ϕ} ∥_{\sup, G} \leq ∥ L_{γ} ϕ - ϕ ∥_{\sup, G} \to 0$ as $γ \to e$ . Therefore $F_{ϕ} \in U C B (G)$ .

2.1F3F6F14step 1.4construct

For $n \in N$ , $ϕ_{g n} (h) = ϕ (g n h) = ϕ_{g} (n h) = L_{n^{- 1}} ϕ_{g} (h)$ ; invariance of $m_{N}$ gives $F_{ϕ} (g n) = F_{ϕ} (g)$ . Thus $F_{ϕ}$ is constant on the fibres of $p$ . By [F3] and [F14], it descends to a continuous function $ψ_{ϕ} : K \to C$ with $ψ_{ϕ} \circ p = F_{ϕ}$ . To verify $ψ_{ϕ} \in U C B (K)$ , fix $ε > 0$ . Since $F_{ϕ} \in U C B (G)$ , choose an identity neighbourhood $V$ in $G$ such that $∥ L_{γ} F_{ϕ} - F_{ϕ} ∥_{\sup, G} < ε$ for every $γ \in V$ . The set $p (V)$ is an identity neighbourhood in $K$ by openness of $p$ . For $k \in p (V)$ , take any representative $γ \in V$ with $p (γ) = k$ . Surjectivity of $p$ gives the exact equality $∥ L_{k} ψ_{ϕ} - ψ_{ϕ} ∥_{\sup, K} = ∥ L_{γ} F_{ϕ} - F_{ϕ} ∥_{\sup, G} < ε,$ so $ψ_{ϕ}$ is UCB. The argument uses a representative separately for each estimate and makes no global section choice.

3.1F7F8step 1.4step 2.1algebra∎

Define $M (ϕ) : = m_{K} (ψ_{ϕ})$ for $ϕ \in U C B (G)$ . The construction of $F_{ϕ}$ and descent are complex-linear in $ϕ$ , preserve pointwise nonnegativity, and send $1_{G}$ to $1_{K}$ ; therefore [F7] makes $M$ a positive complex-linear unital mean. For $γ \in G$ , $F_{L_{γ} ϕ} (g) = F_{ϕ} (γ^{- 1} g)$ , so $ψ_{L_{γ} ϕ} = L_{p (γ)} ψ_{ϕ}$ . Invariance of $m_{K}$ now gives $M (L_{γ} ϕ) = M (ϕ)$ . Thus $M$ is a left-invariant UCB mean on $G$ . By [F8], $G$ satisfies Reiter (P1) and is amenable.

Sources

BHV, Kazhdan's Property (T), Appendix G.2, Proposition G.2.2(i)–(ii) and complete proof (printed p. 451) gives quotient and extension inheritance by UCB pullback and fixed points. Appendix G.3, Corollary G.3.4 and Appendix F.1, Proposition F.1.10 with proof (printed pp. 457 and 426) give closed-subgroup inheritance through weak containment of the restricted regular representation. The local proof expands quotient pullback for the library's actual-function UCB and gives an independent UCB-mean averaging proof of the extension clause under its complex-mean convention.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

113 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

Bachir Bekka, Pierre de la Harpe and Alain Valette, Kazhdan's Property (T) (Cambridge University Press, 2008; author-hosted complete text) (standard reference, not scraped)