Conjugate-linear maps

Stream: maths

[Heather Macbeth]

How should conjugate-linear maps be implemented?

• Does it need to be more general than just for $\mathbb{C}$, like maybe some finite extensions of $\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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Adam Topaz]

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

[Heather Macbeth]

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 :)

[Adam Topaz]

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.

[Heather Macbeth]

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

[Frédéric Dupuis]

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

[Heather Macbeth]

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

[Heather Macbeth]

That might be fastest.

[Adam Topaz]

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

[Frédéric Dupuis]

Are complex conjugate vector spaces defined yet?

[Heather Macbeth]

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

[Frédéric Dupuis]

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