## Stream: maths

### Topic: Conjugate-linear

#### 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?

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

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

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

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

#### Frédéric Dupuis (Jan 20 2021 at 04:27):

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

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

#### Frédéric Dupuis (Jan 20 2021 at 04:30):

Maybe make the dual a typeclass also?

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

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

#### Heather Macbeth (Jan 20 2021 at 04:37):

That would be nice!

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

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

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

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

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

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

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

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

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

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

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

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

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

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

#### 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 ℂ)?

#### 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 ℂ.

#### 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?

#### 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?

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

#### 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?

#### Heather Macbeth (Jan 21 2021 at 15:26):

Well, that's for Rᵒᵖ.

#### 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 $\mathbb{R}$ and $\mathbb{C}$ (edit: docs#ring_invo.id)

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

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

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

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

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

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

#### 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⟩


#### 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 σ = η)].

#### Heather Macbeth (Jan 21 2021 at 16:50):

Then composition gives you a semilinear_map η M M₃.

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

#### Heather Macbeth (Jan 21 2021 at 16:53):

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

#### 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 η

#### 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₃.

#### Heather Macbeth (Jan 21 2021 at 16:56):

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

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

Yup.

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

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

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

#### Heather Macbeth (Jan 21 2021 at 17:03):

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

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

#### 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₂

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

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

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

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

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

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

#### 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?

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

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

#### Johan Commelin (Jan 21 2021 at 17:59):

TC experts: correct me if I'm wrong

#### Frédéric Dupuis (Jan 21 2021 at 18:00):

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

#### 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 }


#### Johan Commelin (Jan 21 2021 at 18:02):

certainly, except that the name seems a bit long

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

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

#### Johan Commelin (Jan 21 2021 at 18:02):

So we should remove those 5

What are they?

#### Johan Commelin (Jan 21 2021 at 18:03):

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

#### Mario Carneiro (Jan 21 2021 at 18:04):

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

#### Johan Commelin (Jan 21 2021 at 18:04):

No, it's not a class, afaik

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

#### 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?

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

#### 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!

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

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

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

#### 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!

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

#### 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?

#### Heather Macbeth (Jan 21 2021 at 21:11):

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

#### 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?

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

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

#### Heather Macbeth (Jan 21 2021 at 21:14):

But do you think an abbreviation would work better?

#### Johan Commelin (Jan 21 2021 at 21:15):

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

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

#### 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?

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

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

#### Heather Macbeth (Jan 21 2021 at 21:35):

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

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

#### 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?

#### 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?

#### Johan Commelin (Feb 17 2021 at 06:08):

I think @Heather Macbeth was experimenting with different approaches

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

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

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