ShortRelators.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KaplanskyCounterexample.ShortPresentation.representative line 14
lemma OAI.KaplanskyCounterexample.ShortPresentation.representative_one line 16
lemma OAI.KaplanskyCounterexample.ShortPresentation.representative_length line 17
lemma OAI.KaplanskyCounterexample.ShortPresentation.representative_eval line 20
lemma OAI.KaplanskyCounterexample.ShortPresentation.kernel_le_of_short line 30
Source documentation
The complete multiplication table needs only words of length at most three. Every zero-sum word follows from these short relations.
```
lemma kernel_le_of_short (g : FreeGroup γ →* B)
    (hshort : ∀ w : List (γ × Bool), w.length ≤ 3 → f (FreeGroup.mk w)=1 →
      g (FreeGroup.mk w)=1) : f.ker ≤ g.ker := by
…
```
def OAI.KaplanskyCounterexample.GluedGroup.shortRelators line 72
lemma OAI.KaplanskyCounterexample.GluedGroup.shortRelators_subset line 77
lemma OAI.KaplanskyCounterexample.GluedGroup.local_generators_cover line 81
lemma OAI.KaplanskyCounterexample.GluedGroup.short_normalClosure line 94
Source documentation
Changing from all local relators to the prescribed finite sublist leaves exactly the same normal subgroup, not just a group with similar properties.
```
lemma short_normalClosure (hc : CoversPoints Inc ℓ incMap) :
    Subgroup.normalClosure (shortRelators Inc ℓ incMap)=
      Subgroup.normalClosure (relators Inc ℓ incMap) := by
…
```
Mentions: OAI.KaplanskyCounterexample.GluedGroup.CoversPoints, OAI.KaplanskyCounterexample.GluedGroup.shortRelators, OAI.KaplanskyCounterexample.GluedGroup.relators
lemma OAI.KaplanskyCounterexample.GluedGroup.shortRelators_finite line 109
Source documentation
Only finitely many of the length-at-most-three relations occur.
```
lemma shortRelators_finite [Finite V] [Finite F] [NeZero ℓ] :
    (shortRelators Inc ℓ incMap).Finite := by
…
```
Mentions: OAI.KaplanskyCounterexample.GluedGroup.shortRelators
def OAI.KaplanskyCounterexample.GluedGroup.shortEquiv line 120
Source documentation
The canonical presentation isomorphism fixes every named generator.
```
def shortEquiv (hc : CoversPoints Inc ℓ incMap) :
    PresentedGroup (shortRelators Inc ℓ incMap) ≃* N Inc ℓ incMap :=
…
```
Mentions: OAI.KaplanskyCounterexample.GluedGroup.CoversPoints, OAI.KaplanskyCounterexample.GluedGroup.shortRelators, OAI.KaplanskyCounterexample.GluedGroup.N
lemma OAI.KaplanskyCounterexample.GluedGroup.shortEquiv_generator line 124