CPTP maps on Hilbert spaces

Stream: maths

[Magalame]

Hi, I'm trying to describe the structure of CPTP maps on Hilbert spaces, but I'm having trouble figuring out how the "[]" and "extends" notation differ, for example I have

import analysis.inner_product_space.basic
import analysis.von_neumann_algebra.basic

class hilbert (H: Type ) [add_comm_group H] [module ℂ H] [finite_dimensional ℂ H] extends inner_product_space ℂ H, complete_space H

class cptp_map {H: Type} (T: von_neumann_algebra H) [hilbert H]

But then it gives me the error

failed to synthesize type class instance for
H : Type
⊢ inner_product_space ℂ H

Which should trivially be resolved since hilbert extends inner_product_space

[Andrew Yang]

Since von_neumann_algebra needs inner_product_space, you should put [hilbert H] before (T: von_neumann_algebra H).

[Yaël Dillies]

Also, I think we've decided not to define the class of Hilbert spaces, but instead use [inner_product_space ℂ H} [complete_space H] everywhere.

[Eric Wieser]

Also I think what you've written provides two separate module structures

[Eric Wieser]

Because docs#inner_product_space extends module and add_comm_monoid

[Magalame]

thank you! That makes sense, so eventually I went with structure along the lines of

class finite_dim_hilbert (H: Type ) extends inner_product_space ℂ H, complete_space H :=
(to_finite: Prop := finite_dimensional  ℂ H)

class cptp_map {H: Type} [finite_dim_hilbert H] (T: von_neumann_algebra H )

[Magalame]

I'm not working on a something that will be merged to mathlib so I'd prefer not having to write [inner_product_space ℂ H} [complete_space H] everywhere if I can avoid it!

[Andrew Yang]

I think it should be this instead:

class finite_dim_hilbert (H: Type) extends inner_product_space ℂ H, complete_space H :=
(to_finite : finite_dimensional ℂ H)

What you wrote meant that to_finite is an arbitrary Prop, whose default value is finite_dimensional ℂ H.

[Eric Wieser]

You'll want to add attribute [instance] finite_dim_hilbert.to_finite after that

[Magalame]

Ooh I see, this line allows elements requiring [finite_dimensional K V] to see the field inside. Is there an intuitive reason why finite_dimensional is not a class? Naively it seems like it would simplify its use?

[Junyan Xu]

docs#finite_dimensional is a reducible definition that unfolds to module.finite which is a class, so it's effectively a class too. You can put it in [] as an argument and it will get inferred.