## Stream: Is there code for X?

### Topic: Hilbert space is isometric to its dual

#### Tomas Skrivan (Oct 26 2020 at 14:54):

Is somewhere in mathlib proven that the map v → ⟪v, ⬝ ⟫ is isometry between a Hilbert space and its dual?

#### Yury G. Kudryashov (Oct 26 2020 at 14:58):

@Frédéric Dupuis :up:

#### Frédéric Dupuis (Oct 26 2020 at 15:55):

#4379, more precisely. It's currently waiting on how we're going to handle conjugate-linear maps. @Yury G. Kudryashov , are you planning to go ahead with the linear_map (f : R →+* S) E F idea that was discussed a few days ago?

#### Yury G. Kudryashov (Oct 26 2020 at 16:01):

I have a few refactors in line, and every time I switch branches I choose one of them and advance it a little:

• bundle direction into affine_subspace;
• review affine combinations by introducing the free affine space {f : α →₀ R | f.sum (λ a b, b) = 1};
• redefine convexity for affine spaces;
• use bundled homs for polynomial.eval etc;
• glue mv_power_series to analytic maps;
• redefine some free constructions using docs#con to get the universal property almost for free;
• add smul_comm_class and migrate some parts of the library to it.

#### Yury G. Kudryashov (Oct 26 2020 at 16:03):

I guess, I'm not going to work on refactoring linear_maps for at least a week, so probably it's better to merge your PR without waiting for this refactor.

#### Heather Macbeth (Oct 26 2020 at 16:55):

I wonder whether it's worth refactoring #4379 (again! Sorry, Frédéric), so that it mostly does the real case, and does it in a way that will be directly generalizable to the conjugate-linear setting now that we have a theory for what that setting will look like.

#### Heather Macbeth (Oct 26 2020 at 16:56):

If this seems like a good idea, I can try this, since I don't want Frédéric to have to spend any more time on this.

#### Heather Macbeth (Oct 26 2020 at 16:57):

Maybe also get rid of the development of conjugate vector spaces, if we think that ultimately these will be treated in mathlib using smul_comm_class?

#### Frédéric Dupuis (Oct 26 2020 at 17:17):

Yeah, if we get conjugate-linear maps soon(ish) we definitely want this code to be based on that. I think the best thing to do would be to remove the conjugate semimodule code and merge it.

#### Heather Macbeth (Oct 26 2020 at 21:44):

@Frédéric Dupuis I would like to change your definition of the dual of a Hilbert space, so that the inner product is given by the polarization identity:

instance : has_inner 𝕜 (normed_space.dual 𝕜 E) :=
{ inner := λ x y, 4⁻¹ * ((𝓚 ∥x + y∥) * (𝓚 ∥x + y∥) - (𝓚 ∥x - y∥) * (𝓚 ∥x - y∥)
+ is_R_or_C.I * (𝓚 ∥x + (@is_R_or_C.I 𝕜 _) • y∥) * (𝓚 ∥x + (@is_R_or_C.I 𝕜 _) • y∥)
- is_R_or_C.I * (𝓚 ∥x - (@is_R_or_C.I 𝕜 _) • y∥) * (𝓚 ∥x - (@is_R_or_C.I 𝕜 _) • y∥)) }


rather than copied over from the primal inner product by means of the equivalence:

instance : has_inner 𝕜 (normed_space.dual 𝕜 E) :=
{ inner := λ x y, ⟪to_primal y, to_primal x⟫ }


as you had written. The advantage is that the new definition works for inner product spaces without a completeness hypothesis. What do you think?

#### Heather Macbeth (Oct 26 2020 at 21:46):

This also would mean that the statement that "the mapping from E to its dual is an isometry" has content, rather than following by definition.

#### Frédéric Dupuis (Oct 26 2020 at 21:47):

That makes sense -- I hadn't thought about the completeness issue. I guess you'll have to prove the is_R_or_C polarization identity first though, only the real case is there now and I've been too lazy so far to generalize it :-)

#### Heather Macbeth (Oct 26 2020 at 21:48):

Yep, I am halfway there after a solid hour's work, it is not pleasant! :)

#### Frédéric Dupuis (Oct 26 2020 at 21:52):

I have no doubt -- that's why I haven't done it...!

#### Heather Macbeth (Oct 26 2020 at 21:58):

I was half-hoping that there were some mysteries of is_R_or_C which you would explain to me and which would improve things ....

#### Frédéric Dupuis (Oct 26 2020 at 22:01):

Not really -- it mostly just works like ℂ. So at least it shouldn't be any more annoying than proving the complex polarization identity directly.

#### Frédéric Dupuis (Oct 26 2020 at 22:03):

The one thing that is more annoying than ℂ is that coercions from reals have to be done manually, so norm_cast doesn't work.

#### Heather Macbeth (Oct 26 2020 at 22:06):

Yep, just figured that out half an hour ago :)

#### Heather Macbeth (Oct 26 2020 at 22:07):

(I wonder if it would be possible to get norm_cast working for is_R_or_C? Need to ask someone who knows about tactics.)

#### Frédéric Dupuis (Oct 26 2020 at 22:11):

I looked into it at the time, and I strongly suspect that the answer is no. We can't have proper coercions, because that causes a circular issue with the 𝕜=ℝ case, and norm_cast really needs coercions from what I could gather from the code. Maybe it's possible to create a specialized version of norm_cast where we replace the coercions by the manual one in is_R_or_C, but I'm afraid that's above my pay grade at the moment :-)

#### Heather Macbeth (Oct 26 2020 at 22:11):

I see, very interesting!

#### Yury G. Kudryashov (Oct 26 2020 at 23:11):

Does docs#has_lift_t work?

#### Yury G. Kudryashov (Oct 26 2020 at 23:12):

This is a coercion that requires an explicit up arrow.

#### Frédéric Dupuis (Oct 26 2020 at 23:50):

Hmm... maybe? It's worth looking into -- for some reason I've never run into these before.

#### Yury G. Kudryashov (Oct 27 2020 at 00:24):

It is (mis)used for coercion of a finset to a set.

#### Frédéric Dupuis (Oct 27 2020 at 01:30):

#check (show has_lift_t ℝ ℝ, by apply_instance)


fails. Doesn't look good...

#### Yury G. Kudryashov (Oct 27 2020 at 02:06):

I think that you can define it and it'll work.

#### Frédéric Dupuis (Oct 27 2020 at 03:00):

instance : has_lift ℝ K := ⟨of_real⟩
#check (show has_lift_t ℝ ℝ, by apply_instance)


This still fails -- I have no idea why...

#mwe?

#### Frédéric Dupuis (Oct 27 2020 at 03:54):

class is_R_or_C (K : Type*)  :=
(of_real : ℝ → K)

namespace is_R_or_C

variables {K : Type*} [is_R_or_C K]

instance : has_lift ℝ K := ⟨of_real⟩
#check (show has_lift_t ℝ ℝ, by apply_instance)

end is_R_or_C


#### Mario Carneiro (Oct 27 2020 at 03:56):

the has_lift instance is not ok

#### Mario Carneiro (Oct 27 2020 at 03:56):

because it causes has_lift_t to loop

#### Frédéric Dupuis (Oct 27 2020 at 03:56):

OK, so basically the same reason we couldn't have the coercion either.

That's a shame.

#### Mario Carneiro (Oct 27 2020 at 03:57):

you could make it a has_{coe|lift}_t instance

#### Frédéric Dupuis (Oct 27 2020 at 03:59):

Really? I'm pretty sure I tried making this a has_coe_t instance directly a while back and it failed.

#### Frédéric Dupuis (Oct 27 2020 at 04:02):

And if I recall correctly, it was you who convinced me I should give up and do coercions manually :-)

#### Mario Carneiro (Oct 27 2020 at 04:05):

right... we don't have reflexive coe_t instances

#### Mario Carneiro (Oct 27 2020 at 04:07):

I think it should be possible to modify norm_cast to work with things other than coe

#### Yury G. Kudryashov (Oct 27 2020 at 04:07):

Are reflexive has_coe_t instances bad, or only has_coe?

#### Yury G. Kudryashov (Oct 27 2020 at 04:07):

A version of #mwe that works

class is_R_or_C (K : Type*)  :=
(of_real : ℝ → K)

namespace is_R_or_C

variables {K : Type*} [is_R_or_C K]

instance : has_lift ℝ K := ⟨of_real⟩
#check (show has_lift_t ℝ ℝ, by apply_instance)

end is_R_or_C


#### Mario Carneiro (Oct 27 2020 at 04:08):

it looks identical to @Frédéric Dupuis 's

#### Heather Macbeth (Oct 27 2020 at 05:17):

Heather Macbeth said:

Yep, I am halfway there after a solid hour's work, it is not pleasant! :)

I posted a WIP PR, #4798, anyone in the mood for some algebra problems is welcome to take over some of the sorries!

#### Gabriel Ebner (Oct 27 2020 at 08:20):

This should really, really be has_coe_t or has_lift_t. Otherwise you get loops, as Mario's pointed out. This works:

import data.real.basic

class is_R_or_C (K : Type*)  :=
(of_real : ℝ → K)

instance : is_R_or_C ℝ := ⟨id⟩

namespace is_R_or_C

variables {K : Type*} [is_R_or_C K]

instance : has_coe_t ℝ K := ⟨of_real⟩

variable (x : ℝ)
#check (↑x : ℝ)
#check (coe x : ℝ)

end is_R_or_C


#### Ruben Van de Velde (Oct 27 2020 at 08:22):

I pushed a fix for the easiest sorry

#### Mario Carneiro (Oct 27 2020 at 08:25):

@Gabriel Ebner Should we add a general reflexive instance for has_lift_t and/or has_coe_t?

#### Gabriel Ebner (Oct 27 2020 at 08:27):

Like docs#coe_base?

#### Mario Carneiro (Oct 27 2020 at 08:28):

That's just the singleton case

#### Mario Carneiro (Oct 27 2020 at 08:28):

it implies that has_coe_t is the transitive closure of has_coe, but I am thinking about the reflexive transitive closure

Ah, I see.

#### Gabriel Ebner (Oct 27 2020 at 08:29):

Type class-wise, I don't think there would be any issues. Except for non-commuting diamonds.

#### Gabriel Ebner (Oct 27 2020 at 08:30):

But I don't think coercions should be used in this way. If you explicitly write (x : α), then you never need the reflexive instance.

#### Mario Carneiro (Oct 27 2020 at 08:31):

I agree, but the alternatives don't look great for Frederic's use case

#### Mario Carneiro (Oct 27 2020 at 08:32):

I don't think we will get non-commuting diamonds since f o id = f is definitional

#### Mario Carneiro (Oct 27 2020 at 08:32):

but it might be tricky to prove that all the time

#### Gabriel Ebner (Oct 27 2020 at 08:35):

We already have other reflexive instances (like nat.cast_coe). These would not be definitionally equal to the general one.

#### Gabriel Ebner (Oct 27 2020 at 08:36):

For Fréderic's use case we need a coercion for is_R_or_C anyhow, I'm not sure how a general reflexive instance helps here.

#### Mario Carneiro (Oct 27 2020 at 08:37):

well it would be weird if we had a reflexive instance only for real

#### Gabriel Ebner (Oct 27 2020 at 08:37):

Another (very realistic) option is to convince norm_cast that is_R_or_C.of_real is a coercion (it already knows about has_coe_to_fun, has_coe_to_sort; this is just one more function).

#### Mario Carneiro (Oct 27 2020 at 08:37):

That's my thought

#### Gabriel Ebner (Oct 27 2020 at 08:37):

Mario Carneiro said:

well it would be weird if we had a reflexive instance only for real

We also have it for nat, int, etc.

#### Gabriel Ebner (Oct 27 2020 at 08:39):

Personally, I think I'd prefer coercions over is_R_or_C.of_real.

#### Mario Carneiro (Oct 27 2020 at 08:40):

you've convinced me that [is_R_or_C K] : has_coe_t real K would be no better or worse than nat.has_coe

#### Mario Carneiro (Oct 27 2020 at 08:40):

it's a bit better, since the induced reflexive instance is definitional

#### Frédéric Dupuis (Oct 27 2020 at 13:41):

Well that's great news! I see there's a great docstring in data/nat/cast that gives the recipe...

#### Ruben Van de Velde (Oct 27 2020 at 15:24):

Did a few more - done for now, though

Great!

#### Heather Macbeth (Oct 27 2020 at 15:27):

Regarding the casting: If I understand correctly, there are two proposals: to have a "conditional" coercion [is_R_or_C K] : has_coe_t real K, or to hard-code coercion-like behaviour into norm_cast. Would the second proposal mean that one only had improved behaviour when using norm_cast, whereas the first proposal would apply to any situation where one wants to use casts (in norm_cast or out)? If so, the first seems better.

#### Mario Carneiro (Oct 27 2020 at 15:28):

yes, that's right. In particular, the first option would let you use \u while the second requires some other notation

#### Heather Macbeth (Oct 27 2020 at 15:38):

And the first option would also let one cast like (3:K), right? (Which you can't currently do.)

#### Heather Macbeth (Oct 27 2020 at 16:08):

Or rather, I think you can do this (because 3 is a numeral), but you can't currently take an x of type ℝ and cast by saying (x:K). The change would permit that.

#### Frédéric Dupuis (Oct 27 2020 at 16:19):

Yes, I would much prefer the coercion as well.

#### Frédéric Dupuis (Oct 30 2020 at 00:58):

The coercion seems to work! See #4824

#### Frédéric Dupuis (Oct 30 2020 at 00:59):

@Heather Macbeth This PR might make the remaining sorries in #4798 a bit less painful :-)

#### Heather Macbeth (Oct 30 2020 at 01:25):

@Frédéric Dupuis Very cool!

Last updated: May 07 2021 at 21:10 UTC