Zulip Chat Archive

Stream: maths

Topic: Conjugacy Classes


view this post on Zulip Aaron Anderson (Mar 26 2021 at 03:48):

For multiple purposes in representation theory, I find myself wanting to work with is_conj.

view this post on Zulip Aaron Anderson (Mar 26 2021 at 03:49):

Currently, is_conj is only defined on groups, but I'd like to be able to talk about, say, two matrices being conjugate. Does anyone see any problems with refactoring the definition of is_conj as I've done at branch#monoid_conj to involve units?

view this post on Zulip Aaron Anderson (Mar 26 2021 at 03:51):

Secondly, I'd really like to use the quotient type of conjugacy classes. Does is_conj exist anywhere as a setoid that I've just missed? If not, should I add it right at algebra.group.conj?

view this post on Zulip Johan Commelin (Mar 26 2021 at 05:17):

@Christopher Hughes I think you've worked most with is_conj.

view this post on Zulip Aaron Anderson (Mar 26 2021 at 17:21):

#6896


Last updated: May 09 2021 at 10:11 UTC