Zulip Chat Archive

Stream: maths

Topic: Conjugate-linear


view this post on Zulip Heather Macbeth (Jan 20 2021 at 03:12):

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:

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?

view this post on Zulip Johan Commelin (Jan 20 2021 at 03:33):

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

view this post on Zulip Frédéric Dupuis (Jan 20 2021 at 04:19):

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.

view this post on Zulip Frédéric Dupuis (Jan 20 2021 at 04:20):

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

view this post on Zulip Frédéric Dupuis (Jan 20 2021 at 04:25):

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.

view this post on Zulip Frédéric Dupuis (Jan 20 2021 at 04:27):

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

view this post on Zulip Heather Macbeth (Jan 20 2021 at 04:28):

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.

view this post on Zulip Frédéric Dupuis (Jan 20 2021 at 04:30):

Maybe make the dual a typeclass also?

view this post on Zulip Heather Macbeth (Jan 20 2021 at 04:36):

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

view this post on Zulip Johan Commelin (Jan 20 2021 at 04:37):

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.

view this post on Zulip Heather Macbeth (Jan 20 2021 at 04:37):

That would be nice!

view this post on Zulip Frédéric Dupuis (Jan 20 2021 at 04:39):

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.

view this post on Zulip Frédéric Dupuis (Jan 20 2021 at 04:42):

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.

view this post on Zulip Eric Wieser (Jan 20 2021 at 09:00):

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.

view this post on Zulip Heather Macbeth (Jan 20 2021 at 14:22):

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

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 08:23):

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.

view this post on Zulip Johan Commelin (Jan 21 2021 at 08:37):

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

view this post on Zulip Johan Commelin (Jan 21 2021 at 08:38):

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

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 08:47):

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.

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 08:53):

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.

view this post on Zulip Johan Commelin (Jan 21 2021 at 08:59):

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.

view this post on Zulip Johan Commelin (Jan 21 2021 at 08:59):

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:

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 09:02):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 14:12):

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

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 14:41):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 14:49):

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

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 14:58):

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 .

view this post on Zulip Heather Macbeth (Jan 21 2021 at 15:22):

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?

view this post on Zulip Eric Wieser (Jan 21 2021 at 15:24):

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?

view this post on Zulip Heather Macbeth (Jan 21 2021 at 15:26):

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.

view this post on Zulip Eric Wieser (Jan 21 2021 at 15:26):

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?

view this post on Zulip Heather Macbeth (Jan 21 2021 at 15:26):

Well, that's for Rᵒᵖ.

view this post on Zulip Eric Wieser (Jan 21 2021 at 15:39):

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

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 15:39):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 15:42):

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 ;)

view this post on Zulip Eric Wieser (Jan 21 2021 at 15:59):

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.

view this post on Zulip Frédéric Dupuis (Jan 21 2021 at 16:02):

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

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 16:29):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:46):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:48):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:49):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:50):

Then composition gives you a semilinear_map η M M₃.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:51):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:53):

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

view this post on Zulip Eric Wieser (Jan 21 2021 at 16:55):

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 η

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:55):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:56):

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

view this post on Zulip Eric Wieser (Jan 21 2021 at 16:56):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 16:57):

Yup.

view this post on Zulip Eric Wieser (Jan 21 2021 at 16:59):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 17:00):

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.

view this post on Zulip Eric Wieser (Jan 21 2021 at 17:02):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 17:03):

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

view this post on Zulip Frédéric Dupuis (Jan 21 2021 at 17:14):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 17:18):

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₂

view this post on Zulip Frédéric Dupuis (Jan 21 2021 at 17:20):

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.

view this post on Zulip Frédéric Dupuis (Jan 21 2021 at 17:49):

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.

view this post on Zulip Frédéric Dupuis (Jan 21 2021 at 17:50):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 17:50):

Frédéric Dupuis said:

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

Ah, you already tried this! :)

view this post on Zulip Frédéric Dupuis (Jan 21 2021 at 17:51):

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.

view this post on Zulip Johan Commelin (Jan 21 2021 at 17:55):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 17:56):

Johan Commelin said:

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

Oh interesting, can you explain?

view this post on Zulip Johan Commelin (Jan 21 2021 at 17:57):

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.

view this post on Zulip Johan Commelin (Jan 21 2021 at 17:59):

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.

view this post on Zulip Johan Commelin (Jan 21 2021 at 17:59):

TC experts: correct me if I'm wrong

view this post on Zulip Frédéric Dupuis (Jan 21 2021 at 18:00):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 18:01):

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 }

view this post on Zulip Johan Commelin (Jan 21 2021 at 18:02):

certainly, except that the name seems a bit long

view this post on Zulip Johan Commelin (Jan 21 2021 at 18:02):

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

view this post on Zulip Mario Carneiro (Jan 21 2021 at 18:02):

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

view this post on Zulip Johan Commelin (Jan 21 2021 at 18:02):

So we should remove those 5

view this post on Zulip Mario Carneiro (Jan 21 2021 at 18:03):

What are they?

view this post on Zulip Johan Commelin (Jan 21 2021 at 18:03):

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

view this post on Zulip Mario Carneiro (Jan 21 2021 at 18:04):

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

view this post on Zulip Johan Commelin (Jan 21 2021 at 18:04):

No, it's not a class, afaik

view this post on Zulip Mario Carneiro (Jan 21 2021 at 18:06):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 18:08):

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?

view this post on Zulip Heather Macbeth (Jan 21 2021 at 18:11):

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 σ)]

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 18:23):

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!

view this post on Zulip Eric Wieser (Jan 21 2021 at 18:51):

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.

view this post on Zulip Frédéric Dupuis (Jan 21 2021 at 19:07):

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.

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 19:51):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 21:00):

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!

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 21:09):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 21:11):

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?

view this post on Zulip Heather Macbeth (Jan 21 2021 at 21:11):

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

view this post on Zulip Johan Commelin (Jan 21 2021 at 21:12):

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?

view this post on Zulip Johan Commelin (Jan 21 2021 at 21:12):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 21:13):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 21:14):

But do you think an abbreviation would work better?

view this post on Zulip Johan Commelin (Jan 21 2021 at 21:15):

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

view this post on Zulip Frédéric Dupuis (Jan 21 2021 at 21:15):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 21:16):

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

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 21:31):

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.

view this post on Zulip Sebastien Gouezel (Jan 21 2021 at 21:34):

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.

view this post on Zulip Heather Macbeth (Jan 21 2021 at 21:35):

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

view this post on Zulip Heather Macbeth (Jan 21 2021 at 21:45):

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.

view this post on Zulip Sebastien Gouezel (Jan 22 2021 at 09:33):

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?

view this post on Zulip Scott Morrison (Feb 17 2021 at 01:08):

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

view this post on Zulip Johan Commelin (Feb 17 2021 at 06:08):

I think @Heather Macbeth was experimenting with different approaches

view this post on Zulip Jason KY. (Feb 17 2021 at 12:19):

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.

view this post on Zulip Bryan Gin-ge Chen (Mar 04 2021 at 18:14):

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

view this post on Zulip Heather Macbeth (Mar 04 2021 at 18:21):

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


Last updated: May 06 2021 at 18:20 UTC