MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/CoefficientProjective.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-/6import MathlibAnnex.Analysis.InnerProductSpace.MatrixCoefficient.RankOneRelations7import MathlibAnnex.Analysis.CStarAlgebra.FacialStructure.FiniteCoefficientRelations8import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.CoefficientKernel9import Mathlib.Data.Fintype.Option1011/-!12# Both projective lines of an irreducible coefficient kernel1314The received finite-relation/WOT theorem moves equalities to the full operator15space before rank-one tests are used. This is not an assumption that the16representation contains rank-one operators. All vectors in the linear-relation17lemmas may be zero; projective uniqueness requires the four stated nonzero18conditions, but no unit normalization, faithfulness, or finite dimension.19-/2021set_option autoImplicit false22noncomputable section23open scoped BigOperators2425namespace MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation2627universe u v28variable {A : Type u} [NonUnitalCStarAlgebra A]29variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]3031/-- The actual finite WOT relation theorem also transfers an inhomogeneous32finite equality, with all scalar factors in the source slot. -/33theorem matrixCoefficient_eq_sum_smul_iff_operator34    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)35    {ι : Type*} [Fintype ι] (x y : ι → H) (z w : H) (c : ι → ℂ) :36    matrixCoefficient pi z w = ∑ i, c i • matrixCoefficient pi (x i) (y i) ↔37      InnerProductSpace.matrixCoefficient ℂ z w =38        ∑ i, c i • InnerProductSpace.matrixCoefficient ℂ (x i) (y i) := by39  classical40  let X : Option ι → H := Option.elim' (-z) (fun i => c i • x i)41  let Y : Option ι → H := Option.elim' w y42  have hzero := sum_matrixCoefficient_eq_zero_iff_sum_operator_matrixCoefficient_eq_zero43    pi hpi X Y44  simpa [X, Y, Fintype.sum_option,45    matrixCoefficient_neg_left, matrixCoefficient_smul_left,46    InnerProductSpace.matrixCoefficient_neg_left,47    InnerProductSpace.matrixCoefficient_smul_left, _root_.neg_add_eq_zero] using hzero4849/-- A single scalar equality is transferred with its scalar unchanged. -/50theorem matrixCoefficient_eq_smul_iff_operator51    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)52    (x y z w : H) (c : ℂ) :53    matrixCoefficient pi z w = c • matrixCoefficient pi x y ↔54      InnerProductSpace.matrixCoefficient ℂ z w =55        c • InnerProductSpace.matrixCoefficient ℂ x y := by56  simpa using matrixCoefficient_eq_sum_smul_iff_operator pi hpi57    (fun _ : Unit => x) (fun _ : Unit => y) z w (fun _ => c)5859/-- General two-pair kernel equality, without assuming a common vector. -/60theorem ker_matrixCoefficient_eq_iff_span_eq_and_span_eq61    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)62    {x₁ x₂ y₁ y₂ : H} (hx₁ : x₁ ≠ 0) (hx₂ : x₂ ≠ 0)63    (hy₁ : y₁ ≠ 0) (hy₂ : y₂ ≠ 0) :64    (matrixCoefficient pi x₁ y₁).ker = (matrixCoefficient pi x₂ y₂).ker ↔65      Submodule.span ℂ {x₁} = Submodule.span ℂ {x₂} ∧66      Submodule.span ℂ {y₁} = Submodule.span ℂ {y₂} := by67  constructor68  · intro hk69    obtain ⟨c, _, hc⟩ := (ContinuousLinearMap.ker_eq_ker_iff_exists_ne_zero_smul70      ((matrixCoefficient_ne_zero_iff pi hpi x₁ y₁).2 ⟨hx₁, hy₁⟩)).mp hk71    exact InnerProductSpace.span_eq_and_span_eq_of_matrixCoefficient_eq_smul72      hx₁ hy₁ hx₂ hy₂ ((matrixCoefficient_eq_smul_iff_operator73        pi hpi x₁ y₁ x₂ y₂ c).mp hc)74  · rintro ⟨hx, hy⟩75    exact ((ker_matrixCoefficient_eq_iff_span_eq_left pi hpi hx₁ hx₂ hy₁).mpr hx).trans76      ((ker_matrixCoefficient_eq_iff_span_eq_right pi hpi hx₂ hy₁ hy₂).mpr hy)7778/-- The two-independent-lines obstruction, now for the original algebra. -/79theorem eq_zero_or_eq_zero_of_matrixCoefficient_eq_smul_add_smul80    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)81    {x₁ x₂ y₁ y₂ z w : H} (hx₁ : x₁ ≠ 0) (hx₂ : x₂ ≠ 0)82    (hy₁ : y₁ ≠ 0) (hy₂ : y₂ ≠ 0)83    (hx : Submodule.span ℂ {x₁} ≠ Submodule.span ℂ {x₂})84    (hy : Submodule.span ℂ {y₁} ≠ Submodule.span ℂ {y₂}) {a b : ℂ}85    (h : matrixCoefficient pi z w =86      a • matrixCoefficient pi x₁ y₁ + b • matrixCoefficient pi x₂ y₂) :87    a = 0 ∨ b = 0 := by88  have hh : InnerProductSpace.matrixCoefficient ℂ z w =89      a • InnerProductSpace.matrixCoefficient ℂ x₁ y₁ +90      b • InnerProductSpace.matrixCoefficient ℂ x₂ y₂ := by91    have h' : matrixCoefficient pi z w =92        ∑ i : Fin 2, (![a, b] i) • matrixCoefficient pi (![x₁, x₂] i) (![y₁, y₂] i) := by93      simpa [Fin.sum_univ_two] using h94    simpa using (matrixCoefficient_eq_sum_smul_iff_operator pi hpi95      ![x₁, x₂] ![y₁, y₂] z w ![a, b]).mp h'96  exact InnerProductSpace.eq_zero_or_eq_zero_of_matrixCoefficient_eq_smul_add_smul97    hx₁ hx₂ hy₁ hy₂ hx hy hh9899end MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation