SimpleLetterPresentation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.HyperbolicObstruction.LetterPresentation.SimpleWordRelator line 16

Source documentation

Exactly the source03 finite presentation: all simple cycles of each included fan and compatible included top graph, plus the two decorations. The underlying template graph is not quotiented by its random labels.

inductive SimpleWordRelator : List (Alphabet n) → Prop
  | fan (l : Field → Alphabet n) (i : Fin 7)
      (present : w (TableModel.row rowSupport l (.inl i)) = true)
      (v : CoreGeometry.Vertex) (p : (CoreWordGraph.graph (fan i)).Walk v v)
      (simple : p.IsCycle) :
      SimpleWordRelator (GraphWordFilling.word (CoreWordGraph.label (fan i) n l) p)
  | top (l : Field → Alphabet n)
      (present : w (TableModel.row rowSupport l (.inr (.inl ()))) = true)
      (fans : ∀ i : Fin 7, w (TableModel.row rowSupport l (.inl i)) = true)
      (v : CoreGeometry.Vertex) (p : (CoreWordGraph.graph Finset.univ).Walk v v)
      (simple : p.IsCycle) :
      SimpleWordRelator (GraphWordFilling.word (CoreWordGraph.label Finset.univ n l) p)
…

Mentions: OAI.HyperbolicObstruction.LetterPresentation.Alphabet, OAI.HyperbolicObstruction.TableModel.row, OAI.HyperbolicObstruction.CoreGeometry.Vertex, OAI.HyperbolicObstruction.CoreWordGraph.graph, OAI.HyperbolicObstruction.GraphWordFilling.word, OAI.HyperbolicObstruction.CoreWordGraph.label

lemma OAI.HyperbolicObstruction.LetterPresentation.simpleWordRelator_length line 33
theorem OAI.HyperbolicObstruction.LetterPresentation.simpleWordRelator_finite line 45
Source documentation
Finiteness is proved from literal words, including coinciding labels and repeated rows, not asserted as an extra presentation hypothesis.
```
theorem simpleWordRelator_finite : Set.Finite {z | SimpleWordRelator n w d z} := by
…
```
Mentions: OAI.HyperbolicObstruction.LetterPresentation.SimpleWordRelator
lemma OAI.HyperbolicObstruction.LetterPresentation.simpleWordRelator_original line 53
lemma OAI.HyperbolicObstruction.LetterPresentation.fan_fields line 72
lemma OAI.HyperbolicObstruction.LetterPresentation.top_fields line 81
theorem OAI.HyperbolicObstruction.LetterPresentation.relator_simple_filling line 89
Source documentation
Every ORIGINAL relator has a quantitative derivation in the finite simple-cycle presentation. The bound is its literal length (zero included).
```
theorem relator_simple_filling {z : List (Alphabet n)} (hz : WordRelator n w d z) :
    ∃ a ≤ z.length, WordPictures.Homotopy (SimpleWordRelator n w d) z [] a := by
…
```
Mentions: OAI.HyperbolicObstruction.LetterPresentation.Alphabet, OAI.HyperbolicObstruction.LetterPresentation.WordRelator, OAI.HyperbolicObstruction.WordPictures.Homotopy, OAI.HyperbolicObstruction.LetterPresentation.SimpleWordRelator
theorem OAI.HyperbolicObstruction.LetterPresentation.simple_presentation_normalClosure line 121
Source documentation
Exact normal-closure equality, giving the same original marked group, not merely a surjection from a conveniently chosen finite presentation.
```
theorem simple_presentation_normalClosure :
    Subgroup.normalClosure (FreeGroup.mk '' SimpleWordRelator n w d) =
    Subgroup.normalClosure (Relator n w d) := by
…
```
Mentions: OAI.HyperbolicObstruction.LetterPresentation.SimpleWordRelator, OAI.HyperbolicObstruction.LetterPresentation.Relator