OAI/Analysis/OInfinity/CocycleFlip.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The finite block flip and the actual row cocycle

The block flip permutes the composed row and is a selfadjoint relative unitary. For commuting rows, multiplying the actual row cocycle by this flip moves that cocycle into the shifted corner. The shifted cocycle is retained: the identity does not make the cocycle finite-order.

  1. def OAI.WeakPureInfiniteness.finiteRowCocycle line 20
  2. def OAI.WeakPureInfiniteness.finiteRowShift line 22
  3. def OAI.WeakPureInfiniteness.finiteRowBlockFlip line 24
  4. lemma OAI.WeakPureInfiniteness.finiteRowCocycle_star line 28
  5. lemma OAI.WeakPureInfiniteness.finiteRow_right_support line 33
  6. lemma OAI.WeakPureInfiniteness.finiteRow_left_support line 39
  7. lemma OAI.WeakPureInfiniteness.finiteRowCocycle_mul_row line 52
  8. lemma OAI.WeakPureInfiniteness.finiteRowCocycle_gram line 66
  9. lemma OAI.WeakPureInfiniteness.finiteRowBlockFlip_star line 87
  10. lemma OAI.WeakPureInfiniteness.finiteRow_composed_gram line 97
  11. lemma OAI.WeakPureInfiniteness.finiteRowBlockFlip_mul_composed line 115
  12. lemma OAI.WeakPureInfiniteness.finiteRow_composed_sum line 144
  13. lemma OAI.WeakPureInfiniteness.finiteRowBlockFlip_sq line 162
  14. lemma OAI.WeakPureInfiniteness.finiteRowBlockFlip_mul_target line 191

    Source documentation

    Commutation is needed here, in contrast to the flip's involution law.

    lemma finiteRowBlockFlip_mul_target (q : E) (s t : I → E)
    (hqstar : star q = q) (hqq : q * q = q)
    (ht : ∀ i j, star (t i) * t j = if i = j then q else 0)
    (hc : ∀ i j, Commute (star (s i)) (t j)) (k : I) :
    finiteRowBlockFlip s t * t k = s k * finiteRowCocycle s t := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteRowBlockFlip, OAI.WeakPureInfiniteness.finiteRowCocycle

  15. lemma OAI.WeakPureInfiniteness.finiteRowBlockFlip_mul_cocycle line 216

    Source documentation

    Multiplying by the involution shifts the actual cocycle; its tail remains.

    lemma finiteRowBlockFlip_mul_cocycle (q : E) (s t : I → E)
    (hqstar : star q = q) (hqq : q * q = q)
    (ht : ∀ i j, star (t i) * t j = if i = j then q else 0)
    (hc : ∀ i j, Commute (star (s i)) (t j)) :
    finiteRowBlockFlip s t * finiteRowCocycle s t = finiteRowShift s (finiteRowCocycle s t) := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteRowBlockFlip, OAI.WeakPureInfiniteness.finiteRowCocycle, OAI.WeakPureInfiniteness.finiteRowShift

  16. lemma OAI.WeakPureInfiniteness.finiteRowCocycle_eq_flip_shift line 227

    Source documentation

    The cocycle has an involution factor and a shifted cocycle factor. This equality retains the second factor rather than treating it as q.

    lemma finiteRowCocycle_eq_flip_shift (q : E) (s t : I → E)
    (hqstar : star q = q) (hqq : q * q = q)
    (hs : ∀ i j, star (s i) * s j = if i = j then q else 0)
    (ht : ∀ i j, star (t i) * t j = if i = j then q else 0)
    (hsum : (∑ i, s i * star (s i)) = q)
    (htsum : (∑ i, t i * star (t i)) = q)
    (hc : ∀ i j, Commute (star (s i)) (t j)) :
    finiteRowCocycle s t = finiteRowBlockFlip s t * finiteRowShift s (finiteRowCocycle s t) := by
…

    Mentions: OAI.WeakPureInfiniteness.finiteRowCocycle, OAI.WeakPureInfiniteness.finiteRowBlockFlip, OAI.WeakPureInfiniteness.finiteRowShift