some lemmas for linear equivs

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

universe u v w
variable (R : Type u) (M₁ : Type v) (M₂ : Type w) [CommRing R]
  [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂]
  (e₁₂ : M₁ ≃ₗ[R] M₂) (e₂₁ : M₂ ≃ₗ[R] M₁)

open LinearEquiv

theorem symm_eq_iff_trans_eq_refl : e₁₂.symm = e₂₁ ↔ e₂₁.trans e₁₂ = refl R M₂ :=
  ⟨(· ▸ by simp), fun h ↦ by ext x; simpa [LinearEquiv.symm_apply_eq] using congr($h.symm x)⟩

theorem symm_eq_iff_trans_eq_refl' : e₁₂.symm = e₂₁ ↔ e₁₂.trans e₂₁ = refl R M₁ :=
  ⟨(· ▸ by simp), fun h ↦ by rw [← trans_refl e₁₂.symm, ← h, ← trans_assoc, symm_trans_self, refl_trans]⟩

-- For comparison:
example (G : Type*) [Group G] (x y : G) : x⁻¹ = y ↔ y * x = 1 := by
  rw [inv_eq_iff_eq_inv, eq_comm, inv_eq_iff_mul_eq_one]

example (G : Type*) [Group G] (x y : G) : x⁻¹ = y ↔ x * y = 1 := inv_eq_iff_mul_eq_one

[Kenny Lau]

am I correct that these two lemmas about linear equivs are missing?

[Kenny Lau]

namely the symm_eq_iff_trans_eq_refl and symm_eq_iff_trans_eq_refl' above

[Kenny Lau]

I think it would also be useful to have LinearEquiv.eq_comp_symm f = g ∘ ⇑e₁₂.symm ↔ f ∘ ⇑e₁₂ = g but not coerced to functions

[Aaron Liu]

We already have one version for equivs which is docs#Equiv.symm_eq_iff_trans_eq_refl

[Aaron Liu]

so I think you should swap the primed and unprimed versions

[Kenny Lau]

What's more unfortunate in this situation is that LinearEquiv.coe_injective is stated using the wrong coe, CoeFun.coe should be replaced with DFunLike.coe

[Kenny Lau]

#27146

[Kenny Lau]

and when i try to use Equiv instead i discover that there is no toEquiv_trans lemma...

[Kenny Lau]

edit: looks like it might be smoother to coerce to LinearMap first

[Kenny Lau]

oh no, the other direction is simp instead, lol

[Kenny Lau]

@[simp]
theorem LinearEquiv.comp_coe :
↑f' ∘ₗ ↑f = ↑(f ≪≫ₗ f')

[Kenny Lau]

update: I think LinearMap is helpful for the x^-1 y = z iff y = xz, but not for the lemmas above

[Kenny Lau]

more update: maybe x^-1 y = z iff y = xz is all we need anyway since x^-1 = y by itself might not show up without being rfl..