JointRohlinWitness.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Cyclic partitions inside the two generated row algebras

The existing finite CAR construction is applied inside a closed generated algebra. Thus the resulting partitions commute with the opposite row and with one another. The scope remains full coisometric binary rows.

def OAI.WeakPureInfiniteness.closedCuntzRowAlgebra line 21
instance OAI.WeakPureInfiniteness.closedCuntzRowAlgebra_isClosed line 24
lemma OAI.WeakPureInfiniteness.mem_closedCuntzRowAlgebra line 28
lemma OAI.WeakPureInfiniteness.closedCuntzRowAlgebra_le_centralizer line 32
lemma OAI.WeakPureInfiniteness.closedCuntzRowAlgebras_commute line 44
lemma OAI.WeakPureInfiniteness.binary_evenRowShift line 53
lemma OAI.WeakPureInfiniteness.sum_zmod_val line 57
lemma OAI.WeakPureInfiniteness.exists_binary_cyclic_partition_in line 69

lemma OAI.WeakPureInfiniteness.exists_joint_binary_cyclic_partition line 142

Source documentation

Actual common cyclic partitions for commuting full binary rows. The commutator estimate is uniform over the cells and explicit in the cocycle length. No commutation with a contraction path is asserted.

lemma exists_joint_binary_cyclic_partition (s t : Fin 2 → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then 1 else 0)
    (hsum : (∑ i, s i * star (s i)) = 1)
    (htsum : (∑ i, t i * star (t i)) = 1)
    (hc : bergRowsCommute s t) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ e : ZMod (2 ^ m) → E,
      (∀ k, IsStarProjection (e k)) ∧ (∑ k, e k) = 1 ∧
      (∀ k l, k ≠ l → e k * e l = 0) ∧
      (∀ k, ‖finiteRowShift s (e k) - e (k + 1)‖ < ε) ∧
      (∀ k, ‖finiteRowShift t (e k) - e (k + 1)‖ < ε) ∧
      (∀ k n, ‖(binaryRowCocycleUnitary s t hs ht hsum htsum n : E) * e k -
…

Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.WeakPureInfiniteness.finiteRowShift, OAI.WeakPureInfiniteness.binaryRowCocycleUnitary