Chapter AbelianCyclicCommutant

import Definitions.Def_ChapterAbelianCyclicModel
import Definitions.Def_ChapterSpectralCommutant
import Definitions.Def_ChapterAbelianGelfandModel
import Definitions.Def_ChapterLinftyMaximalAbelian
import Definitions.Def_ChapterLinftyMultiplication
import Mathlib


/-!
# The commutant of an arbitrary abelian algebra with a cyclic vector (plan GAP-2)

`ChapterSpectralCommutant` computes the commutant of the algebra generated by a
**single** normal operator with a cyclic vector: it is the unitary copy of `L∞(μ)`
acting by multiplication, so that algebra is maximal abelian.
`ChapterAbelianCyclicModel` removes the "single operator" restriction from the
*model*: an arbitrary unital `*`-representation `π : C(X, ℂ) →⋆ₐ[ℂ] (H →L[ℂ] H)`
with a cyclic unit vector is unitarily multiplication on `L²(μ)`.

This module removes it from the *commutant* computation as well, which is the von
Neumann level of the same statement:

* `conjRep` / `conjRepSymm` — conjugation by the unitary of the cyclic model;
* `repSet` — the represented algebra `{π(g) : g ∈ C(X, ℂ)} ⊆ B(H)`;
* `multModelRep` — the unitary copy inside `B(H)` of the multiplication algebra
  `L∞(μ)`;
* `centralizer_repSet` — HEADLINE: the **commutant** of `{π(g)}` is exactly that
  copy of `L∞(μ)`;
* `centralizer_multModelRep`, `bicommutant_repSet` — the copy is its own commutant,
  so the **von Neumann algebra generated by `{π(g)}`** (its bicommutant) is that
  same copy of `L∞(μ)`;
* `commutant_repSet_isCommutative` — the commutant is abelian: the algebra is
  **maximal abelian**;
* `abelian_algebra_maximal_abelian_of_cyclic` — the Gelfand form: for every
  representation `ρ` of a commutative unital C\*-algebra `A` with a cyclic unit
  vector, the commutant of `ρ(A)` is abelian and equals the bicommutant of `ρ(A)`,
  a unitary copy of `L∞(μ)` for a Borel probability measure `μ` on the character
  space of `A`.

Compared with `ChapterSpectralCommutant` no generator of the algebra is assumed:
`A` need not be singly generated, and no separability is used.

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

noncomputable section

open MeasureTheory Complex WeakDual

namespace BookProof.ChapterAbelianCyclicCommutant

open BookProof.ChapterLinftyMultiplication BookProof.ChapterLinftyMaximalAbelian
open BookProof.ChapterAbelianGelfandModel BookProof.ChapterSpectralCommutant
open BookProof.ChapterAbelianCyclicModel

section Rep

variable {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
  [MeasurableSpace X] [BorelSpace X]
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable (pi : C(X, ℂ) →⋆ₐ[ℂ] (H →L[ℂ] H)) (xi : H) (hcyc : DenseRange (repVec pi xi))

/-- Conjugation of an operator on `L²(μ)` by the unitary of the cyclic model. -/
def conjRep (S : Lp ℂ 2 (repMeasure pi xi) →L[ℂ] Lp ℂ 2 (repMeasure pi xi)) : H →L[ℂ] H :=
  ((cyclicRepUnitary pi xi hcyc).toLinearIsometry.toContinuousLinearMap).comp
    (S.comp ((cyclicRepUnitary pi xi hcyc).symm.toLinearIsometry.toContinuousLinearMap))

@[simp] theorem conjRep_apply
    (S : Lp ℂ 2 (repMeasure pi xi) →L[ℂ] Lp ℂ 2 (repMeasure pi xi)) (v : H) :
    conjRep pi xi hcyc S v
      = cyclicRepUnitary pi xi hcyc (S ((cyclicRepUnitary pi xi hcyc).symm v)) := rfl

/-- Conjugation of an operator on `H` back to `L²(μ)`. -/
def conjRepSymm (S : H →L[ℂ] H) :
    Lp ℂ 2 (repMeasure pi xi) →L[ℂ] Lp ℂ 2 (repMeasure pi xi) :=
  ((cyclicRepUnitary pi xi hcyc).symm.toLinearIsometry.toContinuousLinearMap).comp
    (S.comp ((cyclicRepUnitary pi xi hcyc).toLinearIsometry.toContinuousLinearMap))

@[simp] theorem conjRepSymm_apply (S : H →L[ℂ] H) (u : Lp ℂ 2 (repMeasure pi xi)) :
    conjRepSymm pi xi hcyc S u
      = (cyclicRepUnitary pi xi hcyc).symm (S (cyclicRepUnitary pi xi hcyc u)) := rfl







/-- The represented algebra `{π(g)} ⊆ B(H)`. -/
def repSet : Set (H →L[ℂ] H) := Set.range fun g : C(X, ℂ) => pi g

/-- The unitary copy of the multiplication algebra `L∞(μ)` inside `B(H)`. -/
def multModelRep : Set (H →L[ℂ] H) :=
  conjRep pi xi hcyc '' multAlgebra (repMeasure pi xi)













end Rep

/-! ## The Gelfand form -/

section Gelfand

variable {A : Type*} [CommCStarAlgebra A]
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]







end Gelfand

end BookProof.ChapterAbelianCyclicCommutant

end