OAI/GroupTheory/BooneHigman/Trees.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Coordinate grids, binary trees, and tree-pair representatives.

  1. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.count_flatMap_ge line 19
  2. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.extends_of_compatible_of_length_le line 30
  3. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.exists_length_bound line 39

    Source documentation

    A finite list of splitting coordinates can dominate any finite prefix.

    lemma exists_length_bound (p : Prefix X) :
    ∃ l : List X, ∀ x,(p.word x).length≤l.count x := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix

  4. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.grid line 58

    Source documentation

    Repeated simultaneous bisections, recording all colours with multiplicity. This is a genuine finite forest partition, not an assumed normal form.

    abbrev grid : List X → Partition X
  | [] => trivial
  | x::l => (bit x).allRefine (grid l)

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.trivial, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.bit, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.allRefine

  5. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.grid_length line 62
  6. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.exists_grid_bound line 76

    Source documentation

    Any finite collection of bricks has a single grid fine enough for every nonempty intersection to be an entire grid cell.

    lemma exists_grid_bound {I : Type} [Fintype I] (p : I → Prefix X) :
    ∃ l : List X,∀ i j,p i |>.Compatible ((grid l).brick j) →
      (p i).Extends ((grid l).brick j) := by
…

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

  7. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.exists_grid_refinement line 90

    Source documentation

    Every dyadic partition admits an actual iterated-bisection grid refinement.

    lemma exists_grid_refinement (P : Partition X) :
    ∃ l : List X,∀ j : (grid l).index,∃! i : P.index,(P.brick i).Extends ((grid l).brick j) := by
…

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

  8. inductive OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree line 110

    Source documentation

    A finite coloured binary splitting forest with one root.

    inductive Tree (X : Type v) : Type v
  | leaf : Tree X
  | split : X → Tree X → Tree X → Tree X

namespace Prefix
variable {X : Type v}

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix

  9. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.empty_comp line 116
  10. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.comp_empty line 117
  11. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.comp_assoc line 118
  12. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Leaves line 125

    Source documentation

    Leaf indices stay in the small universe, even for large colour sets.

    abbrev Leaves : Tree X → Type
  | .leaf => PUnit
  | .split _ a b => Leaves a ⊕ Leaves b

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree

  13. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.leaves_fintype line 129
  14. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.brick line 137
  15. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.cover line 142
  16. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.partition line 180
  17. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.grid line 186
  18. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.grid_length line 190
  19. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graft line 210
  20. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graftLeaves line 214
  21. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graft_prefix line 244
  22. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.eq_of_compatible_of_length_eq line 270
  23. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.count_repeated_nodup line 276
  24. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.schedule line 288
  25. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.schedule_count line 291
  26. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.brick_injective line 301
  27. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.indexEquivOfBricks line 308
  28. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.indexEquivOfBricks_spec line 323
  29. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.exists_tree_grid_bound line 326
  30. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Partition.grid_bricks_of_lengths line 334
  31. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.reindex line 349
  32. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.FamilyIndex line 371
  33. instance OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.familyIndex_fintype line 373
  34. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.family_source_cover line 379
  35. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.refineFamily line 397

    Source documentation

    Refining each chart by an independently chosen finite partition preserves its actual cube permutation and transports the tail with the original label.

    def refineFamily (A : Table (Γ:=Γ) f) (P : A.index → Partition X) : Table (Γ:=Γ) f where
…

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

  36. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.exists_source_tree line 409
  37. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table.exists_tree_pair line 437

    Source documentation

    Every actual finite labelled table admits a coloured tree-pair model. This is the normal form needed for a forest presentation; it does not by itself prove finite presentation.

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

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Table