TensorInjectivity.lean

theorem sq {R : Type u} [CommRing R] {X Y X' Y' : Type u}
    [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y]
    [AddCommGroup X'] [Module R X'] [AddCommGroup Y'] [Module R Y']
    (a : X →ₗ[R] X') (b : Y →ₗ[R] Y') (t : X ⊗[R] Y) :
    b.lTensor X' (a.rTensor Y t) = a.rTensor Y' (b.lTensor X t)

theorem chase {R : Type u} [CommRing R] {N M P A K F : Type u}
    [AddCommGroup N] [Module R N] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P]
    [AddCommGroup A] [Module R A] [AddCommGroup K] [Module R K] [AddCommGroup F] [Module R F]
    (f : N →ₗ[R] M) (g : M →ₗ[R] P) (hf : Function.Injective f) (hfg : Function.Exact f g)
    (hg : Function.Surjective g) [Module.Flat R P]
    (ι : K →ₗ[R] F) (π : F →ₗ[R] A) (hι : Function.Injective ι) (hιπ : Function.Exact ι π)
    (hπ : Function.Surjective π) [Module.Flat R F] :
    Function.Injective (f.lTensor A)

theorem _root_.Module.Flat.lTensor_injective_of_exact_of_surjective_of_flat
    {R : Type u} [CommRing R] {N M P : Type u}
    [AddCommGroup N] [Module R N] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P]
    (f : N →ₗ[R] M) (g : M →ₗ[R] P) (hf : Function.Injective f) (hfg : Function.Exact f g)
    (hg : Function.Surjective g) [Module.Flat R P]
    (A : Type u) [AddCommGroup A] [Module R A] :
    Function.Injective (f.lTensor A)