OAI/GroupTheory/BooneHigman/EndpointCoherence.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Associators, symmetries, coordinate invariance, and coherence of endpoint quotient data.

  1. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralBinaryData line 25

    Source documentation

    Every algebraic field comes from the finite structural quotient's proved relations. No new relation is postulated in order to invoke coherence.

    def structuralBinaryData : BinaryGroupCategory.Data (StructuralQuotient (Γ:=Γ) x s) where
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Data, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.StructuralQuotient

  2. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralMonoidal line 35

    Source documentation

    The actual finite quotient is the positive-object automorphism group of a monoidal category. Its empty object is separate, with trivial automorphism group.

    @[instance_reducible] def structuralMonoidal :
    MonoidalCategory (BinaryGroupCategory.Object (StructuralQuotient (Γ:=Γ) x s)) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.BinaryGroupCategory.Object, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.StructuralQuotient

  3. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralExpansion line 39
  4. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.coherent_structural_routes line 47

    Source documentation

    All parallel associator/unitor routes agree internally in the finite presentation. This reuses pinned Mathlib's proved monoidal-coherence theorem, not the semantic action's equality or any unproved presentation theorem.

    lemma coherent_structural_routes {A B : FreeMonoidalCategory PUnit} (f g : A ⟶ B) :
    ((structuralExpansion x s hs).map f).val=((structuralExpansion x s hs).map g).val := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralExpansion

  5. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralExpansion_associator line 52
  6. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralSymmetryData line 70
  7. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralSymmetric line 80
  8. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralProject_middleSwapWord line 95
  9. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralMiddleSwap_naturality line 103
  10. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedMiddleSwap_naturality line 110
  11. theorem OAI.FiniteAlgebraicEnvelopes.covariant_interchange line 126

    Source documentation

    A grid relation propagates along ordered-pair orbits, because the middle transposition commutes with four identical leaf labels.

    theorem covariant_interchange (R D : Γ → H) (E : X → X → H) (M : H)
    (hc : ∀ g a b,R g*E a b=E (g • a) (g • b)*D g)
    (hm : ∀ g,Commute M (D g))
    {a b c d : X} (g : Γ) (hga : g • a=c) (hgb : g • b=d)
    (hab : E a b=E b a*M) : E c d=E d c*M := by
…
  12. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpoint_interchange_all line 159

    Source documentation

    Every distinct-colour elementary interchange follows inside the explicit finite endpoint quotient, from its one pair representative and finite label and structural laws. This is not a completeness theorem for arbitrary tables.

    lemma endpoint_interchange_all (a b : X) (hab : a≠b) :
    endpointProject x s t y (gridWord x a b)=
      endpointProject x s t y (gridWord x b a)*endpointProject x s t y (middleSwapWord x) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointProject, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.gridWord, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.middleSwapWord

  13. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointProject_interchange_all line 186

    Source documentation

    The infinite family of pair-colour kernel words is killed by this one finite presentation candidate. No kernel injectivity is used.

    lemma endpointProject_interchange_all (a b : X) (hab : a≠b) :
    endpointProject x s t y (interchangeWord x a b)=1 := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointProject, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.interchangeWord

  14. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.structuralMiddleSwap_interchange line 204
  15. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedMiddleSwap_interchange line 213
  16. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedColourTensor_double line 225
  17. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpoint_decorated_interchange line 251

    Source documentation

    Arbitrary four decorated subtrees obey the colour interchange in the finite endpoint quotient. This is the local contextual law, not only the empty grid law.

    lemma endpoint_decorated_interchange (y z : X) (hyz : y≠z)
    (a b c d : DecoratedQuotient (Γ:=Γ) x s t) :
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.DecoratedQuotient

  18. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedToEndpoint_surjective line 286
  19. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointLocalization line 289
  20. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointRightLocalization line 292
  21. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedToEndpoint_localization line 296
  22. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedToEndpoint_rightLocalization line 301
  23. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointLocalizations_commute line 309
  24. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointTensor line 316
  25. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointTensor_apply line 321
  26. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedToEndpoint_tensor line 325
  27. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointBaker line 331
  28. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointColourTensor line 334
  29. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointColourTensor_apply line 338
  30. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedToEndpoint_colourTensor line 342
  31. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointColourTensor_interchange line 353
  32. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.prefixShift line 375
  33. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.prefixShift_comp line 377
  34. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.labelledFold line 384

    Source documentation

    Interpretation of leaf decorations by coordinate-local binary tensor. Decorations are indexed by literal bricks, not by an arbitrary ordering.

    def labelledFold (T : X → H × H → H) : Tree X → (Prefix X → H) → H
  | .leaf,F => F Prefix.empty
  | .split x a b,F => T x (labelledFold T a (prefixShift F (Prefix.oneBit x false)),
      labelledFold T b (prefixShift F (Prefix.oneBit x true)))

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.empty, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.prefixShift, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.oneBit

  35. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.labelledFold_congr line 389
  36. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.Coherent.labelledFold_eq line 405
  37. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.labelledFold_eq_of_brickSet_eq line 422

    Source documentation

    Coordinate-tree invariance for arbitrary leaf group decorations.

    lemma labelledFold_eq_of_brickSet_eq (a b : Tree X) (hab : brickSet a=brickSet b)
    (F : Prefix X → H) : labelledFold T a F=labelledFold T b F :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.brickSet, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.labelledFold

  38. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpoint_labelledFold_eq line 437
  39. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.labelledFold_naturality line 454

    Source documentation

    Naturality under a coordinate relabelling, stated independently of a particular quotient. It applies to every finite coloured tree, not just grids.

    lemma labelledFold_naturality (T : X → H × H → H) (f : X → X)
    (P : Prefix X → Prefix X) (C : H → H) (hP₀ : P Prefix.empty=Prefix.empty)
    (hP : ∀ y b p,P ((Prefix.oneBit (f y) b).comp p)=(Prefix.oneBit y b).comp (P p))
    (hC : ∀ y a b,C (T y (a,b))=T (f y) (C a,C b))
    (a : Tree X) (F : Prefix X → H) :
    C (labelledFold T a F)=labelledFold T (mapColors f a) (fun p=>C (F (P p))) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.empty, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Prefix.oneBit, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.labelledFold, OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Tree.mapColors

  40. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twistPrefix_comp line 478
  41. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.twistPrefix_empty line 482
  42. def OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointRoot line 491
  43. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.decoratedToEndpoint_root line 494
  44. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpointColourTensor_covariance line 499
  45. lemma OAI.FiniteAlgebraicEnvelopes.TwistedBrinThompson.Generators.endpoint_labelledFold_covariance line 510