Adjoint of linear map between hilbert spaces

Stream: maths

[Apurva Nakade]

Hi,
I'm getting an error when trying to define adjoint of an operator between hilbert spaces. Here's an mwe:

import analysis.inner_product_space.adjoint

noncomputable theory

variables (V : Type*) [add_comm_group V] [module ℝ V] [inner_product_space ℝ V] [complete_space V]
variables (W : Type*) [add_comm_group W] [module ℝ W] [inner_product_space ℝ W] [complete_space W]

variables (E : V →L[ℝ] W)

#check E.adjoint

The error is

type mismatch at application
  ⇑continuous_linear_map.adjoint E
term
  E
has type
  V →L[ℝ] W : Type (max u_1 u_2)
but is expected to have type
  ?m_3 →L[?m_1] ?m_5 : Type (max ? ?)

Not sure what the error means. I'm just trying to define E†.
Any suggestions on how to fix this?
Thanks,

[Eric Wieser]

Try using @ to pass the m_3 and m_5 arguments explicitly

[Eric Wieser]

That usually gives you a better error

[Apurva Nakade]

I tried this code

import analysis.inner_product_space.adjoint

noncomputable theory

variables (V : Type*) [add_comm_group V] [module ℝ V] [hV : inner_product_space ℝ V] [hV' : complete_space V]
variables (W : Type*) [add_comm_group W] [module ℝ W] [hW : inner_product_space ℝ W] [hW' : complete_space W]

variables (E : V →L[ℝ] W)

#check @continuous_linear_map.adjoint ℝ V W _ hV hW hV' hW' E

and the error got enormous :(

  ⇑continuous_linear_map.adjoint E
term
  E
has type
  @continuous_linear_map real real real.semiring real.semiring
    (@ring_hom.id real (@semiring.to_non_assoc_semiring real real.semiring))
    V
    (@uniform_space.to_topological_space V
       (@pseudo_metric_space.to_uniform_space V
          (@semi_normed_group.to_pseudo_metric_space V
             (@normed_group.to_semi_normed_group V (@inner_product_space.to_normed_group real V real.is_R_or_C hV)))))
    (@add_comm_group.to_add_comm_monoid V _inst_1)
    W
    (@uniform_space.to_topological_space W
       (@pseudo_metric_space.to_uniform_space W
          (@semi_normed_group.to_pseudo_metric_space W
             (@normed_group.to_semi_normed_group W (@inner_product_space.to_normed_group real W real.is_R_or_C hW)))))
    (@add_comm_group.to_add_comm_monoid W _inst_3)
    _inst_2
    _inst_4
but is expected to have type
  @continuous_linear_map real real
    (@ring.to_semiring real
       (@normed_ring.to_ring real
          (@normed_comm_ring.to_normed_ring real
             (@normed_field.to_normed_comm_ring real
                (@nondiscrete_normed_field.to_normed_field real
                   (@is_R_or_C.to_nondiscrete_normed_field real real.is_R_or_C))))))
    (@ring.to_semiring real
       (@normed_ring.to_ring real
          (@normed_comm_ring.to_normed_ring real
             (@normed_field.to_normed_comm_ring real
                (@nondiscrete_normed_field.to_normed_field real
                   (@is_R_or_C.to_nondiscrete_normed_field real real.is_R_or_C))))))
    (@ring_hom.id real
       (@semiring.to_non_assoc_semiring real
          (@ring.to_semiring real
             (@normed_ring.to_ring real
                (@normed_comm_ring.to_normed_ring real
                   (@normed_field.to_normed_comm_ring real
                      (@nondiscrete_normed_field.to_normed_field real
                         (@is_R_or_C.to_nondiscrete_normed_field real real.is_R_or_C))))))))
    V
    (@uniform_space.to_topological_space V
       (@pseudo_metric_space.to_uniform_space V
          (@semi_normed_group.to_pseudo_metric_space V
             (@normed_group.to_semi_normed_group V (@inner_product_space.to_normed_group real V real.is_R_or_C hV)))))
    (@add_comm_group.to_add_comm_monoid V
       (@normed_group.to_add_comm_group V (@inner_product_space.to_normed_group real V real.is_R_or_C hV)))
    W
    (@uniform_space.to_topological_space W
       (@pseudo_metric_space.to_uniform_space W
          (@semi_normed_group.to_pseudo_metric_space W
             (@normed_group.to_semi_normed_group W (@inner_product_space.to_normed_group real W real.is_R_or_C hW)))))
    (@add_comm_group.to_add_comm_monoid W
       (@normed_group.to_add_comm_group W (@inner_product_space.to_normed_group real W real.is_R_or_C hW)))
    (@normed_space.to_module real V
       (@nondiscrete_normed_field.to_normed_field real (@is_R_or_C.to_nondiscrete_normed_field real real.is_R_or_C))
       (@normed_group.to_semi_normed_group V (@inner_product_space.to_normed_group real V real.is_R_or_C hV))
       (@inner_product_space.to_normed_space real V real.is_R_or_C hV))
    (@normed_space.to_module real W
       (@nondiscrete_normed_field.to_normed_field real (@is_R_or_C.to_nondiscrete_normed_field real real.is_R_or_C))
       (@normed_group.to_semi_normed_group W (@inner_product_space.to_normed_group real W real.is_R_or_C hW))
       (@inner_product_space.to_normed_space real W real.is_R_or_C hW))

[Apurva Nakade]

I've a feeling that I'm not defining Hilbert spaces V and W properly but can't quite find good examples in mathlib.

[Frédéric Dupuis]

The add_comm_group V and module ℝ V instances are redundant, they're already in inner_product_space ℝ V.

[Eric Wieser]

The fact that docs#inner_product_space is the only two-argument typeclass extending a one-argument typeclass makes it pretty much impossible to make the right guess about how to use it

[Eric Wieser]

It would help a bit if the -- note [is_R_or_C instance] comment were part of the docstring