Quotients concentrated in one internal degree

The degree quotient of a graded module kills the submodule generated by all pieces outside a specified degree. It is the universal quotient concentrated in that degree. For a nonnegatively graded algebra, it is annihilated by positive-degree scalars, and its surviving piece detects the corresponding piece of the module modulo the positive-degree action.

Consequently, maps to modules concentrated in degree p detect whether the source's degree-p piece lies in A₊ M. Combined with graded Nakayama, this detects generating degrees of minimal projective resolution terms from their graded Hom groups.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3.
• A. Beilinson, V. Ginzburg and W. Soergel, Koszul duality patterns in representation theory, Section 1.2, for detection of generating degrees in minimal resolutions.

def TauCeti.GradedModuleCat.offDegreeSpan {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) (p : ℤ) : Submodule A M.carrier

The submodule generated by all homogeneous pieces outside degree p.

theorem TauCeti.GradedModuleCat.offDegreeSpan_le_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) (p : ℤ) (U : Submodule A M.carrier) : M.offDegreeSpan p ≤ U ↔ ∀ (q : ℤ), q ≠ p → M.grading.piece ℤ q ≤ Submodule.restrictScalars k U

The off-degree span is contained in a submodule exactly when every off-degree piece is.

theorem TauCeti.GradedModuleCat.piece_le_offDegreeSpan {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) {p q : ℤ} (hq : q ≠ p) : M.grading.piece ℤ q ≤ Submodule.restrictScalars k (M.offDegreeSpan p)

A piece outside degree p lies in the submodule killed by the degree quotient.

theorem TauCeti.GradedModuleCat.isHomogeneous_offDegreeSpan {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p : ℤ) : DirectSum.SetLike.IsHomogeneous (M.grading.piece ℤ) (M.offDegreeSpan p)

The submodule generated by the off-degree pieces is homogeneous.

@[reducible, inline]

noncomputable abbrev TauCeti.GradedModuleCat.offDegreeObj {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p : ℤ) : GradedModuleCat 𝒜

The homogeneous submodule generated by the off-degree pieces, as a graded module.

theorem TauCeti.GradedModuleCat.mem_offDegreeObj_piece_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p q : ℤ) (x : (M.offDegreeObj p).carrier) : x ∈ (M.offDegreeObj p).grading.piece ℤ q ↔ ↑x ∈ M.grading.piece ℤ q

Membership in a homogeneous piece of the off-degree submodule is ambient membership.

noncomputable def TauCeti.GradedModuleCat.offDegreeι {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p : ℤ) : M.offDegreeObj p ⟶ M

The inclusion of the submodule killed by the degree quotient.

@[simp]

theorem TauCeti.GradedModuleCat.hom_offDegreeι {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p : ℤ) : (M.offDegreeι p).hom = (M.offDegreeSpan p).subtype

The off-degree inclusion has the underlying submodule inclusion as its linear map.

@[reducible, inline]

noncomputable abbrev TauCeti.GradedModuleCat.degreeQuotient {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p : ℤ) : GradedModuleCat 𝒜

The universal quotient of M concentrated in internal degree p.

noncomputable def TauCeti.GradedModuleCat.degreeQuotientπ {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p : ℤ) : M ⟶ M.degreeQuotient p

The projection onto the universal quotient concentrated in degree p.

theorem TauCeti.GradedModuleCat.hom_degreeQuotientπ {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p : ℤ) : (M.degreeQuotientπ p).hom = (M.offDegreeι p).hom.range.mkQ

The underlying quotient projection is the usual projection by the inclusion's range.

@[simp]

theorem TauCeti.GradedModuleCat.degreeQuotientπ_eq_zero_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p : ℤ) (x : M.carrier) : (M.degreeQuotientπ p).hom x = 0 ↔ x ∈ M.offDegreeSpan p

The kernel of the degree quotient projection is the span of the off-degree pieces.

theorem TauCeti.GradedModuleCat.degreeQuotientπ_surjective {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p : ℤ) : Function.Surjective ⇑(M.degreeQuotientπ p).hom

The quotient projection is surjective.

theorem TauCeti.GradedModuleCat.mem_degreeQuotient_piece_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) (p q : ℤ) (y : (M.degreeQuotient p).carrier) : y ∈ (M.degreeQuotient p).grading.piece ℤ q ↔ ∃ x ∈ M.grading.piece ℤ q, (M.degreeQuotientπ p).hom x = y

The degree-q piece of the degree quotient consists of classes of degree-q elements.

@[simp]

theorem TauCeti.GradedModuleCat.degreeQuotient_piece_eq_bot {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (M : GradedModuleCat 𝒜) {p q : ℤ} (hq : q ≠ p) : (M.degreeQuotient p).grading.piece ℤ q = ⊥

The degree quotient vanishes outside its specified degree.

theorem TauCeti.GradedModuleCat.offDegreeSpan_le_ker {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (p : ℤ) (hN : ∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) (f : M ⟶ N) : M.offDegreeSpan p ≤ f.hom.ker

A graded map to a module concentrated in degree p kills the off-degree span.

noncomputable def TauCeti.GradedModuleCat.degreeQuotientLift {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {M N : GradedModuleCat 𝒜} (p : ℤ) (hN : ∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) (f : M ⟶ N) : M.degreeQuotient p ⟶ N

The canonical factorization of a graded map to a module concentrated in degree p through the universal degree quotient.

@[simp]

theorem TauCeti.GradedModuleCat.degreeQuotientπ_degreeQuotientLift {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {M N : GradedModuleCat 𝒜} (p : ℤ) (hN : ∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (M.degreeQuotientπ p) (degreeQuotientLift p hN f) = f

Composing the canonical lift with the quotient projection recovers the original map.

@[simp]

theorem TauCeti.GradedModuleCat.degreeQuotientπ_degreeQuotientLift_assoc {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {M N : GradedModuleCat 𝒜} (p : ℤ) (hN : ∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) (f : M ⟶ N) {Z : GradedModuleCat 𝒜} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.degreeQuotientπ p) (CategoryTheory.CategoryStruct.comp (degreeQuotientLift p hN f) h) = CategoryTheory.CategoryStruct.comp f h

Composing the canonical lift with the quotient projection recovers the original map.

theorem TauCeti.GradedModuleCat.degreeQuotientLift_unique {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {M N : GradedModuleCat 𝒜} (p : ℤ) (hN : ∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) (f : M ⟶ N) (g : M.degreeQuotient p ⟶ N) (hg : CategoryTheory.CategoryStruct.comp (M.degreeQuotientπ p) g = f) : g = degreeQuotientLift p hN f

A map out of the degree quotient is uniquely determined by its composite with the quotient projection.

theorem TauCeti.GradedModuleCat.existsUnique_degreeQuotient_lift {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {M N : GradedModuleCat 𝒜} (p : ℤ) (hN : ∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) (f : M ⟶ N) : ∃! g : M.degreeQuotient p ⟶ N, CategoryTheory.CategoryStruct.comp (M.degreeQuotientπ p) g = f

Every graded map to a module concentrated in degree p factors uniquely through the universal degree quotient.

theorem TauCeti.GradedModuleCat.piece_inf_offDegreeSpan_le_positive_smul_top {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ i < 0, 𝒜 i = ⊥) (M : GradedModuleCat 𝒜) (p : ℤ) : M.grading.piece ℤ p ⊓ Submodule.restrictScalars k (M.offDegreeSpan p) ≤ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤

In the retained degree, the off-degree span contributes only positive-degree action.

theorem TauCeti.GradedModuleCat.piece_le_positive_smul_top_of_subsingleton_hom {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] (hneg : ∀ i < 0, 𝒜 i = ⊥) (M : GradedModuleCat 𝒜) (p : ℤ) (h : Subsingleton (M ⟶ M.degreeQuotient p)) : M.grading.piece ℤ p ≤ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤

Vanishing of maps to the universal degree quotient detects a homogeneous piece modulo positive-degree action.