OAI/Algebra/GroupRing/FullPairing.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.closed_split line 16

   Source documentation

   Transfer the SAME separator sets/parts/cost to the actual short-closed paths. In particular no extra charge for the appended tails is introduced.

   def closed_split (d : DecidableEq (ClosedWords.Piece s cap)) (S : Finset (ClosedWords.Piece s cap))
       (P : @RecursiveSeparator.Split (ClosedWords.Piece s cap) d
         (PairingClusters.Rel (fun z : Position (BalancedRotation.len s.paths cap hc)=>z.1)
           (a.α cap hc)) S) :
       @RecursiveSeparator.Split (ClosedWords.Piece s cap) d
         (PairingClusters.Rel (fun z : Position (fun t=>((a.closed cap hc hL hd).paths t).length)=>z.1)
           (a.closed cap hc hL hd).comparisons.pairing.partner) S :=
   …

   Mentions: OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.Piece, OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split, OAI.TorsionFreeZeroDivisors.PairingClusters.Rel, OAI.TorsionFreeZeroDivisors.BalancedRotation.len

2. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.segmented_genusZero line 38

   Source documentation

   The actual segmented words of a reduced lifted disk picture have genus zero, with their literal segment-boundary rotation and full letter pairing. This does not assert the missing sharp planar separator theorem.

   lemma segmented_genusZero :
       MapEuler.GenusZero
         (BoundaryRotation.perm (BalancedRotation.len (system a hzw hr hz).paths cap hc))
         ((pairing a hzw hr hz).α cap hc) :=
   …

   Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.BoundaryRotation.perm, OAI.TorsionFreeZeroDivisors.BalancedRotation.len, OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.system, OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.pairing

3. theorem OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_subpairing line 56

   Source documentation

   Any submatching of a literal genus-zero map is still genus zero; dangling half-edges are retained as fixed points. No embedding predicate is assumed.

   theorem genusZero_subpairing (σ α β : Equiv.Perm O)
       (ha : Function.Involutive α) (_hb : Function.Involutive β)
       (hsub : ∀ x, β x = x ∨ β x = α x) (hz : GenusZero σ α) :
       GenusZero σ β := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero

4. def OAI.TorsionFreeZeroDivisors.MapEuler.inducedPairFun line 91

   Source documentation

   Keep a pair precisely when both its actual endpoint darts satisfy P.

   def inducedPairFun (α : Equiv.Perm O) (P : O → Prop) (x : O) : O :=
   …

5. lemma OAI.TorsionFreeZeroDivisors.MapEuler.inducedPairFun_involutive line 95
6. def OAI.TorsionFreeZeroDivisors.MapEuler.inducedPair line 104
7. lemma OAI.TorsionFreeZeroDivisors.MapEuler.inducedPair_apply line 112
8. theorem OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_inducedPair line 118

   Source documentation

   The rotation of every vertex is unchanged; only crossing/outside pairs are removed. This handles loops, parallel edges, and disconnected graphs.

   theorem genusZero_inducedPair (σ α : Equiv.Perm O) (ha : Function.Involutive α)
       (P : O → Prop) (hz : GenusZero σ α) : GenusZero σ (inducedPair α ha P) := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.MapEuler.inducedPair

9. def OAI.TorsionFreeZeroDivisors.MapEuler.graph line 127

   Source documentation

   The underlying simple graph of the actual permutation map. Ignoring loops and parallel copies does not discard any adjacency between distinct vertices.

   def graph (σ α : Equiv.Perm O) (ha : Function.Involutive α) : SimpleGraph (Cycle σ) where
   …

10. lemma OAI.TorsionFreeZeroDivisors.MapEuler.graph_adj line 135
11. theorem OAI.TorsionFreeZeroDivisors.MapEuler.graph_inducedPair line 142

    Source documentation

    The graph after matching deletion is exactly the induced relation on the chosen vertices, with the other vertices isolated. This is literal equality of adjacencies, not an assumption of inherited planarity.

    theorem graph_inducedPair (σ α : Equiv.Perm O) (ha : Function.Involutive α)
        (S : Set (Cycle σ)) (v w : Cycle σ) :
        (graph σ (inducedPair α ha (fun x=>cycle σ x∈S))
          (inducedPairFun_involutive α ha _)).Adj v w ↔
        (graph σ α ha).Adj v w ∧ v ∈ S ∧ w ∈ S := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.graph, OAI.TorsionFreeZeroDivisors.MapEuler.inducedPair, OAI.TorsionFreeZeroDivisors.MapEuler.inducedPairFun_involutive

12. lemma OAI.TorsionFreeZeroDivisors.MapEuler.component_rot line 170
13. lemma OAI.TorsionFreeZeroDivisors.MapEuler.component_pair line 172
14. lemma OAI.TorsionFreeZeroDivisors.MapEuler.reachable_pair line 176
15. lemma OAI.TorsionFreeZeroDivisors.MapEuler.reachable_of_component line 183
16. def OAI.TorsionFreeZeroDivisors.MapEuler.vertexComponent line 199
17. lemma OAI.TorsionFreeZeroDivisors.MapEuler.vertexComponent_cycle line 202
18. lemma OAI.TorsionFreeZeroDivisors.MapEuler.vertexComponent_adj line 205
19. lemma OAI.TorsionFreeZeroDivisors.MapEuler.vertexComponent_reachable line 211
20. theorem OAI.TorsionFreeZeroDivisors.MapEuler.component_eq_iff_reachable line 220

    Source documentation

    Equality of actual map components is exactly graph reachability, including unpaired darts, loops and parallel edges. No graph planarity predicate intervenes.

    theorem component_eq_iff_reachable (x y : O) :
        component σ α x=component σ α y ↔
          (graph σ α ha).Reachable (cycle σ x) (cycle σ y) :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.component, OAI.TorsionFreeZeroDivisors.MapEuler.graph

21. def OAI.TorsionFreeZeroDivisors.MapEuler.graphComponentEquiv line 226

    Source documentation

    The map and the underlying simple graph have literally the same components.

    def graphComponentEquiv : Component σ α ≃ (graph σ α ha).ConnectedComponent where
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.Component, OAI.TorsionFreeZeroDivisors.MapEuler.graph

22. lemma OAI.TorsionFreeZeroDivisors.MapEuler.graphComponent_card line 241
23. def OAI.TorsionFreeZeroDivisors.MapEuler.realizeDart line 253

    Source documentation

    Pick an actual occurrence realizing each directed edge; this is injective because both endpoint vertices of an occurrence are fixed.

    def realizeDart (d : (graph σ α ha).Dart) : O := d.adj.2.choose
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.graph

24. lemma OAI.TorsionFreeZeroDivisors.MapEuler.realizeDart_fst line 255
25. lemma OAI.TorsionFreeZeroDivisors.MapEuler.realizeDart_snd line 258
26. lemma OAI.TorsionFreeZeroDivisors.MapEuler.realizeDart_mem line 260
27. lemma OAI.TorsionFreeZeroDivisors.MapEuler.realizeDart_injective line 266
28. theorem OAI.TorsionFreeZeroDivisors.MapEuler.twice_graph_edges_le_support line 274

    Source documentation

    Removing loops and parallel copies lowers the true paired-edge count.

    theorem twice_graph_edges_le_support :
        2*Nat.card (graph σ α ha).edgeSet≤α.support.card := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.graph

29. theorem OAI.TorsionFreeZeroDivisors.MapEuler.graph_isTree_of_support line 287

    Source documentation

    A connected map with the minimal possible true edge count is a tree, even though the ambient definition permits loops and parallel edges.

    theorem graph_isTree_of_support (hc : (graph σ α ha).Connected)
        (he : α.support.card+2=2*Nat.card (Cycle σ)) : (graph σ α ha).IsTree := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.graph

30. lemma OAI.TorsionFreeZeroDivisors.MapEuler.edge_has_realizer line 301
31. def OAI.TorsionFreeZeroDivisors.MapEuler.edgeRep line 314
32. lemma OAI.TorsionFreeZeroDivisors.MapEuler.edgeRep_ne line 315
33. lemma OAI.TorsionFreeZeroDivisors.MapEuler.edgeRep_edge line 317
34. def OAI.TorsionFreeZeroDivisors.MapEuler.edgeOfSubgraph line 322
35. def OAI.TorsionFreeZeroDivisors.MapEuler.pairFinset line 324
36. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pairFinset_card line 328
37. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pairFinset_nonfixed line 330
38. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pairFinset_pair line 336
39. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pairFinset_edge line 342
40. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pairFinset_disjoint line 350
41. def OAI.TorsionFreeZeroDivisors.MapEuler.pickedDarts line 358
42. lemma OAI.TorsionFreeZeroDivisors.MapEuler.mem_pickedDarts line 359
43. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pickedDarts_nonfixed line 362
44. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pickedDarts_pair line 365
45. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pickedDarts_card line 368
46. def OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair line 377

    Source documentation

    A chosen simple subgraph is realized by exactly one original paired edge per simple edge, with the original vertex rotations unchanged.

    def subgraphPair : Equiv.Perm O := inducedPair α ha (fun x=>x∈pickedDarts σ α ha T hT)

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.inducedPair, OAI.TorsionFreeZeroDivisors.MapEuler.pickedDarts

47. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_involutive line 378
48. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_apply line 380
49. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_support line 386
50. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_support_card line 395
51. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_graph line 398
52. lemma OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_subgraphPair line 426