OAI/RingTheory/DirectFiniteness/WordReduction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KaplanskyCounterexample.WordReduction.Word line 13
2. inductive OAI.KaplanskyCounterexample.WordReduction.Delete line 15
3. abbrev OAI.KaplanskyCounterexample.WordReduction.Related line 19
4. lemma OAI.KaplanskyCounterexample.WordReduction.rel_trans line 23
5. lemma OAI.KaplanskyCounterexample.WordReduction.rel_symm line 26
6. lemma OAI.KaplanskyCounterexample.WordReduction.Related.append_left line 29
7. lemma OAI.KaplanskyCounterexample.WordReduction.Related.append_right line 40
8. lemma OAI.KaplanskyCounterexample.WordReduction.Related.inv line 51
9. lemma OAI.KaplanskyCounterexample.WordReduction.related_of_red_step line 65
10. lemma OAI.KaplanskyCounterexample.WordReduction.related_of_red line 72
11. lemma OAI.KaplanskyCounterexample.WordReduction.related_of_mk_eq line 79
12. lemma OAI.KaplanskyCounterexample.WordReduction.related_append_null line 85
13. def OAI.KaplanskyCounterexample.WordReduction.nullSubgroup line 90

    Source documentation

    Words reducible to the empty word form a subgroup of the free group.

    def nullSubgroup (Allowed : Word α → Prop)
        (hinv : ∀ w, Allowed w → Allowed (FreeGroup.invRev w)) : Subgroup (FreeGroup α) where
    …

    Mentions: OAI.KaplanskyCounterexample.WordReduction.Word

14. lemma OAI.KaplanskyCounterexample.WordReduction.nullSubgroup_normal line 101
15. theorem OAI.KaplanskyCounterexample.WordReduction.of_presented_eq_one line 121

    Source documentation

    Equality with the identity in the actual presentation gives a finite sequence of contiguous relator insertions/deletions, with no assumed diagrams.

    theorem of_presented_eq_one (rels : Set (FreeGroup α))
        (hinv : ∀ w, Allowed w → Allowed (FreeGroup.invRev w))
        (hcancel : ∀ a b, Allowed [(a, b), (a, !b)])
        (hrels : ∀ g ∈ rels, ∃ w : Word α, FreeGroup.mk w = g ∧ Allowed w)
        (w : Word α) (hw : PresentedGroup.mk rels (FreeGroup.mk w) = 1) :
        Related Allowed w [] := by
    …

    Mentions: OAI.KaplanskyCounterexample.WordReduction.Word, OAI.KaplanskyCounterexample.WordReduction.Related