One-Step Quotient Split

Abstract

One orthogonal shell canonically splits successive Hilbert quotients.

Theorem 1.1 (One orthogonal shell gives a split quotient sequence).

$$\begin{array}{c}\forall k,H,S,E,\\ \mathrm{Hilbert}\left(k,H\right),\mathrm{HasOrthogonalProjection}\left(S\right),\mathrm{HasOrthogonalProjection}\left(E+S\right),\\ \mathrm{Complete}\left(E\right),S\perp E\Rightarrow \\ \mathrm{Injective}\left(\mathrm{shellEmbedding}\left(S,E\right)\right)\wedge \mathrm{Surjective}\left(\mathrm{stepMap}\left(S,E\right)\right)\wedge \\ \mathrm{range}\left(\mathrm{shellEmbedding}\left(S,E\right)\right)=\ker \left(\mathrm{stepMap}\left(S,E\right)\right)\wedge \\ (\forall e\in E,\mathrm{shellEmbedding}\left(S,E\right)(e)=\mathrm{class}\left(e,S\right))\wedge \\ (\forall e\in E,\mathrm{shellKernelEquiv}\left(S,E\right)(e)=\mathrm{shellEmbedding}\left(S,E\right)(e))\wedge \\ \mathrm{successiveQuotientShellEquiv}\left(S,E\right):\mathrm{Quotient}\left(E+S,S\right)\to E\wedge \\ \mathrm{quotientShellSplit}\left(S,E\right):\mathrm{Quotient}\left(H,S\right)\to L2Sum\left(E,\mathrm{Quotient}\left(H,E+S\right)\right)\wedge \\ (\forall e\in E,\mathrm{fst}\left(\mathrm{quotientShellSplit}\left(S,E\right)(\mathrm{shellEmbedding}\left(S,E\right)(e))\right)=e).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Completion/OneStepQuotientSplit.one_step_quotient_split_exact (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let S be the old visible subspace of a real-or-complex Hilbert space and E an orthogonal shell. The next visible space is constructed as E plus S, and both quotient maps are the canonical submodule quotient maps.

The shell map is injective, the step map is surjective, and the range of the former is exactly the kernel of the latter. The public computation rule sends e to its class modulo S.

The named kernel equivalence and second-isomorphism-law equivalence identify both the kernel and the literal successive quotient with E. The named Hilbert equivalence splits the old quotient as the L2 product of E and the next quotient, with E as its first coordinate.

The proof applies the repository’s canonical quotient-orthogonal isometry and Mathlib’s factor map, kernel formula, second isomorphism law, and orthogonal decomposition. No existing declaration combined all public clauses.

References

• Truth anchor: D5/S3/Quantum/Completion/OneStepQuotientSplit.one_step_quotient_split_exact
• Dependency: D5/S3/Quantum/Algebra/QuotientOrthogonalComplement