Exact source: MathlibAnnex/Analysis/CStarAlgebra/State/ExtensionOfEmbedding.lean, lines 77–99.
Back to Extending the CAR trace to the fixed shell target
1import Mathlib.Analysis.Normed.Module.HahnBanach 2import Mathlib.Analysis.CStarAlgebra.Hom 3import MathlibAnnex.Analysis.CStarAlgebra.State.Extension 4 5/-! 6# Extending a normalized functional along a faithful C⋆-embedding 7 8The source functional is transported to the actual linear range of the 9embedding and extended by norm-preserving Hahn–Banach. No universal property 10of the codomain, and no existence of a codomain representation, is assumed. 11-/ 12 13set_option autoImplicit false 14 15open scoped ComplexOrder 16 17namespace MathlibAnnex.Analysis.CStarAlgebra 18 19universe u v 20 21variable {A : Type u} {D : Type v} [CStarAlgebra A] [CStarAlgebra D] 22 [PartialOrder D] [StarOrderedRing D] 23 24private noncomputable def rangePreimage (j : A →⋆ₐ[ℂ] D) 25 (x : LinearMap.range j.toLinearMap) : A := 26 Classical.choose x.property 27 28private theorem map_rangePreimage (j : A →⋆ₐ[ℂ] D) 29 (x : LinearMap.range j.toLinearMap) : j (rangePreimage j x) = x := 30 Classical.choose_spec x.property 31 32private noncomputable def rangeInverse (j : A →⋆ₐ[ℂ] D) 33 (hj : Function.Injective j) : LinearMap.range j.toLinearMap →ₗ[ℂ] A where 34 toFun := rangePreimage j 35 map_add' x y := by 36 apply hj 37 rw [map_add, map_rangePreimage, map_rangePreimage, map_rangePreimage] 38 rfl 39 map_smul' c x := by 40 apply hj 41 rw [map_smul, map_rangePreimage, map_rangePreimage] 42 rfl 43 44private theorem rangeInverse_map (j : A →⋆ₐ[ℂ] D) 45 (hj : Function.Injective j) (a : A) : 46 rangeInverse j hj ⟨j a, ⟨a, rfl⟩⟩ = a := by 47 apply hj 48 exact map_rangePreimage j _ 49 50private theorem norm_rangeInverse (j : A →⋆ₐ[ℂ] D) 51 (hj : Function.Injective j) (x : LinearMap.range j.toLinearMap) : 52 ‖rangeInverse j hj x‖ = ‖x‖ := by 53 calc 54 ‖rangeInverse j hj x‖ = ‖j (rangeInverse j hj x)‖ := 55 (NonUnitalStarAlgHom.norm_map j hj _).symm 56 _ = ‖x‖ := by rw [show j (rangeInverse j hj x) = (x : D) from 57 map_rangePreimage j x]; rfl 58 59private noncomputable def rangeFunctional (j : A →⋆ₐ[ℂ] D) 60 (hj : Function.Injective j) (τ : A →L[ℂ] ℂ) 61 (hτ : ∀ a, ‖τ a‖ ≤ ‖a‖) : LinearMap.range j.toLinearMap →L[ℂ] ℂ := 62 (τ.toLinearMap.comp (rangeInverse j hj)).mkContinuous 1 fun x ↦ by 63 change ‖τ (rangeInverse j hj x)‖ ≤ 1 * ‖x‖ 64 rw [one_mul, ← norm_rangeInverse j hj x] 65 exact hτ (rangeInverse j hj x) 66 67private theorem norm_rangeFunctional_le (j : A →⋆ₐ[ℂ] D) 68 (hj : Function.Injective j) (τ : A →L[ℂ] ℂ) 69 (hτ : ∀ a, ‖τ a‖ ≤ ‖a‖) : ‖rangeFunctional j hj τ hτ‖ ≤ 1 := by 70 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one 71 intro x 72 change ‖τ (rangeInverse j hj x)‖ ≤ 1 * ‖x‖ 73 simpa only [one_mul, norm_rangeInverse] using hτ (rangeInverse j hj x) 74 75/-- A normalized contractive functional extends along an injective unital 76C⋆-homomorphism to a state of its actual codomain. -/ 77theorem exists_state_extension_of_injective (j : A →⋆ₐ[ℂ] D) 78 (hj : Function.Injective j) (τ : A →L[ℂ] ℂ) 79 (hτ_one : τ 1 = 1) (hτ_norm : ∀ a, ‖τ a‖ ≤ ‖a‖) : 80 ∃ φ : D →L[ℂ] ℂ, φ ∈ stateSpace D ∧ ∀ a, φ (j a) = τ a := by 81 let M : Submodule ℂ D := LinearMap.range j.toLinearMap 82 let f : M →L[ℂ] ℂ := rangeFunctional j hj τ hτ_norm 83 obtain ⟨φ, hφ, hnorm⟩ := exists_extension_norm_eq M f 84 have hrestrict (a : A) : φ (j a) = τ a := by 85 calc 86 φ (j a) = f ⟨j a, ⟨a, rfl⟩⟩ := hφ ⟨j a, ⟨a, rfl⟩⟩ 87 _ = τ (rangeInverse j hj ⟨j a, ⟨a, rfl⟩⟩) := rfl 88 _ = τ a := by rw [rangeInverse_map] 89 have hone : φ 1 = 1 := by simpa only [map_one, hτ_one] using hrestrict 1 90 have hbound : ‖φ‖ ≤ 1 := by 91 rw [hnorm] 92 exact norm_rangeFunctional_le j hj τ hτ_norm 93 letI : Nontrivial D := nontrivial_of_ne (1 : D) 0 (by 94 intro hzero 95 have h := hone 96 rw [hzero, map_zero] at h 97 exact zero_ne_one h) 98 exact ⟨φ, ⟨nonnegative_of_norm_le_one_of_apply_one φ hbound hone, hone⟩, 99 hrestrict⟩ 100 101end MathlibAnnex.Analysis.CStarAlgebra