OAI/Algebra/GroupRing/SupportedImage.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.SupportedImage.vertices line 14

   Source documentation

   Discard isolated ambient vertices as well as unused darts.

   def vertices : Finset V := Q.image Γ.origin

2. def OAI.TorsionFreeZeroDivisors.SupportedImage.graph line 16
3. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.no_isolated line 22
4. def OAI.TorsionFreeZeroDivisors.SupportedImage.inclusion line 28

   Source documentation

   Literal inclusion into the actual source graph subdivision.

   def inclusion : (graph Γ Q hQ).subdivision →g Γ.subdivision where
   …

   Mentions: OAI.TorsionFreeZeroDivisors.SupportedImage.graph

5. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.inclusion_injective line 37
6. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.inclusion_weight line 39
7. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.girth line 50
8. def OAI.TorsionFreeZeroDivisors.SupportedImage.path line 60
9. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.path_val line 61
10. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.length line 64
11. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.nonempty line 66
12. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.chain line 71
13. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.mem_path line 79
14. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.head_value line 86
15. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.cyclic line 92
16. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.covered line 110
17. def OAI.TorsionFreeZeroDivisors.SupportedImage.used line 118

    Source documentation

    The symmetric set of precisely the darts used by the actual paths.

    def used [Fintype P] (paths : P → List D) : Finset D :=
    …

18. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.mem_used line 120
19. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.used_symmetric line 134
20. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.path_in_used line 140
21. lemma OAI.TorsionFreeZeroDivisors.RootPins.pin_map line 147
22. def OAI.TorsionFreeZeroDivisors.SupportedImage.sideVertex line 159
23. def OAI.TorsionFreeZeroDivisors.SupportedImage.sideDart line 161
24. lemma OAI.TorsionFreeZeroDivisors.SupportedImage.side_root line 163
25. def OAI.TorsionFreeZeroDivisors.SupportedImage.embedding line 179

    Source documentation

    Actual embeddings restrict to the used image, with the exact side/root pin.

    def embedding
        (e : RealizationTransport.Embedding (SideRestriction.graph Γ side hs b) (fun d => label d.val)
          outgoing (RootPins.pin (SidePins.root side (root.map Subtype.val) b) target) bar r) :
        RealizationTransport.Embedding
          (SideRestriction.graph (graph Γ Q hQ) (fun v => side v.val) (fun d => hs d.val) b)
          (fun d => label d.val.val) outgoing
          (RootPins.pin (SidePins.root (fun v : vertices Γ Q => side v.val) root b) target) bar r :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding, OAI.TorsionFreeZeroDivisors.SideRestriction.graph, OAI.TorsionFreeZeroDivisors.RootPins.pin, OAI.TorsionFreeZeroDivisors.SidePins.root, OAI.TorsionFreeZeroDivisors.SupportedImage.graph, OAI.TorsionFreeZeroDivisors.SupportedImage.vertices

26. structure OAI.TorsionFreeZeroDivisors.AmbientPattern.Data line 197

    Source documentation

    A path system in an ambient finite graph. The graph need not be the union of the paths; taking its literal supported image constructs the raw data.

    structure Data (B K I rep : ℕ) where
    …

27. abbrev OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.used line 238
28. abbrev OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.symmetric line 239
29. abbrev OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.supportedGraph line 240
30. abbrev OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.vertices line 241
31. abbrev OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.pathUsed line 242
32. abbrev OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.supportedPaths line 243
33. lemma OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.lengths_eq line 244
34. abbrev OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.comparison line 246
35. abbrev OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.iso line 247
36. abbrev OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.position line 248
37. lemma OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.dart_eq line 250
38. def OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.supported line 259

    Source documentation

    Restrict to actual used darts and their incident vertices. Every original length, comparison and counting hypothesis is transported verbatim.

    def supported : RawSourcePattern.Data B K I rep where
    …

    Mentions: OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data

39. abbrev OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.supportedRoot line 310
40. lemma OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.supported_root line 312
41. def OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.event line 321
42. lemma OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.comparing line 337
43. lemma OAI.TorsionFreeZeroDivisors.AmbientPattern.Data.supported_event line 357

    Source documentation

    Restrict the literal realization, including its exact root and labels, to the supported raw source pattern.

    lemma supported_event (x : Types.VertexA rep) (y : Types.VertexB rep) (r : Match rep)
        (h : a.event x y r) : a.supported.event x y r := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.VertexB

44. theorem OAI.TorsionFreeZeroDivisors.AmbientPattern.with_diameter line 376

    Source documentation

    The fixed-sample bounded pattern conclusion applies to every original ambient path system, not only to a presupposed image or suppression.

    theorem with_diameter (B K I : ℕ) (hK : 0<K) (hI : 0<I) :
        ∀ᶠ rep in Filter.atTop,∀ (x : Types.VertexA rep) (y : Types.VertexB rep),
          ∃ r∈samples rep,GraphSample.Diameters rep r ∧ ∀ a : Data B K I rep,¬a.event x y r := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.VertexB, OAI.TorsionFreeZeroDivisors.GraphSample.Diameters, OAI.TorsionFreeZeroDivisors.AmbientPattern.Data