Chapter SchurRepresentation

import Definitions.Def_ChapterA
import Definitions.Def_ChapterA2
import Definitions.Def_ChapterA2b
import Definitions.Def_ChapterSchurIrreducible
import Mathlib


/-!
# Lemma 28 and Lemma 34 — Schur's lemma for unitary representations and for systems of
imprimitivity

Source: `book.tex`, chapter *"Real representations, CPT theorem and the relativistic
position operator"*, §*Schur Systems* (**Lemma 28**, "Schur's lemma for unitary
representations") and §*Systems of Imprimitivity* (**Lemma 34**, "Schur's lemma for systems
of imprimitivity").

Both lemmas are quoted in the book from the representation-theory literature, and the
`FORMALIZATION_ROADMAP.md` gap table lists them as `EXTERNAL` (not available in Mathlib).
`BookProof.ChapterSchurIrreducible` proves the underlying operator-theoretic statement —
the commutant of a topologically irreducible **normal** system is `ℂ · 1` — for an
arbitrary complex Hilbert space.  This file records the two named corollaries, by checking
in each case that the system in question *is* normal (closed under the adjoint):

* a **unitary representation**: the adjoint of `U g` is `U g⁻¹`, again in the system
  (`repSystem_isNormal`), so **Lemma 28** (`schur_unitary_representation`) follows;
* a **system of imprimitivity** `(U, π)`: besides the unitaries, the system contains the
  self-adjoint projections `π A`, which are their own adjoints
  (`imprimitivitySystem_isNormal`), so **Lemma 34** (`schur_imprimitivity`) follows.

Note that the book's proof of Lemma 34 goes through Mackey's imprimitivity theorem; the
proof here does not need it — the covariance relation `U g π A U g⁻¹ = π (g • A)` is not
used at all, only the fact that the generators' adjoints stay inside the system.  The
conclusions are also slightly stronger than the book's: *every* bounded operator commuting
with the system is a scalar, not only every normal one.

Everything is `sorry`-free and `axiom`-free.
-/

open scoped ComplexConjugate InnerProductSpace

namespace BookProof.ChapterSchurRepresentation

open BookProof.ChapterA BookProof.ChapterA BookProof.ChapterSchurIrreducible

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V]

/-! ## Unitaries as bounded operators -/

/-- A `ℂ`-linear isometric equivalence, read as a bounded operator. -/
noncomputable def uCLM (f : V ≃ₗᵢ[ℂ] V) : V →L[ℂ] V :=
  f.toContinuousLinearEquiv.toContinuousLinearMap

omit [CompleteSpace V] in
@[simp] theorem uCLM_apply (f : V ≃ₗᵢ[ℂ] V) (x : V) : uCLM f x = f x := rfl



/-! ## Lemma 28 — unitary representations -/

/-- The system of operators of a unitary representation `U : G →* (V ≃ₗᵢ[ℂ] V)`. -/
noncomputable def repSystem {G : Type*} [Group G] (U : G →* (V ≃ₗᵢ[ℂ] V)) : System ℂ V :=
  ⟨{T : V →L[ℂ] V | ∃ g : G, T = uCLM (U g)}⟩







/-! ## Lemma 34 — systems of imprimitivity -/

/-- The system of operators generated by a pair `(U, π)`: the unitaries `U g` of the
representation together with the self-adjoint projections `π A` of the
projection-valued measure (Def 31/32).  Only the operators matter here; the covariance
relation of Def 32 plays no role in Schur's lemma. -/
noncomputable def imprimitivitySystem {G : Type*} [Group G] {X : Type*}
    (U : G →* (V ≃ₗᵢ[ℂ] V)) (pvm : Set X → (V →L[ℂ] V)) : System ℂ V :=
  ⟨{T : V →L[ℂ] V | (∃ g : G, T = uCLM (U g)) ∨ ∃ A : Set X, T = pvm A}⟩





end BookProof.ChapterSchurRepresentation