Chapter GaugeShiftExample

import Definitions.Def_ChapterContinuityUnitaryInfinite
import Mathlib


/-!
# The book's gauge-symmetry example: lattice translations on `ℓ²(ℤ)`

`book.tex` 2281–2289: *"consider an infinite-dimensional discrete basis `{e_k}`
of an Hilbert space (indexed by the integer numbers `k`) and the gauge symmetry
group generated by the transformation `e_k → e_{k+1}`. There is no normalized
wave-function (and thus no probability measure) which is translation-invariant.
On the other hand, there is a translation-invariant subalgebra of the commutative
von Neumann algebra […] where the expectation value of each operator is the same
for an equivalence class of wave-functions defined up to a gauge symmetry."*

This is the concrete instance of the general statements of
`BookProof.ChapterGaugeIncompleteFixing`: a gauge fixing that is *comprehensive*
(the whole spectrum) and *incomplete* (the remnant gauge symmetry is faithful),
whose physical operators are gauge invariant while no vector of the Hilbert space
is.  The translations are the unitaries `shiftOp m` of
`BookProof.ChapterContinuityUnitaryInfinite`.

This module deliberately depends on the lattice-unitary chapter only, so that it
stays inside that independent part of the development (see `BUILD_COMPONENTS.md`).

Everything is `sorry`-free.
-/

open scoped InnerProductSpace

namespace BookProof.ChapterGaugeShiftExample

open ChapterContinuityUnitaryInfinite





















/-! ## The gauge generators are excluded from the commutative algebra

`book.tex` (~2296): *"We define gauge-fixing as unconstrained whenever the gauge
generators are necessarily excluded from the commutative von Neumann algebra and
thus do not impose constraints on the spectrum of the commutative algebra."*

In this concrete model the commutative von Neumann algebra of the gauge-fixing is
the algebra of the multiplication operators `velocityOp v`, diagonal in the basis
`{e_k}`; the points of its spectrum are the basis labels `k ∈ ℤ`.  The statements
below are the Hilbert-space form of the general theory of
`BookProof.ChapterGaugeUnconstrainedSpectrum`: the translations are *not*
multiplication operators, so they are excluded from the algebra, and they impose
no condition on the spectrum — they merely permute its points, all of which
survive. -/

/-- The basis vector `e_j` of `ℓ²(ℤ)`, i.e. the point `j` of the spectrum of the
commutative algebra. -/
noncomputable def basisVecL2 (j : ℤ) : L2Z := lp.single 2 j (1 : ℂ)













end BookProof.ChapterGaugeShiftExample