Hilbert space is isometric to its dual

Stream: Is there code for X?

[Tomas Skrivan]

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

[Yury G. Kudryashov]

There is a PR about this.

[Yury G. Kudryashov]

@Frédéric Dupuis :up:

[Frédéric Dupuis]

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

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]

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]

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]

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]

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]

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]

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

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]

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]

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

[Frédéric Dupuis]

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

[Heather Macbeth]

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]

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]

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]

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

[Heather Macbeth]

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

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]

I see, very interesting!

[Yury G. Kudryashov]

Does docs#has_lift_t work?

[Yury G. Kudryashov]

This is a coercion that requires an explicit up arrow.

[Frédéric Dupuis]

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

[Yury G. Kudryashov]

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

[Frédéric Dupuis]

#check (show has_lift_t ℝ ℝ, by apply_instance)

fails. Doesn't look good...

[Yury G. Kudryashov]

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

[Frédéric Dupuis]

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

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

[Yury G. Kudryashov]

#mwe?

[Frédéric Dupuis]

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]

the has_lift instance is not ok

[Mario Carneiro]

because it causes has_lift_t to loop

[Frédéric Dupuis]

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

[Frédéric Dupuis]

That's a shame.

[Mario Carneiro]

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

[Frédéric Dupuis]

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]

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

[Frédéric Dupuis]

Indeed it was: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/has_coe.20.E2.84.9D.20.E2.84.9D/near/207775998

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

Are reflexive has_coe_t instances bad, or only has_coe?

[Yury G. Kudryashov]

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]

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

[Heather Macbeth]

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]

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]

I pushed a fix for the easiest sorry

[Mario Carneiro]

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

[Gabriel Ebner]

Like docs#coe_base?

[Mario Carneiro]

That's just the singleton case

[Mario Carneiro]

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

[Gabriel Ebner]

Ah, I see.

[Gabriel Ebner]

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

[Gabriel Ebner]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

but it might be tricky to prove that all the time

[Gabriel Ebner]

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

[Gabriel Ebner]

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]

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

[Gabriel Ebner]

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]

That's my thought

[Gabriel Ebner]

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]

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

[Mario Carneiro]

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]

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

[Frédéric Dupuis]

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

[Ruben Van de Velde]

Did a few more - done for now, though

[Heather Macbeth]

Great!

[Heather Macbeth]

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]

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

[Heather Macbeth]

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

[Heather Macbeth]

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]

Yes, I would much prefer the coercion as well.

[Frédéric Dupuis]

The coercion seems to work! See #4824

[Frédéric Dupuis]

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

[Heather Macbeth]

@Frédéric Dupuis Very cool!