OAI/Analysis/KadisonKastler/FreeHaarMap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.starAlgHom_range_map line 13
2. theorem OAI.KadisonKastler.map_haarPower line 23
3. theorem OAI.KadisonKastler.FreeHaarMoments.map line 31

   Source documentation

   Only preservation of the normalized trace is needed to transfer the alternating moment identities to the image algebra.

   theorem FreeHaarMoments.map {τ : FaithfulTracialState B} {σ : FaithfulTracialState C}
       {A : StarSubalgebra ℂ B} {w : unitary B} (h : FreeHaarMoments τ A w)
       (φ : B →⋆ₐ[ℂ] C) (hφ : ∀ b, σ.toLinearMap (φ b) = τ.toLinearMap b) :
       FreeHaarMoments σ (A.map φ) (Unitary.map (StarMonoidHom.ofClass φ) w) := by
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.FreeHaarMoments

4. theorem OAI.KadisonKastler.map_freeHaar_lift line 55

   Source documentation

   A commuting square of quotient maps transports a unitary lift and its free moments simultaneously.

   theorem map_freeHaar_lift {V W : Type*} [CStarAlgebra V] [CStarAlgebra W]
       {τ : FaithfulTracialState B} {σ : FaithfulTracialState C}
       (A : StarSubalgebra ℂ B) (π : V →⋆ₐ[ℂ] B) (α : V →⋆ₐ[ℂ] W)
       (ρ : W →⋆ₐ[ℂ] C) (φ : B →⋆ₐ[ℂ] C)
       (hφ : ∀ b, σ.toLinearMap (φ b) = τ.toLinearMap b)
       (hcomm : ∀ v, φ (π v) = ρ (α v))
       (hv : ∃ v : unitary V, FreeHaarMoments τ A
         (Unitary.map (StarMonoidHom.ofClass π) v)) :
       ∃ v : unitary V, FreeHaarMoments σ (A.map φ)
         (Unitary.map (StarMonoidHom.ofClass ρ)
           (Unitary.map (StarMonoidHom.ofClass α) v)) := by
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.FreeHaarMoments