MathlibAnnex/Analysis/CStarAlgebra/Ideal/MinimalIdealFamilyModel.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-/67import MathlibAnnex.Analysis.CStarAlgebra.Ideal.OrthogonalElementary8import MathlibAnnex.Analysis.CStarAlgebra.CompactModelEquiv9import MathlibAnnex.Analysis.CStarAlgebra.DirectSum.OrthogonalIdealAssembly10import Mathlib.Tactic1112/-!13# Compact models on the carriers of the canonical minimal-ideal family1415The algebraic supremum of ideal submodules is identified with the literal set16`ClosedStarIdeal.finiteSums`. The proof includes zero padding outside a finite17support and absorbs scalar coefficients into the ideal coordinates.1819For the canonical family of all minimal nonzero closed ideals, orthogonality20and norm density are then supplied as conclusions, not as new hypotheses.21Each ideal chooses its own generator and its own cyclic Hilbert subspace of22the given representation space. Equality with the generated ideal induces an23identity-on-ambient-elements carrier equivalence. Transport through that24carrier equivalence gives an exact compact model on the displayed ideal,25not merely on a propositionally equal generated ideal.2627The final theorem exposes these same fibers, representations and equivalences28together with the actual finite-sum density. It does not use a c₀ completion or29an assembly equivalence. In the assembly module it uses only the already30specified ideal-fiber, finite-sum and orthogonality definitions.31-/3233@[expose] public section3435set_option autoImplicit false36noncomputable section3738open Set39open scoped BigOperators CStarAlgebra Topology4041namespace MathlibAnnex.Analysis.CStarAlgebra4243universe uι u v4445section FiniteSums4647variable {ι : Type uι} {A : Type u} [NonUnitalCStarAlgebra A]4849/-- The algebraic supremum of the ideal submodules and the displayed finite50ideal sums have literally the same ambient carrier. No orthogonality, order,51closedness argument, or density hypothesis is required for this equality. -/52theorem coe_closedStarIdealFiniteSumSubmodule_eq_finiteSums53    (J : ι → ClosedStarIdeal A) :54    (closedStarIdealFiniteSumSubmodule J : Set A) = ClosedStarIdeal.finiteSums J := by55  classical56  let S : Submodule ℂ A :=57    { carrier := ClosedStarIdeal.finiteSums J58      zero_mem' := by59        exact ⟨∅, fun _ => 0, by simp⟩60      add_mem' := by61        rintro a b ⟨s, x, rfl⟩ ⟨t, y, rfl⟩62        let z (i : ι) : ClosedStarIdeal.Fiber J i :=63          (if i ∈ s then x i else 0) + (if i ∈ t then y i else 0)64        refine ⟨s ∪ t, z, ?_⟩65        have hs : (∑ i ∈ s ∪ t, if i ∈ s then (x i : A) else 0) =66            ∑ i ∈ s, (x i : A) := by67          calc68            _ = ∑ i ∈ s, (if i ∈ s then (x i : A) else 0) :=69              (Finset.sum_subset Finset.subset_union_left70                (by intro i _ hi; simp only [if_neg hi])).symm71            _ = _ := Finset.sum_congr rfl (by intro i hi; simp only [if_pos hi])72        have ht : (∑ i ∈ s ∪ t, if i ∈ t then (y i : A) else 0) =73            ∑ i ∈ t, (y i : A) := by74          calc75            _ = ∑ i ∈ t, (if i ∈ t then (y i : A) else 0) :=76              (Finset.sum_subset Finset.subset_union_right77                (by intro i _ hi; simp only [if_neg hi])).symm78            _ = _ := Finset.sum_congr rfl (by intro i hi; simp only [if_pos hi])79        calc80          (∑ i ∈ s, (x i : A)) + (∑ i ∈ t, (y i : A)) =81              (∑ i ∈ s ∪ t, if i ∈ s then (x i : A) else 0) +82                (∑ i ∈ s ∪ t, if i ∈ t then (y i : A) else 0) := by rw [hs, ht]83          _ = ∑ i ∈ s ∪ t,84              ((if i ∈ s then (x i : A) else 0) +85                (if i ∈ t then (y i : A) else 0)) := by rw [Finset.sum_add_distrib]86          _ = ∑ i ∈ s ∪ t, (z i : A) := by87            apply Finset.sum_congr rfl88            intro i _89            by_cases his : i ∈ s <;> by_cases hit : i ∈ t <;> simp [z, his, hit]90      smul_mem' := by91        rintro c a ⟨s, x, rfl⟩92        refine ⟨s, fun i => c • x i, ?_⟩93        simp only [Finset.smul_sum, SetLike.val_smul] }94  have hle : closedStarIdealFiniteSumSubmodule J ≤ S := by95    apply iSup_le96    intro i a ha97    change a ∈ ClosedStarIdeal.finiteSums J98    let x (j : ι) : ClosedStarIdeal.Fiber J j :=99      ⟨if j = i then a else 0, by100        by_cases hji : j = i101        · subst j102          change a ∈ (J i).toNonUnitalStarSubalgebra at ha103          simpa using ha104        · rw [if_neg hji]105          exact zero_mem _⟩106    refine ⟨{i}, x, ?_⟩107    simp [x]108  apply Set.Subset.antisymm109  · exact hle110  · rintro a ⟨s, x, ha⟩111    rw [ha]112    exact (closedStarIdealFiniteSumSubmodule J).sum_mem fun i _ =>113      (le_iSup (fun j => (J j).toNonUnitalStarSubalgebra.toSubmodule) i) (x i).property114115/-- The original two-sided pairwise statement supplies the ordered116orthogonality predicate used by the assembly interface. -/117theorem pairwiseOrthogonal_minimalClosedStarIdealFamily :118    ClosedStarIdeal.PairwiseOrthogonal (minimalClosedStarIdealFamily (A := A)) := by119  letI : PartialOrder A := _root_.CStarAlgebra.spectralOrder A120  letI : StarOrderedRing A := _root_.CStarAlgebra.spectralOrderedRing A121  intro i j hij x y122  exact (pairwise_orthogonal_minimalClosedStarIdealFamily hij).1 x.property y.property123124end FiniteSums125126section CompactModels127128variable {A : Type u} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]129variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]130131/-- Quantitative norm density of the canonical finite-ideal-sum submodule,132transported through the literal carrier equality to the assembly's finite sums.133In particular, density is produced from the faithful compact representation. -/134theorem dense_finiteSums_minimalClosedStarIdealFamily135    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :136    Dense (ClosedStarIdeal.finiteSums (minimalClosedStarIdealFamily (A := A))) := by137  rw [← coe_closedStarIdealFiniteSumSubmodule_eq_finiteSums]138  exact dense_minimalClosedStarIdealFiniteSumSubmodule pi hpi139140namespace MinimalClosedStarIdeal141142/-- A single chosen generator/vector pair for one displayed minimal ideal.143All properties are proved by `exists_generator_compactOperatorModel`; none is144an additional provider argument. Choosing the pair once fixes the fibers used145by all subsequent definitions. -/146def compactModelWitness (i : MinimalClosedStarIdeal A)147    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :148    {w : A × H //149      IsMinimalStarProjection w.1 ∧ closedIdealGeneratedBy w.1 = i.1 ∧150      w.2 ≠ 0 ∧ pi w.1 w.2 = w.2 ∧151      IsCompactOperatorModel (pi.restrictClosedIdealGeneratedByCyclic w.1 w.2)} :=152  Classical.choice (show Nonempty {w : A × H //153      IsMinimalStarProjection w.1 ∧ closedIdealGeneratedBy w.1 = i.1 ∧154      w.2 ≠ 0 ∧ pi w.1 w.2 = w.2 ∧155      IsCompactOperatorModel (pi.restrictClosedIdealGeneratedByCyclic w.1 w.2)} from by156    obtain ⟨p, _, hp, hI, x, hx, hpx, hmodel⟩ :=157      i.exists_generator_compactOperatorModel pi hpi158    exact ⟨⟨(p, x), hp, hI, hx, hpx, hmodel⟩⟩)159160/-- The closed cyclic subspace associated with the chosen generator/vector161pair. Different ideal indices are not identified with a fixed common fiber. -/162def compactModelSubspace (i : MinimalClosedStarIdeal A)163    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :164    Submodule ℂ H :=165  (pi.restrictClosedIdealGeneratedBy (i.compactModelWitness pi hpi).val.1).cyclicSubspace166    (i.compactModelWitness pi hpi).val.2167168/-- The actual dependent Hilbert carrier, with its inherited subspace norm169and complex inner product. -/170abbrev CompactModelSpace (i : MinimalClosedStarIdeal A)171    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) : Type v :=172  i.compactModelSubspace pi hpi173174/-- The displayed cyclic fiber is norm closed in the ambient Hilbert space. -/175theorem isClosed_compactModelSubspace (i : MinimalClosedStarIdeal A)176    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :177    IsClosed (i.compactModelSubspace pi hpi : Set H) :=178  NonUnitalCStarRepresentation.isClosed_cyclicSubspace _ _179180/-- Completeness comes from the very cyclic subspace used in the fiber's181 definition, not from an independently chosen Hilbert structure. -/182instance instCompleteSpaceCompactModelSpace (i : MinimalClosedStarIdeal A)183    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :184    CompleteSpace (i.CompactModelSpace pi hpi) :=185  (i.isClosed_compactModelSubspace pi hpi).completeSpace_coe186187/-- A minimal nonzero ideal has a nonzero cyclic Hilbert fiber. -/188instance instNontrivialCompactModelSpace (i : MinimalClosedStarIdeal A)189    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :190    Nontrivial (i.CompactModelSpace pi hpi) := by191  let w := i.compactModelWitness pi hpi192  have hx : w.val.2 ∈ i.compactModelSubspace pi hpi := by193    have h := (pi.restrictClosedIdealGeneratedBy w.val.1).apply_mem_cyclicSubspace194      w.val.2 ⟨w.val.1, self_mem_closedIdealGeneratedBy w.val.1⟩195    change pi w.val.1 w.val.2 ∈ i.compactModelSubspace pi hpi at h196    rw [w.property.2.2.2.1] at h197    exact h198  refine ⟨⟨⟨w.val.2, hx⟩, 0, ?_⟩⟩199  intro hzero200  exact w.property.2.2.1 (congrArg Subtype.val hzero)201202/-- Equality of the generated and displayed ideals induces an equivalence of203actual carriers. Its underlying ambient function is the identity. -/204def compactModelCarrierEquiv (i : MinimalClosedStarIdeal A)205    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :206    i.1.toNonUnitalStarSubalgebra ≃⋆ₐ[ℂ]207      (closedIdealGeneratedBy (i.compactModelWitness pi hpi).val.1).toNonUnitalStarSubalgebra where208  toFun a := ⟨a.val, by209    have heq := congrArg (fun J : ClosedStarIdeal A => a.val ∈ J.toNonUnitalStarSubalgebra)210      (i.compactModelWitness pi hpi).property.2.1211    exact Eq.mpr heq a.property⟩212  invFun a := ⟨a.val, by213    have heq := congrArg (fun J : ClosedStarIdeal A => a.val ∈ J.toNonUnitalStarSubalgebra)214      (i.compactModelWitness pi hpi).property.2.1215    exact Eq.mp heq a.property⟩216  left_inv a := Subtype.ext rfl217  right_inv a := Subtype.ext rfl218  map_add' a b := Subtype.ext rfl219  map_mul' a b := Subtype.ext rfl220  map_star' a := Subtype.ext rfl221  map_smul' c a := Subtype.ext rfl222223@[simp]224theorem coe_compactModelCarrierEquiv_apply (i : MinimalClosedStarIdeal A)225    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented)226    (a : i.1.toNonUnitalStarSubalgebra) :227    (i.compactModelCarrierEquiv pi hpi a : A) = a := rfl228229/-- The exact cyclic action transported to the displayed ideal carrier. -/230def compactModelRepresentation (i : MinimalClosedStarIdeal A)231    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :232    NonUnitalCStarRepresentation i.1.toNonUnitalStarSubalgebra233      (i.CompactModelSpace pi hpi) :=234  (pi.restrictClosedIdealGeneratedByCyclic235    (i.compactModelWitness pi hpi).val.1 (i.compactModelWitness pi hpi).val.2).comp236      (i.compactModelCarrierEquiv pi hpi).toNonUnitalStarAlgHom237238/-- On ambient vectors the transported action is still the original action. -/239@[simp]240theorem coe_compactModelRepresentation_apply (i : MinimalClosedStarIdeal A)241    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented)242    (a : i.1.toNonUnitalStarSubalgebra) (z : i.CompactModelSpace pi hpi) :243    (i.compactModelRepresentation pi hpi a z : H) = pi (a : A) (z : H) := rfl244245/-- Transport proves injectivity, compactness of every value, and a preimage246for every compact operator on the very same dependent fiber. -/247theorem isCompactOperatorModel_compactModelRepresentation (i : MinimalClosedStarIdeal A)248    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :249    IsCompactOperatorModel (i.compactModelRepresentation pi hpi) := by250  let w := i.compactModelWitness pi hpi251  let e := i.compactModelCarrierEquiv pi hpi252  let sigma := pi.restrictClosedIdealGeneratedByCyclic w.val.1 w.val.2253  have hmodel : IsCompactOperatorModel sigma := w.property.2.2.2.2254  refine ⟨?_, ?_, ?_⟩255  · intro a b hab256    change sigma (e a) = sigma (e b) at hab257    exact e.injective (hmodel.1 hab)258  · intro a259    change IsCompactOperator (sigma (e a))260    exact hmodel.2.1 (e a)261  · intro T hT262    obtain ⟨b, hb⟩ := hmodel.2.2 T hT263    refine ⟨e.symm b, ?_⟩264    change sigma (e (e.symm b)) = T265    rw [e.apply_symm_apply]266    exact hb267268/-- An actual star-algebra equivalence whose domain is the displayed minimal269ideal, not just an equal generated ideal. The codomain carries the original270operator norm on the actual compact operators on its chosen cyclic fiber. -/271def compactModelEquiv (i : MinimalClosedStarIdeal A)272    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :273    ClosedStarIdeal.Fiber (minimalClosedStarIdealFamily (A := A)) i ≃⋆ₐ[ℂ]274      ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi) :=275  compactOperatorStarAlgEquiv (i.compactModelRepresentation pi hpi)276    (i.isCompactOperatorModel_compactModelRepresentation pi hpi)277278/-- The equivalence and the representation agree as literal operators. -/279@[simp]280theorem coe_compactModelEquiv_apply (i : MinimalClosedStarIdeal A)281    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented)282    (a : ClosedStarIdeal.Fiber (minimalClosedStarIdealFamily (A := A)) i) :283    (i.compactModelEquiv pi hpi a).val = i.compactModelRepresentation pi hpi a := rfl284285/-- The inverse equivalence produces an actual preimage of every compact286operator, with no representation or fiber change. -/287theorem compactModelRepresentation_compactModelEquiv_symm (i : MinimalClosedStarIdeal A)288    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented)289    (T : ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi)) :290    i.compactModelRepresentation pi hpi ((i.compactModelEquiv pi hpi).symm T) = T.val :=291  compactOperatorStarAlgEquiv_symm_apply (i.compactModelRepresentation pi hpi)292    (i.isCompactOperatorModel_compactModelRepresentation pi hpi) T293294/-- The displayed ideal's inherited C-star norm agrees with the fiber's295operator norm under the chosen exact equivalence. -/296@[simp]297theorem norm_compactModelEquiv_apply (i : MinimalClosedStarIdeal A)298    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented)299    (a : ClosedStarIdeal.Fiber (minimalClosedStarIdealFamily (A := A)) i) :300    ‖i.compactModelEquiv pi hpi a‖ = ‖a‖ :=301  norm_compactOperatorStarAlgEquiv_apply (i.compactModelRepresentation pi hpi)302    (i.isCompactOperatorModel_compactModelRepresentation pi hpi) a303304end MinimalClosedStarIdeal305306/-- The canonical producer boundary: the same displayed family is pairwise307orthogonal and has norm-dense actual finite sums, and every displayed carrier308has its fixed faithful exact compact model and its fixed norm-preserving309star-algebra equivalence on the associated dependent cyclic Hilbert fiber.310No orthogonality, density, fiber model, or terminal assembly is assumed. -/311theorem minimalClosedStarIdealFamily_compactModel_spec312    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :313    ClosedStarIdeal.PairwiseOrthogonal (minimalClosedStarIdealFamily (A := A)) ∧314    Dense (ClosedStarIdeal.finiteSums (minimalClosedStarIdealFamily (A := A))) ∧315    ∀ i : MinimalClosedStarIdeal A,316      IsCompactOperatorModel (i.compactModelRepresentation pi hpi) ∧317      (∀ a : ClosedStarIdeal.Fiber (minimalClosedStarIdealFamily (A := A)) i,318        (i.compactModelEquiv pi hpi a).val = i.compactModelRepresentation pi hpi a ∧319        ‖i.compactModelEquiv pi hpi a‖ = ‖a‖) ∧320      (∀ T : ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi),321        i.compactModelRepresentation pi hpi ((i.compactModelEquiv pi hpi).symm T) = T.val) := by322  refine ⟨pairwiseOrthogonal_minimalClosedStarIdealFamily,323    dense_finiteSums_minimalClosedStarIdealFamily pi hpi, ?_⟩324  intro i325  refine ⟨i.isCompactOperatorModel_compactModelRepresentation pi hpi, ?_, ?_⟩326  · intro a327    exact ⟨i.coe_compactModelEquiv_apply pi hpi a, i.norm_compactModelEquiv_apply pi hpi a⟩328  · exact i.compactModelRepresentation_compactModelEquiv_symm pi hpi329330end CompactModels331332end MathlibAnnex.Analysis.CStarAlgebra