Zulip Chat Archive

Stream: maths

Topic: Conjugate-linear maps


view this post on Zulip Heather Macbeth (Oct 05 2020 at 15:17):

How should conjugate-linear maps be implemented?

  • Does it need to be more general than just for C\mathbb{C}, like maybe some finite extensions of Q\mathbb{Q}? At the moment in the related docs#sesq_form, there is a one-off definition using a ring isomorphism I : R ≃+* Rᵒᵖ. Is this the right setting in general? @Johan Commelin @Kevin Buzzard
  • Does the entire API of linear maps need to be duplicated? Or is there a trick to borrow the lemmas without re-proving them?

Question motivated by @Frédéric Dupuis 's new PR #4379, although the PR shouldn't be delayed for this.

view this post on Zulip Johan Commelin (Oct 05 2020 at 15:52):

In number theory we encounter Frobenius linear maps... but Frobenius rarely has order two.

view this post on Zulip Johan Commelin (Oct 05 2020 at 15:52):

I don't think you should wait with this definition till we have a complete semi-linear algebra library.

view this post on Zulip Johan Commelin (Oct 05 2020 at 15:53):

We also work a lot with CM fields, which behave very similar to the pair (real, complex), but I wouldn't wait for those either.

view this post on Zulip Adam Topaz (Oct 05 2020 at 15:58):

You can certainly define maps which are semilinear with respect to any morphism of (semi)rings. I think this covers all cases, right?

view this post on Zulip Heather Macbeth (Oct 05 2020 at 16:01):

Adam Topaz said:

You can certainly define maps which are semilinear with respect to any morphism of (semi)rings. I think this covers all cases, right?

Would this be the first definition, and then the existing linear algebra library be derived from it as a special case? I will not sign up to do that refactor myself :)

view this post on Zulip Adam Topaz (Oct 05 2020 at 16:01):

There's also a trick that's fairly common in number theory where you consider a semilinear map as a linear map using the base-change.

view this post on Zulip Heather Macbeth (Oct 05 2020 at 16:01):

But would be happy enough for someone else to do it.

view this post on Zulip Frédéric Dupuis (Oct 05 2020 at 16:01):

I think it might make sense to have a general version and a continuous version, mirroring linear_map and continuous_linear_map.

view this post on Zulip Heather Macbeth (Oct 05 2020 at 16:01):

Another trick: conjugate-linear is linear to the
https://en.wikipedia.org/wiki/Complex_conjugate_vector_space

view this post on Zulip Heather Macbeth (Oct 05 2020 at 16:02):

That might be fastest.

view this post on Zulip Adam Topaz (Oct 05 2020 at 16:02):

Yeah, that's exactly the base-change trick :)

view this post on Zulip Frédéric Dupuis (Oct 05 2020 at 16:02):

Are complex conjugate vector spaces defined yet?

view this post on Zulip Heather Macbeth (Oct 05 2020 at 16:03):

I don't think so. But probably not too hard?

view this post on Zulip Frédéric Dupuis (Oct 05 2020 at 16:03):

Right. Yeah that's probably the best way to do it.


Last updated: May 06 2021 at 18:20 UTC