OAI/GroupTheory/ArtinCAT0/Wires.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ArtinCAT0.WireSystem line 7
  2. lemma OAI.ArtinCAT0.WireSystem.mate_mate line 17
  3. lemma OAI.ArtinCAT0.WireSystem.pass_pass line 18
  4. abbrev OAI.ArtinCAT0.WireSystem.Live line 19
  5. structure OAI.ArtinCAT0.WireSystem.Cut line 21
  6. abbrev OAI.ArtinCAT0.WireSystem.Cut.q line 27
  7. def OAI.ArtinCAT0.WireSystem.Cut.Removed line 29
  8. abbrev OAI.ArtinCAT0.WireSystem.Cut.Kept line 30
  9. lemma OAI.ArtinCAT0.WireSystem.Cut.removed_pass line 32
  10. lemma OAI.ArtinCAT0.WireSystem.Cut.pass_ne line 47
  11. lemma OAI.ArtinCAT0.WireSystem.Cut.internal line 52
  12. lemma OAI.ArtinCAT0.WireSystem.Cut.mate_pass_outside line 62
  13. def OAI.ArtinCAT0.WireSystem.Cut.splice line 71
  14. lemma OAI.ArtinCAT0.WireSystem.Cut.splice_inside line 75
  15. lemma OAI.ArtinCAT0.WireSystem.Cut.splice_outside line 77
  16. lemma OAI.ArtinCAT0.WireSystem.Cut.splice_kept line 80
  17. lemma OAI.ArtinCAT0.WireSystem.Cut.splice_splice line 87
  18. lemma OAI.ArtinCAT0.WireSystem.Cut.splice_ne line 96
  19. def OAI.ArtinCAT0.WireSystem.Cut.reduced line 106
  20. lemma OAI.ArtinCAT0.WireSystem.Cut.live_kept line 113
  21. def OAI.ArtinCAT0.WireSystem.Cut.liveEquiv line 117
  22. def OAI.ArtinCAT0.WireSystem.Cut.extend line 123
  23. lemma OAI.ArtinCAT0.WireSystem.Cut.extend_kept line 129
  24. lemma OAI.ArtinCAT0.WireSystem.Cut.extend_pass_removed line 132
  25. lemma OAI.ArtinCAT0.WireSystem.Cut.extend_mate line 149
  26. lemma OAI.ArtinCAT0.WireSystem.Cut.extend_pass line 162
  27. lemma OAI.ArtinCAT0.WireSystem.Cut.reduced_color line 172
  28. structure OAI.ArtinCAT0.WireSystem.Resolution line 186

    Source documentation

    The bivalent parts of a finite graph can be suppressed. In addition to its boundary matching we retain extension of every antisymmetric edge weight.

    structure Resolution where
…
  29. def OAI.ArtinCAT0.WireSystem.Resolution.expand line 198
  30. lemma OAI.ArtinCAT0.WireSystem.Resolution.expand_color line 217
  31. def OAI.ArtinCAT0.WireSystem.Resolution.of_all_live line 224
  32. theorem OAI.ArtinCAT0.WireSystem.resolve line 239

    Source documentation

    Suppression of all bivalent vertices of a finite matching graph, with reversal-compatible labels and a cocycle lifting property. A closed component without live ends receives zero in the lift.

    theorem resolve {C : Type*} (r : C → C) (hr : Function.Involutive r) :
    ∀ (D : Type u) [Fintype D] (W : WireSystem D) (c : D → C),
      (∀ d, c (W.mate d) = r (c d)) →
      (∀ d, W.pass d ≠ d → c (W.pass d) = r (c d)) →
      ∃ R : W.Resolution, ∀ d, c (R.mate d).val = r (c d.val) := by
…

    Mentions: OAI.ArtinCAT0.WireSystem