OAI/GroupTheory/BooneHigman/BinaryCategory.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Self-similar binary group categories, associativity, symmetry, naturality, and braids.

  1. structure OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Data line 20

    Source documentation

    Binary self-similarity data for a group, with the associativity laws in explicit multiplicative orientation. The concrete finite structural quotient supplies every field; this is not an assumption on the main theorem's input.

    structure Data (H : Type u) [Group H] where
…
  2. inductive OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Object line 26
  3. structure OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Hom line 32
  4. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Hom.eq_one line 38
  5. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Hom.id line 40
  6. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Hom.comp line 41
  7. instance OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.(instance at line 47) line 47
  8. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.id_val line 55
  9. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.comp_val line 56
  10. abbrev OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Object.tensor line 61
  11. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Object.tensor_zero line 64
  12. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Object.zero_tensor line 65
  13. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Object.tensor_assoc line 66
  14. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.tensorVal line 72
  15. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.tensorVal_zero_left line 78
  16. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.tensorHom line 80
  17. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.tensorHom_val line 89
  18. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.tensor_id line 92
  19. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.tensor_comp line 97
  20. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.iso line 106
  21. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.associatorVal line 112
  22. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.associator line 116
  23. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.leftUnitor line 121
  24. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.rightUnitor line 122
  25. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.monoidalStruct line 125
  26. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.associator_natural line 135
  27. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.leftUnitor_natural line 152
  28. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.rightUnitor_natural line 157
  29. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.pentagon line 165
  30. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.triangle line 182
  31. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.monoidal line 190
  32. structure OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.SymmetryData line 210
  33. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.symmetry_inv line 217
  34. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.braidingVal line 219
  35. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.braiding line 223
  36. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.braiding_natural line 227
  37. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.hexagon_equation line 241
  38. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.hexagon_equation_reverse line 245
  39. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.braiding_hexagon_forward line 249
  40. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.braiding_hexagon_reverse line 263
  41. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.braiding_symmetry line 278
  42. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.symmetric line 285
  43. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.tensor_conjugate line 301
  44. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.tensor_commute line 306
  45. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.middleSwap line 314

    Source documentation

    The four-leaf middle transposition, expressed only in associator, symmetry and binary tensor; its naturality is needed in the colour-orbit reduction.

    def middleSwap : H :=
…
  46. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.middleSwap_naturality line 317
  47. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.reassociate_four line 358
  48. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.middleSwap_interchange line 376

    Source documentation

    Full four-leaf naturality, not just the identical-label specialization.

    lemma middleSwap_interchange (a b c e : H) :
    middleSwap d q*d.tensor (d.tensor (a,b),d.tensor (c,e))*(middleSwap d q)⁻¹=
      d.tensor (d.tensor (a,c),d.tensor (b,e)) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.middleSwap

  49. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.middleSwap_involutive line 403
  50. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.firstSwap line 438

    Source documentation

    Adjacent swaps in a fixed left-associated triple.

    def firstSwap : H := d.tensor (q.c,1)
  51. def OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.secondSwap line 439
  52. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.adjacent_braid line 441
  53. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.firstSwap_square line 455
  54. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.secondSwap_square line 461
  55. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.firstSwap_naturality line 478
  56. lemma OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.secondSwap_naturality line 484