Direct sums of internally graded modules

This file equips an external direct sum of internally graded modules with its canonical internal grading. Its degree-p piece is the direct sum of the componentwise degree-p pieces, included in the ambient direct sum, so membership is characterized componentwise.

This is the direct-sum compatibility target in Layer 0 of the DGAInfinity roadmap.

The file also records how the decomposition of a graded module interacts with the action of a graded ring: TauCeti.DirectSum.coe_decompose_smul_add_of_right_mem computes the components of a • x for homogeneous x.

Main definitions

• TauCeti.InternalGrading.directSumPieceInclusion: the inclusion of homogeneous summands of one fixed degree into the ambient direct sum.
• TauCeti.InternalGrading.directSumPiece: the corresponding homogeneous submodule.
• TauCeti.InternalGrading.directSum: the canonical internal grading on an external direct sum.

Main results

• TauCeti.DirectSum.coe_decompose_smul_add_of_right_mem: the components of a • x, for x homogeneous in a graded module, are the products of the components of a with x.

References

• Mathlib's DirectSum API.
• B. Keller, Introduction to A-infinity algebras and modules, Section 3.6.

def TauCeti.InternalGrading.directSumPieceInclusion {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) (p : ℤ) : (DirectSum ι fun (i : ι) => ↥((G i).piece p)) →ₗ[R] DirectSum ι fun (i : ι) => M i

The canonical inclusion of the direct sum of degree-p pieces into the direct sum of the underlying modules.

Equations

• TauCeti.InternalGrading.directSumPieceInclusion G p = TauCeti.DirectSum.piInclusion fun (i : ι) => (G i).piece p

@[simp]

theorem TauCeti.InternalGrading.directSumPieceInclusion_apply {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) (p : ℤ) (x : DirectSum ι fun (i : ι) => ↥((G i).piece p)) (i : ι) : ((directSumPieceInclusion G p) x) i = ↑(x i)

The componentwise formula for the graded direct-sum inclusion.

def TauCeti.InternalGrading.directSumPiece {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) (p : ℤ) : Submodule R (DirectSum ι fun (i : ι) => M i)

The degree-p piece in the direct sum of a family of internally graded modules.

Equations

• TauCeti.InternalGrading.directSumPiece G p = TauCeti.DirectSum.piSubmodule fun (i : ι) => (G i).piece p

@[simp]

theorem TauCeti.InternalGrading.directSumPieceInclusion_lof {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) (p : ℤ) (i : ι) (x : ↥((G i).piece p)) [DecidableEq ι] : (directSumPieceInclusion G p) ((DirectSum.lof R ι (fun (i : ι) => ↥((G i).piece p)) i) x) = (DirectSum.lof R ι M i) ↑x

On a homogeneous summand, directSumPieceInclusion is the usual external direct-sum inclusion.

noncomputable def TauCeti.InternalGrading.directSumPieceEquiv {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) (p : ℤ) : (DirectSum ι fun (i : ι) => ↥((G i).piece p)) ≃ₗ[R] ↥(directSumPiece G p)

The linear equivalence from the external direct sum of degree-p pieces to its range in the ambient direct sum.

Equations

• TauCeti.InternalGrading.directSumPieceEquiv G p = TauCeti.DirectSum.piSubmoduleEquiv fun (i : ι) => (G i).piece p

@[simp]

theorem TauCeti.InternalGrading.directSumPieceEquiv_apply {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) (p : ℤ) (x : DirectSum ι fun (i : ι) => ↥((G i).piece p)) : ↑((directSumPieceEquiv G p) x) = (directSumPieceInclusion G p) x

The underlying element of directSumPieceEquiv is the canonical inclusion.

@[simp]

theorem TauCeti.InternalGrading.directSumPieceEquiv_symm_apply {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) (p : ℤ) (y : ↥(directSumPiece G p)) (i : ι) : ↑(((directSumPieceEquiv G p).symm y) i) = ↑y i

The componentwise formula for the inverse of directSumPieceEquiv.

theorem TauCeti.InternalGrading.isInternal_directSumPiece {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) : DirectSum.IsInternal (directSumPiece G)

The canonical degreewise ranges in an external direct sum form an internal direct sum.

def TauCeti.InternalGrading.directSum {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) : InternalGrading R (DirectSum ι fun (i : ι) => M i)

The external direct sum of internally graded modules, with degree-p piece the image of the direct sum of the degree-p pieces.

Equations

• TauCeti.InternalGrading.directSum G = { piece := TauCeti.InternalGrading.directSumPiece G, isInternal := ⋯ }

@[simp]

theorem TauCeti.InternalGrading.mem_directSumPiece_iff {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) (p : ℤ) (x : DirectSum ι fun (i : ι) => M i) : x ∈ directSumPiece G p ↔ ∀ (i : ι), x i ∈ (G i).piece p

Membership in the direct sum of degree-p pieces is componentwise.

@[simp]

theorem TauCeti.InternalGrading.directSum_piece {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) (p : ℤ) : (directSum G).piece p = directSumPiece G p

The homogeneous pieces of directSum are the ranges of the canonical degreewise inclusions.

theorem TauCeti.InternalGrading.lof_mem_directSumPiece {R : Type u} {ι : Type v} {M : ι → Type w} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (G : (i : ι) → InternalGrading R (M i)) (p : ℤ) (i : ι) (x : ↥((G i).piece p)) [DecidableEq ι] : (DirectSum.lof R ι M i) ↑x ∈ directSumPiece G p

The inclusion of a degree-p element from one summand belongs to the degree-p piece of the direct-sum grading.

Decomposition and the action of a graded ring

theorem TauCeti.DirectSum.coe_decompose_smul_add_of_right_mem {ι : Type u_1} {A : Type u_2} {M : Type u_3} {σA : Type u_4} {σM : Type u_5} [DecidableEq ι] [AddRightCancelMonoid ι] [Semiring A] [AddCommMonoid M] [Module A M] [SetLike σA A] [AddSubmonoidClass σA A] (𝒜 : ι → σA) [GradedRing 𝒜] [SetLike σM M] [AddSubmonoidClass σM M] (ℳ : ι → σM) [DirectSum.Decomposition ℳ] [SetLike.GradedSMul 𝒜 ℳ] {a : A} {x : M} {i j : ι} (hx : x ∈ ℳ j) : ↑(((DirectSum.decompose ℳ) (a • x)) (i + j)) = ↑(((DirectSum.decompose 𝒜) a) i) • x

In a graded module over a graded ring, the degree-i + j component of a • x, for x homogeneous of degree j, is the degree-i component of a acting on x. This is the module analogue of DirectSum.coe_decompose_mul_add_of_right_mem.