theorem HomSheafCoherent.hom_module_finite_of_noetherian {R : Type u_1} [CommRing R] [IsNoetherianRing R] (M : Type u_2) (N : Type u_3) [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module.Finite R N] : Module.Finite R (M →ₗ[R] N)

Over a Noetherian ring, Hom_R(M, N) is a finitely generated R-module whenever both M and N are.

noncomputable def HomSheafCoherent.hom_localization_equiv {R : Type u_1} [CommRing R] (M : Type u_2) (N : Type u_3) [AddCommGroup M] [Module R M] [Module.FinitePresentation R M] [AddCommGroup N] [Module R N] (S : Submonoid R) : LocalizedModule S (M →ₗ[R] N) ≃ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S N

Localization commutes with Hom when M is finitely presented: the natural map S⁻¹ Hom(M, N) → Hom(S⁻¹ M, S⁻¹ N) is a linear equivalence.

noncomputable def HomSheafCoherent.hom_localization_equiv_noetherian {R : Type u_1} [CommRing R] [IsNoetherianRing R] (M : Type u_2) (N : Type u_3) [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup N] [Module R N] (S : Submonoid R) : LocalizedModule S (M →ₗ[R] N) ≃ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S N

Noetherian version of hom_localization_equiv: over a Noetherian ring, finitely generated implies finitely presented, so the Hom-localization equivalence holds.

theorem HomSheafCoherent.sheafHom_coherent_on_affine {R : Type u_1} [CommRing R] [IsNoetherianRing R] (M : Type u_2) (N : Type u_3) [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module.Finite R N] : Module.Finite R (M →ₗ[R] N) ∧ ∀ (S : Submonoid R), Nonempty (LocalizedModule S (M →ₗ[R] N) ≃ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S N)

Combined statement: on an affine Noetherian scheme, the sheaf Hom(F, G) of two coherent sheaves is again coherent — module-finiteness of Hom plus compatibility with localization.