LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pendingjudge pass (gpt-6-luna)

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.

Open mapping theorem for Fréchet spaces

Statement

Assume the full Axiom of Choice. Let $E$ and $F$ be Fréchet spaces over $C$ and let $T : E \to F$ be a continuous, surjective, complex-linear map. Then $T$ is open: it sends every open subset of $E$ to an open subset of $F$ .

Statement references

Jean-Pierre Demailly, Complex Analytic and Differential Geometry, Chapter IX §1.B

Facts & Assumptions

Given: Full AC; Fréchet spaces $E, F$ ; and a continuous surjective complex-linear map $T : E \to F$ .

[A1]

Full AC is the set-choice postulate (The Axiom of Choice).

[F1]

A Fréchet space is a Hausdorff locally convex topological vector space with a countable seminorm basis and a compatible complete metric (Fréchet spaces used in analytic coherent cohomology).

[F2]

In a nonempty complete metric space, a countable closed cover has a member with nonempty interior (Baire category theorem for complete metric spaces).

Proof

1.1A1F1givenconstruct

Fix an open neighborhood $U$ of $0$ in $E$ . Since $E$ is metrizable and locally convex, choose an absolutely convex neighborhood $W_{0}$ whose closure is contained in $U$ . Choose a decreasing sequence of absolutely convex neighborhoods $W_{n}$ such that $W_{n} \subseteq 2^{- n} W_{0}$ and, for each of the first $n$ members $p_{1}, \dots, p_{n}$ of a defining countable seminorm family, $p_{j} (x) \leq 2^{- n}$ for all $x \in W_{n}$ . For each fixed $j$ , the seminorms of the tails are bounded by a convergent geometric series, so any series $\sum_{n \geq 1} x_{n}$ with $x_{n} \in W_{n}$ is Cauchy in the Fréchet topology and converges by completeness. Its partial sums lie in $W_{0}$ because $W_{0}$ is convex and balanced and $\sum_{n \geq 1} 2^{- n} = 1$ ; hence its limit lies in $\overline{W_{0}} \subset U$ .

2.1A1F1F2step 1.1algebra

For each $n$ , the neighborhoods $k W_{n}$ ( $k \geq 1$ ) cover $E$ , since every neighborhood of $0$ in a topological vector space is absorbing. Surjectivity gives $F = ⋃_{k \geq 1} k T (W_{n}) \subseteq ⋃_{k \geq 1} \overline{k T (W_{n})}$ . By [F2], some $\overline{k T (W_{n})}$ has nonempty interior; scaling shows $\overline{T (W_{n})}$ has nonempty interior. If $O_{n} \subseteq \overline{T (W_{n})}$ is a nonempty open set, then $O_{n} - O_{n}$ is an open neighborhood of $0$ contained in $\overline{T (W_{n}) - T (W_{n})} \subseteq \overline{T (2 W_{n})}$ ; scaling by $1 / 2$ gives a neighborhood $V_{n} \subseteq \overline{T (W_{n})}$ . Shrink $V_{n}$ so its diameter tends to $0$ in a compatible metric on $F$ .

3.1A1F1step 1.1step 2.1construct

Take $y_{1} \in V_{1}$ . If $y_{n} \in V_{n}$ , then $y_{n} \in \overline{T (W_{n})}$ , so choose $x_{n} \in W_{n}$ such that $y_{n + 1} : = y_{n} - T x_{n} \in V_{n + 1}$ . The series $x = \sum_{n \geq 1} x_{n}$ converges in $E$ and belongs to $U$ by step 1.1, while $y_{n} \to 0$ by the diameter choice. Continuity of $T$ gives $T x = \sum_{n \geq 1} T x_{n} = y_{1}$ . Hence $V_{1} \subseteq T (U)$ , so $T (U)$ is a neighborhood of $0$ .

4.1step 3.1givenalgebra∎

Let $O \subseteq E$ be open and choose any $y \in T (O)$ with $T x = y$ for some $x \in O$ . There is an open neighborhood $N$ of $0$ with $x + N \subseteq O$ . Step 3.1 gives a neighborhood $V$ of $0$ contained in $T (N)$ , so $y + V \subseteq T (O)$ . Every point of $T (O)$ is therefore interior, hence $T (O)$ is open and $T$ is open.

Open mapping theorem for Fréchet spaces

Statement

Statement references

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources