The natural comparison of graded and ungraded Ext

Let A be a graded algebra over a field k and let U be the functor forgetting the grading of graded A-modules. Since U is exact and U(Y{j}) is the underlying module of Y, every class in Extⁿ(X, Y{j}) gives a class in Extⁿ(U X, U Y). Summing over the internal degrees gives a k-linear map

⨁ j, Extⁿ(X, Y{j}) → Extⁿ(U X, U Y),

TauCeti.GradedModuleCat.gradedExtForget. It is natural in both variables and commutes with the connecting maps of the long exact Ext sequences in both variables. In degree zero, when 𝒜 is a grading of A and X is finitely generated, it is the decomposition of an ungraded module map into its homogeneous parts, TauCeti.GradedModuleCat.gradedExtZeroForgetEquiv.

If A is left Noetherian and X is finitely generated, the map is bijective in every degree. The proof shifts dimension along a finite graded free presentation 0 → K → F → X → 0, whose kernel is again finitely generated, using the five lemma on the two contravariant long exact Ext sequences. The resulting isomorphisms make (U X, U Y) a comparison pair in the sense of TauCeti.IsGradedExtComparison. For such a pair that is moreover graded Euler-admissible (TauCeti.IsGradedEulerAdmissible), the q-Euler characteristic therefore specializes at q = 1 to the ordinary Ext-Euler characteristic.

Main definitions

• TauCeti.GradedModuleCat.gradedExtForgetComponent: the map Extⁿ(X, Y{j}) → Extⁿ(U X, U Y) in a single internal degree.
• TauCeti.GradedModuleCat.gradedExtForget: their sum over all internal degrees.
• TauCeti.GradedModuleCat.gradedExtForgetEquiv: the comparison as a linear equivalence, for a finitely generated source over a left Noetherian graded algebra.

Main results

• TauCeti.GradedModuleCat.gradedExtForgetComponent_extClass_comp and TauCeti.GradedModuleCat.gradedExtForgetComponent_comp_extClass: compatibility with the connecting maps in the source and in the target.
• TauCeti.GradedModuleCat.gradedExtForget_comp_lmap_precomp_mk₀, TauCeti.GradedModuleCat.gradedExtForget_comp_lmap_postcomp_mk₀, TauCeti.GradedModuleCat.gradedExtForget_comp_lmap_precomp_extClass and TauCeti.GradedModuleCat.gradedExtForget_comp_lmap_postcomp_extClass: the same naturality and connecting-map compatibilities for the whole direct-sum comparison.
• TauCeti.GradedModuleCat.gradedExtForget_zero: in degree zero the comparison is the homogeneous decomposition of module maps.
• TauCeti.GradedModuleCat.gradedExtForget_bijective: the comparison is bijective for a finitely generated source over a left Noetherian graded algebra.
• TauCeti.GradedModuleCat.isGradedExtComparison_toModuleCat: such a pair of graded modules is a graded Ext comparison pair with its underlying modules.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Lecture Notes in Mathematics 1836, Springer (2004), Section 2.4, for graded Hom and Ext of a finitely generated module over a Noetherian graded ring and their agreement with the ungraded groups.
• The dimension-shifting proof of TauCeti.GradedModuleCat.gradedExtForget_bijective follows Mathlib's CategoryTheory.Functor.mapExt_bijective_of_preservesProjectiveObjects (Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective), adapted from a single fully faithful functor to a direct sum over internal degrees, and from an arbitrary projective presentation to a finite graded free one so that the kernel stays finitely generated.

noncomputable def TauCeti.GradedModuleCat.gradedExtForgetComponent {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] (X Y : GradedModuleCat 𝒜) (n : ℕ) (j : ℤ) : GradedExt (shift 𝒜) X Y n j →ₗ[k] CategoryTheory.Abelian.Ext (toModuleCat.obj X) (toModuleCat.obj Y) n

The map from graded Ext in a single internal degree j to ungraded Ext: forget the grading of a class in Extⁿ(X, Y{j}) and identify the underlying module of Y{j} with that of Y.

theorem TauCeti.GradedModuleCat.gradedExtForgetComponent_apply {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] (X Y : GradedModuleCat 𝒜) (n : ℕ) (j : ℤ) (x : GradedExt (shift 𝒜) X Y n j) : (gradedExtForgetComponent 𝒜 X Y n j) x = (CategoryTheory.Abelian.Ext.mapExactFunctor toModuleCat x).comp (CategoryTheory.Abelian.Ext.mk₀ ((shiftPowCompToModuleCatIso 𝒜 j).hom.app Y)) ⋯

The value of gradedExtForgetComponent: apply the forgetful functor, then compose with the identification of U(Y{j}) with U Y.

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

The natural comparison of graded and ungraded Ext. The sum over all internal degrees j of the maps Extⁿ(X, Y{j}) → Extⁿ(X, Y) forgetting the grading.

@[simp]

theorem TauCeti.GradedModuleCat.gradedExtForget_of {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] (X Y : GradedModuleCat 𝒜) (n : ℕ) (j : ℤ) (x : GradedExt (shift 𝒜) X Y n j) : (gradedExtForget 𝒜 X Y n) ((DirectSum.of (GradedExt (shift 𝒜) X Y n) j) x) = (CategoryTheory.Abelian.Ext.mapExactFunctor toModuleCat x).comp (CategoryTheory.Abelian.Ext.mk₀ ((shiftPowCompToModuleCatIso 𝒜 j).hom.app Y)) ⋯

On a single internal degree, gradedExtForget is gradedExtForgetComponent.

Naturality and connecting maps

theorem TauCeti.GradedModuleCat.gradedExtForgetComponent_mk₀_comp {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] {X' X Y : GradedModuleCat 𝒜} (f : X' ⟶ X) {n : ℕ} {j : ℤ} (x : GradedExt (shift 𝒜) X Y n j) : (gradedExtForgetComponent 𝒜 X' Y n j) ((CategoryTheory.Abelian.Ext.mk₀ f).comp x ⋯) = (CategoryTheory.Abelian.Ext.mk₀ (toModuleCat.map f)).comp ((gradedExtForgetComponent 𝒜 X Y n j) x) ⋯

The comparison is natural in the source.

theorem TauCeti.GradedModuleCat.gradedExtForgetComponent_comp_mk₀ {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] {X Y Y' : GradedModuleCat 𝒜} (g : Y ⟶ Y') {n : ℕ} {j : ℤ} (x : GradedExt (shift 𝒜) X Y n j) : (gradedExtForgetComponent 𝒜 X Y' n j) (CategoryTheory.Abelian.Ext.comp x (CategoryTheory.Abelian.Ext.mk₀ ((shift 𝒜 ^ j).functor.map g)) ⋯) = ((gradedExtForgetComponent 𝒜 X Y n j) x).comp (CategoryTheory.Abelian.Ext.mk₀ (toModuleCat.map g)) ⋯

The comparison is natural in the target.

theorem TauCeti.GradedModuleCat.gradedExtForgetComponent_extClass_comp {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] {S : CategoryTheory.ShortComplex (GradedModuleCat 𝒜)} (hS : S.ShortExact) (Y : GradedModuleCat 𝒜) {n m : ℕ} (h : 1 + n = m) {j : ℤ} (x : GradedExt (shift 𝒜) S.X₁ Y n j) : (gradedExtForgetComponent 𝒜 S.X₃ Y m j) (hS.extClass.comp x h) = ⋯.extClass.comp ((gradedExtForgetComponent 𝒜 S.X₁ Y n j) x) h

The comparison commutes with the connecting maps in the source. For a short exact sequence 0 → S₁ → S₂ → S₃ → 0 of graded modules, the connecting map Extⁿ(S₁, Y{j}) → Extⁿ⁺¹(S₃, Y{j}) corresponds to the connecting map of the underlying short exact sequence of modules.

theorem TauCeti.GradedModuleCat.gradedExtForgetComponent_comp_extClass {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] {S : CategoryTheory.ShortComplex (GradedModuleCat 𝒜)} (hS : S.ShortExact) (X : GradedModuleCat 𝒜) {n m : ℕ} (h : n + 1 = m) {j : ℤ} (x : GradedExt (shift 𝒜) X S.X₃ n j) : (gradedExtForgetComponent 𝒜 X S.X₁ m j) (CategoryTheory.Abelian.Ext.comp x ⋯.extClass h) = ((gradedExtForgetComponent 𝒜 X S.X₃ n j) x).comp ⋯.extClass h

The comparison commutes with the connecting maps in the target. For a short exact sequence 0 → S₁ → S₂ → S₃ → 0 of graded modules, the connecting map Extⁿ(X, S₃{j}) → Extⁿ⁺¹(X, S₁{j}) of the shifted sequence corresponds to the connecting map of the underlying short exact sequence of modules.

Bijectivity

theorem TauCeti.GradedModuleCat.gradedExtForget_zero {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] (X Y : GradedModuleCat 𝒜) [GradedAlgebra 𝒜] [Module.Finite A X.carrier] : gradedExtForget 𝒜 X Y 0 = ↑(gradedExtZeroForgetEquiv 𝒜 X Y)

In cohomological degree zero the comparison is the homogeneous decomposition of ungraded module maps.

theorem TauCeti.GradedModuleCat.gradedExtForget_comp_lmap_precomp_mk₀ {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] {X' X Y : GradedModuleCat 𝒜} (f : X' ⟶ X) (n : ℕ) : (gradedExtForget 𝒜 X' Y n ∘ₗ DirectSum.lmap fun (j : ℤ) => (CategoryTheory.Abelian.Ext.mk₀ f).precompOfLinear k ((shift 𝒜 ^ j).functor.obj Y) ⋯) = (CategoryTheory.Abelian.Ext.mk₀ (toModuleCat.map f)).precompOfLinear k (toModuleCat.obj Y) ⋯ ∘ₗ gradedExtForget 𝒜 X Y n

The comparison commutes with precomposition by a graded map, on the whole direct sum.

theorem TauCeti.GradedModuleCat.gradedExtForget_comp_lmap_postcomp_mk₀ {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] {X Y Y' : GradedModuleCat 𝒜} (g : Y ⟶ Y') (n : ℕ) : (gradedExtForget 𝒜 X Y' n ∘ₗ DirectSum.lmap fun (j : ℤ) => (CategoryTheory.Abelian.Ext.mk₀ ((shift 𝒜 ^ j).functor.map g)).postcompOfLinear k X ⋯) = (CategoryTheory.Abelian.Ext.mk₀ (toModuleCat.map g)).postcompOfLinear k (toModuleCat.obj X) ⋯ ∘ₗ gradedExtForget 𝒜 X Y n

The comparison commutes with postcomposition by a graded map, on the whole direct sum.

theorem TauCeti.GradedModuleCat.gradedExtForget_comp_lmap_precomp_extClass {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] {S : CategoryTheory.ShortComplex (GradedModuleCat 𝒜)} (hS : S.ShortExact) (Y : GradedModuleCat 𝒜) (n : ℕ) : (gradedExtForget 𝒜 S.X₃ Y (n + 1) ∘ₗ DirectSum.lmap fun (j : ℤ) => hS.extClass.precompOfLinear k ((shift 𝒜 ^ j).functor.obj Y) ⋯) = ⋯.extClass.precompOfLinear k (toModuleCat.obj Y) ⋯ ∘ₗ gradedExtForget 𝒜 S.X₁ Y n

The comparison commutes with the connecting maps in the source, on the whole direct sum.

theorem TauCeti.GradedModuleCat.gradedExtForget_comp_lmap_postcomp_extClass {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] {S : CategoryTheory.ShortComplex (GradedModuleCat 𝒜)} (hS : S.ShortExact) (X : GradedModuleCat 𝒜) (n : ℕ) : (gradedExtForget 𝒜 X S.X₁ (n + 1) ∘ₗ DirectSum.lmap fun (j : ℤ) => ⋯.extClass.postcompOfLinear k X ⋯) = ⋯.extClass.postcompOfLinear k (toModuleCat.obj X) ⋯ ∘ₗ gradedExtForget 𝒜 X S.X₃ n

The comparison commutes with the connecting maps in the target, on the whole direct sum.

theorem TauCeti.GradedModuleCat.gradedExtForget_bijective {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] [GradedAlgebra 𝒜] [IsNoetherianRing A] (X Y : GradedModuleCat 𝒜) [Module.Finite A X.carrier] (n : ℕ) : Function.Bijective ⇑(gradedExtForget 𝒜 X Y n)

Graded and ungraded Ext agree after summing over internal degrees. Over a left Noetherian graded algebra, for a finitely generated graded module X and any graded module Y, the comparison ⨁ⱼ Extⁿ(X, Y{j}) → Extⁿ(X, Y) forgetting the grading is bijective in every cohomological degree.

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

The natural comparison of graded and ungraded Ext, as a linear equivalence: over a left Noetherian graded algebra, for a finitely generated graded module X, the direct sum over all internal degrees of Extⁿ(X, Y{j}) is Extⁿ(X, Y) of the underlying modules.

@[simp]

theorem TauCeti.GradedModuleCat.gradedExtForgetEquiv_apply {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] [GradedAlgebra 𝒜] [IsNoetherianRing A] (X Y : GradedModuleCat 𝒜) [Module.Finite A X.carrier] (n : ℕ) (x : DirectSum ℤ fun (j : ℤ) => GradedExt (shift 𝒜) X Y n j) : (X.gradedExtForgetEquiv Y n) x = (gradedExtForget 𝒜 X Y n) x

theorem TauCeti.GradedModuleCat.isGradedExtComparison_toModuleCat {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [CategoryTheory.HasExt (ModuleCat A)] [GradedAlgebra 𝒜] [IsNoetherianRing A] (X Y : GradedModuleCat 𝒜) [Module.Finite A X.carrier] : IsGradedExtComparison k (shift 𝒜) X Y (toModuleCat.obj X) (toModuleCat.obj Y)

Over a left Noetherian graded algebra, a finitely generated graded module and any graded module form a graded Ext comparison pair with their underlying modules.