MathlibAnnex/Analysis/CStarAlgebra/DirectSum/OrthogonalIdealAssembly.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6module78public import MathlibAnnex.Analysis.CStarAlgebra.DirectSum.C0DirectSum9public import MathlibAnnex.Analysis.CStarAlgebra.Ideal.ClosedStarIdeal10public import Mathlib.Analysis.CStarAlgebra.GelfandDuality11public import Mathlib.Analysis.Normed.Operator.Extend1213/-!14# Assembly of orthogonal closed C-star ideals as a c₀-direct sum1516Let `J i` be an arbitrary family of concrete norm-closed two-sided star ideals17in a nonunital complex C-star algebra `A`.  If different ideals annihilate one18another, the ambient sum of a finitely supported family has norm equal to the19maximum of its coordinate norms.  Consequently the finite-support summation20map extends uniquely to an isometric nonunital star-algebra homomorphism from21the actual completed dependent `C0DirectSum` into `A`.2223The range of this homomorphism is exactly the norm closure of the ambient24finite ideal sums.  A star-algebra equivalence with `A` is therefore obtained25from the explicit boundary hypothesis that these finite sums are norm dense.26This file does not construct the ideal family and does not prove that density27hypothesis for a particular ambient algebra.2829No countability, separability, finiteness, or nonzero-fibre assumption is made.30The empty index type and zero ideals are included.31-/3233@[expose] public section3435set_option autoImplicit false36set_option maxHeartbeats 80000037noncomputable section3839open Function Set Topology40open scoped BigOperators CStarAlgebra ENNReal NNReal4142namespace MathlibAnnex.Analysis.CStarAlgebra4344universe uι uA4546variable {ι : Type uι} {A : Type uA} [NonUnitalCStarAlgebra A]4748namespace ClosedStarIdeal4950/-- The actual C-star algebra carried by one member of a family of closed51star ideals. -/52abbrev Fiber (J : ι → ClosedStarIdeal A) (i : ι) : Type uA :=53  (J i).toNonUnitalStarSubalgebra5455/-- Different members of a family of concrete closed star ideals annihilate56one another in the ambient algebra.  Since the quantification is ordered, the57same hypothesis also supplies the reverse product after swapping the indices.58-/59def PairwiseOrthogonal (J : ι → ClosedStarIdeal A) : Prop :=60  ∀ ⦃i j : ι⦄, i ≠ j → ∀ (x : Fiber J i) (y : Fiber J j),61    (x : A) * (y : A) = 06263variable (J : ι → ClosedStarIdeal A)6465/-- The set of actual finite ambient sums with one term from each selected66ideal.  Repetitions are unnecessary because every ideal is additively closed.67-/68def finiteSums : Set A :=69  {a | ∃ (s : Finset ι) (x : ∀ i, Fiber J i),70    a = ∑ i ∈ s, (x i : A)}7172@[simp]73theorem zero_mem_finiteSums : (0 : A) ∈ finiteSums J := by74  classical75  refine ⟨∅, fun i => 0, ?_⟩76  simp7778/-- A two-term C-star norm computation used in the finite orthogonal-sum79induction.  The four displayed cross terms are exactly what remains after80expanding `(a + b)⁎(a + b)` and the product of its two diagonal summands. -/81private theorem norm_add_eq_max_of_star_cross_eq_zero82    {a b : A}83    (hsab : star a * b = 0) (hsba : star b * a = 0)84    (hasb : a * star b = 0) (hbsa : b * star a = 0) :85    ‖a + b‖ = max ‖a‖ ‖b‖ := by86  let p : A := star a * a87  let q : A := star b * b88  have hpq : p * q = 0 := by89    dsimp [p, q]90    calc91      (star a * a) * (star b * b) = star a * (a * star b) * b := by92        simp only [mul_assoc]93      _ = 0 := by rw [hasb]; simp94  have hqp : q * p = 0 := by95    dsimp [p, q]96    calc97      (star b * b) * (star a * a) = star b * (b * star a) * a := by98        simp only [mul_assoc]99      _ = 0 := by rw [hbsa]; simp100  have hpq_comm : Commute p q := by101    change p * q = q * p102    rw [hpq, hqp]103  have hp_normal : IsStarNormal p := by104    dsimp [p]105    exact (IsSelfAdjoint.star_mul_self a).isStarNormal106  have hq_normal : IsStarNormal q := by107    dsimp [q]108    exact (IsSelfAdjoint.star_mul_self b).isStarNormal109  have hdiag : star (a + b) * (a + b) = p + q := by110    dsimp [p, q]111    simp only [star_add, add_mul, mul_add]112    rw [hsab, hsba]113    abel114  have hsq : ‖a + b‖ ^ 2 = max (‖a‖ ^ 2) (‖b‖ ^ 2) := by115    calc116      ‖a + b‖ ^ 2 = ‖star (a + b) * (a + b)‖ := by117        simpa only [pow_two] using118          (CStarRing.norm_star_mul_self (x := a + b)).symm119      _ = ‖p + q‖ := by rw [hdiag]120      _ = max ‖p‖ ‖q‖ :=121        hp_normal.norm_add_eq_max hq_normal hpq_comm hpq122      _ = max (‖a‖ ^ 2) (‖b‖ ^ 2) := by123        dsimp [p, q]124        simp only [CStarRing.norm_star_mul_self, pow_two]125  have hmaxsq : max (‖a‖ ^ 2) (‖b‖ ^ 2) = (max ‖a‖ ‖b‖) ^ 2 := by126    rcases le_total ‖a‖ ‖b‖ with hab | hba127    · have hs : ‖a‖ ^ 2 ≤ ‖b‖ ^ 2 := by128        nlinarith [norm_nonneg a, norm_nonneg b]129      simp [max_eq_right hab, max_eq_right hs]130    · have hs : ‖b‖ ^ 2 ≤ ‖a‖ ^ 2 := by131        nlinarith [norm_nonneg a, norm_nonneg b]132      simp [max_eq_left hba, max_eq_left hs]133  rw [hmaxsq] at hsq134  have hmax_nonneg : 0 ≤ max ‖a‖ ‖b‖ :=135    (norm_nonneg a).trans (le_max_left _ _)136  nlinarith [norm_nonneg (a + b), hmax_nonneg]137138/-- The ambient norm of an actual finite sum from pairwise orthogonal ideals is139the supremum of the finitely many coordinate norms. -/140theorem nnnorm_sum_eq_sup (hJ : PairwiseOrthogonal J)141    (s : Finset ι) (x : ∀ i, Fiber J i) :142    ‖∑ i ∈ s, (x i : A)‖₊ = s.sup fun i => ‖x i‖₊ := by143  classical144  induction s using Finset.induction with145  | empty => simp146  | @insert j s hj ih =>147      have hsab : star (x j : A) * ∑ i ∈ s, (x i : A) = 0 := by148        rw [Finset.mul_sum]149        apply Finset.sum_eq_zero150        intro i hi151        have hji : j ≠ i := fun h => hj (h.symm ▸ hi)152        simpa using hJ hji (star (x j)) (x i)153      have hsba : star (∑ i ∈ s, (x i : A)) * (x j : A) = 0 := by154        rw [star_sum, Finset.sum_mul]155        apply Finset.sum_eq_zero156        intro i hi157        have hij : i ≠ j := fun h => hj (h ▸ hi)158        simpa using hJ hij (star (x i)) (x j)159      have hasb : (x j : A) * star (∑ i ∈ s, (x i : A)) = 0 := by160        rw [star_sum, Finset.mul_sum]161        apply Finset.sum_eq_zero162        intro i hi163        have hji : j ≠ i := fun h => hj (h.symm ▸ hi)164        simpa using hJ hji (x j) (star (x i))165      have hbsa : (∑ i ∈ s, (x i : A)) * star (x j : A) = 0 := by166        rw [Finset.sum_mul]167        apply Finset.sum_eq_zero168        intro i hi169        have hij : i ≠ j := fun h => hj (h ▸ hi)170        simpa using hJ hij (x i) (star (x j))171      have ih' : ‖∑ i ∈ s, (x i : A)‖ =172          ((s.sup fun i => ‖x i‖₊ : ℝ≥0) : ℝ) := by173        simpa only [coe_nnnorm] using congrArg (fun t : ℝ≥0 => (t : ℝ)) ih174      apply NNReal.eq175      change ‖∑ i ∈ insert j s, (x i : A)‖ = ((insert j s).sup fun i => ‖x i‖₊ : ℝ≥0)176      rw [Finset.sum_insert hj,177        norm_add_eq_max_of_star_cross_eq_zero hsab hsba hasb hbsa,178        Finset.sup_insert, NNReal.coe_max, ih']179      rfl180181/-- Real-norm form of `nnnorm_sum_eq_sup`. -/182theorem norm_sum_eq_sup (hJ : PairwiseOrthogonal J)183    (s : Finset ι) (x : ∀ i, Fiber J i) :184    ‖∑ i ∈ s, (x i : A)‖ = ((s.sup fun i => ‖x i‖₊ : ℝ≥0) : ℝ) := by185  simpa only [coe_nnnorm] using congrArg (fun t : ℝ≥0 => (t : ℝ)) (nnnorm_sum_eq_sup J hJ s x)186187/-- Every finitely supported bounded family belongs to the actual completed188c₀-direct sum. -/189private theorem vanishesAtInfinity_of_finite_support190    {x : lp (Fiber J) ∞} (hx : Set.Finite {i : ι | x i ≠ 0}) :191    C0DirectSum.VanishesAtInfinity (Fiber J) x := by192  intro ε hε193  refine hx.subset ?_194  intro i hi195  change ε ≤ ‖x i‖ at hi196  change x i ≠ 0197  intro hxi198  rw [hxi, norm_zero] at hi199  exact (not_lt_of_ge hi) hε200201/-- The finitely supported star subalgebra embeds into the actual completed202c₀-direct sum without changing its underlying bounded family. -/203def finiteSupportInclusion :204    C0DirectSum.finiteSupportStarSubalgebra (Fiber J) →⋆ₙₐ[ℂ]205      C0DirectSum (Fiber J) where206  toFun x := ⟨x.1, by exact vanishesAtInfinity_of_finite_support J x.2⟩207  map_zero' := by apply Subtype.ext; rfl208  map_add' := by intro x y; apply Subtype.ext; rfl209  map_mul' := by intro x y; apply Subtype.ext; rfl210  map_smul' := by intro c x; apply Subtype.ext; rfl211  map_star' := by intro x; apply Subtype.ext; rfl212213@[simp]214theorem coe_finiteSupportInclusion215    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J)) :216    (finiteSupportInclusion J x : lp (Fiber J) ∞) = x.1 := rfl217218@[simp]219theorem norm_finiteSupportInclusion220    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J)) :221    ‖finiteSupportInclusion J x‖ = ‖x‖ := rfl222223/-- The finite-support inclusion has dense range in the actual c₀-direct sum.224This statement is valid for arbitrary index types. -/225theorem denseRange_finiteSupportInclusion :226    DenseRange (finiteSupportInclusion J) := by227  classical228  refine Metric.denseRange_iff.mpr ?_229  intro x ε hε230  obtain ⟨s, hs⟩ := C0DirectSum.exists_finset_norm_sub_truncate_lt231    (Fiber J) x hε232  let y : C0DirectSum.finiteSupportStarSubalgebra (Fiber J) :=233    ⟨(C0DirectSum.truncate (Fiber J) s x).1, by234      change Set.Finite {i | (C0DirectSum.truncate (Fiber J) s x).1 i ≠ 0}235      exact C0DirectSum.finite_support_truncate (Fiber J) s x⟩236  have hy : finiteSupportInclusion J y = C0DirectSum.truncate (Fiber J) s x := rfl237  refine ⟨y, ?_⟩238  simpa only [hy, dist_eq_norm, norm_sub_rev] using hs239240/-- The exact finite support of a bounded family, viewed as a finset. -/241private def supportFinset242    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J)) : Finset ι :=243  x.2.toFinset244245@[simp]246private theorem mem_supportFinset247    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J)) (i : ι) :248    i ∈ supportFinset J x ↔ x.1 i ≠ 0 := by249  classical250  exact x.2.mem_toFinset251252/-- The ambient sum of one finitely supported family. -/253private def finiteSupportSumValue254    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J)) : A :=255  ∑ i ∈ supportFinset J x, (x.1 i : A)256257/-- The support finset in `finiteSupportSumValue` may be replaced by any258larger finset on which the family is zero off its exact support. -/259private theorem finiteSupportSumValue_eq_sum_of_support_subset260    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J))261    (s : Finset ι) (hxs : supportFinset J x ⊆ s) :262    finiteSupportSumValue J x = ∑ i ∈ s, (x.1 i : A) := by263  classical264  unfold finiteSupportSumValue265  rw [Finset.sum_subset hxs]266  intro i hi his267  have hzero : x.1 i = 0 := by268    by_contra hne269    exact his ((mem_supportFinset J x i).2 hne)270  simp [hzero]271272/-- The norm of a finitely supported bounded family is the supremum over its273exact finite support. -/274private theorem nnnorm_eq_support_sup275    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J)) :276    ‖x‖₊ = (supportFinset J x).sup fun i => ‖x.1 i‖₊ := by277  classical278  apply le_antisymm279  · apply NNReal.coe_le_coe.mp280    change ‖x.1‖ ≤ (((supportFinset J x).sup fun i => ‖x.1 i‖₊ : ℝ≥0) : ℝ)281    refine lp.norm_le_of_forall_le (NNReal.coe_nonneg ((supportFinset J x).sup fun i => ‖x.1 i‖₊)) ?_282    intro i283    by_cases hi : x.1 i = 0284    · simp [hi]285    · change (‖x.1 i‖₊ : ℝ) ≤ _286      exact NNReal.coe_le_coe.mpr (Finset.le_sup (f := fun i => ‖x.1 i‖₊) ((mem_supportFinset J x i).2 hi))287  · apply Finset.sup_le288    intro i hi289    apply NNReal.coe_le_coe.mp290    exact lp.norm_apply_le_norm (by simp) x.1 i291292/-- Finite-support summation into the ambient algebra.  Orthogonality is used293only for multiplication; additivity, scalar compatibility, and star294compatibility are the ordinary finite-sum identities. -/295def finiteSupportSum (hJ : PairwiseOrthogonal J) :296    C0DirectSum.finiteSupportStarSubalgebra (Fiber J) →⋆ₙₐ[ℂ] A where297  toFun x := ∑ i ∈ x.2.toFinset, (x.1 i : A)298  map_zero' := by299    change finiteSupportSumValue J 0 = 0300    simp [finiteSupportSumValue, supportFinset]301  map_add' := by302    intro x y303    change finiteSupportSumValue J (x + y) = finiteSupportSumValue J x + finiteSupportSumValue J y304    classical305    let s := supportFinset J x ∪ supportFinset J y306    have hxs : supportFinset J x ⊆ s := Finset.subset_union_left307    have hys : supportFinset J y ⊆ s := Finset.subset_union_right308    have hxys : supportFinset J (x + y) ⊆ s := by309      intro i hi310      have hxyne : x.1 i + y.1 i ≠ 0 :=311        (mem_supportFinset J (x + y) i).1 hi312      by_contra his313      have hxi : x.1 i = 0 := by314        by_contra hxne315        exact his (Finset.mem_union_left _ ((mem_supportFinset J x i).2 hxne))316      have hyi : y.1 i = 0 := by317        by_contra hyne318        exact his (Finset.mem_union_right _ ((mem_supportFinset J y i).2 hyne))319      exact hxyne (by simp [hxi, hyi])320    rw [finiteSupportSumValue_eq_sum_of_support_subset J (x + y) s hxys,321      finiteSupportSumValue_eq_sum_of_support_subset J x s hxs,322      finiteSupportSumValue_eq_sum_of_support_subset J y s hys]323    change (∑ i ∈ s, ((x.1 i : A) + (y.1 i : A))) =324      (∑ i ∈ s, (x.1 i : A)) + ∑ i ∈ s, (y.1 i : A)325    rw [Finset.sum_add_distrib]326  map_smul' := by327    intro c x328    change finiteSupportSumValue J (c • x) = c • finiteSupportSumValue J x329    classical330    have hsub : supportFinset J (c • x) ⊆ supportFinset J x := by331      intro i hi332      have hne : c • x.1 i ≠ 0 := (mem_supportFinset J (c • x) i).1 hi333      by_contra hxi334      have hzero : x.1 i = 0 := by335        by_contra hxne336        exact hxi ((mem_supportFinset J x i).2 hxne)337      exact hne (by simp only [hzero, smul_zero])338    rw [finiteSupportSumValue_eq_sum_of_support_subset J (c • x)339        (supportFinset J x) hsub]340    change (∑ i ∈ supportFinset J x, c • (x.1 i : A)) =341      c • (∑ i ∈ supportFinset J x, (x.1 i : A))342    rw [Finset.smul_sum]343  map_star' := by344    intro x345    change finiteSupportSumValue J (star x) = star (finiteSupportSumValue J x)346    classical347    have hsub : supportFinset J (star x) ⊆ supportFinset J x := by348      intro i hi349      have hne : star (x.1 i) ≠ 0 := (mem_supportFinset J (star x) i).1 hi350      by_contra hxi351      have hzero : x.1 i = 0 := by352        by_contra hxne353        exact hxi ((mem_supportFinset J x i).2 hxne)354      exact hne (by simp only [hzero, star_zero])355    rw [finiteSupportSumValue_eq_sum_of_support_subset J (star x)356        (supportFinset J x) hsub]357    change (∑ i ∈ supportFinset J x, star (x.1 i : A)) =358      star (∑ i ∈ supportFinset J x, (x.1 i : A))359    rw [star_sum]360  map_mul' := by361    intro x y362    change finiteSupportSumValue J (x * y) = finiteSupportSumValue J x * finiteSupportSumValue J y363    classical364    let s := supportFinset J x ∪ supportFinset J y365    have hxs : supportFinset J x ⊆ s := Finset.subset_union_left366    have hys : supportFinset J y ⊆ s := Finset.subset_union_right367    have hxys : supportFinset J (x * y) ⊆ s := by368      intro i hi369      have hne : x.1 i * y.1 i ≠ 0 :=370        (mem_supportFinset J (x * y) i).1 hi371      by_contra his372      have hxi : x.1 i = 0 := by373        by_contra hxne374        exact his (Finset.mem_union_left _ ((mem_supportFinset J x i).2 hxne))375      exact hne (by simp [hxi])376    rw [finiteSupportSumValue_eq_sum_of_support_subset J (x * y) s hxys,377      finiteSupportSumValue_eq_sum_of_support_subset J x s hxs,378      finiteSupportSumValue_eq_sum_of_support_subset J y s hys]379    change (∑ i ∈ s, ((x.1 i : A) * (y.1 i : A))) =380      (∑ i ∈ s, (x.1 i : A)) * ∑ i ∈ s, (y.1 i : A)381    rw [Finset.sum_mul]382    apply Finset.sum_congr rfl383    intro i hi384    rw [Finset.mul_sum]385    rw [Finset.sum_eq_single i]386    · intro j hj hji387      simpa using hJ hji.symm (x.1 i) (y.1 j)388    · exact fun hnot => (hnot hi).elim389390@[simp]391theorem finiteSupportSum_apply (hJ : PairwiseOrthogonal J)392    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J)) :393    finiteSupportSum J hJ x = ∑ i ∈ x.2.toFinset, (x.1 i : A) := rfl394395private theorem nnnorm_finiteSupportSum (hJ : PairwiseOrthogonal J)396    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J)) :397    ‖finiteSupportSum J hJ x‖₊ = ‖x‖₊ := by398  change ‖finiteSupportSumValue J x‖₊ = ‖x‖₊399  rw [finiteSupportSumValue, nnnorm_sum_eq_sup J hJ]400  exact (nnnorm_eq_support_sup J x).symm401402@[simp]403theorem norm_finiteSupportSum (hJ : PairwiseOrthogonal J)404    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J)) :405    ‖finiteSupportSum J hJ x‖ = ‖x‖ := by406  simpa only [coe_nnnorm] using congrArg (fun t : ℝ≥0 => (t : ℝ)) (nnnorm_finiteSupportSum J hJ x)407408/-- The underlying continuous linear extension of finite-support summation to409the completed c₀-direct sum. -/410private def c0SumLinearMap (hJ : PairwiseOrthogonal J) :411    C0DirectSum (Fiber J) →L[ℂ] A :=412  ({ toFun := finiteSupportSum J hJ, map_add' := map_add _, map_smul' := fun c x => by exact map_smul (finiteSupportSum J hJ) c x } : C0DirectSum.finiteSupportStarSubalgebra (Fiber J) →ₗ[ℂ] A).extendOfNorm413    ({ toFun := finiteSupportInclusion J, map_add' := map_add _, map_smul' := fun c x => by exact map_smul (finiteSupportInclusion J) c x } : C0DirectSum.finiteSupportStarSubalgebra (Fiber J) →ₗ[ℂ] C0DirectSum (Fiber J))414415@[simp]416private theorem c0SumLinearMap_finiteSupportInclusion417    (hJ : PairwiseOrthogonal J)418    (x : C0DirectSum.finiteSupportStarSubalgebra (Fiber J)) :419    c0SumLinearMap J hJ (finiteSupportInclusion J x) =420      finiteSupportSum J hJ x := by421  apply LinearMap.extendOfNorm_eq422    (f := ({ toFun := finiteSupportSum J hJ, map_add' := map_add _, map_smul' := fun c x => by exact map_smul (finiteSupportSum J hJ) c x } : C0DirectSum.finiteSupportStarSubalgebra (Fiber J) →ₗ[ℂ] A))423    (e := ({ toFun := finiteSupportInclusion J, map_add' := map_add _, map_smul' := fun c x => by exact map_smul (finiteSupportInclusion J) c x } : C0DirectSum.finiteSupportStarSubalgebra (Fiber J) →ₗ[ℂ] C0DirectSum (Fiber J)))424    (denseRange_finiteSupportInclusion J)425  refine ⟨1, ?_⟩426  intro y427  change ‖finiteSupportSum J hJ y‖ ≤ 1 * ‖finiteSupportInclusion J y‖428  rw [one_mul, norm_finiteSupportSum, norm_finiteSupportInclusion]429430/-- The extension remains norm preserving on the completed c₀-direct sum. -/431private theorem norm_c0SumLinearMap (hJ : PairwiseOrthogonal J)432    (x : C0DirectSum (Fiber J)) :433    ‖c0SumLinearMap J hJ x‖ = ‖x‖ := by434  have hdense : DenseRange (finiteSupportInclusion J) :=435    denseRange_finiteSupportInclusion J436  have hclosed : IsClosed {z : C0DirectSum (Fiber J) |437      ‖c0SumLinearMap J hJ z‖ = ‖z‖} :=438    isClosed_eq (continuous_norm.comp (c0SumLinearMap J hJ).continuous) continuous_norm439  refine DenseRange.induction_on hdense x hclosed ?_440  intro y441  rw [c0SumLinearMap_finiteSupportInclusion, norm_finiteSupportSum,442    norm_finiteSupportInclusion]443444/-- The isometric nonunital star-algebra homomorphism from the actual completed445c₀-direct sum of a pairwise orthogonal ideal family into the ambient algebra.446-/447def c0SumHom (hJ : PairwiseOrthogonal J) :448    C0DirectSum (Fiber J) →⋆ₙₐ[ℂ] A where449  toFun := ({ toFun := finiteSupportSum J hJ, map_add' := map_add _, map_smul' := fun c x => by exact map_smul (finiteSupportSum J hJ) c x } : C0DirectSum.finiteSupportStarSubalgebra (Fiber J) →ₗ[ℂ] A).extendOfNorm ({ toFun := finiteSupportInclusion J, map_add' := map_add _, map_smul' := fun c x => by exact map_smul (finiteSupportInclusion J) c x } : C0DirectSum.finiteSupportStarSubalgebra (Fiber J) →ₗ[ℂ] C0DirectSum (Fiber J))450  map_zero' := map_zero _451  map_add' := map_add _452  map_smul' := map_smul _453  map_mul' := by454    intro x y455    change c0SumLinearMap J hJ (x * y) = c0SumLinearMap J hJ x * c0SumLinearMap J hJ y456    have hdense : DenseRange (finiteSupportInclusion J) :=457      denseRange_finiteSupportInclusion J458    refine DenseRange.induction_on₂ hdense ?_ ?_ x y459    · exact isClosed_eq460        ((c0SumLinearMap J hJ).continuous.comp continuous_mul)461        (((c0SumLinearMap J hJ).continuous.comp continuous_fst).mul462          ((c0SumLinearMap J hJ).continuous.comp continuous_snd))463    · intro u v464      rw [← map_mul (finiteSupportInclusion J),465        c0SumLinearMap_finiteSupportInclusion,466        c0SumLinearMap_finiteSupportInclusion,467        c0SumLinearMap_finiteSupportInclusion]468      exact map_mul (finiteSupportSum J hJ) u v469  map_star' := by470    intro x471    change c0SumLinearMap J hJ (star x) = star (c0SumLinearMap J hJ x)472    have hdense : DenseRange (finiteSupportInclusion J) :=473      denseRange_finiteSupportInclusion J474    refine DenseRange.induction_on hdense x ?_ ?_475    · exact isClosed_eq476        ((c0SumLinearMap J hJ).continuous.comp continuous_star)477        (continuous_star.comp (c0SumLinearMap J hJ).continuous)478    · intro y479      rw [← map_star (finiteSupportInclusion J),480        c0SumLinearMap_finiteSupportInclusion,481        c0SumLinearMap_finiteSupportInclusion]482      exact map_star (finiteSupportSum J hJ) y483484@[simp]485theorem norm_c0SumHom (hJ : PairwiseOrthogonal J)486    (x : C0DirectSum (Fiber J)) :487    ‖c0SumHom J hJ x‖ = ‖x‖ :=488  norm_c0SumLinearMap J hJ x489490/-- The completed orthogonal-ideal assembly map is an isometry. -/491theorem isometry_c0SumHom (hJ : PairwiseOrthogonal J) :492    Isometry (c0SumHom J hJ) := by493  rw [AddMonoidHomClass.isometry_iff_norm]494  exact norm_c0SumHom J hJ495496/-- The completed orthogonal-ideal assembly map is injective. -/497theorem c0SumHom_injective (hJ : PairwiseOrthogonal J) :498    Function.Injective (c0SumHom J hJ) :=499  (isometry_c0SumHom J hJ).injective500501/-- A single c₀-coordinate is sent to the corresponding ambient ideal element.502-/503@[simp]504theorem c0SumHom_single (hJ : PairwiseOrthogonal J) (i : ι) (x : Fiber J i) :505    c0SumHom J hJ (C0DirectSum.single (Fiber J) i x) = (x : A) := by506  classical507  let y : C0DirectSum.finiteSupportStarSubalgebra (Fiber J) :=508    ⟨(C0DirectSum.single (Fiber J) i x).1, by509      refine Set.finite_singleton i |>.subset ?_510      intro j hj511      simp only [Set.mem_singleton_iff]512      by_contra hji513      have hz : C0DirectSum.eval (Fiber J) j514          (C0DirectSum.single (Fiber J) i x) = 0 :=515        C0DirectSum.eval_single_of_ne (Fiber J) hji x516      exact hj (by simpa only [C0DirectSum.eval_apply] using hz)⟩517  have hy : finiteSupportInclusion J y = C0DirectSum.single (Fiber J) i x := rfl518  rw [← hy]519  change c0SumLinearMap J hJ (finiteSupportInclusion J y) = (x : A)520  rw [c0SumLinearMap_finiteSupportInclusion]521  change finiteSupportSumValue J y = (x : A)522  rw [finiteSupportSumValue_eq_sum_of_support_subset J y {i}]523  · rw [Finset.sum_singleton]524    change (C0DirectSum.eval (Fiber J) i525      (C0DirectSum.single (Fiber J) i x) : A) = (x : A)526    exact congrArg (fun z : Fiber J i => (z : A))527      (C0DirectSum.eval_single_same (Fiber J) i x)528  · intro j hj529    have hjne : y.1 j ≠ 0 := (mem_supportFinset J y j).1 hj530    by_contra hji531    have hji' : j ≠ i := by simpa using hji532    have hz : y.1 j = 0 := by533      change C0DirectSum.eval (Fiber J) j534        (C0DirectSum.single (Fiber J) i x) = 0535      exact C0DirectSum.eval_single_of_ne (Fiber J) hji' x536    exact hjne hz537538/-- Finite coordinate truncations are sent to the corresponding actual ambient539finite sums. -/540@[simp]541theorem c0SumHom_truncate (hJ : PairwiseOrthogonal J)542    (s : Finset ι) (x : C0DirectSum (Fiber J)) :543    c0SumHom J hJ (C0DirectSum.truncate (Fiber J) s x) =544      ∑ i ∈ s, (C0DirectSum.eval (Fiber J) i x : A) := by545  simp only [C0DirectSum.truncate, map_sum, c0SumHom_single]546547/-- Every actual finite ideal sum lies in the range of the completed c₀548assembly map. -/549theorem finiteSums_subset_range_c0SumHom (hJ : PairwiseOrthogonal J) :550    finiteSums J ⊆ Set.range (c0SumHom J hJ) := by551  classical552  rintro a ⟨s, x, rfl⟩553  refine ⟨∑ i ∈ s, C0DirectSum.single (Fiber J) i (x i), ?_⟩554  simp555556/-- The range of the completed c₀ assembly map is exactly the norm closure of557the actual finite ideal sums. -/558theorem range_c0SumHom_eq_closure_finiteSums (hJ : PairwiseOrthogonal J) :559    Set.range (c0SumHom J hJ) = closure (finiteSums J) := by560  apply Set.Subset.antisymm561  · rintro _ ⟨x, rfl⟩562    refine Metric.mem_closure_iff.mpr ?_563    intro ε hε564    obtain ⟨s, hs⟩ := C0DirectSum.exists_finset_norm_sub_truncate_lt565      (Fiber J) x hε566    refine ⟨c0SumHom J hJ (C0DirectSum.truncate (Fiber J) s x), ?_, ?_⟩567    · refine ⟨s, fun i => C0DirectSum.eval (Fiber J) i x, ?_⟩568      exact c0SumHom_truncate J hJ s x569    · rw [dist_eq_norm, ← map_sub (c0SumHom J hJ), norm_c0SumHom]570      exact hs571  · apply closure_minimal (finiteSums_subset_range_c0SumHom J hJ)572    exact (isometry_c0SumHom J hJ).isClosedEmbedding.isClosed_range573574/-- Explicit norm density of the actual finite ideal sums is precisely the575boundary hypothesis needed for surjectivity of the assembly map. -/576theorem c0SumHom_surjective (hJ : PairwiseOrthogonal J)577    (hdense : Dense (finiteSums J)) :578    Function.Surjective (c0SumHom J hJ) := by579  intro a580  have ha : a ∈ closure (finiteSums J) := by581    rw [hdense.closure_eq]582    exact Set.mem_univ a583  rw [← range_c0SumHom_eq_closure_finiteSums J hJ] at ha584  exact ha585586/-- The C-star equivalence obtained from a pairwise orthogonal ideal family and587the explicit hypothesis that its actual finite ambient sums are norm dense.588The theorem does not produce either the family or the density proof. -/589def c0SumEquivOfDense (hJ : PairwiseOrthogonal J)590    (hdense : Dense (finiteSums J)) :591    C0DirectSum (Fiber J) ≃⋆ₐ[ℂ] A :=592  { Equiv.ofBijective (c0SumHom J hJ)593      ⟨c0SumHom_injective J hJ, c0SumHom_surjective J hJ hdense⟩ with594    map_add' := map_add (c0SumHom J hJ)595    map_mul' := map_mul (c0SumHom J hJ)596    map_smul' := map_smul (c0SumHom J hJ)597    map_star' := map_star (c0SumHom J hJ) }598599@[simp]600theorem c0SumEquivOfDense_apply (hJ : PairwiseOrthogonal J)601    (hdense : Dense (finiteSums J)) (x : C0DirectSum (Fiber J)) :602    c0SumEquivOfDense J hJ hdense x = c0SumHom J hJ x := rfl603604@[simp]605theorem norm_c0SumEquivOfDense (hJ : PairwiseOrthogonal J)606    (hdense : Dense (finiteSums J)) (x : C0DirectSum (Fiber J)) :607    ‖c0SumEquivOfDense J hJ hdense x‖ = ‖x‖ :=608  norm_c0SumHom J hJ x609610end ClosedStarIdeal611612end MathlibAnnex.Analysis.CStarAlgebra