# Zulip Chat Archive

## Stream: maths

### Topic: Orthogonal/Unitary Group

#### Shing Tak Lam (Jan 11 2021 at 18:05):

I was looking at the undegrad to do list (https://leanprover-community.github.io/undergrad_todo.html), and I saw that Orthogonal and Unitary groups were on there. Initally, I implemented the two separately, on `ℝ`

and `ℂ`

matrices respectively. @Eric Wieser suggested to generalise it to any `star_ring`

, and with the `star_ring`

instance, both could be implemented at once.

@Heather Macbeth also commented on the PR, saying "I would have thought that the right way to define unitary/orthogonal groups is in analysis.normed_space.inner_product, after first defining the adjoint of a continuous linear map. Or at least, we need a plan for the "glue" between that and the matrix perspective."

Therefore, I'm not sure whether we want to have the Orthogonal/Unitary group defined on matrices as in the PR right now, or if it would make sense to define adjoints of continuous linear maps first, and then define the orthogonal/unitary group afterwards.

The PR is #5702, I haven't pushed the changes to using `star_ring`

yet, but the file using `star_ring`

is very similar to the `unitary_group.lean`

file in the PR.

#### Damiano Testa (Jan 11 2021 at 18:19):

As a beginning user of Lean, what I am going to say may be unfeasible. However, it would be nice if the definition of unitary group could also be applied in the case in which the field of coefficients is finite. With some sporadic exceptions, all finite simple groups are either cyclic, alternating or groups of Lie type (e.g. unitary groups). It would be very nice if Lean could at least contain all but finitely many finite simple groups!

#### Frédéric Dupuis (Jan 11 2021 at 18:20):

I'm also very interested in getting unitaries into mathlib, and my thoughts on this are very close to what Heather said. I think the main roadblock right now is the lack of conjugate-linear maps: ideally we would want the adjoint to be a bundled conjugate-linear map, and then start defining unitaries based on this. For the actual definition, I was actually thinking of something a bit more general, namely defining continuous linear maps and equivalences that are also isometries, with notation `E →U[𝕜] F`

and `E ≃U[𝕜] F`

or something like that.

#### Frédéric Dupuis (Jan 11 2021 at 18:24):

Regarding conjugate-linear maps (and semilinear maps more generally), @Yury G. Kudryashov was suggesting redefining `linear_map`

a while back to be something like `linear_map σ M N`

where `σ : R →+* S`

is some ring homomorphism. I played around a bit with this idea and it looks a lot less disruptive than I thought, but I haven't mustered the courage to actually try implementing it myself yet.

#### Heather Macbeth (Jan 11 2021 at 18:27):

Frédéric Dupuis said:

Regarding conjugate-linear maps (and semilinear maps more generally), Yury G. Kudryashov was suggesting redefining

`linear_map`

a while back to be something like`linear_map σ M N`

where`σ : R →+* S`

is some ring homomorphism. I played around a bit with this idea and it looks a lot less disruptive than I thought, but I haven't mustered the courage to actually try implementing it myself yet.

Yury has thought about this much more than I have, and I know he had thought of some potential roadblocks which I have forgotten. One point: one wants `linear_map`

to be useable in the current form without having to specify `σ`

, so maybe there's something like `to_additive`

that can be written, to allow all theorems to be written for `generalized_linear_map σ M N`

and automatically have a special case produced for `linear_map R M N`

, with `σ : R →+* R`

the identity.

#### Johan Commelin (Jan 11 2021 at 18:27):

I have no idea whether we can find a framework that treats unitary groups over arbitrary fields (e.g. finite fields) coming from hermitian forms, and also treat continuous linear maps, and matrices, all in the same framework.

#### Johan Commelin (Jan 11 2021 at 18:27):

If we can, that would be great! It's probably worth thinking about a bit.

#### Heather Macbeth (Jan 11 2021 at 18:29):

Frédéric Dupuis said:

For the actual definition, I was actually thinking of something a bit more general, namely defining continuous linear maps and equivalences that are also isometries, with notation

`E →U[𝕜] F`

and`E ≃U[𝕜] F`

or something like that.

It'd be nice also to have a constructor for elements of the unitary group, given a map satisfying just the condition that it fixes 0 and is an isometry. This should come from docs#isometric.to_affine_equiv (also written by Yury).

#### Frédéric Dupuis (Jan 11 2021 at 18:31):

Heather Macbeth said:

Yury has thought about this much more than I have, and I know he had thought of some potential roadblocks which I have forgotten. One point: one wants

`linear_map`

to be useable in the current form without having to specify`σ`

, so maybe there's something like`to_additive`

that can be written, to allow all theorems to be written for`generalized_linear_map σ M N`

and automatically have a special case produced for`linear_map R M N`

, with`σ : R \to R`

the identity.

For making `linear_map`

usable without specifying `σ`

, it seems to be enough to just keep the current notation `E →ₗ[R] F`

to mean `linear_map (ring_hom.id R) E F`

. There are very few instances in mathlib where `linear_map`

is used directly without notation.

#### Heather Macbeth (Jan 11 2021 at 18:32):

But I think there are a lot of linear-algebra lemmas where one currently has to provide the scalar field as an explicit argument; won't the usage pattern have to change so that one provides `(id : R →+* R)`

as that explicit argument instead? (which would get tedious)

#### Frédéric Dupuis (Jan 11 2021 at 18:34):

Yeah, we would probably want two versions of those lemmas, one for the current version of `linear_map`

and one that works for any `σ`

.

#### Heather Macbeth (Jan 11 2021 at 18:34):

And it would be great if the special-case version could be automatically generated from the general version, like in `to_additive`

; don't know if that's possible.

#### Frédéric Dupuis (Jan 11 2021 at 18:36):

Yes, Yury mentioned this last time. I have no idea how to do this, and I'm not sure if it's really worth it. At the very least we would have to come up with a very consistent naming scheme for this to have any hope of success.

#### Frédéric Dupuis (Jan 11 2021 at 18:38):

Of course the other option is to just define `semilinear_map`

in parallel to what we currently have, but this will be much less pleasant when (for example), we have a conjugate-linear map over an `is_R_or_C`

field and want to use the fact that it's linear in the real case.

#### Eric Wieser (Jan 11 2021 at 18:43):

How would this `σ`

transfer to `multilinear_map`

?

#### Heather Macbeth (Jan 11 2021 at 18:44):

@Yury G. Kudryashov was concerned about another issue, which I hope he will come and summarize because my description is going to get it wrong. But it was about issues that come when you compose maps.

The idea, I think: what if you have `conj : ℂ →+ ℂ`

, and linear maps `linear_map conj E F`

and `linear_map conj F G`

; you compose them and get a linear map `linear_map (conj ∘ conj) E G`

, but it's not automatic to identify this type with `linear_map id E G`

.

#### Frédéric Dupuis (Jan 11 2021 at 18:45):

We could have a composition lemma that is specialized for this case, no?

#### Heather Macbeth (Jan 11 2021 at 18:46):

Well, the problems multiply when you start to talk about these Frobenius-linear maps that Johan and Kevin talk about, with a bigger automorphism group of R.

#### Eric Wieser (Jan 11 2021 at 18:46):

Above we said `σ : R →+* S`

, but for the conj case you say you want the weaker `R →+ S`

. Was one a typo?

#### Frédéric Dupuis (Jan 11 2021 at 18:48):

Heather Macbeth said:

Well, the problems multiply when you start to talk about these Frobenius-linear maps that Johan and Kevin talk about, with a bigger automorphism group of R.

Right, but it seems unavoidable, these maps really do have different composition properties.

#### Kevin Buzzard (Jan 11 2021 at 18:48):

If $L/K$ is finite Galois of degree 2 then number theorists talk about unitary groups in this setting too.

#### Frédéric Dupuis (Jan 11 2021 at 18:49):

Eric Wieser said:

How would this

`σ`

transfer to`multilinear_map`

?

Good question! I haven't given this much thought to be honest. Would it really be worth having some sort of multilinear map with a different `σ`

for each of the spaces?

#### Frédéric Dupuis (Jan 11 2021 at 18:51):

Eric Wieser said:

Above we said

`σ : R →+* S`

, but for the conj case you say you want the weaker`R →+ S`

. Was one a typo?

I guess I was thinking of the commutative case.

#### Heather Macbeth (Jan 11 2021 at 22:20):

Frédéric Dupuis said:

Eric Wieser said:

How would this

`σ`

transfer to`multilinear_map`

?Good question! I haven't given this much thought to be honest. Would it really be worth having some sort of multilinear map with a different

`σ`

for each of the spaces?

This is certainly necessary, and this linear algebra is well-developed. See, as a starting point, https://en.wikipedia.org/wiki/Linear_complex_structure#Extension_to_related_vector_spaces

or section 1.2 of https://www.springer.com/gp/book/9783540212904

#### Frédéric Dupuis (Jan 11 2021 at 22:36):

Looks like we have our work cut out for us then!

Last updated: May 12 2021 at 07:17 UTC