# Zulip Chat Archive

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

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