Exact source: MathlibAnnex/Analysis/CStarAlgebra/CyclicTransport.lean, lines 24–86.
Back to Pointed unitary transport between trace-cyclic target representations · Back to An inequivalent GNS fiber has no residual common range
1import MathlibAnnex.Analysis.CStarAlgebra.Cyclic 2import MathlibAnnex.Analysis.InnerProductSpace.DenseTransport 3 4/-! 5# Pointed cyclic transport 6 7Equality of vector states gives equality of the full orbit Gram kernel. The 8dense transport theorem then supplies a unique unitary carrying orbit to 9orbit; multiplication yields intertwining on the dense cyclic subspace and 10continuity extends it everywhere. 11-/ 12 13set_option autoImplicit false 14 15open scoped InnerProduct 16 17namespace StarAlgHom 18 19variable {A H K : Type*} 20variable [CStarAlgebra A] 21variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 22variable [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 23 24theorem existsUnique_pointedCyclicTransport 25 (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) 26 (ξ : H) (η : K) 27 (hπ : DenseRange (orbitMap π ξ)) (hσ : DenseRange (orbitMap σ η)) 28 (hstate : ∀ a, inner ℂ ξ (π a ξ) = inner ℂ η (σ a η)) : 29 ∃! W : H ≃ₗᵢ[ℂ] K, 30 (∀ a, W (π a ξ) = σ a η) ∧ 31 W ξ = η ∧ 32 ∀ a, (W : H →L[ℂ] K).comp (π a) = (σ a).comp (W : H →L[ℂ] K) := by 33 have hgram : ∀ a b, inner ℂ ((orbitMap π ξ) a) ((orbitMap π ξ) b) = 34 inner ℂ ((orbitMap σ η) a) ((orbitMap σ η) b) := by 35 intro a b 36 simp only [orbitMap] 37 have hπadj : ContinuousLinearMap.adjoint (π a) = π (star a) := by 38 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star] 39 have hσadj : ContinuousLinearMap.adjoint (σ a) = σ (star a) := by 40 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star] 41 have hπmul : π (star a * b) ξ = π (star a) (π b ξ) := by 42 rw [map_mul] 43 rfl 44 have hσmul : σ (star a * b) η = σ (star a) (σ b η) := by 45 rw [map_mul] 46 rfl 47 calc 48 inner ℂ (π a ξ) (π b ξ) = inner ℂ ξ (π (star a * b) ξ) := by 49 rw [← ContinuousLinearMap.adjoint_inner_right] 50 rw [hπadj, hπmul] 51 _ = inner ℂ η (σ (star a * b) η) := hstate _ 52 _ = inner ℂ (σ a η) (σ b η) := by 53 rw [← ContinuousLinearMap.adjoint_inner_right] 54 rw [hσadj, hσmul] 55 obtain ⟨W, hW, hWuniq⟩ := LinearMap.existsUnique_linearIsometryEquiv_of_inner_eq 56 (orbitMap π ξ) (orbitMap σ η) hπ hσ hgram 57 have hW' : ∀ a, W (π a ξ) = σ a η := by 58 intro a 59 have ha := hW a 60 change W (π a ξ) = σ a η at ha 61 exact ha 62 have hintertwine : ∀ a, 63 (W : H →L[ℂ] K).comp (π a) = (σ a).comp (W : H →L[ℂ] K) := by 64 intro a 65 apply ContinuousLinearMap.ext 66 intro x 67 exact hπ.induction_on x (isClosed_eq 68 ((W : H →L[ℂ] K).comp (π a)).continuous 69 ((σ a).comp (W : H →L[ℂ] K)).continuous) fun b ↦ by 70 change W (π a (π b ξ)) = σ a (W (π b ξ)) 71 have hπmul : π (a * b) ξ = π a (π b ξ) := by 72 rw [map_mul] 73 rfl 74 have hσmul : σ (a * b) η = σ a (σ b η) := by 75 rw [map_mul] 76 rfl 77 calc 78 W (π a (π b ξ)) = W (π (a * b) ξ) := congrArg W hπmul.symm 79 _ = σ (a * b) η := hW' _ 80 _ = σ a (σ b η) := hσmul 81 _ = σ a (W (π b ξ)) := congrArg (σ a) (hW' b).symm 82 have hpoint : W ξ = η := by 83 simpa using hW' (1 : A) 84 refine ⟨W, ⟨hW', hpoint, hintertwine⟩, ?_⟩ 85 intro W' hW' 86 exact hWuniq W' hW'.1 87 88end StarAlgHom