Hom Localized equiv Localized Hom

Stream: Is there code for X?

[syur2]

First, I need the left/right exact sequence.Second, the Hom functor is left exact.

[syur2]

More easily, the Hom functor map surjective to injective.

lemma Hom_inj_of_surj (f : N →ₗ[R] P) (hf : Function.Surjective f) : Function.Injective (LinearMap.lcomp R M f) := sorry

[syur2]

import Mathlib

variable {R M N P: Type*} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [AddCommGroup P] [Module R P]

[syur2]

Also, though no need for my code, the TensorProduct functor is right exact.

[Aaron Liu]

import Mathlib.LinearAlgebra.BilinearMap

variable {R M N P : Type*} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [AddCommMonoid P] [Module R P]
lemma Function.Surjective.injective_lcomp_right {f : N →ₗ[R] P} (hf : Function.Surjective f) : Function.Injective (LinearMap.lcomp R M f) := by
  intro a b hab
  rw [← DFunLike.coe_fn_eq] at hab ⊢
  apply hf.injective_comp_right
  simpa [LinearMap.lcomp_apply'] using hab

[syur2]

So there is no these theorem, especially the "Hom_inj_of_surj" in Mathlib?

[Aaron Liu]

This is not in mathlib yet.

[Junyan Xu]

LinearMap.dualMap_injective_of_surjective is a special case of this.