injectivity of linear maps

Stream: mathlib4

[Kevin Buzzard]

In the theory of flatness one is sometimes interested in whether certain linear maps are injective (indeed one definition of flatness for an R-module M is "if a linear map f : X -> Y is injective then f tensor id_M is also injective").

Another way of saying that a linear map is injective is "ker = bot". But using ker = bot everywhere would be a deviation from the literature. However it might make things
easier in the below.

I have a bilinear map f : M →ₗ[R] N →ₗ[R] P which lifts to lift f : M ⊗[R] N →ₗ[R] P.
I have another module M' isomorphic to M with e : M' ≃ₗ[R] M. I'd like to prove the the mathematical triviality that lift f is injective iff lift (f ∘ₗ e) is injective (proof: it's the same picture).

Writing down a proof more carefully, the map lift (f ∘ₗ e) from $M'\otimes N$ to $P$ is just the composite of lift f and $i:M'\otimes N\cong M\otimes N$ coming from $e\otimes id_N$, and because $i$ is an isomorphism it's bijective, so one map is injective iff the other is.

Writing this down in Lean was more annoying than expected, because Function.Injective coerces a linear map / linear equiv to a function, and I had to use a possibly missing norm_cast lemma to do it. Should those four norm_cast lemmas be in mathlib?

import Mathlib.LinearAlgebra.TensorProduct.Tower

variable (R : Type*) [CommRing R]
  variable (M : Type*) [AddCommGroup M] [Module R M]
  variable (M' : Type*) [AddCommGroup M'] [Module R M']
  variable (N : Type*) [AddCommGroup N] [Module R N]
  variable (P : Type*) [AddCommGroup P] [Module R P]

variable (f : M →ₗ[R] N →ₗ[R] P)
variable (e : M' ≃ₗ[R] M)

-- If `M` and `M'` are isomorphic via `e`, and `f : M →ₗ[R] N →ₗ[R] P` is a bilinear map,
-- then `lift f : M ⊗ N → P` is injective iff the corresponding map `lift (f ∘ e) : M' ⊗ N → P`
-- is injective

open scoped TensorProduct

-- Should this be a thing? (and three more such lemmas, because f and g can be linear maps
-- or linear equivs, and the coercions to functions are all syntactically different)
@[norm_cast]
lemma foobar' (f : M ≃ₗ[R] N) (g : N →ₗ[R] P) : (g ∘ₗ f : M → P) = (g : N → P) ∘ (f : M → N) := rfl

example : Function.Injective (TensorProduct.lift f) ↔
    Function.Injective (TensorProduct.lift (f ∘ₗ e : M' →ₗ[R] N →ₗ[R] P)) := by
  -- rw theorem saying Function.Injective (f ∘ g) ↔ Function.Injective f if g is bijective
  rw [← Function.Injective.of_comp_iff' _ (LinearEquiv.rTensor _ e).bijective]
  -- the next line works because of foobar'
  norm_cast
  -- goal now `Function.Injective (⇑f) ↔ Function.Injective (⇑g)` for `f` and `g` linear maps
  congr!
  -- goal now f = g, an equality of linear maps out of a tensor product so the good ext lemma works
  ext
  rfl

[Andrew Yang]

I would rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp] in this case, but I guess we should try to make automation work too?