FiniteAbelianMerge.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite merging of positive abelian-range maps. The orthogonality is relative to finitely many positive values, so this construction works in the nonunital ambient ultrapower without assuming a multiplier Cuntz family.

theorem OAI.WeakPureInfiniteness.finite_abelian_merge line 27

Source documentation

On any finite set, all matrix coefficients of a finite family can be recovered from one positive abelian-range map. This is the local corner-sum step in KR02 Lemma 7.16, with no unitality assumption on the ambient algebra.

theorem finite_abelian_merge (hP : MainGap.PropertyP A)
    (β : B →⋆ₙₐ[ℂ] N) (T : J → B →L[ℂ] N)
    (hinner : ∀ j, ApproximatelyInnerAlong β (T j))
    (hpos : ∀ j b, 0 ≤ b → 0 ≤ T j b)
    (hcomm : ∀ j b c, Commute (T j b) (T j c)) (F : Finset B) :
    ∃ (R : B →L[ℂ] N) (r : J → N),
      ApproximatelyInnerAlong β R ∧ (∀ b, 0 ≤ b → 0 ≤ R b) ∧
      (∀ b c, Commute (R b) (R c)) ∧
      ∀ b ∈ F, ∀ i j, star (r i) * R b * r j = if i = j then T i b else 0 := by
…

Mentions: OAI.MainGap.PropertyP, OAI.WeakPureInfiniteness.ApproximatelyInnerAlong