Homogeneous pieces of the divided power algebra

For a module M over a commutative semiring R, this file defines the degree-d homogeneous piece of DividedPowerAlgebra R M. It is the R-submodule spanned by products of divided-power generators whose indices sum to d. In particular, dp R d m belongs to the degree-d piece.

A linear map M →ₗ[R] N restricts the functorial map on divided power algebras to every homogeneous piece. These restricted maps preserve divided-power generators and satisfy the identity and composition laws. For a second module N, the product x ⊗ y ↦ Γ(inl)(x) Γ(inr)(y) maps Γ^d_R(M) ⊗[R] Γ^e_R(N) to Γ^{d + e}_R(M × N) (DividedPowerAlgebra.homogeneousProdMul), naturally in both modules.

The construction follows Roby's grading of the divided power algebra. The ambient DividedPowerAlgebra, its generators and its functorial map are the Mathlib formalization by Antoine Chambert-Loir and María Inés de Frutos-Fernández.

References

• [N. Roby, Lois polynômes et lois formelles en théorie des modules (1963), III §§1–2][Roby-1963]

def DividedPowerAlgebra.homogeneousGenerators {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (d : ℕ) : Set (DividedPowerAlgebra R M)

The products of divided-power generators whose indices sum to d.

noncomputable def DividedPowerAlgebra.homogeneousSubmodule {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (d : ℕ) : Submodule R (DividedPowerAlgebra R M)

The degree-d homogeneous piece of the divided power algebra.

theorem DividedPowerAlgebra.prod_dp_mem_homogeneousSubmodule {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (l : List (ℕ × M)) : (List.map (fun (nm : ℕ × M) => dp R nm.1 nm.2) l).prod ∈ homogeneousSubmodule (List.map Prod.fst l).sum

A product of divided-power generators belongs to the piece indexed by the sum of their degrees.

theorem DividedPowerAlgebra.homogeneousSubmodule_le_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {d : ℕ} {p : Submodule R (DividedPowerAlgebra R M)} : homogeneousSubmodule d ≤ p ↔ ∀ (l : List (ℕ × M)), (List.map Prod.fst l).sum = d → (List.map (fun (nm : ℕ × M) => dp R nm.1 nm.2) l).prod ∈ p

A submodule contains the degree-d piece if and only if it contains every product of divided-power generators whose indices sum to d.

theorem DividedPowerAlgebra.homogeneousSubmodule_induction {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {d : ℕ} {motive : (x : DividedPowerAlgebra R M) → x ∈ homogeneousSubmodule d → Prop} (prod_dp : ∀ (l : List (ℕ × M)) (hl : (List.map Prod.fst l).sum = d), motive (List.map (fun (nm : ℕ × M) => dp R nm.1 nm.2) l).prod ⋯) (zero : motive 0 ⋯) (add : ∀ (x y : DividedPowerAlgebra R M) (hx : x ∈ homogeneousSubmodule d) (hy : y ∈ homogeneousSubmodule d), motive x hx → motive y hy → motive (x + y) ⋯) (smul : ∀ (r : R) (x : DividedPowerAlgebra R M) (hx : x ∈ homogeneousSubmodule d), motive x hx → motive (r • x) ⋯) {x : DividedPowerAlgebra R M} (hx : x ∈ homogeneousSubmodule d) : motive x hx

An induction principle for the degree-d piece: a property of its elements holds as soon as it holds for products of divided-power generators whose indices sum to d and is stable under zero, addition and scalar multiplication.

theorem DividedPowerAlgebra.homogeneousSubmodule_ext {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {d : ℕ} {f g : ↥(homogeneousSubmodule d) →ₗ[R] N} (h : ∀ (l : List (ℕ × M)) (hl : (List.map Prod.fst l).sum = d), f ⟨(List.map (fun (nm : ℕ × M) => dp R nm.1 nm.2) l).prod, ⋯⟩ = g ⟨(List.map (fun (nm : ℕ × M) => dp R nm.1 nm.2) l).prod, ⋯⟩) : f = g

Linear maps from a homogeneous piece agree if they agree on every product of divided-power generators of the prescribed total degree.

theorem DividedPowerAlgebra.dp_mem_homogeneousSubmodule {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (d : ℕ) (m : M) : dp R d m ∈ homogeneousSubmodule d

The generator dp R d m is homogeneous of degree d.

theorem DividedPowerAlgebra.one_mem_homogeneousSubmodule {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : 1 ∈ homogeneousSubmodule 0

The unit is homogeneous of degree zero.

theorem DividedPowerAlgebra.mul_mem_homogeneousSubmodule {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {a b : ℕ} {x y : DividedPowerAlgebra R M} (hx : x ∈ homogeneousSubmodule a) (hy : y ∈ homogeneousSubmodule b) : x * y ∈ homogeneousSubmodule (a + b)

Products of homogeneous elements have the sum of their degrees.

instance DividedPowerAlgebra.instGradedMonoid {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : SetLike.GradedMonoid homogeneousSubmodule

The homogeneous submodules form a graded monoid under multiplication.

theorem DividedPowerAlgebra.prod_dp_mem_homogeneousSubmodule_of_sum_finset_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_5} (F : Finset ι) {d : ℕ} (m : ι → M) (k : ι → ℕ) (hk : ∑ j ∈ F, k j = d) : ∏ j ∈ F, dp R (k j) (m j) ∈ homogeneousSubmodule d

A product ∏_{j ∈ F} dp R kⱼ mⱼ over a finite set belongs to the homogeneous piece of its total degree.

theorem DividedPowerAlgebra.prod_dp_mem_homogeneousSubmodule_of_sum_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_5} [Fintype ι] {d : ℕ} (m : ι → M) (k : ι → ℕ) (hk : ∑ j : ι, k j = d) : ∏ j : ι, dp R (k j) (m j) ∈ homogeneousSubmodule d

A finite product of divided-power generators belongs to the homogeneous piece of its total degree.

theorem DividedPowerAlgebra.homogeneousSubmodule_ext_prod_dp {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {d : ℕ} {f g : ↥(homogeneousSubmodule d) →ₗ[R] N} (h : ∀ (n : ℕ) (m : Fin n → M) (k : Fin n → ℕ) (hk : ∑ j : Fin n, k j = d), f ⟨∏ j : Fin n, dp R (k j) (m j), ⋯⟩ = g ⟨∏ j : Fin n, dp R (k j) (m j), ⋯⟩) : f = g

Linear maps from a homogeneous piece agree if they agree on every product ∏ⱼ dp R kⱼ mⱼ of a finite family whose indices sum to d.

theorem DividedPowerAlgebra.map_mem_homogeneousSubmodule {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {S : Type u_5} [CommSemiring S] [Algebra R S] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) {d : ℕ} {x : DividedPowerAlgebra R M} (hx : x ∈ homogeneousSubmodule d) : (map S f) x ∈ homogeneousSubmodule d

The functorial map on divided power algebras preserves every homogeneous piece, including when it changes the base ring to an R-algebra S.

noncomputable def DividedPowerAlgebra.mapHomogeneousSubmodule {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (d : ℕ) : ↥(homogeneousSubmodule d) →ₗ[R] ↥(homogeneousSubmodule d)

A linear map induces a linear map between homogeneous pieces of the same degree.

@[simp]

theorem DividedPowerAlgebra.coe_mapHomogeneousSubmodule_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (d : ℕ) (x : ↥(homogeneousSubmodule d)) : ↑((mapHomogeneousSubmodule f d) x) = (map R f) ↑x

The map on homogeneous pieces is the restriction of DividedPowerAlgebra.map.

@[simp]

theorem DividedPowerAlgebra.mapHomogeneousSubmodule_dp {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (d : ℕ) (m : M) : (mapHomogeneousSubmodule f d) ⟨dp R d m, ⋯⟩ = ⟨dp R d (f m), ⋯⟩

The map on homogeneous pieces sends a divided-power generator to the corresponding divided-power generator.

@[simp]

theorem DividedPowerAlgebra.mapHomogeneousSubmodule_id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (d : ℕ) : mapHomogeneousSubmodule LinearMap.id d = LinearMap.id

The identity linear map induces the identity on every homogeneous piece.

@[simp]

theorem DividedPowerAlgebra.mapHomogeneousSubmodule_comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (d : ℕ) : mapHomogeneousSubmodule g d ∘ₗ mapHomogeneousSubmodule f d = mapHomogeneousSubmodule (g ∘ₗ f) d

Maps on homogeneous pieces respect composition.

noncomputable def DividedPowerAlgebra.homogeneousProdMul (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d e : ℕ) : TensorProduct R ↥(homogeneousSubmodule d) ↥(homogeneousSubmodule e) →ₗ[R] ↥(homogeneousSubmodule (d + e))

The product x ⊗ y ↦ Γ(inl)(x) Γ(inr)(y) of homogeneous pieces, from Γ^d_R(M) ⊗[R] Γ^e_R(N) to Γ^{d + e}_R(M × N).

@[simp]

theorem DividedPowerAlgebra.coe_homogeneousProdMul_tmul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (d e : ℕ) (x : ↥(homogeneousSubmodule d)) (y : ↥(homogeneousSubmodule e)) : ↑((homogeneousProdMul R M N d e) (x ⊗ₜ[R] y)) = (map R (LinearMap.inl R M N)) ↑x * (map R (LinearMap.inr R M N)) ↑y

The product of homogeneous pieces sends x ⊗ y to Γ(inl)(x) Γ(inr)(y).

theorem DividedPowerAlgebra.homogeneousProdMul_comp_map {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {M' : Type u_5} {N' : Type u_6} [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N'] (d e : ℕ) (f : M →ₗ[R] M') (g : N →ₗ[R] N') : homogeneousProdMul R M' N' d e ∘ₗ TensorProduct.map (mapHomogeneousSubmodule f d) (mapHomogeneousSubmodule g e) = mapHomogeneousSubmodule (f.prodMap g) (d + e) ∘ₗ homogeneousProdMul R M N d e

The product of homogeneous pieces is natural in both modules.