Orthogonal/Unitary Group

Stream: maths

[Shing Tak Lam]

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]

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]

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]

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]

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]

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]

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

[Heather Macbeth]

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]

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]

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]

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]

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]

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]

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]

How would this σ transfer to multilinear_map?

[Heather Macbeth]

@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]

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

[Heather Macbeth]

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]

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]

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]

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

[Frédéric Dupuis]

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]

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]

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]

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