BinaryCoherence.lean`

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

Binary combs, folds, permutations, and coherent exchanges.

def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.left line 18
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.right line 22
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.left_right line 27
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.assoc_LL line 32
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.assoc_LR line 35
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.assoc_RR line 37
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combHead line 42
Source documentation
The first adjacent swap on a right-associated comb with at least three leaves.
```
def combHead : H := d.a⁻¹*left d q.c*d.a
```
Mentions: OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.left
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combHead_square line 44
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combHead_distant line 51
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combHead_braid_last line 60
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combHead_conj_first line 71
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combHead_conj_second line 78
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combHead_braid line 87
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.rightPower line 99
Source documentation
Whisker an endomorphism past n initial leaves of a right comb.
```
def rightPower : ℕ → H →* H
  | 0 => MonoidHom.id H
  | n+1 => (right d).comp (rightPower n)
```
Mentions: OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.right
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.rightPower_zero line 103
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.rightPower_succ line 104
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.rightPower_add line 106
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.rightPower_succ' line 111
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap line 116
Source documentation
n adjacent generators acting on the n+1 leaf right comb.
```
def combSwap (n i : ℕ) : H :=
…
```
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_last line 119
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_internal line 121
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_square line 125
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_braid line 131
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_distant line 142
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_relations line 152
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combPermutation line 158
Source documentation
The literal symmetric-group action on every nonempty right comb.
```
def combPermutation (n : ℕ) : Equiv.Perm (Fin (n+1)) →* H :=
…
```
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combPermutation_swap line 161
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.merge line 173
Source documentation
Flatten (comb (m+1), comb (n+1)) to the right comb. As every nonempty object is positive, the value only depends on the size of the left block.
```
def merge : ℕ → H
  | 0 => 1
  | m+1 => right d (merge m) * d.a⁻¹
```
Mentions: OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.right
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.merge_zero line 177
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.merge_succ line 178
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.merge_coherence line 180
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.blockMap line 213
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.blockMap_id line 216
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.blockMap_comp line 219
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.blockMap_assoc line 226
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combFold line 256
Source documentation
Tensor a nonempty string of n+1 labels in the right comb.
```
def combFold : ℕ → (ℕ → H) → H
  | 0,f => f 0
  | n+1,f => d.tensor (f 0, combFold n (fun i=>f (i+1)))
```
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combFold_congr line 260
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combHead_naturality line 267
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_succ line 279
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.natSwap_succ_apply line 284
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_fold line 289
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.merge_right line 318
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.merge_left_right line 334
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.merge_left_head_base line 344
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.merge_left_head line 357
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_left line 372
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_shift line 392
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combSwap_right line 397
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.permutation_induction line 407
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natExtend_apply line 417
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natExtend_of_lt line 423
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combPermutation_fold line 430
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.finFold line 447
Source documentation
The same labelled right-comb tensor with its exact finite indexing.
```
def finFold (n : ℕ) (f : Fin (n+1) → H) : H :=
…
```
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.finFold_nat line 450
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.finFold_zero line 456
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.finFold_succ line 458
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.finFold_mul line 469
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.finFold_one line 477
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combPermutation_finFold line 482
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumIndex line 500
Source documentation
Consecutive indexing of two positive blocks, in predecessor-size notation.
```
def sumIndex (m n : ℕ) : Fin (m+1) ⊕ Fin (n+1) ≃ Fin (m+n+1+1) :=
…
```
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumIndex_left_val line 503
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumIndex_right_val line 505
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumPermutation line 508
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumPermutation_swap_left line 512
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumPermutation_swap_right line 519
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combPermutation_sum_left line 526
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combPermutation_sum_right line 545
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combPermutation_sum line 564
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equiv_size line 576
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal line 582
Source documentation
The symmetric coherence value of a bijection of two positive finite ordinals. Both sides may use different (provably equal) numeral expressions.
```
def equivVal {m n : ℕ} (e : Fin (m+1) ≃ Fin (n+1)) : H :=
…
```
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal_same line 585
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal_refl line 588
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal_cast line 591
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal_trans line 596
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal_symm line 603
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumEquiv line 609
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumEquiv_left line 613
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumEquiv_right line 617
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumEquiv_self line 621
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal_sum line 624
def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.exchangeEquiv line 632
Source documentation
Exchange two consecutive positive blocks.
```
def exchangeEquiv (m n : ℕ) : Fin (m+n+1+1) ≃ Fin (n+m+1+1) :=
…
```
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.exchangeEquiv_left line 635
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.exchangeEquiv_right line 639
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_congr line 649
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_head line 659
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.descending_nat_zero_apply line 667
lemma OAI.FiniteAlgebraicEnvelopes.Adjacent.natExtend_descending line 676
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal_transport line 687
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal_order line 697
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combPermutation_finSwap line 704
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.combPermutation_descending line 711
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.descending_comb_head line 719
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal_exchange_zero line 742
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.exchangeEquiv_val line 773
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.sumEquiv_valWith line 781
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.merge_left_merge line 791
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.exchange_scalar_step line 794
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.equivVal_exchange line 814
lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.exchange_naturality line 858