Transport and realization

Proof of Theorem 10.1

Conjugation preserves products and sums, so

The block identity is direct multiplication:

All listed invariants are determined by these transported blocks.

Back to statement · Read statement and proof side by side · Permalink · Source line 26 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 10.4

Every element of \(\Phi({\operatorname{Hull}}_{{\mathcal A}}(S))\) is a finite sum of vectors

so it belongs to \({\operatorname{Hull}}_{\varphi({\mathcal A})}(\Phi(S))\). Conversely, every generator \(\varphi(A)\Phi(s)\) equals \(\Phi(As)\), giving equality.

For the block formula, use intertwining and packet compatibility twice:

If \(\Phi\) is surjective and \({\operatorname{Hull}}_{{\mathcal A}}(S)=X\), the hull equality gives \(Y={\operatorname{Hull}}_{\varphi({\mathcal A})}(\Phi(S))\). If \(\Phi(S)\subseteq{\operatorname{Hull}}_{{\mathcal B}}(S')\), then \({\operatorname{Hull}}_{{\mathcal B}}(\Phi(S))\subseteq{\operatorname{Hull}}_{{\mathcal B}}(S')\), so \(S'\) generates \(Y\).

Back to statement · Read statement and proof side by side · Permalink · Source line 114 · Claim record · Lean coverage · Code · Worked examples

Proof of Proposition 10.5

Let \((\Phi,\varphi,\sigma):(X,{\mathcal A},{\mathcal P})\to(Y,{\mathcal B},{\mathcal Q})\) and \((\Psi,\psi,\tau):(Y,{\mathcal B},{\mathcal Q})\to(Z,{\mathcal C},{\mathcal R})\) be morphisms. Intertwining is preserved because

For \(k\) in the target packet set,

Thus the composite packet map is \(\tau\circ\sigma\). If the morphisms are seeded, then

By Theorem 10.4,

Identity maps satisfy the definitions with identity algebra and packet maps.

Back to statement · Read statement and proof side by side · Permalink · Source line 147 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 10.6

Restriction preserves idempotency, pairwise annihilation, and the identity sum on \(K\). If \(x\in K\cap X_\alpha\), then \(x=P_\alpha x\in P_\alpha K\), proving \(K_\alpha=K\cap X_\alpha\).

The quotient operator is well defined because replacing \(x\) by \(x+k\) changes \(P_\alpha x\) by \(P_\alpha k\in K\). The idempotent and annihilation identities descend, and the sum is the identity on \(X/K\). The map \(X_\alpha\to X/K\) has image \((X_\alpha+K)/K\) and kernel \(X_\alpha\cap K\), giving the short exact sequence and the quotient isomorphisms. Exact packet coordinates identify the original sequence with the direct sum over \(\alpha\).

Back to statement · Read statement and proof side by side · Permalink · Source line 221 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 10.7

All assertions are the quotient part of Theorem 10.6. The intertwining identity follows directly from the definition:

Back to statement · Read statement and proof side by side · Permalink · Source line 247 · Claim record · Lean coverage · Code · Worked examples

Proof of Corollary 10.8

If \(x\in K_\alpha\), then \(Tx\in K\), so

On the quotient,

Back to statement · Read statement and proof side by side · Permalink · Source line 269 · Claim record · Lean coverage · Code · Worked examples

Proof of Corollary 10.9

Closedness of \(K\) makes \(X/K\) Banach. The restricted projectors are bounded, and the quotient projectors are bounded because

The packet spaces are closed ranges of bounded idempotents.

Back to statement · Read statement and proof side by side · Permalink · Source line 292 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 10.10

Given \(y=\Phi(x)\), choose a net \(x_\lambda\in{\operatorname{Hull}}_{{\mathcal A}}(S)\) converging to \(x\). Then

and naturality places every \(\Phi(x_\lambda)\) in \({\operatorname{Hull}}_{{\mathcal B}}(\Phi(S))\). Hence the latter hull is dense. For packets, one inclusion follows from compatibility. Conversely, if \(y=Q_jy\), choose \(x\) with \(\Phi(x)=y\). Then

Back to statement · Read statement and proof side by side · Permalink · Source line 322 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 10.11

The algebraic first isomorphism theorem gives a bijection \(\widetilde\Phi\). By definition of the quotient topology, a set \(U\subseteq X/K\) is open exactly when its preimage in \(X\) is open. Because \(\Phi\) is a quotient map, this is equivalent to \(\widetilde\Phi(U)\) being open in \(Y\). Thus \(\widetilde\Phi\) is a homeomorphism. The second statement applies the dense completion argument of Theorem 3.6 to the injective map \(D/(D\cap K)\to Y\).

Back to statement · Read statement and proof side by side · Permalink · Source line 348 · Claim record · Lean coverage · Code · Worked examples

Proof of Theorem 11.2

Functoriality gives

and additivity gives

If the declared enrichment is present, linearity additionally gives \(F(af)=aF(f)\) for every coefficient \(a\). A structural induction on the construction of a morphism expression therefore carries every permitted equational proof to its image under \(F\). If a step invokes a universal construction, preservation means that the image diagram satisfies the same universal property. The uniquely induced morphism in the source proof is therefore carried to the uniquely induced morphism in the target proof. Repeating this argument through the finite proof diagram transports the conclusion.

Back to statement · Read statement and proof side by side · Permalink · Source line 408 · Claim record · Lean coverage · Code · Worked examples

Proof of Proposition 11.3

The first assertion is Theorem 11.2. The second is a logical boundary: a functor transports established identities and preserved universal constructions, but it does not create an unverified analytic, topological, positivity, finiteness, or integrality hypothesis.

Back to statement · Read statement and proof side by side · Permalink · Source line 439 · Claim record · Lean coverage · Code · Worked examples