ext for linear maps from a tensor product

Stream: Is there code for X?

[Kevin Buzzard]

Could ext be made to reduce this goal to "for all m and n, f(m \otimes_t n) = m \otimes_t n"?

import tactic
import linear_algebra.tensor_algebra.basic

open_locale tensor_product

example (R M N : Type) [comm_ring R] [add_comm_group M] [add_comm_group N]
  [module R M] [module R N] (f : M ⊗[R] N →ₗ[R] M ⊗[R] N) : ∀ x, f x = x :=
begin
  ext, -- no applicable extensionality rule found for tensor_product
end

[Kevin Buzzard]

Should this be a thing?

import tactic
import linear_algebra.tensor_algebra.basic

open_locale tensor_product

@[ext] def foo (R M N P : Type*) [comm_ring R] [add_comm_group M] [add_comm_group N]
  [add_comm_group P] [module R M] [module R N] [module R P] (f g : M ⊗[R] N →ₗ[R] P)
  (h : ∀ m n, f (m ⊗ₜ n) = g (m ⊗ₜ n)) : f = g :=
begin
  suffices : ⊤ ≤ linear_map.ker (f - g),
  { ext x,
    exact sub_eq_zero.1 (this submodule.mem_top), }, -- i ♥ defeq
  rw [← tensor_product.span_tmul_eq_top R M N, submodule.span_le],
  rintro - ⟨m, n, rfl⟩,
  exact sub_eq_zero.2 (h m n),
end

-- my use case
example (R M N : Type) [comm_ring R] [add_comm_group M] [add_comm_group N]
  [module R M] [module R N] (f g : M ⊗[R] N →ₗ[R] M ⊗[R] N)
  (h : ∀ m n, f (m ⊗ₜ n) = m ⊗ₜ n) : ∀ x, f x = x :=
begin
  suffices : f = linear_map.id,
  { simp [this] },
  ext,
  exact h m n,
end

[Kevin Buzzard]

I almost felt dirty writing that first proof; I abuse defeq, making the proof unreadable to a beginner. Am I a bad person?

[Eric Rodriguez]

docs#tensor_product.ext, docs#tensor_product.ext'? The first one seems to have a discussion on why the ext isn't on (although I don't know what compr2 does - I assume it's equivalent to what's written), and the primed is the version you have here

[Kevin Buzzard]

Oh I see, so I'm just supposed to apply them manually? I'll take the experts' word for it :-)

[Antoine Labelle]

I think it's usually added as a local attribute in files where it is important

[Eric Wieser]

The compr₂ version means that it chains for nested tensor products