module

public import Papers.OaiNearInclusionsVon.Helpers.MainRepresentation

/-! Commuting von Neumann algebras generated by the two factors of Sigma. -/

@[expose] public section

namespace Papers.OaiNearInclusionsVon

variable {H G J : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] [Group G] [Group J]

-- @node: unitary_rep_range_star
/-- For [a unitary representation of a group on a Hilbert space](hyp:ρ),
[taking adjoints leaves the set of represented operators unchanged](goal). -/
lemma unitary_rep_range_star (ρ : G →* unitary (H →L[ℂ] H)) :
    star (Set.range (fun g => (ρ g : H →L[ℂ] H))) =
      Set.range (fun g => (ρ g : H →L[ℂ] H)) := by
  have hinv (g : G) : (ρ g⁻¹ : H →L[ℂ] H) = star (ρ g : H →L[ℂ] H) := by
    rw [map_inv, ← Unitary.star_eq_inv, Unitary.coe_star]
  ext T
  change star T ∈ Set.range (fun g => (ρ g : H →L[ℂ] H)) ↔
    T ∈ Set.range (fun g => (ρ g : H →L[ℂ] H))
  constructor
  · rintro ⟨g, hg⟩
    exact ⟨g⁻¹, (hinv g).trans ((congrArg star hg).trans (star_star T))⟩
  · rintro ⟨g, rfl⟩
    exact ⟨g⁻¹, hinv g⟩

-- @node: unitaryRepVN
/-- For [a group](hyp:G), [a complex Hilbert space](hyp:H), and
[a unitary representation of that group on that space](hyp:ρ), the
[generated von Neumann algebra](goal) is the commutant of the commutant of the
represented operators. -/
noncomputable def unitaryRepVN (ρ : G →* unitary (H →L[ℂ] H)) : VonNeumannAlgebra H :=
  (commutantVN (Set.range (fun g => (ρ g : H →L[ℂ] H)))).commutant

-- @node: unitaryRepVN_carrier
/-- For [a unitary representation](hyp:ρ), [the operators in its generated von
Neumann algebra are exactly those in the double commutant of its range](goal). -/
lemma unitaryRepVN_carrier (ρ : G →* unitary (H →L[ℂ] H)) :
    (unitaryRepVN ρ : Set (H →L[ℂ] H)) =
      commutant (commutant (Set.range (fun g => (ρ g : H →L[ℂ] H)))) := by
  simp only [unitaryRepVN, VonNeumannAlgebra.coe_commutant]
  change Set.centralizer (StarSubalgebra.centralizer ℂ
    (Set.range (fun g => (ρ g : H →L[ℂ] H))) : Set (H →L[ℂ] H)) = _
  rw [StarSubalgebra.coe_centralizer, unitary_rep_range_star, Set.union_self]

-- @node: unitaryRepVN_mem
/-- For [a unitary representation](hyp:ρ) and [a group element](hyp:g),
[the represented operator belongs to the generated von Neumann algebra](goal). -/
lemma unitaryRepVN_mem (ρ : G →* unitary (H →L[ℂ] H)) (g : G) :
    (ρ g : H →L[ℂ] H) ∈ unitaryRepVN ρ := by
  rw [← SetLike.mem_coe, unitaryRepVN_carrier]
  intro T hT
  exact (hT _ ⟨g, rfl⟩).symm

-- @node: unitaryRepVN_commute
/-- For [two unitary representations](hyp:ρ,τ), if [every operator represented
by the first commutes with every operator represented by the second](hyp:h),
[an operator in the first generated von Neumann algebra](hyp:hX) and
[an operator in the second generated von Neumann algebra](hyp:hY)
[commute with each other](goal).

Two commutant arguments establish this without multiplying weak operator limits. -/
lemma unitaryRepVN_commute
    (ρ : G →* unitary (H →L[ℂ] H)) (τ : J →* unitary (H →L[ℂ] H))
    (h : ∀ g j, Commute (ρ g : H →L[ℂ] H) (τ j : H →L[ℂ] H))
    (X Y : H →L[ℂ] H) (hX : X ∈ unitaryRepVN ρ) (hY : Y ∈ unitaryRepVN τ) :
    Commute X Y := by
  rw [← SetLike.mem_coe, unitaryRepVN_carrier] at hX hY
  apply hY X
  rintro _ ⟨j, rfl⟩
  apply hX (τ j)
  rintro _ ⟨g, rfl⟩
  exact (h g j).eq

-- @node: unitaryRep_firstFactor
/-- For [a complex Hilbert space](hyp:H) and [a unitary representation of the
product of two free groups on that space](hyp:σ), the
[first-factor representation](goal) sends each free-group element to the operator
representing that element paired with the identity. -/
noncomputable def unitaryRep_firstFactor
    (σ : ProdGrp →* unitary (H →L[ℂ] H)) : FreeGrp →* unitary (H →L[ℂ] H) :=
  σ.comp (MonoidHom.inl FreeGrp FreeGrp)

-- @node: unitaryRep_secondFactor
/-- For [a complex Hilbert space](hyp:H) and [a unitary representation of the
product of two free groups on that space](hyp:σ), the
[second-factor representation](goal) sends each free-group element to the operator
representing the identity paired with that element. -/
noncomputable def unitaryRep_secondFactor
    (σ : ProdGrp →* unitary (H →L[ℂ] H)) : FreeGrp →* unitary (H →L[ℂ] H) :=
  σ.comp (MonoidHom.inr FreeGrp FreeGrp)

-- @node: unitaryRep_factor_ranges_commute
/-- For [a unitary representation of the product of two free groups](hyp:σ),
[an element of the first factor](hyp:g), and [an element of the second factor](hyp:h),
[the two represented factor operators commute](goal). -/
lemma unitaryRep_factor_ranges_commute
    (σ : ProdGrp →* unitary (H →L[ℂ] H)) (g h : FreeGrp) :
    Commute (unitaryRep_firstFactor σ g : H →L[ℂ] H)
      (unitaryRep_secondFactor σ h : H →L[ℂ] H) := by
  change (σ (g, 1) : H →L[ℂ] H) * (σ (1, h) : H →L[ℂ] H) =
    (σ (1, h) : H →L[ℂ] H) * (σ (g, 1) : H →L[ℂ] H)
  have he : (g, 1) * (1, h) = (1, h) * (g, 1) := by simp
  have hs : σ (g, 1) * σ (1, h) = σ (1, h) * σ (g, 1) := by
    rw [← map_mul, ← map_mul, he]
  exact congrArg (fun U : unitary (H →L[ℂ] H) => (U : H →L[ℂ] H))
    hs

-- @node: unitaryRep_factor_algebras_commute
/-- For [a unitary representation of the product of two free groups](hyp:σ),
if [one operator belongs to the von Neumann algebra generated by the first
factor](hyp:hX) and [another belongs to the algebra generated by the second
factor](hyp:hY), [these operators commute](goal). -/
lemma unitaryRep_factor_algebras_commute
    (σ : ProdGrp →* unitary (H →L[ℂ] H)) (X Y : H →L[ℂ] H)
    (hX : X ∈ unitaryRepVN (unitaryRep_firstFactor σ))
    (hY : Y ∈ unitaryRepVN (unitaryRep_secondFactor σ)) : Commute X Y :=
  unitaryRepVN_commute _ _ (unitaryRep_factor_ranges_commute σ) X Y hX hY

end Papers.OaiNearInclusionsVon