OAI/GroupTheory/BooneHigman/CantorBricks.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Cube line 18

   Source documentation

   The Cantor cube used by the twisted Brin--Thompson construction.

   abbrev Cube (X : Type u) := X → Stream' Bool

2. structure OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix line 21

   Source documentation

   A dyadic brick has only finitely many nonempty coordinate prefixes.

   structure Prefix (X : Type u) where
   …

3. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.empty line 28
4. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.attach line 30
5. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.empty_attach line 33
6. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.attach_injective line 37
7. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.oneBit line 42
8. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.oneBit_word line 50
9. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.mem_oneBit line 53
10. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist line 74

    Source documentation

    Coordinate permutation by the input group; precomposition is contravariant.

    def twist (g : Γ) : Equiv.Perm (Cube X) where
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Cube

11. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist_apply line 80
12. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist_one line 83
13. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist_mul line 87
14. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twistHom line 91
15. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist_injective line 96
16. structure OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table line 110

    Source documentation

    A finite prefix-replacement table, with one input-group twist on each brick. The uniqueness clauses say that the source and target bricks are partitions.

    structure Table (f : Equiv.Perm (Cube X)) where
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Cube

17. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group line 121

    Source documentation

    Concrete permutation model generated by finite twisted dyadic tables.

    def group : Subgroup (Equiv.Perm (Cube X)) :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Cube

18. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist_table line 124
19. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.embedding line 134
20. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.embedding_injective line 138
21. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.bitFlip line 144

    Source documentation

    The elementary swap in a single cube coordinate.

    def bitFlip (x : X) : Equiv.Perm (Cube X) := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Cube

22. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.bitFlip_apply line 152
23. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.bitFlip_table line 155
24. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.bitFlip_ne_one line 175
25. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group_nontrivial line 182
26. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.ext line 197
27. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.mem_range_iff line 203
28. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.comp line 215
29. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.comp_word line 223
30. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.comp_attach line 226
31. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.Extends line 231
32. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.extends_refl line 233
33. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.remainder line 235
34. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.remainder_word line 239
35. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.comp_remainder line 242
36. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.extends_of_ranges line 250
37. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.Compatible line 275

    Source documentation

    Nonempty intersection of the two dyadic bricks.

    def Compatible (p q : Prefix X) : Prop := ∃ z, (∃ w,p.attach w=z) ∧ ∃ w,q.attach w=z

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix

38. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.commonPoint line 277
39. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.commonPoint_mem_left line 279
40. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.commonPoint_mem_right line 282
41. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.meet line 286

    Source documentation

    Intersection is again one brick: take the longer prefix at each coordinate.

    def meet {p q : Prefix X} (h : p.Compatible q) : Prefix X :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix

42. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.meet_extends_left line 295
43. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.meet_extends_right line 301
44. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.mem_range_of_extends line 307
45. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.mem_meet_iff line 313
46. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twistPrefix line 338

    Source documentation

    The induced coordinate permutation on finite prefixes.

    def twistPrefix (g : Γ) (p : Prefix X) : Prefix X :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix

47. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twistPrefix_word line 342
48. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist_attach line 345
49. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.untwist_attach line 348
50. structure OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition line 360

    Source documentation

    A finite dyadic partition of the entire cube.

    structure Partition (X : Type u) where
    …

51. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.trivial line 369
52. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.bit line 375
53. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.RefineIndex line 382
54. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.refineIndex_finite line 384
55. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.refineBrick line 389
56. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.refine_cover line 393
57. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.refinement line 424
58. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.HasPartition line 436

    Source documentation

    The brick occurs as one member of an actual finite partition.

    def HasPartition (p : Prefix X) : Prop := ∃ P : Partition X, ∃ i, P.brick i=p

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition

59. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.empty_hasPartition line 438
60. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.oneBit_hasPartition line 441
61. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.comp_hasPartition line 444
62. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.atWord line 452
63. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.atWord_word line 458
64. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.atWord_nil line 461
65. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.atWord_cons line 466
66. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.atWord_hasPartition line 472
67. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.erase line 479
68. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.erase_word line 484
69. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.atWord_comp_erase line 487
70. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.hasPartition line 496

    Source documentation

    Every finite dyadic brick has a finite dyadic complement partition.

    theorem hasPartition (p : Prefix X) : p.HasPartition := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix

71. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist_inv_twist line 532
72. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist_twist_inv line 536
73. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist_twist line 540
74. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.transport_partition line 547

    Source documentation

    Target partition follows from the source partition and the bijective charts.

    lemma transport_partition {I : Type} (f : Equiv.Perm (Cube X))
        (p q : I → Prefix X) (a : I → Γ)
        (hp : ∀ z : Cube X, ∃! i, ∃ w, (p i).attach w=z)
        (hchart : ∀ i z, f ((p i).attach z) = (q i).attach (twist (a i) z)) :
        ∀ z : Cube X, ∃! i, ∃ w, (q i).attach w=z := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Cube, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twist

75. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.inverse line 563
76. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.Overlap line 579

    Source documentation

    The nonempty intersections of the intermediate partitions.

    def Overlap (A : Table (Γ:=Γ) f) (B : Table (Γ:=Γ) g) :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table

77. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.overlap_fintype line 582
78. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.middle line 588
79. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.leftRemainder line 591
80. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.rightRemainder line 594
81. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.domain line 597
82. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.codomain line 600
83. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.leftFactor line 603
84. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.rightFactor line 607
85. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.domain_chart line 611
86. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.compose_chart line 616
87. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.mem_domain_iff line 624
88. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.domain_partition line 644
89. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.compose line 661

    Source documentation

    Composition is obtained by the literal common refinement of the middle bricks.

    def compose (A : Table (Γ:=Γ) f) (B : Table (Γ:=Γ) g) : Table (Γ:=Γ) (g*f) where
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table

90. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.tableSubgroup line 673
91. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.mem_group_iff_table line 679
92. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.box line 705

    Source documentation

    A finite rectangular neighbourhood of a cube point.

    def box (z : Cube X) (s : Finset X) (n : ℕ) : Prefix X :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Cube, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix

93. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.box_word line 711
94. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.box_mem line 714
95. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.agree_before line 719
96. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.refined_chart line 734
97. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.image_refinement line 739
98. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.exists_displaced_brick line 751

    Source documentation

    Every nonidentity table displaces a nonempty dyadic brick.

    theorem exists_displaced_brick (A : Table (Γ:=Γ) f) (hf : f≠1) :
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table

99. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.exists_displaced_brick line 794
100. def OAI.FiniteAlgebraicEnvelopes.DisplacementCommutator.Supported line 806

     Source documentation

     A permutation is supported in a set when it fixes its complement pointwise.

     def Supported (ρ : G →* Equiv.Perm Y) (s : Set Y) (g : G) : Prop :=
     …

101. lemma OAI.FiniteAlgebraicEnvelopes.DisplacementCommutator.supported_inv line 811
102. lemma OAI.FiniteAlgebraicEnvelopes.DisplacementCommutator.supported_conjugate line 816
103. lemma OAI.FiniteAlgebraicEnvelopes.DisplacementCommutator.commute_of_disjoint_support line 826
104. lemma OAI.FiniteAlgebraicEnvelopes.DisplacementCommutator.commutator_factor line 837
105. theorem OAI.FiniteAlgebraicEnvelopes.DisplacementCommutator.local_commutator_mem line 845

     Source documentation

     Double-commutator localization. All commutators supported in a displaced set lie in the normal subgroup containing the displacing element.

     theorem local_commutator_mem (hρ : Function.Injective ρ)
         (N : Subgroup G) [N.Normal] {n a b : G} (hn : n∈N) {s : Set Y}
         (hdis : Disjoint s (ρ n '' s)) (ha : Supported ρ s a) (hb : Supported ρ s b) :
         a*b*a⁻¹*b⁻¹∈N := by
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.DisplacementCommutator.Supported

106. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localizePerm line 870

     Source documentation

     Conjugate a cube permutation into a brick, extending by identity.

     def localizePerm (p : Prefix X) : Equiv.Perm (Cube X) →* Equiv.Perm (Cube X) :=
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Cube

107. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localizePerm_attach line 874
108. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localizePerm_outside line 881
109. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localizePerm_injective line 885
110. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.sourcePartition line 895
111. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.targetPartition line 898
112. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.localize line 902

     Source documentation

     Insert a whole finite table into one member of a finite partition.

     def localize (A : Table (Γ:=Γ) f) (P : Partition X) (i : P.index) :
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition

113. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localizePerm_table line 930
114. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localize line 938

     Source documentation

     Every brick contains a canonical isomorphic copy of the entire twisted group.

     def localize (p : Prefix X) : group (Γ:=Γ) (X:=X) →* group (Γ:=Γ) (X:=X) :=
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group

115. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localize_val line 943
116. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localize_injective line 946
117. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localize_supported line 950
118. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.normal_contains_local_commutators line 958

     Source documentation

     A nontrivial normal subgroup contains all commutators of a whole localized copy of the group. No simplicity assumption is used.

     theorem normal_contains_local_commutators (N : Subgroup (group (Γ:=Γ) (X:=X))) [N.Normal]
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group