Exact source: MathlibAnnex/Analysis/CStarAlgebra/CyclicTransport.lean
Pinned GitHub source · Raw UTF-8 source
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.Cyclic2import MathlibAnnex.Analysis.InnerProductSpace.DenseTransport34/-!5# Pointed cyclic transport67Equality of vector states gives equality of the full orbit Gram kernel. The8dense transport theorem then supplies a unique unitary carrying orbit to9orbit; multiplication yields intertwining on the dense cyclic subspace and10continuity extends it everywhere.11-/1213set_option autoImplicit false1415open scoped InnerProduct1617namespace StarAlgHom1819variable {A H K : Type*}20variable [CStarAlgebra A]21variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]22variable [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]2324theorem existsUnique_pointedCyclicTransport25 (π : 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) := by33 have hgram : ∀ a b, inner ℂ ((orbitMap π ξ) a) ((orbitMap π ξ) b) =34 inner ℂ ((orbitMap σ η) a) ((orbitMap σ η) b) := by35 intro a b36 simp only [orbitMap]37 have hπadj : ContinuousLinearMap.adjoint (π a) = π (star a) := by38 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star]39 have hσadj : ContinuousLinearMap.adjoint (σ a) = σ (star a) := by40 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star]41 have hπmul : π (star a * b) ξ = π (star a) (π b ξ) := by42 rw [map_mul]43 rfl44 have hσmul : σ (star a * b) η = σ (star a) (σ b η) := by45 rw [map_mul]46 rfl47 calc48 inner ℂ (π a ξ) (π b ξ) = inner ℂ ξ (π (star a * b) ξ) := by49 rw [← ContinuousLinearMap.adjoint_inner_right]50 rw [hπadj, hπmul]51 _ = inner ℂ η (σ (star a * b) η) := hstate _52 _ = inner ℂ (σ a η) (σ b η) := by53 rw [← ContinuousLinearMap.adjoint_inner_right]54 rw [hσadj, hσmul]55 obtain ⟨W, hW, hWuniq⟩ := LinearMap.existsUnique_linearIsometryEquiv_of_inner_eq56 (orbitMap π ξ) (orbitMap σ η) hπ hσ hgram57 have hW' : ∀ a, W (π a ξ) = σ a η := by58 intro a59 have ha := hW a60 change W (π a ξ) = σ a η at ha61 exact ha62 have hintertwine : ∀ a,63 (W : H →L[ℂ] K).comp (π a) = (σ a).comp (W : H →L[ℂ] K) := by64 intro a65 apply ContinuousLinearMap.ext66 intro x67 exact hπ.induction_on x (isClosed_eq68 ((W : H →L[ℂ] K).comp (π a)).continuous69 ((σ a).comp (W : H →L[ℂ] K)).continuous) fun b ↦ by70 change W (π a (π b ξ)) = σ a (W (π b ξ))71 have hπmul : π (a * b) ξ = π a (π b ξ) := by72 rw [map_mul]73 rfl74 have hσmul : σ (a * b) η = σ a (σ b η) := by75 rw [map_mul]76 rfl77 calc78 W (π a (π b ξ)) = W (π (a * b) ξ) := congrArg W hπmul.symm79 _ = σ (a * b) η := hW' _80 _ = σ a (σ b η) := hσmul81 _ = σ a (W (π b ξ)) := congrArg (σ a) (hW' b).symm82 have hpoint : W ξ = η := by83 simpa using hW' (1 : A)84 refine ⟨W, ⟨hW', hpoint, hintertwine⟩, ?_⟩85 intro W' hW'86 exact hWuniq W' hW'.18788end StarAlgHom