OAI/GroupTheory/Hyperbolic/Chains.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Release075.FreeChain line 8

   Source documentation

   The free integral module on copies of the regular left group action.

   abbrev FreeChain (A G : Type) := (A × G) →₀ ℤ

2. def OAI.Release075.chainShift line 10
3. theorem OAI.Release075.chainShift_single line 14
4. abbrev OAI.Release075.BlockPresentation.C₀ line 22
5. abbrev OAI.Release075.BlockPresentation.C₁ line 23
6. def OAI.Release075.BlockPresentation.PositiveFace line 25
7. abbrev OAI.Release075.BlockPresentation.FaceBase line 29
8. abbrev OAI.Release075.BlockPresentation.C₂ line 30
9. def OAI.Release075.BlockPresentation.edgeChain line 33

   Source documentation

   An oriented edge is represented in a free module on the positive orientations.

   noncomputable def edgeChain (e : d.LiftedEdge) : d.C₁ :=
   …

10. theorem OAI.Release075.BlockPresentation.edgeChain_flip line 37
11. def OAI.Release075.BlockPresentation.boundary₁ line 42
12. theorem OAI.Release075.BlockPresentation.boundary₁_edgeChain line 47
13. def OAI.Release075.BlockPresentation.boundary₂ line 53
14. theorem OAI.Release075.BlockPresentation.boundary₁_boundary₂ line 59
15. def OAI.Release075.BlockPresentation.positiveAtom line 79

    Source documentation

    The positively oriented, O-based atom. Nonfaces give zero.

    noncomputable def positiveAtom (a b c : d.LiftedEdge) : d.C₂ :=
    …

16. def OAI.Release075.BlockPresentation.orderedEval line 83

    Source documentation

    Exactly one O-corner, with its orientation sign.

    noncomputable def orderedEval (a b c : d.LiftedEdge) : d.C₂ :=
    …

17. def OAI.Release075.BlockPresentation.faceEval line 87

    Source documentation

    Cyclic evaluation of one oriented face.

    noncomputable def faceEval (a b c : d.LiftedEdge) : d.C₂ :=
    …

18. theorem OAI.Release075.BlockPresentation.faceEval_rotate line 90
19. theorem OAI.Release075.BlockPresentation.orderedEval_mirror line 94
20. theorem OAI.Release075.BlockPresentation.faceEval_mirror line 99
21. theorem OAI.Release075.BlockPresentation.positiveAtom_eq_zero line 104
22. theorem OAI.Release075.BlockPresentation.positiveAtom_degenerate line 111
23. theorem OAI.Release075.BlockPresentation.faceEval_degenerate line 118
24. theorem OAI.Release075.BlockPresentation.positiveAtom_zero_first line 130
25. theorem OAI.Release075.BlockPresentation.positiveAtom_zero_second line 137
26. theorem OAI.Release075.BlockPresentation.faceEval_positive line 144
27. theorem OAI.Release075.BlockPresentation.boundary₂_positiveAtom line 160
28. theorem OAI.Release075.BlockPresentation.TriangleFace.positive_orient line 170
29. theorem OAI.Release075.BlockPresentation.boundary₂_faceEval line 189
30. def OAI.Release075.BlockPresentation.wordChain line 224
31. def OAI.Release075.BlockPresentation.diskChain line 226
32. theorem OAI.Release075.BlockPresentation.triple_diskChain line 230
33. theorem OAI.Release075.BlockPresentation.boundary₂_diskChain line 237
34. theorem OAI.Release075.MarkedLineData.diskChain_unique line 260