Equivalences determined by one direction

Stream: new members

[Heather Macbeth]

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]

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]

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]

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)

[Heather Macbeth]

Thanks!

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Bryan Gin-ge Chen]

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

[Yury G. Kudryashov]

See also the proofs of src#alg_hom.coe_ring_hom_injective and src#ring_hom.coe_monoid_hom_injective