Exact source: MathlibAnnex/Analysis/CStarAlgebra/State/ExtensionOfEmbedding.lean
Pinned GitHub source · Raw UTF-8 source
Back to Extending the CAR trace to the fixed shell target
1import Mathlib.Analysis.Normed.Module.HahnBanach2import Mathlib.Analysis.CStarAlgebra.Hom3import MathlibAnnex.Analysis.CStarAlgebra.State.Extension45/-!6# Extending a normalized functional along a faithful C⋆-embedding78The source functional is transported to the actual linear range of the9embedding and extended by norm-preserving Hahn–Banach. No universal property10of the codomain, and no existence of a codomain representation, is assumed.11-/1213set_option autoImplicit false1415open scoped ComplexOrder1617namespace MathlibAnnex.Analysis.CStarAlgebra1819universe u v2021variable {A : Type u} {D : Type v} [CStarAlgebra A] [CStarAlgebra D]22 [PartialOrder D] [StarOrderedRing D]2324private noncomputable def rangePreimage (j : A →⋆ₐ[ℂ] D)25 (x : LinearMap.range j.toLinearMap) : A :=26 Classical.choose x.property2728private theorem map_rangePreimage (j : A →⋆ₐ[ℂ] D)29 (x : LinearMap.range j.toLinearMap) : j (rangePreimage j x) = x :=30 Classical.choose_spec x.property3132private noncomputable def rangeInverse (j : A →⋆ₐ[ℂ] D)33 (hj : Function.Injective j) : LinearMap.range j.toLinearMap →ₗ[ℂ] A where34 toFun := rangePreimage j35 map_add' x y := by36 apply hj37 rw [map_add, map_rangePreimage, map_rangePreimage, map_rangePreimage]38 rfl39 map_smul' c x := by40 apply hj41 rw [map_smul, map_rangePreimage, map_rangePreimage]42 rfl4344private theorem rangeInverse_map (j : A →⋆ₐ[ℂ] D)45 (hj : Function.Injective j) (a : A) :46 rangeInverse j hj ⟨j a, ⟨a, rfl⟩⟩ = a := by47 apply hj48 exact map_rangePreimage j _4950private theorem norm_rangeInverse (j : A →⋆ₐ[ℂ] D)51 (hj : Function.Injective j) (x : LinearMap.range j.toLinearMap) :52 ‖rangeInverse j hj x‖ = ‖x‖ := by53 calc54 ‖rangeInverse j hj x‖ = ‖j (rangeInverse j hj x)‖ :=55 (NonUnitalStarAlgHom.norm_map j hj _).symm56 _ = ‖x‖ := by rw [show j (rangeInverse j hj x) = (x : D) from57 map_rangePreimage j x]; rfl5859private 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 ↦ by63 change ‖τ (rangeInverse j hj x)‖ ≤ 1 * ‖x‖64 rw [one_mul, ← norm_rangeInverse j hj x]65 exact hτ (rangeInverse j hj x)6667private theorem norm_rangeFunctional_le (j : A →⋆ₐ[ℂ] D)68 (hj : Function.Injective j) (τ : A →L[ℂ] ℂ)69 (hτ : ∀ a, ‖τ a‖ ≤ ‖a‖) : ‖rangeFunctional j hj τ hτ‖ ≤ 1 := by70 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one71 intro x72 change ‖τ (rangeInverse j hj x)‖ ≤ 1 * ‖x‖73 simpa only [one_mul, norm_rangeInverse] using hτ (rangeInverse j hj x)7475/-- A normalized contractive functional extends along an injective unital76C⋆-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 := by81 let M : Submodule ℂ D := LinearMap.range j.toLinearMap82 let f : M →L[ℂ] ℂ := rangeFunctional j hj τ hτ_norm83 obtain ⟨φ, hφ, hnorm⟩ := exists_extension_norm_eq M f84 have hrestrict (a : A) : φ (j a) = τ a := by85 calc86 φ (j a) = f ⟨j a, ⟨a, rfl⟩⟩ := hφ ⟨j a, ⟨a, rfl⟩⟩87 _ = τ (rangeInverse j hj ⟨j a, ⟨a, rfl⟩⟩) := rfl88 _ = τ a := by rw [rangeInverse_map]89 have hone : φ 1 = 1 := by simpa only [map_one, hτ_one] using hrestrict 190 have hbound : ‖φ‖ ≤ 1 := by91 rw [hnorm]92 exact norm_rangeFunctional_le j hj τ hτ_norm93 letI : Nontrivial D := nontrivial_of_ne (1 : D) 0 (by94 intro hzero95 have h := hone96 rw [hzero, map_zero] at h97 exact zero_ne_one h)98 exact ⟨φ, ⟨nonnegative_of_norm_le_one_of_apply_one φ hbound hone, hone⟩,99 hrestrict⟩100101end MathlibAnnex.Analysis.CStarAlgebra