The direct-sum grading of the divided power algebra

For a module M over a commutative semiring R, the homogeneous pieces Γ^d_R(M) of DividedPowerAlgebra R M (see DividedPowerAlgebra.homogeneousSubmodule) form an internal direct sum: every element is uniquely a finite sum of homogeneous elements. Together with the multiplicativity of the pieces this makes DividedPowerAlgebra R M an ℕ-graded R-algebra, in which dp R d m has degree d. In particular DirectSum.decomposeLinearEquiv identifies DividedPowerAlgebra R M with ⨁ d, Γ^d_R(M), and its inverse is the sum map.

No freeness, finiteness or characteristic hypothesis is imposed. The degree-zero projection of the grading is the augmentation followed by the structure map R → Γ_R(M).

Main declarations

• DividedPowerAlgebra.isInternal_homogeneousSubmodule: the homogeneous pieces form an internal direct sum.
• DividedPowerAlgebra.instGradedAlgebra: the resulting ℕ-graded algebra structure.
• DividedPowerAlgebra.decompose_dp: dp R d m is homogeneous of degree d.
• DividedPowerAlgebra.decompose_prod_dp: a product ∏ⱼ dp R aⱼ vⱼ with ∑ⱼ aⱼ = d is its own degree-d component.
• DividedPowerAlgebra.homogeneousProj: the linear projection onto the degree-d piece.
• DividedPowerAlgebra.coe_decompose_map: the functorial map preserves the grading.
• DividedPowerAlgebra.coe_decompose_apply_zero: the degree-zero component is algebraMap R _ ∘ augmentation R M.

Implementation notes

Directness cannot be obtained by dividing by factorials: over ZMod 2, dp 1 1 ^ 2 = 0 while dp 2 1 ≠ 0. Instead, giving the generator dp R n m the weight n defines an algebra map DividedPowerAlgebra R M → (DividedPowerAlgebra R M)[X], dp R n m ↦ dp R n m • X ^ n, through the universal property DividedPowerAlgebra.lift'. It is multiplication by X ^ d on the degree-d piece, so the X ^ d-coefficient of its value recovers the degree-d component of a sum of homogeneous elements.

References

• [N. Roby, Lois polynômes et lois formelles en théorie des modules (1963), III §§1–2][Roby-1963]
• The ambient DividedPowerAlgebra, its generators and lift' are the Mathlib formalization by Antoine Chambert-Loir and María Inés de Frutos-Fernández.

theorem DividedPowerAlgebra.isInternal_homogeneousSubmodule {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : DirectSum.IsInternal homogeneousSubmodule

The homogeneous pieces of the divided power algebra form an internal direct sum: the sum map ⨁ d, Γ^d_R(M) → Γ_R(M) is bijective.

@[instance_reducible]

noncomputable instance DividedPowerAlgebra.instGradedAlgebra {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : GradedAlgebra homogeneousSubmodule

The divided power algebra is an ℕ-graded algebra, with degree-d piece homogeneousSubmodule R M d.

@[simp]

theorem DividedPowerAlgebra.decompose_dp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (d : ℕ) (m : M) : (DirectSum.decompose homogeneousSubmodule) (dp R d m) = (DirectSum.of (fun (i : ℕ) => ↥(homogeneousSubmodule i)) d) ⟨dp R d m, ⋯⟩

The divided-power generator dp R d m is homogeneous of degree d.

theorem DividedPowerAlgebra.decompose_prod_dp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [Fintype ι] {d : ℕ} (v : ι → M) (a : ι → ℕ) (ha : ∑ j : ι, a j = d) : ((DirectSum.decompose homogeneousSubmodule) (∏ j : ι, dp R (a j) (v j))) d = ⟨∏ j : ι, dp R (a j) (v j), ⋯⟩

The degree-d component of a product of divided powers of total degree d is the product itself.

noncomputable def DividedPowerAlgebra.homogeneousProj (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (d : ℕ) : DividedPowerAlgebra R M →ₗ[R] ↥(homogeneousSubmodule d)

The linear projection of Γ_R(M) onto its degree-d piece, sending x to its degree-d component.

@[simp]

theorem DividedPowerAlgebra.homogeneousProj_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (d : ℕ) (x : DividedPowerAlgebra R M) : (homogeneousProj R M d) x = ((DirectSum.decompose homogeneousSubmodule) x) d

@[simp]

theorem DividedPowerAlgebra.homogeneousProj_comp_subtype {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (d : ℕ) : homogeneousProj R M d ∘ₗ (homogeneousSubmodule d).subtype = LinearMap.id

The projection onto the degree-d piece is the identity on that piece.

theorem DividedPowerAlgebra.coe_decompose_map {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} {N : Type u_4} [CommSemiring S] [Algebra R S] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) (x : DividedPowerAlgebra R M) (d : ℕ) : ↑(((DirectSum.decompose homogeneousSubmodule) ((map S f) x)) d) = (map S f) ↑(((DirectSum.decompose homogeneousSubmodule) x) d)

The functorial map on divided power algebras, possibly changing the base ring to an R-algebra S, commutes with taking degree-d components.

@[simp]

theorem DividedPowerAlgebra.coe_decompose_apply_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : DividedPowerAlgebra R M) : ↑(((DirectSum.decompose homogeneousSubmodule) x) 0) = (algebraMap R (DividedPowerAlgebra R M)) ((augmentation R M) x)

The degree-zero component of an element is its augmentation, viewed in Γ_R(M) through the structure map. Thus the degree-zero projection GradedRing.projZeroRingHom is the identity on scalars and kills every positive homogeneous piece.