Degreewise products of internally graded modules

The product of graded modules consists of families with a common finite set of possible degrees. Its degree-p piece is the product of the degree-p pieces of the factors. The total module is the range of the canonical map from the direct sum of these degreewise products to the product of the total modules. An arbitrary family of inhomogeneous elements need not belong to it.

The internal grading is transported from the canonical summands of the direct sum. Homogeneous maps of one common degree lift componentwise into this product. This includes degree-one differentials and degree-minus-one homotopies, as well as degree-zero graded morphisms.

References

• Mathlib's direct-sum decomposition and module APIs.
• DirectSum.summand and its decomposition from TauCeti.Algebra.DirectSum.Internal.

def TauCeti.InternalGrading.productPiece {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) (p : ℤ) : Submodule R ((j : J) → M j)

Families all of whose components have degree p.

@[simp]

theorem TauCeti.InternalGrading.mem_productPiece_iff {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) (p : ℤ) (x : (j : J) → M j) : x ∈ productPiece G p ↔ ∀ (j : J), x j ∈ (G j).piece ℤ p

Homogeneity of a family is checked componentwise.

def TauCeti.InternalGrading.productCarrier {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) : Submodule R ((j : J) → M j)

The families that are finite sums of homogeneous families.

theorem TauCeti.InternalGrading.productPiece_le_productCarrier {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) (p : ℤ) : productPiece G p ≤ productCarrier G

Every homogeneous family belongs to the graded product.

theorem TauCeti.InternalGrading.mem_productCarrier_iff {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) (x : (j : J) → M j) : x ∈ productCarrier G ↔ ∃ (s : Finset ℤ), ∀ (j : J), (Function.support fun (p : ℤ) => ↑(((DirectSum.decompose ((G j).piece ℤ)) (x j)) p)) ⊆ ↑s

A family belongs to the total graded product exactly when one finite set contains the supports of the homogeneous decompositions of all its components.

noncomputable def TauCeti.InternalGrading.productEquiv {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) : (DirectSum ℤ fun (p : ℤ) => ↥(productPiece G p)) ≃ₗ[R] ↥(productCarrier G)

The sum of the degreewise products is the total graded product.

@[simp]

theorem TauCeti.InternalGrading.productEquiv_apply {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) (x : DirectSum ℤ fun (p : ℤ) => ↥(productPiece G p)) : ↑((productEquiv G) x) = (DirectSum.coeLinearMap (productPiece G)) x

The comparison sums the finitely many homogeneous families.

noncomputable def TauCeti.InternalGrading.product {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) : InternalGrading R ↥(productCarrier G) ℤ

The internal grading on the product, obtained from its degreewise product presentation.

@[simp]

theorem TauCeti.InternalGrading.mem_product_piece_iff {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) (p : ℤ) (x : ↥(productCarrier G)) : x ∈ (product G).piece ℤ p ↔ ∀ (j : J), ↑x j ∈ (G j).piece ℤ p

An element of the graded product has degree p exactly when each component does.

def TauCeti.InternalGrading.productEval {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) (j : J) : ↥(productCarrier G) →ₗ[R] M j

Evaluation at one factor, as a linear map on the graded product.

@[simp]

theorem TauCeti.InternalGrading.productEval_apply {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) (j : J) (x : ↥(productCarrier G)) : (productEval G j) x = ↑x j

Evaluation is the corresponding coordinate of the underlying family.

theorem TauCeti.InternalGrading.productLift_mem {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) {N : Type z} [AddCommMonoid N] [Module R N] (H : InternalGrading R N ℤ) (r : ℤ) (f : (j : J) → N →ₗ[R] M j) (hf : ∀ (j : J), LinearMap.IsHomogeneous (f j) (H.piece ℤ) ((G j).piece ℤ) r) (x : N) : (fun (j : J) => (f j) x) ∈ productCarrier G

A family of maps of one common degree has values in the total graded product: the finite degree support of the source element controls every component at once.

noncomputable def TauCeti.InternalGrading.productLiftLinear {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) {N : Type z} [AddCommMonoid N] [Module R N] (H : InternalGrading R N ℤ) (r : ℤ) (f : (j : J) → N →ₗ[R] M j) (hf : ∀ (j : J), LinearMap.IsHomogeneous (f j) (H.piece ℤ) ((G j).piece ℤ) r) : N →ₗ[R] ↥(productCarrier G)

The componentwise lift of homogeneous maps into the graded product.

@[simp]

theorem TauCeti.InternalGrading.productLiftLinear_apply {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) {N : Type z} [AddCommMonoid N] [Module R N] (H : InternalGrading R N ℤ) (r : ℤ) (f : (j : J) → N →ₗ[R] M j) (hf : ∀ (j : J), LinearMap.IsHomogeneous (f j) (H.piece ℤ) ((G j).piece ℤ) r) (x : N) (j : J) : ↑((productLiftLinear G H r f hf) x) j = (f j) x

The homogeneous lift has the prescribed components.

theorem TauCeti.InternalGrading.productLiftLinear_isHomogeneous {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) {N : Type z} [AddCommMonoid N] [Module R N] (H : InternalGrading R N ℤ) (r : ℤ) (f : (j : J) → N →ₗ[R] M j) (hf : ∀ (j : J), LinearMap.IsHomogeneous (f j) (H.piece ℤ) ((G j).piece ℤ) r) : LinearMap.IsHomogeneous (productLiftLinear G H r f hf) (H.piece ℤ) ((product G).piece ℤ) r

The lift has the same common degree as its components.

theorem TauCeti.InternalGrading.productCarrier_smul_mem {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) {S : Type u_1} [Semiring S] [(j : J) → Module S (M j)] {σ : Type u_2} [SetLike σ S] [AddSubmonoidClass σ S] (𝒜 : ℤ → σ) [DirectSum.Decomposition 𝒜] [∀ (j : J), SetLike.GradedSMul 𝒜 ((G j).piece ℤ)] (a : S) {x : (j : J) → M j} (hx : x ∈ productCarrier G) : a • x ∈ productCarrier G

The graded product is stable under the graded scalar action. A scalar also has finite homogeneous support, so multiplication preserves a common finite degree support.

@[implicit_reducible]

def TauCeti.InternalGrading.productScalarSubmodule {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) {S : Type u_1} [Semiring S] [(j : J) → Module S (M j)] {σ : Type u_2} [SetLike σ S] [AddSubmonoidClass σ S] (𝒜 : ℤ → σ) [DirectSum.Decomposition 𝒜] [∀ (j : J), SetLike.GradedSMul 𝒜 ((G j).piece ℤ)] : Submodule S ((j : J) → M j)

The same graded product as a submodule over the acting graded scalars.

@[simp]

theorem TauCeti.InternalGrading.productScalarSubmodule_restrictScalars {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) {S : Type u_1} [Semiring S] [(j : J) → Module S (M j)] {σ : Type u_2} [SetLike σ S] [AddSubmonoidClass σ S] (𝒜 : ℤ → σ) [DirectSum.Decomposition 𝒜] [∀ (j : J), SetLike.GradedSMul 𝒜 ((G j).piece ℤ)] [SMul R S] [∀ (j : J), IsScalarTower R S (M j)] : Submodule.restrictScalars R (productScalarSubmodule G 𝒜) = productCarrier G

Restricting scalars recovers the base-linear graded-product submodule.

noncomputable def TauCeti.InternalGrading.productLift {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) {S : Type u_1} [Semiring S] [(j : J) → Module S (M j)] {σ : Type u_2} [SetLike σ S] [AddSubmonoidClass σ S] (𝒜 : ℤ → σ) [DirectSum.Decomposition 𝒜] [∀ (j : J), SetLike.GradedSMul 𝒜 ((G j).piece ℤ)] [SMul R S] [∀ (j : J), IsScalarTower R S (M j)] {N : Type z} [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (H : InternalGrading R N ℤ) (r : ℤ) (f : (j : J) → N →ₗ[S] M j) (hf : ∀ (j : J), LinearMap.IsHomogeneous (↑R (f j)) (H.piece ℤ) ((G j).piece ℤ) r) : N →ₗ[S] ↥(productScalarSubmodule G 𝒜)

The componentwise lift is linear over the acting scalars as well as the base ring.

@[simp]

theorem TauCeti.InternalGrading.productLift_apply {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) {S : Type u_1} [Semiring S] [(j : J) → Module S (M j)] {σ : Type u_2} [SetLike σ S] [AddSubmonoidClass σ S] (𝒜 : ℤ → σ) [DirectSum.Decomposition 𝒜] [∀ (j : J), SetLike.GradedSMul 𝒜 ((G j).piece ℤ)] [SMul R S] [∀ (j : J), IsScalarTower R S (M j)] {N : Type z} [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (H : InternalGrading R N ℤ) (r : ℤ) (f : (j : J) → N →ₗ[S] M j) (hf : ∀ (j : J), LinearMap.IsHomogeneous (↑R (f j)) (H.piece ℤ) ((G j).piece ℤ) r) (x : N) (j : J) : ↑((productLift G 𝒜 H r f hf) x) j = (f j) x

The scalar-linear product lift is computed componentwise.

theorem TauCeti.InternalGrading.productLift_isHomogeneous {R : Type u} [Semiring R] {J : Type v} {M : J → Type w} [(j : J) → AddCommMonoid (M j)] [(j : J) → Module R (M j)] (G : (j : J) → InternalGrading R (M j) ℤ) {S : Type u_1} [Semiring S] [(j : J) → Module S (M j)] {σ : Type u_2} [SetLike σ S] [AddSubmonoidClass σ S] (𝒜 : ℤ → σ) [DirectSum.Decomposition 𝒜] [∀ (j : J), SetLike.GradedSMul 𝒜 ((G j).piece ℤ)] [SMul R S] [∀ (j : J), IsScalarTower R S (M j)] {N : Type z} [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (H : InternalGrading R N ℤ) (r : ℤ) (f : (j : J) → N →ₗ[S] M j) (hf : ∀ (j : J), LinearMap.IsHomogeneous (↑R (f j)) (H.piece ℤ) ((G j).piece ℤ) r) : LinearMap.IsHomogeneous (↑R (productLift G 𝒜 H r f hf)) (H.piece ℤ) ((product G).piece ℤ) r

The scalar-linear lift retains the common homogeneous degree.