gersten_presentation.jl

using Groups
using KnuthBendix

import Groups: ϱ, λ

KnuthBendix.Word(A::Alphabet{T}, v::AbstractVector{T}) where {T} = Word([A[s] for s in v])
invof(A::Alphabet{T}, a::T) where {T} = A[-A[a]]
comm(A::Alphabet, x::S, y::S) where {S<:Groups.GSymbol} =
    Word([A[x], A[y], A[invof(A, x)], A[invof(A, y)]])

_indexing(n) = [(i, j) for i = 1:n for j in 1:n if i ≠ j]

function gersten_alphabet(n; commutative::Bool = true)

    G = SAut(FreeGroup(n))
    S = first.(gens(G))
    if commutative
        S = S[1:length(S)÷2]
    end

    S = [S; Groups.change_pow.(S, -1)]

    A = Alphabet(S)
    for a in A.alphabet
        KnuthBendix.set_inversion!(A, a, inv(a))
    end
    return A
end

function gersten_relations(n::Integer, commutative::Val{true})
    A = gersten_alphabet(n, commutative = true)
    rels = [Word(A, [l, invof(A, l)]) => Word() for l in A.alphabet]

    for (i, j, k, l) in Iterators.product(1:n, 1:n, 1:n, 1:n)
        if (i ≠ j && k ≠ l && k ≠ i && k ≠ j && l ≠ i)
            push!(rels, comm(A, ϱ(i, j), ϱ(k, l)) => Word())
        end
    end

    for (i, j, k) in Iterators.product(1:n, 1:n, 1:n)
        if (i ≠ j && k ≠ i && k ≠ j)
            push!(rels, comm(A, ϱ(i, j, -1), ϱ(j, k, -1)) => Word(A, [ϱ(i, k, -1)]))
            push!(rels, inv(A, comm(A, ϱ(i, j, -1), ϱ(j, k))) => Word(A, [ϱ(i, k, -1)]))
        end
    end

    return rels, A
end

function gersten_relations(n::Integer, commutative::Val{false})

    A::Alphabet = gersten_alphabet(n, commutative = false)
    rels = [Word(A, [l, invof(A, l)]) => Word() for l in A.alphabet]

    for (i, j, k, l) in Iterators.product(1:n, 1:n, 1:n, 1:n)
        if (i ≠ j && k ≠ l && k ≠ i && k ≠ j && l ≠ i)
            push!(rels, comm(A, ϱ(i, j), ϱ(k, l)) => Word())
            push!(rels, comm(A, λ(i, j), λ(k, l)) => Word())
        end
    end

    for (i, j, k, l) in Iterators.product(1:n, 1:n, 1:n, 1:n)
        if (i ≠ j && k ≠ l && k ≠ j && l ≠ i)
            push!(rels, comm(A, ϱ(i, j), λ(k, l)) => Word())
            push!(rels, comm(A, λ(i, j), ϱ(k, l)) => Word())
        end
    end

    for (i, j, k) in Iterators.product(1:n, 1:n, 1:n)
        if (i ≠ j && k ≠ i && k ≠ j)
            push!(rels, comm(A, ϱ(i, j, -1), ϱ(j, k, -1)) => Word(A, [ϱ(i, k, -1)]))
            push!(rels, comm(A, ϱ(i, j), λ(j, k)) => Word(A, [ϱ(i, k, -1)]))
            push!(rels, inv(A, comm(A, ϱ(i, j, -1), ϱ(j, k))) => Word(A, [ϱ(i, k, -1)]))
            push!(rels, inv(A, comm(A, ϱ(i, j), λ(j, k, -1))) => Word(A, [ϱ(i, k, -1)]))

            push!(rels, comm(A, λ(i, j, -1), λ(j, k, -1)) => Word(A, [λ(i, k, -1)]))
            push!(rels, comm(A, λ(i, j), ϱ(j, k)) => Word(A, [λ(i, k, -1)]))
            push!(rels, inv(A, comm(A, λ(i, j, -1), λ(j, k))) => Word(A, [λ(i, k, -1)]))
            push!(rels, inv(A, comm(A, λ(i, j), ϱ(j, k, -1))) => Word(A, [λ(i, k, -1)]))
        end
    end

    for (i, j) in Iterators.product(1:n, 1:n)
        if i ≠ j
            push!(
                rels,
                Word(A, [ϱ(i, j), ϱ(j, i, -1), λ(i, j)]) =>
                    Word(A, [λ(i, j), λ(j, i, -1), ϱ(i, j)]),
            )
            push!(rels, Word(A, [ϱ(i, j), ϱ(j, i, -1), λ(i, j)])^4 => Word())
        end
    end

    for j = 1:n
        push!(rels, prod(Word(A, [ϱ(i, j), λ(i, j, -1)]) for i in 1:n if i ≠ j) => Word())
    end

    return rels, A
end

gersten_relations(n::Integer; commutative::Bool) = gersten_relations(n, Val(commutative))