Stream: new members

Topic: Equivalences determined by one direction

Heather Macbeth (Aug 01 2020 at 20:56):

What is the most efficient way to prove this?

import linear_algebra.basic
variables (R : Type*) (M₁ : Type*) (M₂ : Type*)
variables [ring R] [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂]

example (e f : linear_equiv R M₁ M₂) (h : (e : linear_map R M₁ M₂) = f) : e = f := sorry


I found docs#equiv.coe_fn_injective but can't figure out how to use it here.

Kevin Buzzard (Aug 01 2020 at 21:01):

Here's a kind of annoying proof:

example (e f : linear_equiv R M₁ M₂) (h : (e : linear_map R M₁ M₂) = f) : e = f :=
begin
ext x,
show (e : linear_map R M₁ M₂) x = f x,
rw h,
refl,
end


The coe_fn_injective thing is just the first ext. Looking at the goal I think one should train norm_cast to do this.

Kevin Buzzard (Aug 01 2020 at 21:02):

example (e f : linear_equiv R M₁ M₂) (h : (e : linear_map R M₁ M₂) = f) : e = f :=
begin
apply linear_equiv.ext,
rwa linear_map.ext_iff at h,
end


Kevin Buzzard (Aug 01 2020 at 21:03):

example (e f : linear_equiv R M₁ M₂) (h : (e : linear_map R M₁ M₂) = f) : e = f :=
linear_equiv.ext (linear_map.ext_iff.1 h)


Thanks!

Bryan Gin-ge Chen (Aug 01 2020 at 21:13):

I'm sad that library_search doesn't work on this. library_search! and suggest just time out. @Scott Morrison

Kevin Buzzard (Aug 01 2020 at 21:16):

Is it already in the library? I use two theorems not one.

Kevin Buzzard (Aug 01 2020 at 21:18):

oh, library_search finds this proof of the non-linear-algebra version:

example (e f : equiv M₁ M₂) (h : (e : M₁ → M₂) = f) : e = f :=
equiv.ext (congr_fun h)


Bryan Gin-ge Chen (Aug 01 2020 at 21:20):

Oh, I think you're right. library_search uses solve_by_elim which has congr_fun in its set of lemmas.

Bryan Gin-ge Chen (Aug 01 2020 at 21:20):

So library_search can't usually apply more than one theorem.

Bryan Gin-ge Chen (Aug 01 2020 at 21:36):

I guess that's an argument for adding this to the library.