Zulip Chat Archive

Stream: new members

Topic: Equivalences determined by one direction


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Heather Macbeth (Aug 01 2020 at 21:12):

Thanks!

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 01 2020 at 21:16):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Aug 01 2020 at 21:20):

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

view this post on Zulip Bryan Gin-ge Chen (Aug 01 2020 at 21:36):

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

view this post on Zulip Yury G. Kudryashov (Aug 01 2020 at 23:06):

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


Last updated: May 11 2021 at 00:31 UTC