Finite Laurent support of graded Hom spaces

Let P be a finitely generated graded module and M a finite-dimensional graded module over a graded algebra over a field. Only finitely many shifts M{j} receive a nonzero graded map from P, and each Hom space is finite-dimensional, so the Hom spaces Hom(P, M{j}) have finite Laurent support. A surjection from a finite graded free module ⨁ᵢ A{dᵢ} embeds Hom(P, M{j}) into ∏ᵢ M_{dᵢ-j}. No projectivity of P and no finite-dimensionality of the algebra are needed.

Main results

• The instance Module.Finite k (M ⟶ N): graded maps between finite-dimensional graded modules form a finite-dimensional space.
• TauCeti.GradedModuleCat.hasFiniteLaurentSupport_hom_shiftObj: graded maps from a finitely generated graded module into the shifts of a finite-dimensional one have finite Laurent support.
• TauCeti.GradedModuleCat.homShiftDirectSumEquiv: for a finitely generated graded source, the direct sum of the graded maps into all shifts is the space of ungraded module maps.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded free modules and degree shifts.

instance TauCeti.GradedModuleCat.instFiniteHomOfCarrier {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M N : GradedModuleCat 𝒜) [Module.Finite k M.carrier] [Module.Finite k N.carrier] : Module.Finite k (M ⟶ N)

Graded maps between finite-dimensional graded modules form a finite-dimensional space: forgetting the grading and the A-linearity embeds them in the k-linear maps.

Decomposition of an ungraded map into homogeneous parts

noncomputable def TauCeti.GradedModuleCat.homShiftDirectSumEquiv {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M N : GradedModuleCat 𝒜) [Module.Finite A M.carrier] : (DirectSum ℤ fun (j : ℤ) => M ⟶ N.shiftObj j) ≃ₗ[k] M.carrier →ₗ[A] N.carrier

An ungraded map out of a finitely generated graded module is the finite sum of its homogeneous parts. Equivalently, the direct sum of the graded morphism spaces M ⟶ N{j} over all internal shifts is linearly equivalent to the space of underlying module maps M →ₗ[A] N. No finiteness is needed on the target.

The shift convention means that a morphism to N{j} has underlying homogeneous degree -j.

@[simp]

theorem TauCeti.GradedModuleCat.homShiftDirectSumEquiv_of {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M N : GradedModuleCat 𝒜) [Module.Finite A M.carrier] (j : ℤ) (f : M ⟶ N.shiftObj j) : (M.homShiftDirectSumEquiv N) ((DirectSum.of (fun (j : ℤ) => M ⟶ N.shiftObj j) j) f) = f.hom

On a single homogeneous summand, homShiftDirectSumEquiv forgets the grading.

@[simp]

theorem TauCeti.GradedModuleCat.homShiftDirectSumEquiv_symm_apply_hom {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M N : GradedModuleCat 𝒜) [Module.Finite A M.carrier] (f : M.carrier →ₗ[A] N.carrier) (j : ℤ) : (((M.homShiftDirectSumEquiv N).symm f) j).hom = M.grading.homogeneousPartOfGradedSMul N.grading 𝒜 f (-j)

The j-th summand of homShiftDirectSumEquiv.symm f is the degree--j homogeneous part of the ungraded map f.

Finite Laurent support

theorem TauCeti.GradedModuleCat.hasFiniteLaurentSupport_hom_shiftObj {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (P M : GradedModuleCat 𝒜) [Module.Finite A P.carrier] [Module.Finite k M.carrier] : HasFiniteLaurentSupport k fun (j : ℤ) => P ⟶ M.shiftObj j

Graded maps into the shifts of a finite-dimensional graded module have finite Laurent support when the source is finitely generated. A surjection from a finite graded free module ⨁ᵢ A{dᵢ} embeds Hom(P, M{j}) into ∏ᵢ M_{dᵢ-j}, and M has only finitely many nonzero pieces.