OAI/Algebra/GroupRing/GraphConePresentation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.edgeSetoid line 15

    Source documentation

    Physical unoriented edges, retaining loops and parallel edges.

    def edgeSetoid : Setoid D where
…
  2. abbrev OAI.TorsionFreeZeroDivisors.GraphConePresentation.Edge line 28
  3. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.edge line 29
  4. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.representative line 30
  5. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.representative_cases line 31
  6. abbrev OAI.TorsionFreeZeroDivisors.GraphConePresentation.Generator line 37

    Source documentation

    Radial edges except for the one edge collapsed at the root of each component.

    abbrev Generator := S ⊕ {v : V // v≠R.base v}
  7. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.old line 38
  8. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.radial line 39
  9. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.triangle line 41
  10. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.attachment line 44

    Source documentation

    There is one two-cell per physical edge, NOT one per directed dart.

    def attachment (e : Edge Γ) : FreeGroup (Generator (S:=S) Γ R) := triangle Γ letters R (representative Γ e)

    Mentions: OAI.TorsionFreeZeroDivisors.GraphConePresentation.Edge, OAI.TorsionFreeZeroDivisors.GraphConePresentation.Generator, OAI.TorsionFreeZeroDivisors.GraphConePresentation.triangle, OAI.TorsionFreeZeroDivisors.GraphConePresentation.representative

  11. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.relations line 45
  12. abbrev OAI.TorsionFreeZeroDivisors.GraphConePresentation.Group line 46
  13. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.radialValue line 47
  14. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.oldMap line 48
  15. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.triangle_reverse line 49
  16. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.triangle_trivial line 53
  17. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.edge_value line 60
  18. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.path_value line 66
  19. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.radial_base line 75
  20. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.old_word line 77
  21. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.fromGraph line 84

    Source documentation

    The original graph-loop group maps to the nonredundant cone group.

    def fromGraph (hl : ∀ d,letters (Γ.reverse d)=(letters d)⁻¹)
    (hbase : ∀v,R.base (R.base v)=R.base v) :
    GraphPresentation.Group Γ letters R →* Group Γ letters R :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.GraphPresentation.Group, OAI.TorsionFreeZeroDivisors.GraphConePresentation.Group

  22. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.graph_value_base line 95
  23. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.toGraphGenerator line 104
  24. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.lift_old line 107
  25. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.lift_radial line 111
  26. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.toGraph line 118

    Source documentation

    The precise reverse Tietze map, keeping each new radial generator's value.

    def toGraph (hbase : ∀v,R.base (R.base v)=R.base v) :
    Group Γ letters R →* GraphPresentation.Group Γ letters R :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.GraphConePresentation.Group, OAI.TorsionFreeZeroDivisors.GraphPresentation.Group

  27. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.fromGraph_mk line 127
  28. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.fromGraph_value line 135
  29. def OAI.TorsionFreeZeroDivisors.GraphConePresentation.equivalence line 140
  30. lemma OAI.TorsionFreeZeroDivisors.GraphConePresentation.canonical_base line 163
  31. instance OAI.TorsionFreeZeroDivisors.GraphConePresentation.(instance at line 167) line 167