OAI/GroupTheory/BooneHigman/Diagrams.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram line 18

   Source documentation

   A full finite decorated tree pair, including the entire leaf bijection.

   structure Diagram (Γ:Type u) (X:Type v) where
   …

2. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value line 28
3. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.Realizes line 31
4. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.root line 34
5. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value_root line 36
6. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.realizes_root line 39
7. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.inverse line 42
8. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value_inverse line 46
9. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.Realizes.inverse line 54
10. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.compose line 64

    Source documentation

    Compose after identifying the two intermediate partitions.

    def compose (A C:Diagram Γ X) (e:A.target.Leaves ≃ C.source.Leaves) : Diagram Γ X where
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram

11. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value_compose line 71
12. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.Realizes.compose line 85
13. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value_one_of_realizes_one line 94
14. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.graft_brick_symm line 113
15. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.expansionFamily line 119
16. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.expand line 123

    Source documentation

    Expand the whole target and pull every fibre back through its true label.

    def expand (A:Diagram Γ X) (F:A.target.Leaves → Tree X) : Diagram Γ X where
    …

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

17. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.expand_label line 130
18. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value_expand line 137
19. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.Realizes.expand line 149
20. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.gridFill line 176
21. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.gridFill_length line 178
22. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.gridFill_equiv line 189
23. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.refine_target_grid line 201
24. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.refine_source_grid line 208
25. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.product line 218

    Source documentation

    The actual tree-pair value is closed under multiplication, synchronizing all intermediate bricks by a finite grid; no patching assumption is used.

    lemma product (gl:Tree.GridLaw d q B) {A C:Diagram Γ X} {f g:Equiv.Perm (Cube X)}
        (ha:Realizes A f) (hc:Realizes C g) :
        ∃ D:Diagram Γ X,Realizes D (g*f) ∧ value d q B R D=value d q B R C*value d q B R A := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.GridLaw, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Cube, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.Realizes, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value

26. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.plain line 239

    Source documentation

    Undecorated full tree wiring.

    def plain (a b:Tree X) (e:a.Leaves ≃ b.Leaves) : Diagram Γ X := ⟨a,b,e,fun _=>1⟩
    …

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

27. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value_plain line 241
28. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.realizes_plain line 245
29. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.half line 255

    Source documentation

    Prefix-localize an entire diagram, including its bijection and labels.

    def half (x:X) (A:Diagram Γ X) : Diagram Γ X where
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram

30. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value_half line 262
31. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.Realizes.half line 273
32. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.rotation line 287
33. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value_rotation line 292
34. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.realizes_rotation line 295
35. abbrev OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.exchange line 298
36. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.value_exchange line 301
37. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.realizes_exchange line 303
38. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.represented line 331

    Source documentation

    Elements with a genuine decorated-tree witness for both their algebraic value and their actual cube action form a subgroup.

    def represented : Subgroup K where
    …

39. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Diagram.mem_represented line 349
40. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.seedRepresented line 375
41. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.root_mem_seedRepresented line 379
42. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.half_mem_seedRepresented line 384
43. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.associator_mem_seedRepresented line 394
44. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.flip_mem_seedRepresented line 399
45. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.half_associator_mem_seedRepresented line 404
46. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.half_flip_mem_seedRepresented line 417
47. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.generator_mem_seedRepresented line 430
48. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.all_seedRepresented line 442

    Source documentation

    The entire finite presentation seed, not just its selected finite subgenerators, is represented by genuine decorated diagrams.

    lemma all_seedRepresented (g:Seed (Γ:=Γ) x) : g∈seedRepresented x s t y₀ hs ht hxy htwo := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.Seed, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.seedRepresented

49. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointProject_surjective line 471
50. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointEvaluation_project line 473
51. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpoint_diagram line 480

    Source documentation

    Every element of the actual finite endpoint presentation has a finite coloured decorated tree-pair whose value and semantics agree with it.

    lemma endpoint_diagram (z:EndpointQuotient (Γ:=Γ) x s t y₀) :
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.EndpointQuotient

52. theorem OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointEvaluation_injective line 491

    Source documentation

    Completeness of the explicit finite presentation via whole permutations and decorated common refinement; semantic injectivity follows from the construction.

    theorem endpointEvaluation_injective [FaithfulSMul Γ X] :
        Function.Injective (endpointEvaluation x s t y₀ hxy) := by
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointEvaluation

53. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointEquivalence line 503