OAI/GroupTheory/BooneHigman/TreeCoherence.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.arity line 20

   Source documentation

   Number of internal nodes, so that the number of leaves is arity+1.

   abbrev arity : Tree X → ℕ
     | .leaf => 0
     | .split _ a b => arity a+arity b+1
   
   /-- Left-to-right exact ordinal enumeration of the leaves. -/

   Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinal

2. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinal line 25

   Source documentation

   Left-to-right exact ordinal enumeration of the leaves.

   def ordinal : (a : Tree X) → a.Leaves ≃ Fin (a.arity+1)
     | .leaf => {
         toFun := fun _=>0
   …

   Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree

3. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinal_leaf line 33
4. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinal_left line 34
5. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinal_right line 36
6. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinalEquiv line 39
7. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinalEquiv_apply line 42
8. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinalEquiv_trans line 45
9. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinalEquiv_sum line 50
10. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinalEquiv_exchange line 59
11. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.flatten line 77

    Source documentation

    Interpret the split tree as a map from its ordered comb of leaves.

    def flatten : Tree X → H
      | .leaf => 1
      | .split x a b => B x*d.tensor (flatten a,flatten b)*(merge d a.arity)⁻¹
    
    /-- The actual groupoid interpretation of a whole permutation of leaves. -/

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree

12. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue line 82

    Source documentation

    The actual groupoid interpretation of a whole permutation of leaves.

    def leafValue {a b:Tree X} (e:a.Leaves ≃ b.Leaves) : H :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree

13. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_refl line 85
14. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_trans line 90
15. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_symm line 96
16. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_sum line 102
17. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_exchange line 115
18. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.equivVal_ordinal_assoc line 126
19. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.flatten_assoc line 139
20. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_assoc line 169
21. inductive OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Route line 185

    Source documentation

    Structural routes made only from tensor, associativity and exchange. The arbitrary-permutation completeness theorem below is proved, not a constructor.

    inductive Route : {a b:Tree X} → (a.Leaves ≃ b.Leaves) → Prop
      | refl (a) : Route (a:=a) (b:=a) (Equiv.refl _)
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree

22. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Ordered line 196
23. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Ordered.trans line 199
24. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Ordered.symm line 201
25. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Ordered.unique line 204
26. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Ordered.arity line 209
27. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Ordered.sum line 212
28. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordered_assoc line 220
29. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.comb line 227
30. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.arity_comb line 231
31. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.route_merge line 236
32. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.route_normal line 253
33. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.combIndex line 264
34. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.combIndex_left line 267
35. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.combIndex_right line 269
36. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.combPerm line 273

    Source documentation

    Conjugate an ordinal permutation to the exact leaves of the comb.

    def combPerm (x:X) (n:ℕ) (p:Equiv.Perm (Fin (n+1))) : Equiv.Perm (comb x n).Leaves :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.comb, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Leaves

37. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.combIndex_perm line 276
38. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.combPerm_one line 279
39. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.combPerm_mul line 281
40. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.route_comb_adjacent line 285
41. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.route_comb_perm line 360
42. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.route_comb_equiv line 367
43. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.route_complete line 379

    Source documentation

    Every bijection of leaves is generated by associativity, symmetries and tensor. This is a finite-permutation coherence theorem, not an extra relation.

    lemma route_complete (x:X) {a b:Tree X} (e:a.Leaves ≃ b.Leaves) : Route e := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Route

44. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftLift line 397

    Source documentation

    Replace each leaf by the tree attached to its image. This is cabling of a bijection, defined on the actual dependent leaf sets.

    def graftLift {a b:Tree X} (e:a.Leaves ≃ b.Leaves) (F:b.Leaves → Tree X) :
        (a.graft (fun i=>F (e i))).Leaves ≃ (b.graft F).Leaves :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Leaves

45. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftLift_apply line 402
46. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftLift_refl line 408
47. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftLift_trans line 414
48. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftLift_sum line 425
49. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftLift_assoc line 440
50. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftLift_exchange line 456
51. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.cableValue line 474
52. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.cableValue_refl line 477
53. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.cableValue_trans line 483
54. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.cableValue_sum line 491
55. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.cableValue_assoc line 501
56. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.cableValue_exchange line 510
57. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Route.cableValue_eq line 519

    Source documentation

    Structural routes are invariant under replacing their wires by arbitrary (nonempty) trees. This is cabling coherence for whole leaf permutations.

    lemma Route.cableValue_eq {a b:Tree X} {e:a.Leaves ≃ b.Leaves} (h:Route e)
        (F:b.Leaves → Tree X) : cableValue d q B e F=leafValue d q B e := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Route, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.cableValue, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue

58. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_graftLift line 535
59. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.quad line 539
60. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.flatten_bit line 541
61. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.flatten_quad line 544
62. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.ordinalEquiv_quad line 549
63. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_quad_middle line 555
64. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_middle line 568
65. structure OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.GridLaw line 586

    Source documentation

    The only additional colour relation needed for all tree-partition coherence.

    structure GridLaw : Prop where
    …

66. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_interchange line 589
67. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.SameBricks line 594
68. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.SameBricks.unique line 597
69. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.SameBricks.symm line 602
70. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.SameBricks.trans line 605
71. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.SameBricks.brickSet_eq line 609
72. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.sameBricks_sum line 616
73. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.sameBricks_interchange line 623
74. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Coherent.exists_value_one line 631
75. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_of_sameBricks line 655

    Source documentation

    All equality between actual tree partitions follows from the finite colour interchange law, including the induced full permutation of their leaves.

    lemma leafValue_of_sameBricks (g:GridLaw d q B) {a b:Tree X} (e:a.Leaves ≃ b.Leaves)
        (he:SameBricks e) : leafValue d q B e=1 := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.GridLaw, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.SameBricks, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue

76. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralToEndpoint line 671
77. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralToEndpoint_project line 673
78. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralToEndpoint_surjective line 675
79. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralToEndpoint_tensor line 677
80. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointData line 684

    Source documentation

    The finite endpoint quotient supplies the full binary symmetric structure.

    def endpointData : Data (EndpointQuotient (Γ:=Γ) x s t y₀) where
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.EndpointQuotient

81. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointSymmetryData line 700
82. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointProject_middleSwapWord line 718
83. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointProject_gridWord line 725
84. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointBaker_base line 734
85. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointBaker_covariance line 736
86. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointGridLaw line 747
87. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold line 765

    Source documentation

    Tensor leaf decorations along the literal coloured tree.

    def fold : (a:Tree X) → (a.Leaves → H) → H
      | .leaf,F => F PUnit.unit
      | .split x a b,F => B x*d.tensor (fold a (fun i=>F (Sum.inl i)),
          fold b (fun i=>F (Sum.inr i)))*(B x)⁻¹

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree

88. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold_congr line 770
89. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold_one line 773
90. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold_mul line 779
91. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold_inv line 793
92. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold_graft line 799

    Source documentation

    Substitution of arbitrary decorated trees at all leaves.

    lemma fold_graft (a:Tree X) (F:a.Leaves → Tree X) (L:(a.graft F).Leaves → H) :
        fold d B (a.graft F) L=fold d B a
          (fun i=>fold d B (F i) (fun j=>L ((a.graftLeaves F).symm ⟨i,j⟩))) := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Leaves, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold

93. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.tensor_square line 811

    Source documentation

    Scalar naturality for a tensor square, preventing dependent tree rewrites.

    lemma tensor_square (A C U V F G I J:H)
        (h₁:U*F=I*U) (h₂:V*G=J*V) :
        (C*d.tensor (U,V)*A⁻¹)*(A*d.tensor (F,G)*A⁻¹)=
          (C*d.tensor (I,J)*C⁻¹)*(C*d.tensor (U,V)*A⁻¹) := by
    …

94. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold_left_algebra line 822

    Source documentation

    Flatten nested conjugations in a left-associated tree.

    lemma fold_left_algebra (x y:X) (A C E:H) :
        B x*d.tensor (B y*d.tensor (A,C)*(B y)⁻¹,E)*(B x)⁻¹=
          (B x*d.tensor (B y,1))*d.tensor (d.tensor (A,C),E)*(B x*d.tensor (B y,1))⁻¹ := by
    …

95. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold_right_algebra line 829
96. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_fold_route line 837
97. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_fold line 886
98. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftMap line 892

    Source documentation

    Whole dependent substitution of a bijection and bijections in every fibre.

    def graftMap {a b:Tree X} (e:a.Leaves ≃ b.Leaves) (F:a.Leaves → Tree X) (G:b.Leaves → Tree X)
        (h:∀ i,(F i).Leaves ≃ (G (e i)).Leaves) : (a.graft F).Leaves ≃ (b.graft G).Leaves :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Leaves

99. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftMap_apply line 895
100. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftMap_leaf line 900
101. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftMap_sum line 905
102. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_graftWithin line 923
103. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftMap_factor line 934
104. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_graftMap line 945
105. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.colourLeaves line 958

     Source documentation

     Leaf transport of a coordinate relabelling, with the same binary shape.

     def colourLeaves (f:X → X) : (a:Tree X) → a.Leaves ≃ (mapColors f a).Leaves
       | .leaf => Equiv.refl _
       | .split _ a b => Equiv.sumCongr (colourLeaves f a) (colourLeaves f b)

     Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.mapColors, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Leaves

106. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.colour_brick line 962
107. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_colour line 976

     Source documentation

     Root-label splitting, derived solely from the proved baker covariance law.

     lemma leafValue_colour (R:Γ →* H)
         (hR:∀ g x,R g*B x=B (g • x)*d.tensor (R g,R g)) (g:Γ) (a:Tree X) :
         leafValue d q B (colourLeaves (fun x=>g • x) a)*fold d B a (fun _=>R g)=R g := by
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.colourLeaves, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.fold

108. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leafValue_uncolour line 996