Adjoint of linear map

Stream: new members

[Daniel Packer]

I've been working with @Hans Parshall on singular value stuff, and we both haven't been able to troubleshoot the error message from the following code:

variables {n : Type*} {F : Type*}
variables [fintype n]
variables [decidable_eq n]
variables [field F]
variables [is_R_or_C F]
variables [inner_product_space F (n → F)]
variables [module.finite F (n → F)]
variables {A : matrix n n F}
#check (matrix.to_lin' A).adjoint

Which yields the error message:

type mismatch at application
  ⇑linear_map.adjoint (⇑matrix.to_lin' A)
term
  ⇑matrix.to_lin' A
has type
  (n → F) →ₗ[F] n → F : Type (max u_1 u_2)
but is expected to have type
  ?m_3 →ₗ[?m_1] ?m_4 : Type (max ? ?)

It seems like the types line up, so the error message is quite confusing.
If anyone has any insight on this error, let me know!

[Anne Baanen]

Maybe you need to remove the inner_product_space F (n → F) and/or module.finite F (n → F) variables?

[Kevin Buzzard]

Can you add imports? I can't get your code working.

[Anne Baanen]

Presumably:

import analysis.inner_product_space.adjoint
import linear_algebra.matrix.to_lin

[Daniel Packer]

I think this import should be sufficient:

import analysis.inner_product_space.adjoint

[Daniel Packer]

Removing the variables in any combination didn't work either

[Daniel Packer]

Oh, you're right about the other import

[Daniel Packer]

A perhaps simpler example (without the matrix part):

import analysis.inner_product_space.adjoint

variables {ι : Type*} {R : Type*} {m n p : Type*}
variables [fintype m] [fintype n] [fintype p]
variables [decidable_eq m] [decidable_eq n] [decidable_eq p]

variables [inner_product_space ℂ (m → ℂ)] [inner_product_space ℂ (n → ℂ)]
variables [finite_dimensional ℂ (m → ℂ)] [finite_dimensional ℂ (n → ℂ)]

variable f : (m → ℂ) →ₗ[ℂ] (n → ℂ)

#check f.adjoint

[Kevin Buzzard]

(deleted)

[Daniel Packer]

Woops, edited now for that

[Kevin Buzzard]

I usually debug this sort of thing by rewriting as #check @linear_map.adjoint _ _ _ _ _ _ _ _ f and then I start filling in the holes.

[Kevin Buzzard]

#check @linear_map.adjoint ℂ (m → ℂ) (n → ℂ) _ _ _ _ _ f

->

failed to synthesize type class instance for
ι : Type u_1,
R : Type u_2,
m : Type u_3,
n : Type u_4,
p : Type u_5,
_inst_1 : fintype m,
_inst_2 : fintype n,
_inst_3 : fintype p,
_inst_4 : decidable_eq m,
_inst_5 : decidable_eq n,
_inst_6 : decidable_eq p,
_inst_7 : inner_product_space ℂ (m → ℂ),
_inst_8 : inner_product_space ℂ (n → ℂ),
_inst_9 : finite_dimensional ℂ (m → ℂ),
_inst_10 : finite_dimensional ℂ (n → ℂ),
f : (m → ℂ) →ₗ[ℂ] n → ℂ
⊢ finite_dimensional ℂ (m → ℂ)

[Anne Baanen]

That should not fail (even without _inst_9), since n is a fintype...

[Anne Baanen]

Aha, I see the likely issue: adding the variable [inner_product_space ℂ (m → ℂ)] gives an incompatible instance with the standard vector space on m → ℂ.

[Kevin Buzzard]

So filling in the _s with instances you get

type mismatch at application
  linear_map.adjoint
term
  _inst_9
has type
  @finite_dimensional ℂ (m → ℂ) (@field.to_division_ring ℂ complex.field)
    (@pi.add_comm_group m (λ (ᾰ : m), ℂ) (λ (i : m), @normed_group.to_add_comm_group ℂ complex.normed_group))
    (@pi.module m (λ (ᾰ : m), ℂ) ℂ
       (@ring.to_semiring ℂ (@division_ring.to_ring ℂ (@field.to_division_ring ℂ complex.field)))
       (λ (i : m), @add_comm_group.to_add_comm_monoid ℂ (@normed_group.to_add_comm_group ℂ complex.normed_group))
       (λ (i : m),
          @semiring.to_module ℂ
            (@ring.to_semiring ℂ (@division_ring.to_ring ℂ (@field.to_division_ring ℂ complex.field)))))
but is expected to have type
  @finite_dimensional ℂ (m → ℂ)
    (@field.to_division_ring ℂ
       (@normed_field.to_field ℂ
          (@nondiscrete_normed_field.to_normed_field ℂ
             (@is_R_or_C.to_nondiscrete_normed_field ℂ complex.is_R_or_C))))
    (@normed_group.to_add_comm_group (m → ℂ)
       (@inner_product_space.to_normed_group ℂ (m → ℂ) complex.is_R_or_C _inst_7))
    (@normed_space.to_module ℂ (m → ℂ)
       (@nondiscrete_normed_field.to_normed_field ℂ (@is_R_or_C.to_nondiscrete_normed_field ℂ complex.is_R_or_C))
       (@inner_product_space.to_normed_group ℂ (m → ℂ) complex.is_R_or_C _inst_7)
       (@inner_product_space.to_normed_space ℂ (m → ℂ) complex.is_R_or_C _inst_7))

[Hans Parshall]

this looks familiar :)

[Anne Baanen]

This is not a corner of the library I'm familiar with, but it looks like the solution is to use docs#euclidean_space instead of n → ℂ:

import analysis.inner_product_space.pi_L2
import analysis.inner_product_space.adjoint

variables {ι : Type*} {R : Type*} {m n p : Type*}
variables [fintype m] [fintype n] [fintype p]
variables [decidable_eq m] [decidable_eq n] [decidable_eq p]

variable f : (m → ℂ) →ₗ[ℂ] (n → ℂ)

-- Works:
#check @linear_map.adjoint ℂ (euclidean_space ℂ m) (euclidean_space ℂ n) _ _ _ _ _ f

[Anne Baanen]

Ah, but euclidean_space isn't a ℂ-vector space...

[Daniel Packer]

Will this still work for the old problem? Since the linear map generated from the matrix is automatically of type

(n → ℂ) →ₗ[ℂ] m → ℂ

[Frédéric Dupuis]

Anne Baanen said:

Ah, but euclidean_space isn't a ℂ-vector space...

It really should be! For some weird reason it finds the module instance for an is_R_or_C field but not for ℂ:

import analysis.inner_product_space.pi_L2
import analysis.inner_product_space.adjoint

noncomputable theory

variables {m : Type*} {𝕜 : Type*} [is_R_or_C 𝕜] [fintype m] [decidable_eq m]

example : module ℂ (m → ℂ) := by apply_instance    -- works
example : module 𝕜 (m → 𝕜) := by apply_instance    -- works
example : module ℂ (euclidean_space ℂ m) := by apply_instance     -- fails
example : module 𝕜 (euclidean_space 𝕜 m) := by apply_instance     -- works
example : module ℂ (pi_Lp 2 (λ i : m, ℂ)) := by apply_instance   -- fails
example : module 𝕜 (pi_Lp 2 (λ i : m, 𝕜)) := by apply_instance    -- works
example : inner_product_space ℂ (euclidean_space ℂ m) := by apply_instance   -- works
example : inner_product_space 𝕜 (euclidean_space 𝕜 m) := by apply_instance    -- works
example : normed_space ℂ (euclidean_space ℂ m) := by apply_instance          -- works
example : normed_space 𝕜 (euclidean_space 𝕜 m) := by apply_instance          -- works

Does anyone know what's going on?

[Rob Lewis]

Still looking into this, but the type class trace looks very suspicious, and local attribute [-instance] pi_Lp.normed_group makes it work

[Heather Macbeth]

@Daniel Packer, if you're dealing with the adjoints of linear maps defined by matrices, you'll probably want to know that you can get them concretely by transposing the matrix. I had some code lying around for this which you have inspired me to clean up and PR: #11551

[Daniel Packer]

@Heather Macbeth Oh nice! Looking at the PR, it looks like you used some trick with id to get the type to work out--what purpose is the id filling in? Does it tell Lean what type to coerce (n \to \C) to be?

[Heather Macbeth]

@Daniel Packer Yes, this is because euclidean_space 𝕜 n is a "type synonym" for n → 𝕜 so one sometimes has to engage in trickery to get Lean to recognize something of the one type as being of the other type.

But it's clearly unsatisfactory (and just hasn't been a big obstacle before because not many people have done explicit calculations on euclidean_space 𝕜 n). See this discussion, probably to be continued on Zulip at some point, for some points of view.

[Heather Macbeth]

(The issue is that by default n → 𝕜 has the l-infinity norm, not the l-2 norm.)

[Yakov Pechersky]

Similar issue is that while matrix n n R is just n -> n -> R, (1 : matrix n n R) is supposed to be the diagonal matrix with 1 on the diagonal, while (1 : n -> n -> R) is the constant function giving 1 : R for all inputs 1 x y (docs#matrix.has_one vs docs#pi.has_one). And sometimes, the wrong 1 is inferred for matrix, somehow falling back to the pi one.

[Eric Wieser]

Do you have an example of when that happens, Yakov?

[Yakov Pechersky]

I've had this issue when working with explicit matrices and trying to prove something like

![![1, 0], ![0, 1]] = 1

[Eric Wieser]

Ah right; the problem there being that docs#matrix.vec_cons has the wrong type, just as docs#matrix.to_lin' has the wrong type for @Heather Macbeth.

[Eric Wieser]

That's a little easier to solve though, we could just have a matrix_of constructor like set_of. The to_lin case is harder because we want to change only subterms of the type, not the head term