Simplifying Iwasawa decomposition with Symbolics.jl

Specific Domains Optimization (Mathematical)
, , ,
1

I’m trying to verify the following matrix identity using Symbolics.jl:

image
image778×338 16 KB

Here’s my attempt:

using Symbolics
function SL2CIwasawaDecomp(X)
    # given matrix X in SL2C, return tuple (z, r, α, β) such that
    # X = n(z) a(r) k(α, β).
    a,b,c,d = transpose(X);    # julia destructures by columns for some reason
    r = 1/(abs(c)^2 + abs(d)^2)
    z = r*(a*conj(c) + b*conj(d))
    α = conj(d) * sqrt(r)
    β = - conj(c) * sqrt(r)
    return r,z,α,β
end

k_mat(α,β) = [α β; -conj(β) conj(α)]
a_mat(r) = [sqrt(r) 0; 0 1/sqrt(r)]
n_mat(z) = [1 z; 0 1]

@variables a::Complex b::Complex c::Complex d::Complex
g = [a b; c d];
r,z,α,β = SL2CIwasawaDecomp(g);
h = n_mat(z)*a_mat(r)*k_mat(α,β);
# should have h == g!
simplify(h) # <- the top row of this is messy!

The problem is that the identity requires the condition a d - b c = 1. If you do it by hand, then you can factor the top two entries in the matrix h in such a way that everything collapses, and you end up with just a and b. In Julia, I tried things like
substitute(h, Dict([d => (1 + b*c)/a]))
and
simplify(h, Rewriters.Prewalk(Rewriters.PassThrough(@rule d => (1+b*c)/a)))
but I haven’t been able to get anything working. Any ideas?

1 Like