Degree-zero graded Ext after forgetting the grading

For graded modules over a graded algebra with a finitely generated source, the direct sum over all internal degrees of degree-zero graded Ext is canonically the degree-zero Ext of the underlying ungraded modules. Degree-zero Ext is Hom on both sides, and an ungraded module map is the finite sum of its homogeneous parts.

Main results

• TauCeti.GradedModuleCat.gradedExtZeroForgetEquiv: the direct sum of degree-zero graded Ext groups is canonically equivalent to ungraded degree-zero Ext.
• TauCeti.GradedModuleCat.gradedExtZeroForgetEquiv_of: on a single internal degree, the equivalence forgets the grading of the corresponding graded map.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for homogeneous decomposition of maps between graded modules.

noncomputable def TauCeti.GradedModuleCat.gradedExtZeroForgetEquiv {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] (X Y : GradedModuleCat 𝒜) [Module.Finite A X.carrier] : (DirectSum ℤ fun (j : ℤ) => GradedExt (shift 𝒜) X Y 0 j) ≃ₗ[k] CategoryTheory.Abelian.Ext (toModuleCat.obj X) (toModuleCat.obj Y) 0

Degree-zero graded Ext assembles canonically into ungraded degree-zero Ext. The equivalence decomposes an ungraded module map into its finitely many homogeneous parts.

@[simp]

theorem TauCeti.GradedModuleCat.gradedExtZeroForgetEquiv_of {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] (X Y : GradedModuleCat 𝒜) [Module.Finite A X.carrier] (j : ℤ) (e : GradedExt (shift 𝒜) X Y 0 j) : (gradedExtZeroForgetEquiv 𝒜 X Y) ((DirectSum.of (GradedExt (shift 𝒜) X Y 0) j) e) = CategoryTheory.Abelian.Ext.linearEquiv₀.symm (ModuleCat.ofHom ((homShiftPowEquiv 𝒜 X Y j) (CategoryTheory.Abelian.Ext.linearEquiv₀ e)).hom)

On a single internal degree, gradedExtZeroForgetEquiv forgets the grading of the graded map represented by a degree-zero Ext class.