## Stream: maths

### Topic: Conjugate-linear maps

#### 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 $\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 (Oct 05 2020 at 15:52):

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

#### 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.

#### 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.

#### 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?

#### Heather Macbeth (Oct 05 2020 at 16:01):

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 (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.

#### Heather Macbeth (Oct 05 2020 at 16:01):

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

#### 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.

#### 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

#### Heather Macbeth (Oct 05 2020 at 16:02):

That might be fastest.

#### Adam Topaz (Oct 05 2020 at 16:02):

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

#### Frédéric Dupuis (Oct 05 2020 at 16:02):

Are complex conjugate vector spaces defined yet?

#### Heather Macbeth (Oct 05 2020 at 16:03):

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

#### 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