OAI/GroupTheory/BooneHigman/TwistedSimplicity.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

Partition refinement, simplicity, faithful group embedding, and countability.

  1. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.coordinateEquiv line 20

    Source documentation

    The chart coordinates of a finite dyadic partition.

    def coordinateEquiv (P : Partition X) : P.index × Cube X ≃ Cube X :=
…

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

  2. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.coordinateEquiv_apply line 32
  3. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.coordinateEquiv_symm_attach line 35
  4. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.mapPerm line 40

    Source documentation

    Untwisted chart bijection between any two equally sized dyadic partitions.

    def mapPerm (P Q : Partition X) (e : P.index ≃ Q.index) : Equiv.Perm (Cube X) :=
…

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

  5. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.mapPerm_attach line 43
  6. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.mapTable line 50
  7. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.changeChart line 68
  8. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.changeChart_apply line 71
  9. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.componentTwist line 81

    Source documentation

    Separate coordinate twists on the components of a disjoint union of cubes.

    def componentTwist {I : Type} : (I → Γ) →* Equiv.Perm (I × Cube X) where
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Cube

  10. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.decoratePerm line 97
  11. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.decoratePerm_attach line 100
  12. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.decorateTable line 106
  13. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.decorate line 117

    Source documentation

    A direct product of local coordinate copies of the acting group.

    def decorate (P : Partition X) : (P.index → Γ) →* group (Γ:=Γ) (X:=X) :=
…

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

  14. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.decorate_val line 120
  15. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.decorate_injective line 123
  16. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.decomposition line 140

    Source documentation

    Every table is an untwisted prefix rearrangement followed by finitely many independent local coordinate twists.

    lemma decomposition (A : Table (Γ:=Γ) f) :
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table

  17. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.eq_of_range_eq line 163
  18. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.chart_prefix_rigidity line 182
  19. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.chart_rigidity line 194
  20. structure OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.Refines line 209

    Source documentation

    A literal chart refinement: attach a finite prefix to each tail, then transport it with the original coordinate label.

    structure Refines (A B : Table (Γ:=Γ) f) where
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table

  21. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.CommonIndex line 217
  22. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.commonIndex_finite line 220
  23. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.commonSource line 226
  24. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.commonTargetLeft line 229
  25. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.commonTargetRight line 233
  26. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.common_chart_left line 237
  27. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.common_chart_right line 249
  28. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.common_source_cover line 261
  29. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.common line 274

    Source documentation

    Source-intersection table, retaining the left-hand transported charts.

    def common (A B : Table (Γ:=Γ) f) : Table (Γ:=Γ) f where
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table

  30. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.common_refines_left line 284
  31. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.common_chart_rigidity line 291
  32. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.common_refines_right line 298
  33. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.common_refinement line 307

    Source documentation

    Completeness of the finite table equivalence: two tables for the same permutation have an actual simultaneous chart refinement, including labels.

    theorem common_refinement [FaithfulSMul Γ X] (A B : Table (Γ:=Γ) f) :
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table

  34. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localizePerm_conj line 320
  35. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localize_conj line 337
  36. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.exists_other line 344
  37. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.splitShift line 358

    Source documentation

    Shift a split from an exterior brick to the selected one.

    def splitShift (P : Partition X) (i j : P.index) :
    ({k : P.index // k≠j} ⊕ Bool) ≃ ({k : P.index // k≠i} ⊕ Bool) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition

  38. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.compressIndex line 371
  39. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.compressIndex_apply line 376
  40. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.exists_compressor line 391

    Source documentation

    Every proper brick can be compressed into either dyadic half by an element of the actual finite-table group.

    theorem exists_compressor (p : Prefix X) (hp : p≠Prefix.empty) (x : X) (b : Bool) :
    ∃ h : group (Γ:=Γ) (X:=X), ∀ z,
…

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

  41. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.exists_localize_half_conjugacy line 409

    Source documentation

    Uniform conjugacy of a proper local copy with either half-copy.

    theorem exists_localize_half_conjugacy (p : Prefix X) (hp : p≠Prefix.empty)
    (x : X) (b : Bool) : ∃ h : group (Γ:=Γ) (X:=X), ∀ f,
…

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

  42. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.comp_oneBit_comm line 422
  43. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.oneBit_ne_empty line 430
  44. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localizePerm_comp line 435
  45. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localize_comp line 455
  46. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.diagonal line 460

    Source documentation

    Two equal local copies in the coordinate halves.

    def diagonal (x : X) (f : group (Γ:=Γ) (X:=X)) : group (Γ:=Γ) (X:=X) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group

  47. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.diagonal_attach line 463
  48. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.exists_fresh line 483

    Source documentation

    A coordinate unused by the finite prefix data exists in the infinite cube.

    lemma exists_fresh [Infinite X] (A : Table (Γ:=Γ) f) :
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table

  49. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.untwisted_commutes_attach line 494
  50. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Untwisted line 509

    Source documentation

    A table with no coordinate twisting on any chart.

    def Untwisted (f : group (Γ:=Γ) (X:=X)) : Prop :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group

  51. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Untwisted.localize line 512
  52. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Untwisted.exists_diagonal line 523
  53. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.allRefine line 544

    Source documentation

    Simultaneously refine every brick by the same finite partition.

    abbrev allRefine (P Q : Partition X) : Partition X where
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition

  54. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.permute line 561

    Source documentation

    Permute all members of a partition, preserving their cube tails.

    def permute (P : Partition X) : Equiv.Perm P.index →* group (Γ:=Γ) (X:=X) where
…

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

  55. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.permute_attach line 578
  56. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.permute_allRefine line 583
  57. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.doubled_swap_commutator line 596
  58. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.swap_mem_commutatorSet line 609

    Source documentation

    Bisection turns every finite brick transposition into a double transposition, which is an actual commutator in the finite-table group.

    lemma Partition.swap_mem_commutatorSet (P : Partition X) (x : X) (i j : P.index) :
    P.permute (Γ:=Γ) (Equiv.swap i j)∈commutatorSet (group (Γ:=Γ) (X:=X)) := by
…

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

  59. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.permute_mem_commutator line 620

    Source documentation

    Every permutation of a finite dyadic partition has trivial abelianization.

    theorem Partition.permute_mem_commutator (P : Partition X) (x : X)
    (e : Equiv.Perm P.index) : P.permute (Γ:=Γ) e∈commutator (group (Γ:=Γ) (X:=X)) := by
…

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

  60. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.CorrectionIndex line 640
  61. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.correctionIndex_finite line 642
  62. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.correctionSource line 646
  63. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.correctionTarget line 649
  64. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.correction_chart line 652
  65. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.correction line 674

    Source documentation

    All coordinate labels cancel when a table is compared with its double along a coordinate unused by its source prefixes.

    def correction (A : Table (Γ:=Γ) f.val) (x : X)
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table

  66. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.exists_untwisted_correction line 691

    Source documentation

    Every twisted table differs from two half-copies of itself by an untwisted finite table. This is a literal table construction, not an abelianized identity.

    theorem exists_untwisted_correction [Infinite X] (f : group (Γ:=Γ) (X:=X)) :
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group

  67. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.map_localize_half line 705
  68. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.map_localize_diagonal line 712
  69. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.eq_one_of_square_eq_self line 718
  70. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.map_localize_untwisted_eq_one line 722
  71. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.map_untwisted_eq_one line 731
  72. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.map_localize_eq_one line 741
  73. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.map_eq_one line 752

    Source documentation

    Every commutative image of the infinite-coordinate twisted table group is trivial. The proof uses actual finite table label cancellation and compression.

    theorem map_eq_one [Infinite X] (h : group (Γ:=Γ) (X:=X) →* H)
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group

  74. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.infinite_group_perfect line 762
  75. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.size line 777
  76. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.size_refinement_bit line 779
  77. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.pad line 790

    Source documentation

    Add arbitrarily many complement bricks while leaving a proper selected brick unchanged.

    lemma pad (P : Partition X) (i : P.index) (hi : P.brick i≠Prefix.empty) (x : X) (n : ℕ) :
    ∃ Q : Partition X, ∃ j : Q.index, Q.brick j=P.brick i ∧ Q.size=P.size+n := by
…

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

  78. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.exists_brick_extension line 805

    Source documentation

    Any two proper finite dyadic bricks are related by an actual untwisted finite table chart, with no equal-volume or equal-depth restriction.

    theorem exists_brick_extension [Nonempty X] (p q : Prefix X)
    (hp : p≠Prefix.empty) (hq : q≠Prefix.empty) :
    ∃ h : group (Γ:=Γ) (X:=X), ∀ z,h.val (p.attach z)=q.attach z := by
…

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

  79. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.normal_transport_localize line 825
  80. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.localize_empty line 841
  81. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.normal_contains_local_copy line 850

    Source documentation

    Perfection upgrades the localized double-commutator conclusion to a full local copy inside every nontrivial normal subgroup.

    lemma normal_contains_local_copy [Infinite X]
    (N : Subgroup (group (Γ:=Γ) (X:=X))) [N.Normal] (hN : N≠⊥) :
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group

  82. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.normal_eq_top line 863

    Source documentation

    Simplicity of the actual twisted finite-table permutation group on an infinite coordinate set. No finite-presentation or simplicity endpoint is assumed.

    theorem normal_eq_top [Infinite X]
    (N : Subgroup (group (Γ:=Γ) (X:=X))) [N.Normal] (hN : N≠⊥) : N=⊤ := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group

  83. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.infinite_group_simple line 885
  84. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.(instance at line 899) line 899
  85. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.code line 914

    Source documentation

    A finite code for all chart data, not a code for arbitrary cube points.

    def code (A : Table (Γ:=Γ) f) : List (Prefix X × Prefix X × Γ) := by
…

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

  86. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.mem_code line 920
  87. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.eq_of_code_eq line 932
  88. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group_countable line 946

    Source documentation

    The concrete twisted group is countable under the standing countability hypotheses, although the Cantor cube itself is uncountable.

    instance group_countable [Countable Γ] [Countable X] : Countable (group (Γ:=Γ) (X:=X)) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.group