Conjugate-linear

Stream: maths

[Heather Macbeth]

The problem of conjugate-linear maps has reared its head again: for prior (inconclusive) discussion see
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Orthogonal.2FUnitary.20Group
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/4770.20smul_comm_class
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Conjugate-linear.20maps

This time the problem is that we have two open PRs constructing orthogonal bases:

• one (#5734) for docs#inner_product_space, Euclidean inner products over ℝ and Hermitian inner products over ℂ
• one (#5814) for docs#bilin_form, symmetric nondegenerate bilinear forms over an arbitrary domain

If these both go through, there's going to be a lot of duplicated theory: the definition and properties of the orthogonal complement, the induced bilinear form on a submodule, as well as the existence of the orthogonal basis.

It would be really nice to find a flexible joint generalization, if that's possible. If not, can we try to make the development (and naming conventions) of the theories as parallel as possible, and build glue between them?

[Johan Commelin]

I think we should try our best to go for the generalization. But I haven't had time to play with this :expressionless:

[Frédéric Dupuis]

I haven't given this much thought, but the tricky part with the joint generalization is that inner_product_space is a typeclass (and should remain one in my opinion) whereas a bilinear form as currently defined is just a regular structure.

[Frédéric Dupuis]

Also, note that we also have sesquilinear products as a third incarnation of this sort of structure.

[Frédéric Dupuis]

It might be tempting to have some sort of proto-inner product typeclass to replace bilinear forms and sesquilinear forms and then build the inner product space typeclass on top of that, but I'm not sure that would play well with the fact that inner product spaces are built on top of normed spaces.

[Frédéric Dupuis]

Maybe having the bilinear/sesquilinear typeclass as a mixin would work.

[Heather Macbeth]

Frédéric Dupuis said:

I'm not sure that would play well with the fact that inner product spaces are built on top of normed spaces.

Right, there is the further distinction between linear maps and continuous linear maps. This latter distinction means, eg, that there need to be two separate constructions of a "dual", one for linear maps and one for continuous linear maps.

[Frédéric Dupuis]

Maybe make the dual a typeclass also?

[Heather Macbeth]

I don't quite follow ... I am not proposing any particular change here, just noting that there is an existing, large-scale parallel development of linear maps and continuous linear maps, culminating in docs#module.dual and docs#normed_space.dual.

Or are you proposing a change? :)

[Johan Commelin]

I agree that the dichotomy between structures and classes puts some restrictions. But I would imagine developing the theory for the generic structure first, and then have 1-liner specializations (maybe automated??) for type classes like inner_product_space.

[Heather Macbeth]

That would be nice!

[Frédéric Dupuis]

Yeah maybe that's the simplest thing to do. Which brings us back to conjugate-linear maps, because we would want to do this for a joint bilinear/sesquilinear form.

[Frédéric Dupuis]

Heather Macbeth said:

I don't quite follow ... I am not proposing any particular change here, just noting that there is an existing, large-scale parallel development of linear maps and continuous linear maps, culminating in docs#module.dual and docs#normed_space.dual.

Or are you proposing a change? :)

I was thinking of defining a typeclass dual 𝕜 E with whatever axioms we would want a reasonable dual to have, with E →L[𝕜] 𝕜 being an instance for normed_space 𝕜 E, and this would allow us to generalize the concept. But it does open a whole can of worms regarding the uniqueness of duals, and on second thought it's probably a bad idea.

[Eric Wieser]

Can we associate a bilinear form with the typeclass, and move as many proofs as possible over to bilinear_form? So add a inner_product_space.bilinear member computed from the existing fields.

[Heather Macbeth]

@Eric Wieser The problem is that the inner product is not necessarily bilinear. In the complex case it's sesquilinear. This is why the lack of conjugate-linear maps is the real issue here.

[Sebastien Gouezel]

I don't think we should go in the direction of generalizing linear maps to "linear maps with an automorphism in the target" everywhere in mathlib: the real concept is that of a linear map, and the issue is that we don't want to rely on the usual vector space structure in the target, but on a twisted one. It would seem more natural to me to introduce a type synonym for the target, in which the vector space structure should be changed. Something like restrict_scalars -- in fact, restrict_scalars is a particular case of this situation: suppose that you have a field morphism u : R -> C, and a C vector space E. Then you can define an R-vector space structure on E, by setting r • x := u(r) • x. When R is the reals and C is the complexes and u is the inclusion, this is the usual scalar restriction. When both are the complexes and u is complex conjugation, this twists the complex structure. So a "conjugate-linear map" on E is just a linear map in the usual sense from E to twist_structure u E.

[Johan Commelin]

But we try to avoid restrict_scalars in favour of scalar_tower, because type synonyms have their own disadvantages...

[Johan Commelin]

For example, you can't compose a conjugate-linear endomorphism with itself, because the domain is no longer the same as the target.

[Sebastien Gouezel]

You can compose them as maps, but not as linear maps, which is good because for general field automorphisms the composition is not a linear map.

[Sebastien Gouezel]

Sorry, there is something that always works here: a linear map from E to twisted u E gives also a linear map from twisted v E to twisted (u o v) E, or something like that.

[Johan Commelin]

Right, but those target types quickly become quite messy. That second map is not defeq to a map from E' to twisted _ E', so you would have to rewrite the target to twisted v (twisted u E) which doesn't look nice.

[Johan Commelin]

I don't mean to say this is not the way to go. I don't have a better idea. It's just that... you know, I wish life would be easier :wink:

[Sebastien Gouezel]

It's definitely defeq to a map from E to E, as twisted u E is defeq to E. As linear maps, I agree they are not defeq, but it's normal since it's a theorem, in a sense.

[Heather Macbeth]

@Sebastien Gouezel This approach with a type synonym sounds similar to @Frédéric Dupuis' experiment a while ago, in one version of #4379, to write down the "complex conjugate vector space" structure (see discussion) and express conjugate-linear maps as linear maps to it. Here's about the right range of commits:
https://github.com/leanprover-community/mathlib/pull/4379/files/46f75e1e2e460e9be46e699067656f641d790f80?file-filters%5B%5D=.lean

Is this more or less the method you're suggesting, or are there things you would change?

One point is that he worked with a map I : R ≃+* Rᵒᵖ, and it sounds like you're suggesting a map I : R ≃+* R.

[Sebastien Gouezel]

Yes, it is essentially this idea (thanks for the pointer!) except that in fact I am suggesting a map I : R ->+* C to be able to cover both scalar restriction and structure twisting with a single construction.

[Heather Macbeth]

Can you explain how the Hermitian inner product would look under this construction? Is it something like, a map from E × E to ℂ ⊗ (twisted ℂ)?

[Sebastien Gouezel]

A bilinear map is in general a linear map on E ⊗ E. A map which is linear in the first variable and antilinear in the second variable is therefore a linear map on E ⊗ (twisted E). But I don't know if it is worth taking a tensor product viewpoint like that, or saying that it is a map of two variables on E x E which, when you fix a second variable, is a linear map, and when you fix a first variable is linear from E to twisted ℂ or, equivalently, is linear from twisted E to ℂ.

[Heather Macbeth]

Currently docs#bilin_form (which is what's used in #5814) is a map from M x M to R, that is linear in both arguments.

You propose that this would be generalized to an object which takes as a parameter a map I : R ≃+* R, and is a map from M x M to R, that is linear in the first argument and I-twisted linear in the second argument?

And then inner_product_space gets redefined to be a tuple of normed_space, plus such a twisted form (with I = is_R_or_C.conj), plus a compatibility condition? And then there's a refactor to move much of the material in inner_product_space to bilin_form?

[Eric Wieser]

I don't really have the background, but should it be I : R ≃+* Rᵒᵖ to allow for conjugate-linearity in non-commutative rings? Or can we not build bilinear maps of those anyway?

[Heather Macbeth]

I believe this caused Frédéric some headaches (see the code I linked above), but I don't remember exactly, maybe he will comment.

[Eric Wieser]

Heather Macbeth said:

You propose that this would be generalized to an object which takes as a parameter a map I : R ≃+* R, and is a map from M x M to R, that is linear in the first argument and I-twisted linear in the second argument?

This object is precisely docs#sesq_form, isn't it?

[Heather Macbeth]

Well, that's for Rᵒᵖ.

[Eric Wieser]

Do we have somewhere that id is a R ≃+* Rᵒᵖ for commutative rings? Maybe that would glue over the awkwardness for $\mathbb{R}$ and $\mathbb{C}$ (edit: docs#ring_invo.id)

[Sebastien Gouezel]

I don't have an opinion for R or Rᵒᵖ. I have no meaningful application of sesquilinear forms taking values in a non-commutative ring in mind, but of course it doesn't mean such applications don't exist.

[Heather Macbeth]

Heather Macbeth said:

And then inner_product_space gets redefined to be a tuple of normed_space, plus such a twisted form (with I = is_R_or_C.conj), plus a compatibility condition? And then there's a refactor to move much of the material in inner_product_space to bilin_form?

Are you in favour of having this big refactor of inner_product_space? ... in which case we need to find someone to do it ;)

[Eric Wieser]

Heather Macbeth said:

see the code I linked above

I've merged this with master and pushed it to branch#conjugate-module, to encourage it not to get completely lost.

[Frédéric Dupuis]

I would argue against the type synonym approach, after having experimented a bit with it. It's very unpleasant to work with, since you almost never actually want to work in the the "twisted" space, so you have to dance around to get back to space you actually want. Just to give an example: suppose I want to define the adjoint of a map E →ₗ[ℂ] F where E and F are complex vector spaces. The natural thing to do would be to define adj as a bundled conjugate-linear map from E →ₗ[ℂ] F to F →ₗ[ℂ] E. With the type synonyms, this just becomes a nightmare. I think generalizing linear maps would work a lot better in practice. If calling it a "linear map" is a sacrilege, we can always rename it to semilinear_map :-)

[Sebastien Gouezel]

Since you have experimented with this, I'll trust your word on it! My concern is that, if one starts to define linear maps for twisted structures, one will also want to define modules for twisted structures, matrices for twisted structures, and in the end redo all the linear algebra library by adding everywhere a twisting factor (and for linear maps one should maybe even have the possibility to add one twisting factor in the source and one in the target) -- otherwise, twisted linear maps will just be gadget that doesn't play well with the rest of the library. And that doesn't seem reasonable.

[Heather Macbeth]

I have been thinking lately about the "composition problem" if we go the route of generalizing linear maps to semilinear. I have an idea and would be interested on comments about whether it's workable.

[Heather Macbeth]

Let me first outline the "naive method", @Frédéric Dupuis this is what we both have in mind, right? One has modules M over R, M₂ over S, and a homomorphism σ : R →+* S; then composition of two such semilinear maps associated to homomorphisms σ : R →+* S and τ : S →+* T gives a semilinear map for the homomorphism τ.comp σ : R →+* T.

variables {R : Type*} {S : Type*} [semiring R] [semiring S] (σ : R →+* S)
variables (M : Type*) [add_comm_monoid M] [semimodule R M]
variables (M₂ : Type*) [add_comm_monoid M₂] [semimodule S M₂]

structure semilinear_map  :=
(to_fun : M → M₂)
(map_add' : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y)
(map_smul' : ∀ (m : R) (x : M), to_fun (m • x) = (σ m) • to_fun x)

instance : has_coe_to_fun (semilinear_map σ M M₂) := ⟨_, semilinear_map.to_fun⟩

variables {T : Type*} [semiring T] (τ : S →+* T)
variables (M₃ : Type*) [add_comm_monoid M₃] [semimodule T M₃]

def comp (f : semilinear_map σ M M₂) (g : semilinear_map τ M₂ M₃) :
  semilinear_map (τ.comp σ) M M₃ :=
⟨g ∘ f, sorry, sorry⟩

[Heather Macbeth]

The variation I had in mind was to instead make composition take as extra parameters a third homomorphism(η : R →+* T), together with [fact (τ.comp σ = η)].

[Heather Macbeth]

Then composition gives you a semilinear_map η M M₃.

[Heather Macbeth]

And we could provide instances for the facts we expect to use regularly, such as [fact (id.comp id = id)], which means that the composition of standard-linear maps is just a standard-linear map, rather than an id.comp id-linear map.

[Heather Macbeth]

Likewise, instances for [fact (conj.comp id = conj)] and [fact (id.comp conj = conj)].

[Eric Wieser]

Does that help though? semilinear_map (conj.comp conj) M M₃ is still a different type to semilinear_map id M M₃ ah, that's η

[Heather Macbeth]

What do you mean? The idea is that one would never have to use semilinear_map (conj.comp conj) M M₃.

[Heather Macbeth]

(another instance one would provide is [fact (conj.comp conj = id)])

[Eric Wieser]

To be explicit, you're proposing

def comp' (f : semilinear_map σ M M₂) (g : semilinear_map τ M₂ M₃) (η : R →+* T) [fact (τ.comp σ = η)] :
  semilinear_map η M M₃ :=
⟨g ∘ f, sorry, sorry⟩

My comment above was me failing to match your code to your prose, and should be ignored

[Heather Macbeth]

Yup.

[Eric Wieser]

Instead of an argument to comp, there could just be a version of docs#linear_map.restrict_scalars to rewrite the value of the →+* instead of the base ring, making it (f.comp g).restrict_σ η or similar

[Heather Macbeth]

The thing is, I think we often want that this kind of rewriting occur by default, eg, we want the default composition of two id-linear maps to be an id-linear map.

[Eric Wieser]

That's fair - but I think we'd also want a not-by-default version for when the proof needed is too involved to belong in a fact, from which the default could be implemented.

[Heather Macbeth]

For that I was hoping one could use [fact (τ.comp σ = τ.comp σ)] :)

[Frédéric Dupuis]

Heather Macbeth said:

Let me first outline the "naive method", Frédéric Dupuis this is what we both have in mind, right? One has modules M over R, M₂ over S, and a homomorphism σ : R →+* S; then composition of two such semilinear maps associated to homomorphisms σ : R →+* S and τ : S →+* T gives a semilinear map for the homomorphism τ.comp σ : R →+* T.

Yes, that's what I was thinking of, and I like your proposal for composition, it seems like it should work.

[Heather Macbeth]

Another idea -- perhaps one could implement linear maps just as a notational overlay on semilinear maps, i.e. M →ₗ[R] M₂ means semilinear_map (ring_hom.id R) M M₂

[Frédéric Dupuis]

Sebastien Gouezel said:

Since you have experimented with this, I'll trust your word on it! My concern is that, if one starts to define linear maps for twisted structures, one will also want to define modules for twisted structures, matrices for twisted structures, and in the end redo all the linear algebra library by adding everywhere a twisting factor (and for linear maps one should maybe even have the possibility to add one twisting factor in the source and one in the target) -- otherwise, twisted linear maps will just be gadget that doesn't play well with the rest of the library. And that doesn't seem reasonable.

I'm not sure what you mean by needing modules and matrices for twisted structures -- I think having semilinear maps would solve most of the issues I'm thinking of. Of course this would still be a fairly big refactor and this is the main downside, but judging from the quick tests I did it's not nearly as disruptive as I had initially thought.

[Frédéric Dupuis]

Heather Macbeth said:

Another idea -- perhaps one could implement linear maps just as a notational overlay on semilinear maps, i.e. M →ₗ[R] M₂ means semilinear_map (ring_hom.id R) M M₂

Yes, this seemed to work surprisingly well when I tried it.

[Frédéric Dupuis]

linear_map is almost never used directly in the library, it's nearly always through this notation.

[Heather Macbeth]

Frédéric Dupuis said:

Yes, this seemed to work surprisingly well when I tried it.

Ah, you already tried this! :)

[Frédéric Dupuis]

Yes, I just tried redefining linear_map as in this proposal and setting up the notation like this. It didn't break much, but of course we would then have to start generalizing theorems to semilinear maps.

[Johan Commelin]

Heather Macbeth said:

Likewise, instances for [fact (conj.comp id = conj)] and [fact (id.comp conj = conj)].

The only downside is that fact shouldn't have global instances. The easy work around is to not use fact but a dedicated fact' (name too be discussed :rofl:)

[Heather Macbeth]

Johan Commelin said:

The only downside is that fact shouldn't have global instances.

Oh interesting, can you explain?

[Johan Commelin]

As I understand it, the typeclass system indexes on the head symbol. So if there are many instances about fact ((foo.comp bar) = quux), then everytime the p-adic numbers need fact p.prime, TC will also try all those composition facts.

[Johan Commelin]

So, instances of the form [fact foobar] : [fact xyzzy] are fine, because they keep everything local, and hence when TC searches for fact xyzzy there will only be a small set of facts in scope.
Currently there are 5 (or so) global instances. If we start adding a lot to those, TC search might explode.

[Johan Commelin]

TC experts: correct me if I'm wrong

[Frédéric Dupuis]

Either way, we could definitely live with a dedicated version of fact for this.

[Heather Macbeth]

Would something like this work?

class is_composition_tuple : Prop :=
(comp_property : τ.comp σ = η)

instance foo : is_composition_tuple (ring_hom.id R) (ring_hom.id R) (ring_hom.id R) :=
{ comp_property := (ring_hom.id R).comp_id }

[Johan Commelin]

certainly, except that the name seems a bit long

[Johan Commelin]

Also, you don't need one for id.comp id because it follows from id.comp f = f... :wink:

[Mario Carneiro]

Johan Commelin said:

So, instances of the form [fact foobar] : [fact xyzzy] are fine, because they keep everything local, and hence when TC searches for fact xyzzy there will only be a small set of facts in scope.
Currently there are 5 (or so) global instances. If we start adding a lot to those, TC search might explode.

No? Any fact instance will make the global search problem harder. There aren't supposed to be any global instances

[Johan Commelin]

So we should remove those 5

[Mario Carneiro]

What are they?

[Johan Commelin]

Probably fact (0 < 1) and fact (nat.prime 2) and the likes.

[Mario Carneiro]

Isn't nat.prime a class? Why can't that be an instance?

[Johan Commelin]

No, it's not a class, afaik

[Mario Carneiro]

We could put those facts into a locale, if there are enough of them to make the organization worthwhile

[Heather Macbeth]

Johan Commelin said:

Also, you don't need one for id.comp id because it follows from id.comp f = f... :wink:

I didn't immediately understand, but your point is that we would definitely have the instance

is_composition_tuple (ring_hom.id R) f f

and so it's unnecessary also to have the instance

is_composition_tuple (ring_hom.id R) (ring_hom.id R) (ring_hom.id R)

Is that right?

[Heather Macbeth]

Mario Carneiro said:

We could put those facts into a locale, if there are enough of them to make the organization worthwhile

I think we need:

• [fact (id.comp σ = σ)]
• [fact (σ.comp id = σ)]
• [fact (conj.comp conj = id)]
• [fact (τ.comp σ = τ.comp σ)]

[Sebastien Gouezel]

Note that the right-hand side can in general not be deduced from the left-hand side, so there should be some outparam trickery to make this work. If I understand correctly, when setting up the general theory there would be some typeclass assumption like [is_composition_tuple u v w] where u, v and w are some generic automorphisms, and in concrete applications it would pick the right w automatically? This sounds like a pretty idea!

[Eric Wieser]

are some generic automorphisms,

I'm pretty sure we don't have a way of generalizing across types of homomorphisms (linear_map, add_monoid_hom, etc), ignoring the category library that is used in a self-contained way.

[Frédéric Dupuis]

Eric Wieser said:

ignoring the category library that is used in a self-contained way.

Yeah, I've always thought that we could save a lot of boilerplate code by using category theory for these kinds of objects.

[Sebastien Gouezel]

Eric Wieser said:

are some generic automorphisms,

I'm pretty sure we don't have a way of generalizing across types of homomorphisms (linear_map, add_monoid_hom, etc), ignoring the category library that is used in a self-contained way.

Yeah, I meant "generic" in the sense of "not a prescribed one" (i.e., not just the identity or complex conjugation), but still within the realm of field automorphisms.

[Heather Macbeth]

Sebastien Gouezel said:

Note that the right-hand side can in general not be deduced from the left-hand side, so there should be some outparam trickery to make this work. If I understand correctly, when setting up the general theory there would be some typeclass assumption like [is_composition_tuple u v w] where u, v and w are some generic automorphisms, and in concrete applications it would pick the right w automatically? This sounds like a pretty idea!

@Sebastien Gouezel I think maybe you have had a further idea beyond what I said, could you explain? I was imagining that given a u-linear map f and v-linear map g, one would have to specify the desired w when composing, like f.comp w g. The composition would require an instance [is_composition_tuple u v w] (i.e., w = v.comp u), and we would write down the "usual" instances, so that typeclass inference could find them silently in the concrete applications.

But you are saying there might be a way to use out_param to find the w automatically, so one could write f.comp g? That would be better!

[Sebastien Gouezel]

Yes, that's exactly what out_params do. Otherwise, you would need to write f.comp id g most of the time, and this would get really boring.

[Heather Macbeth]

I was thinking that one would provide [is_composition_tuple u v (v.comp u)], as a backup for when there is no better way of expressing the composition. Can you do this but also ensure that the better w is chosen when it's available?

[Heather Macbeth]

Maybe by putting a very low priority on [is_composition_tuple u v (v.comp u)]?

[Johan Commelin]

Sebastien Gouezel said:

Otherwise, you would need to write f.comp id g most of the time, and this would get really boring.

We could still have abbreviations linear_map and linear_map.comp that take care of this, right?

[Johan Commelin]

If the outparams work, that would be great. But if they don't work, they can be very painful.

[Heather Macbeth]

From Frédéric's experiments, apparently one may not even need an abbreviation linear_map, just notation.

[Heather Macbeth]

But do you think an abbreviation would work better?

[Johan Commelin]

It would allow for dot-notation, if we need that

[Frédéric Dupuis]

For composition, an abbreviation would be a good plan B in case the out_param thing fails.

[Heather Macbeth]

Another question (which Frédéric raised before): will there still be out_param in Lean 4, and will it work the same way?

[Sebastien Gouezel]

Heather Macbeth said:

I was thinking that one would provide [is_composition_tuple u v (v.comp u)], as a backup for when there is no better way of expressing the composition. Can you do this but also ensure that the better w is chosen when it's available?

The problem if you state a theorem that way is that it will only apply when the is_composition_tuple mechanism chooses exactly v.comp u, which is not what you want because you want to apply your theorems in all situations. So I guess we should state theorems with generic assumptions [is_composition_tuple u v w], so that they apply in all situations.

[Sebastien Gouezel]

For applications of the theorems, on the other hand, I agree we can have the instance you're mentioning, with a low priority to make sure that the other ones are found first.

[Heather Macbeth]

Yes, great! For use when @Johan Commelin does Frobenius-semilinear algebra, whatever that is :)

[Heather Macbeth]

By the way, another point is that sometimes one has to deal with three maps, and thus with associativity (I remember Yury mentioning this). I'm not sure if the existence of

[is_composition_tuple (v.comp u) w ((w.comp v).comp u)]

is enough to solve all problems there.

[Sebastien Gouezel]

Given that it will probably take some time before someone finds the courage to do the refactor, it might make sense, for now, to merge separately the two PRs that give the existence of orthonormal basis in the two contexts, to avoid blocking further progress. What do you think?

[Scott Morrison]

It seems we stalled on @Jason KY.'s PR #5814. (It's currently the oldest PR on #queue!) Shall we merge it?

[Johan Commelin]

I think @Heather Macbeth was experimenting with different approaches

[Jason KY.]

No longer the oldest on the queue now that I made some style changes :) Can we merge this and make changes to it afterwards however? I'm proving some stuff about nondegenerate forms and I would like to use some definitions found in that pr.

[Bryan Gin-ge Chen]

@Heather Macbeth do you mind taking a look at #5814 again? It looks to me like it's waiting on your OK...

[Heather Macbeth]

Sorry, I didn't realise! I'll take a look.