TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Quotients of reflexive spaces are reflexive

Statement

Assume HB and the Axiom of Countable Choice ${A C}_{ω}$ . If $X$ is a real or complex reflexive Banach space and $Y \subseteq X$ is a closed linear subspace, then the quotient Banach space $X / Y$ is reflexive.

Facts & Assumptions

Given: HB, ${A C}_{ω}$ , a real or complex reflexive Banach space $X$ , and a closed scalar-linear subspace $Y \subseteq X$ .

[F1]

Reflexivity means that the canonical map $J_{X} : X \to X^{* *}$ is surjective, so every $x^{* *} \in X^{* *}$ is evaluation at a vector of $X$ (Reflexivity is surjectivity of the canonical map).

[F2]

For the quotient map $q : X \to X / Y$ , pullback is a scalar-linear isometric bijection $Q : (X / Y)^{*} \to Y^{⊥}$ , $Q h = h \circ q$ (The dual of a quotient is its annihilator).

[F3]

Under HB, every bounded scalar-linear functional on an arbitrary linear subspace of a real or complex normed space extends to the whole space without increasing its norm (Relative norm-preserving Hahn–Banach extension over the real and complex fields).

[F4]

Assuming ${A C}_{ω}$ , the quotient of a Banach space by a closed linear subspace is Banach for the quotient norm (A quotient of a Banach space by a closed subspace is Banach).

[F5]

HB is the real dominated-extension principle over ZF, while ${A C}_{ω}$ chooses from each supplied sequence of nonempty sets (The real dominated-extension principle as an additional hypothesis over ZF, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

Proof technique: extend a quotient-bidual functional and represent the extension in the reflexive ambient space.

1.1

Put $Z = X / Y$ and write $q : X \to Z$ for the quotient map. By [F4], under the assumed ${A C}_{ω}$ the normed quotient $Z$ is Banach. This includes $Y = X$ , when $Z = {0}$ , and $Y = {0}$ , when the quotient norm is the original norm.

F4F5given

1.2

Let $z^{* *} \in Z^{* *}$ be arbitrary. The isometric bijection $Q : Z^{*} \to Y^{⊥}$ from [F2] has a scalar-linear isometric inverse. Define $g : Y^{⊥} \to K$ by $g (u) = z^{* *} (Q^{- 1} u)$ . It is a bounded scalar-linear functional with $∥ g ∥ = ∥ z^{* *} ∥$ ; if $Y^{⊥} = {0}$ , both sides are zero.

F2givenalgebra

2.1

Apply [F3] under HB to the subspace $Y^{⊥} \subseteq X^{*}$ . There is $x^{* *} \in X^{* *}$ with $x^{* *} ∣_{Y^{⊥}} = g$ and $∥ x^{* *} ∥ = ∥ g ∥$ . Only this one supplied functional is extended; no family of extensions is chosen.

F3F5step 1.2

3.1

Reflexivity of $X$ supplies an $x \in X$ with $x^{* *} = J_{X} x$ . Put $z = q (x) \in Z$ .

F1step 2.1

4.1

For every $h \in Z^{*}$ , [F2] gives $Q h = h \circ q \in Y^{⊥}$ , and therefore $J_{Z} z (h) = h (q x) = Q h (x) = J_{X} x (Q h) = x^{* *} (Q h) = g (Q h) = z^{* *} (h)$ . Hence $J_{Z} z = z^{* *}$ . The calculation is scalar-linear over both fields and uses the bilinear evaluation convention, with no conjugation.

F2step 1.2step 2.1step 3.1

5.1

Since $z^{* *} \in Z^{* *}$ was arbitrary, $J_{Z}$ is surjective; together with the Banach conclusion in step 1.1, [F1] shows that $Z = X / Y$ is reflexive. When $Y = X$ , step 1.2 starts from the unique zero bidual functional and the same computation gives the zero representer; when $Y = 0$ , $Q$ is the usual identification and the computation reduces to ambient reflexivity. HB is spent only in step 2.1, and ${A C}_{ω}$ only in step 1.1.

F1F3F4step 1.1step 4.1∎

Source notes

Bühler–Salamon, Theorem 2.71(ii), printed pp. 91–92, gives the complete annihilator-extension computation. The proof above keeps its exact algebra but states the repository's weak-choice costs: the selected quotient- completeness theorem requires ${A C}_{ω}$ , while the extension from $Y^{⊥}$ to $X^{*}$ requires HB. It does not claim that the quotient map sends the ambient closed unit ball onto the quotient closed unit ball.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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

Bühler–Salamon, Functional Analysis (standard reference, not scraped)