OAI/Algebra/GroupRing/ListPassages.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TorsionFreeZeroDivisors.ListPassages.rotate_val line 12
2. def OAI.TorsionFreeZeroDivisors.ListPassages.start line 26
3. def OAI.TorsionFreeZeroDivisors.ListPassages.cut line 28
4. lemma OAI.TorsionFreeZeroDivisors.ListPassages.last_mem line 31
5. lemma OAI.TorsionFreeZeroDivisors.ListPassages.first_mem line 41
6. theorem OAI.TorsionFreeZeroDivisors.ListPassages.passage line 51

   Source documentation

   The cyclic successor on actual list occurrences pairs exactly the internal passages, plus the closing passage precisely when the path is cyclic.

   theorem passage {R : D → D → Prop} (hc : p.IsChain R) (cyclic : Bool)
       (hclose : cyclic=true → ∀ᵉ (x∈p.getLast?) (y∈p.head?),R x y)
       (i : Fin p.length) (hcut : cut p hp cyclic ≠ some (finRotate p.length i)) :
       R (p.get i) (p.get (finRotate p.length i)) := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.ListPassages.cut

7. lemma OAI.TorsionFreeZeroDivisors.ChainPathTransport.outWord_head line 84
8. lemma OAI.TorsionFreeZeroDivisors.ChainPathTransport.word_head line 88
9. lemma OAI.TorsionFreeZeroDivisors.ChainPathTransport.word_last line 91
10. lemma OAI.TorsionFreeZeroDivisors.ChainPathTransport.word_ne_nil line 96
11. theorem OAI.TorsionFreeZeroDivisors.ChainPathTransport.isChain line 106

    Source documentation

    A genuine reduced original path transports to a genuine reduced path in its suppressed graph. Adjacency is read from the actual last/first darts; no graph path property is imposed on the decomposition as a hypothesis.

    theorem isChain (ds : List B)
        (hp : (ds.flatMap w).IsChain (PortWalk.step Γ.origin Γ.reverse)) :
        ds.IsChain (PortWalk.step (S).origin (S).reverse) := by
    …

12. lemma OAI.TorsionFreeZeroDivisors.ChainPathTransport.flatMap_head line 124
13. lemma OAI.TorsionFreeZeroDivisors.ChainPathTransport.flatMap_last line 132
14. theorem OAI.TorsionFreeZeroDivisors.ChainPathTransport.closing line 142

    Source documentation

    The closing passage of a cyclically immersed path survives suppression.

    theorem closing (ds : List B)
        (hc : ∀ᵉ (x∈(ds.flatMap w).getLast?) (y∈(ds.flatMap w).head?),
          PortWalk.step Γ.origin Γ.reverse x y) :
        ∀ᵉ (a∈ds.getLast?) (b∈ds.head?),PortWalk.step (S).origin (S).reverse a b := by
    …

15. theorem OAI.TorsionFreeZeroDivisors.ChainPathTransport.decomposes line 160

    Source documentation

    The decomposition retains all reduced passages and both geometric endpoints. Cyclic closing passages therefore also transport unchanged.

    theorem decomposes (p : List D)
        (hp : p.IsChain (PortWalk.step Γ.origin Γ.reverse))
        (hs : ∀ d∈p.head?,mark (Γ.origin d))
        (ht : ∀ d∈p.getLast?,mark (Γ.origin (Γ.reverse d))) :
        ∃ ds : List B, ds.flatMap w=p ∧
          ds.IsChain (PortWalk.step (S).origin (S).reverse) ∧
          ds.head?.map Subtype.val=p.head? ∧
          ds.getLast?.map (fun d => Γ.reverse ((S).reverse d).val)=p.getLast? := by
    …

16. abbrev OAI.TorsionFreeZeroDivisors.ListStageExponents.edge line 184
17. abbrev OAI.TorsionFreeZeroDivisors.ListStageExponents.mult line 185
18. theorem OAI.TorsionFreeZeroDivisors.ListStageExponents.cut_count line 188
19. theorem OAI.TorsionFreeZeroDivisors.ListStageExponents.exponent_nonpos line 198

    Source documentation

    The exact signed stage exponent of literal immersed paths, including a root saving for each noncyclic interval only at the first stage.

    theorem exponent_nonpos (M : ℕ) (hM : 0<M) (hm : ∀ d,mult Γ p d ≤ M) :
        (∑ j : Fin M, ((Fintype.card (ActiveV Γ (mult Γ p) j.val):ℤ)-
          (edges (stage Γ (mult Γ p) (multiplicity_reverse Γ (edge p)) j.val)).card-
          if j.val=0 then Fintype.card {i : I // cyclic i=false} else 0)) ≤ 0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ListStageExponents.mult, OAI.TorsionFreeZeroDivisors.ListStageExponents.edge

20. def OAI.TorsionFreeZeroDivisors.InvolutionOrientation.rank line 225
21. def OAI.TorsionFreeZeroDivisors.InvolutionOrientation.Chosen line 227
22. abbrev OAI.TorsionFreeZeroDivisors.InvolutionOrientation.Representative line 228
23. lemma OAI.TorsionFreeZeroDivisors.InvolutionOrientation.rank_ne line 233
24. lemma OAI.TorsionFreeZeroDivisors.InvolutionOrientation.chosen_or_reverse line 239
25. lemma OAI.TorsionFreeZeroDivisors.InvolutionOrientation.chosen_reverse_iff line 244
26. def OAI.TorsionFreeZeroDivisors.InvolutionOrientation.orient line 249
27. lemma OAI.TorsionFreeZeroDivisors.InvolutionOrientation.orient_injective line 251
28. lemma OAI.TorsionFreeZeroDivisors.InvolutionOrientation.orient_surjective line 268
29. def OAI.TorsionFreeZeroDivisors.InvolutionOrientation.equiv line 274
30. lemma OAI.TorsionFreeZeroDivisors.InvolutionOrientation.equiv_false line 277
31. lemma OAI.TorsionFreeZeroDivisors.InvolutionOrientation.equiv_true line 278
32. lemma OAI.TorsionFreeZeroDivisors.InvolutionOrientation.rep_card line 280
33. lemma OAI.TorsionFreeZeroDivisors.InvolutionOrientation.sum_invariant line 284
34. abbrev OAI.TorsionFreeZeroDivisors.ChainIsomorphism.Rep line 304
35. abbrev OAI.TorsionFreeZeroDivisors.ChainIsomorphism.repLength line 305
36. abbrev OAI.TorsionFreeZeroDivisors.ChainIsomorphism.Mark line 306
37. def OAI.TorsionFreeZeroDivisors.ChainIsomorphism.first line 308
38. def OAI.TorsionFreeZeroDivisors.ChainIsomorphism.last line 310
39. def OAI.TorsionFreeZeroDivisors.ChainIsomorphism.dartMap line 315
40. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.forward_mem line 318
41. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.dart_mem line 322
42. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.same_word line 331
43. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.dartMap_injective line 336
44. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.dartMap_surjective line 352
45. def OAI.TorsionFreeZeroDivisors.ChainIsomorphism.dartEquiv line 365
46. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.dartMap_reverse line 369
47. def OAI.TorsionFreeZeroDivisors.ChainIsomorphism.vertexMap line 375
48. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.internal_unmarked line 379
49. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.origin_map line 387
50. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.original_two_ports line 417
51. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.vertexMap_injective line 437
52. lemma OAI.TorsionFreeZeroDivisors.ChainIsomorphism.vertexMap_surjective line 459
53. def OAI.TorsionFreeZeroDivisors.ChainIsomorphism.vertexEquiv line 470
54. theorem OAI.TorsionFreeZeroDivisors.ChainIsomorphism.subdivision_isomorphic line 476

    Source documentation

    Replacing each actual maximal marked chain by a coordinate interval loses no vertices, darts, loop chains, parallel chains or reversal information.

    theorem subdivision_isomorphic (hcovered : ∀ d : D, ChainCoverage.Covered Γ.reverse (turn Γ.origin mark h2) Γ.reverse_reverse (turn_involutive Γ.origin mark h2) d) :
        ∃ (eV : ChainSubdivision.Vertex (repLength Γ mark h2) (V := Mark mark) ≃ V)
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainCoverage.Covered, OAI.TorsionFreeZeroDivisors.ChainSubdivision.Vertex, OAI.TorsionFreeZeroDivisors.ChainIsomorphism.repLength, OAI.TorsionFreeZeroDivisors.ChainIsomorphism.Mark

55. theorem OAI.TorsionFreeZeroDivisors.ChainIsomorphism.total_length line 485

    Source documentation

    Both orientations of every actual-image edge are retained exactly once.

    theorem total_length
        (hcovered : ∀ d : D, ChainCoverage.Covered Γ.reverse (turn Γ.origin mark h2) Γ.reverse_reverse
          (turn_involutive Γ.origin mark h2) d) :
        2 * ∑ c : Rep Γ mark h2, repLength Γ mark h2 c = Fintype.card D := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainCoverage.Covered, OAI.TorsionFreeZeroDivisors.ChainIsomorphism.Rep, OAI.TorsionFreeZeroDivisors.ChainIsomorphism.repLength

56. theorem OAI.TorsionFreeZeroDivisors.ChainIsomorphism.vertex_count line 494

    Source documentation

    The marked/interior count gives the precise signed stage vertex exponent.

    theorem vertex_count
        (hcovered : ∀ d : D, ChainCoverage.Covered Γ.reverse (turn Γ.origin mark h2) Γ.reverse_reverse
          (turn_involutive Γ.origin mark h2) d) :
        Fintype.card V + Fintype.card (Rep Γ mark h2) =
          Fintype.card (Mark mark) + ∑ c : Rep Γ mark h2, repLength Γ mark h2 c := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ChainCoverage.Covered, OAI.TorsionFreeZeroDivisors.ChainIsomorphism.Rep, OAI.TorsionFreeZeroDivisors.ChainIsomorphism.Mark, OAI.TorsionFreeZeroDivisors.ChainIsomorphism.repLength

57. theorem OAI.TorsionFreeZeroDivisors.ChainIsomorphism.actual_image_isomorphic line 505

    Source documentation

    The needed coverage is furnished by the actual immersed path system, not asserted as an additional structural property of a proposed pattern.

    theorem actual_image_isomorphic {J : Type*} (paths : J → List D)
        (hpaths : ∀ j, (paths j).IsChain (WeightedMoore.PortWalk.step Γ.origin Γ.reverse))
        (hstarts : ∀ j d, d∈(paths j).head? → mark (Γ.origin d))
        (himage : ∀ d : D, ∃ j, d∈paths j ∨ Γ.reverse d∈paths j) :
        ∃ (eV : ChainSubdivision.Vertex (repLength Γ mark h2) (V := Mark mark) ≃ V)
    …

    Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.step, OAI.TorsionFreeZeroDivisors.ChainSubdivision.Vertex, OAI.TorsionFreeZeroDivisors.ChainIsomorphism.repLength, OAI.TorsionFreeZeroDivisors.ChainIsomorphism.Mark