[Merged by Bors] - feat(analysis/inner_product_space/adjoint): matrix and linear map adjoints agree

[hrmacbeth]

---

[eric-wieser]

Can you add a comment explaining why the id is needed here? Is this a pattern used anywhere else?

I think this is equivalent but the motivation is slightly clearer:

Suggested change

	/-- The adjoint of the linear map associated to a matrix is the linear map associated to the
	conjugate transpose of that matrix. -/
	lemma conj_transpose_eq_adjoint (A : matrix m n 𝕜) :
	(id (to_lin' A.conj_transpose) : euclidean_space 𝕜 m →ₗ[𝕜] euclidean_space 𝕜 n) =
	linear_map.adjoint (id (to_lin' A) : euclidean_space 𝕜 n →ₗ[𝕜] euclidean_space 𝕜 m) :=
	begin
	/-- The adjoint of the linear map associated to a matrix is the linear map associated to the
	conjugate transpose of that matrix. -/
	lemma conj_transpose_eq_adjoint (A : matrix m n 𝕜) :
	(show euclidean_space 𝕜 m →ₗ[𝕜] euclidean_space 𝕜 n, from to_lin' A.conj_transpose) =
	linear_map.adjoint (show euclidean_space 𝕜 n →ₗ[𝕜] euclidean_space 𝕜 m, from to_lin' A) :=
	begin

[hrmacbeth]

I had thought the id was a fairly common pattern for forcing something to be interpreted as a defeq but not syntactically equal type ... perhaps not.

I'm not really a fan of the show idiom, I think it suggests a proof to the casual user where no such proof exists. But I've replaced it with a third option, where linear_map.adjoint has some of its implicit arguments filled in explicitly.

[eric-wieser]

I had thought the id was a fairly common pattern for forcing something to be interpreted as a defeq but not syntactically equal type ... perhaps not.

I'd argue that show is better, as it's more of a flag in the goal view that something weird is going on with the types. id just makes it look like you've managed to simplify something away.

I think it suggests a proof to the casual user where no such proof exists

If you read show as "the next statement will have this type" then there's no mention of proofs specifically, but I can see how a casual user might be confused.

But I've replaced it with a third option, where linear_map.adjoint has some of its implicit arguments filled in explicitly.

I think this new version is probably worse, as it doesn't work well with rw - both id and show ought to be better in this regard. Note also that your original version had different implicit arguments to the eq too.

Probably the cleanest thing to do would be add a variant of matrix.to_lin for euclidean_space, as:

/-- `matrix.to_lin'`, with the domain and codomain living in `euclidean_space` -/
def to_lin'_euclid (A : matrix m n 𝕜) : euclidean_space 𝕜 n →ₗ[𝕜] euclidean_space 𝕜 m :=
A.to_lin'

/-- The adjoint of the linear map associated to a matrix is the linear map associated to the
conjugate transpose of that matrix. -/
lemma conj_transpose_eq_adjoint (A : matrix m n 𝕜) :
  (A.conj_transpose.to_lin'_euclid) = (linear_map.adjoint A.to_lin'_euclid) :=
begin

[hrmacbeth]

I'm afraid I don't like this! We would have to duplicate all the API of to_lin', and this seems really unfortunate.

Shall we discuss on Zulip?

[hrmacbeth]

Perhaps we could go so far as to demote our current metric_space_pi instance to a def, allowing for a locale in which pi_Lp 2 is the default instance.

[eric-wieser]

I went ahead with this in #18574, since we already have an ad-hoc implementation of to_lin'_euclid inside another lemma statement.

[dupuisf]

Looks good to me!

One thought (not necessarily for this PR): what do you think about creating a typeclass has_standard_basis ι 𝕜 E to express the fact that a space E has a standard basis indexed by ι? Having to specify the type constantly as is done here doesn't seem sustainable.

[hrmacbeth]

Hmm, I'm not sure. I almost never work with bases, though, so maybe I'm not the best qualified to have an opinion!

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests