Graded modules generated in one degree

An internally graded module is generated in degree d when its degree-d homogeneous piece generates the underlying module. This is the module-theoretic condition imposed on the ith projective in a linear resolution: after choosing the degree of the resolved module, its ith projective is generated in the correspondingly shifted degree.

The definition is phrased using Submodule.span, so it does not depend on a choice of homogeneous generators. The results below give the API needed to use it without unfolding: generation is invariant under transport by a linear equivalence, its degree changes predictably when the grading is shifted, and linear maps out of the module are determined by the indicated homogeneous piece.

Main definitions

• TauCeti.InternalGrading.IsGeneratedInDegree: the degree-d piece spans the whole module.

Main results

• TauCeti.InternalGrading.isGeneratedInDegree_map_iff: generation in a degree is invariant under transport of the grading along a linear equivalence.
• TauCeti.InternalGrading.isGeneratedInDegree_shift_iff: shifting an internal grading reindexes the generating degree.
• TauCeti.InternalGrading.isGeneratedInDegree_directSum_iff: a direct sum is generated in one degree exactly when every summand is generated in that degree.
• TauCeti.InternalGrading.linearMap_ext_of_isGeneratedInDegree: two linear maps out of a module generated in degree d agree when they agree on its degree-d piece.
• TauCeti.InternalGrading.IsGeneratedInDegree.piece_add_eq_smul: over a graded algebra 𝒜, a graded module generated in degree d has degree-m + d piece 𝒜 m • M_d.
• TauCeti.InternalGrading.IsGeneratedInDegree.piece_eq_bot_of_lt: over a nonnegatively graded algebra, a graded module generated in degree d vanishes in every degree below d.
• TauCeti.InternalGrading.IsGeneratedInDegree.piece_le_smul_top: a graded module generated in degree d has all of its pieces of degree above d inside A₊ M, where A₊ is the sum of the pieces of positive degree.
• TauCeti.InternalGrading.apply_mem_smul_top_of_isGeneratedInDegree: over a nonnegatively graded algebra, a degree-zero map from a module generated in degree d' to a module generated in a lower degree lands in A₊ M.

References

• S. Priddy, "Koszul resolutions", Transactions of the American Mathematical Society 152 (1970), 39--60, for linear resolutions of graded modules.
• Z. Dancso and A. Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Section 2.2, for the graded-module conventions used by the downstream Grothendieck-group constructions.

def TauCeti.InternalGrading.IsGeneratedInDegree {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (A : Type u') [Semiring A] [Module A M] (d : ℤ) : Prop

An internally graded module is generated in degree d if the A-span of its degree-d homogeneous piece is the whole module. The grading pieces are R-submodules, while A is the scalar semiring whose span measures generation (typically the graded algebra acting on the module).

Equations

• G.IsGeneratedInDegree A d = (Submodule.span A ↑(G.piece d) = ⊤)

theorem TauCeti.InternalGrading.isGeneratedInDegree_iff {R : Type u} {A : Type u'} {M : Type v} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] (G : InternalGrading R M) (d : ℤ) : G.IsGeneratedInDegree A d ↔ ∀ (x : M), x ∈ Submodule.span A ↑(G.piece d)

Generation in degree d, restated as membership of every element in the span of the degree-d piece.

theorem TauCeti.InternalGrading.isGeneratedInDegree_of_piece_eq_top {R : Type u} {A : Type u'} {M : Type v} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] (G : InternalGrading R M) (d : ℤ) (h : G.piece d = ⊤) : G.IsGeneratedInDegree A d

If the degree-d piece is the whole module, then the module is generated in degree d.

theorem TauCeti.InternalGrading.IsGeneratedInDegree.mono {R : Type u} {A : Type u'} {M : Type v} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] {G H : InternalGrading R M} {d e : ℤ} (hG : G.IsGeneratedInDegree A d) (h : G.piece d ≤ H.piece e) : H.IsGeneratedInDegree A e

Enlarging the proposed homogeneous generating piece preserves generation.

@[simp]

theorem TauCeti.InternalGrading.isGeneratedInDegree_map_iff {A : Type u'} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] {N : Type w} [AddCommMonoid N] [Module A N] {k : Type u} [CommSemiring k] [Algebra k A] [Module k M] [IsScalarTower k A M] [Module k N] [IsScalarTower k A N] (G : InternalGrading k M) (e : M ≃ₗ[A] N) (d : ℤ) : (G.map (LinearEquiv.restrictScalars k e)).IsGeneratedInDegree A d ↔ G.IsGeneratedInDegree A d

Transporting an internal grading along a linear equivalence preserves generation in every degree.

@[simp]

theorem TauCeti.InternalGrading.isGeneratedInDegree_shift_iff {R : Type u} {A : Type u'} {M : Type v} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] (G : InternalGrading R M) (c d : ℤ) : (G.shift c).IsGeneratedInDegree A d ↔ G.IsGeneratedInDegree A (d + c)

A shift by c reindexes generation in degree d as generation in degree d + c for the original grading.

theorem TauCeti.InternalGrading.linearMap_eq_iff_of_isGeneratedInDegree {R : Type u} {A : Type u'} {M : Type v} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] {N : Type w} [AddCommMonoid N] [Module A N] (G : InternalGrading R M) {d : ℤ} (hG : G.IsGeneratedInDegree A d) (f g : M →ₗ[A] N) : f = g ↔ ∀ (x : ↥(G.piece d)), f ↑x = g ↑x

Two linear maps out of a module generated in degree d are equal exactly when they agree on homogeneous elements of degree d.

theorem TauCeti.InternalGrading.linearMap_ext_of_isGeneratedInDegree {R : Type u} {A : Type u'} {M : Type v} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] {N : Type w} [AddCommMonoid N] [Module A N] (G : InternalGrading R M) {d : ℤ} (hG : G.IsGeneratedInDegree A d) {f g : M →ₗ[A] N} (h : ∀ (x : ↥(G.piece d)), f ↑x = g ↑x) : f = g

Two linear maps out of a module generated in degree d agree everywhere if they agree on homogeneous elements of degree d.

theorem TauCeti.InternalGrading.linearMap_eq_zero_iff_of_isGeneratedInDegree {R : Type u} {A : Type u'} {M : Type v} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] {N : Type w} [AddCommMonoid N] [Module A N] (G : InternalGrading R M) {d : ℤ} (hG : G.IsGeneratedInDegree A d) (f : M →ₗ[A] N) : f = 0 ↔ ∀ (x : ↥(G.piece d)), f ↑x = 0

A linear map out of a module generated in degree d vanishes exactly when it vanishes on homogeneous elements of degree d.

theorem TauCeti.InternalGrading.linearMap_eq_zero_of_isGeneratedInDegree {R : Type u} {A : Type u'} {M : Type v} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] {N : Type w} [AddCommMonoid N] [Module A N] (G : InternalGrading R M) {d δ : ℤ} (hG : G.IsGeneratedInDegree A d) [Module R N] {H : InternalGrading R N} {f : M →ₗ[A] N} (hf : LinearMap.IsHomogeneous f G.piece H.piece δ) (hH : H.piece (d + δ) = ⊥) : f = 0

A homogeneous map from a module generated in degree d vanishes when the target piece in degree d + δ vanishes.

theorem TauCeti.InternalGrading.isGeneratedInDegree_directSum {R : Type u} {A : Type u'} [Semiring R] [Semiring A] {ι : Type u_1} {M : ι → Type v} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module A (M i)] (G : (i : ι) → InternalGrading R (M i)) (d : ℤ) (hG : ∀ (i : ι), (G i).IsGeneratedInDegree A d) : (directSum G).IsGeneratedInDegree A d

An external direct sum is generated in degree d if every summand is generated in degree d.

theorem TauCeti.InternalGrading.IsGeneratedInDegree.of_directSum {R : Type u} {A : Type u'} [Semiring R] [Semiring A] {ι : Type u_1} {M : ι → Type v} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module A (M i)] (G : (i : ι) → InternalGrading R (M i)) (d : ℤ) (hG : (directSum G).IsGeneratedInDegree A d) (i : ι) : (G i).IsGeneratedInDegree A d

If an external direct sum is generated in degree d, then every summand is generated in degree d.

@[simp]

theorem TauCeti.InternalGrading.isGeneratedInDegree_directSum_iff {R : Type u} {A : Type u'} [Semiring R] [Semiring A] {ι : Type u_1} {M : ι → Type v} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Module A (M i)] (G : (i : ι) → InternalGrading R (M i)) (d : ℤ) : (directSum G).IsGeneratedInDegree A d ↔ ∀ (i : ι), (G i).IsGeneratedInDegree A d

An external direct sum is generated in degree d exactly when every summand is generated in degree d.

Generation over a graded algebra

theorem TauCeti.InternalGrading.isHomogeneous_span_piece {k : Type u} {A : Type u'} {M : Type v} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid M] [Module k M] [Module A M] (𝒜 : ℤ → Submodule k A) [GradedAlgebra 𝒜] {G : InternalGrading k M} [SetLike.GradedSMul 𝒜 G.piece] (d : ℤ) : DirectSum.SetLike.IsHomogeneous G.piece (Submodule.span A ↑(G.piece d))

The span of a homogeneous piece is a homogeneous submodule over a graded algebra.

theorem TauCeti.InternalGrading.IsGeneratedInDegree.piece_add_eq_smul {k : Type u} {A : Type u'} {M : Type v} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (𝒜 : ℤ → Submodule k A) [GradedAlgebra 𝒜] {G : InternalGrading k M} [SetLike.GradedSMul 𝒜 G.piece] {d : ℤ} (hG : G.IsGeneratedInDegree A d) (m : ℤ) : G.piece (m + d) = 𝒜 m • G.piece d

Over a graded algebra 𝒜, a graded module generated in degree d has degree-m + d piece 𝒜 m • M_d: its homogeneous elements of degree m + d are exactly the sums of products of degree-m elements of the algebra with degree-d elements of the module.

theorem TauCeti.InternalGrading.IsGeneratedInDegree.piece_eq_bot_of_lt {k : Type u} {A : Type u'} {M : Type v} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (𝒜 : ℤ → Submodule k A) [GradedAlgebra 𝒜] {G : InternalGrading k M} [SetLike.GradedSMul 𝒜 G.piece] {d : ℤ} (h𝒜 : ∀ i < 0, 𝒜 i = ⊥) (hG : G.IsGeneratedInDegree A d) {p : ℤ} (hp : p < d) : G.piece p = ⊥

Over a nonnegatively graded algebra, a graded module generated in degree d has no nonzero homogeneous elements of degree below d.

theorem TauCeti.InternalGrading.IsGeneratedInDegree.piece_le_smul_top {k : Type u} {A : Type u'} {M : Type v} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (𝒜 : ℤ → Submodule k A) [GradedAlgebra 𝒜] {G : InternalGrading k M} [SetLike.GradedSMul 𝒜 G.piece] {d : ℤ} (hG : G.IsGeneratedInDegree A d) {p : ℤ} (hp : d < p) : G.piece p ≤ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤

A graded module generated in degree d has every homogeneous piece of degree above d inside A₊ M, the products of elements of positive degree with elements of the module.

theorem TauCeti.InternalGrading.apply_mem_smul_top_of_isGeneratedInDegree {k : Type u} {A : Type u'} {M : Type v} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (𝒜 : ℤ → Submodule k A) [GradedAlgebra 𝒜] {G : InternalGrading k M} [SetLike.GradedSMul 𝒜 G.piece] {d : ℤ} (h𝒜 : ∀ i < 0, 𝒜 i = ⊥) {M' : Type w} [AddCommMonoid M'] [Module k M'] [Module A M'] [IsScalarTower k A M'] {G' : InternalGrading k M'} [SetLike.GradedSMul 𝒜 G'.piece] {d' : ℤ} (hG' : G'.IsGeneratedInDegree A d') (hG : G.IsGeneratedInDegree A d) (hd : d < d') {f : M' →ₗ[A] M} (hf : LinearMap.IsHomogeneous f G'.piece G.piece 0) (x : M') : f x ∈ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤

Over a nonnegatively graded algebra, a degree-zero homogeneous map from a graded module generated in degree d' to a graded module generated in a lower degree d takes values in A₊ M. The source has no homogeneous elements below degree d', and the target has all of its homogeneous elements of degree at least d' in A₊ M.