Power series over a monoid algebra

For a commutative semiring R, an R-algebra A and a monoid M, the monoid algebra of M over the power-series ring A⟦X⟧ maps to the power-series ring over the monoid algebra A[M] by collecting, for each n, the coefficients of Xⁿ of the monomial coefficients:

∑ₘ φₘ · m  ↦  ∑ₙ (∑ₘ (coeff n φₘ) · m) Xⁿ.

This is an R-algebra homomorphism MonoidAlgebra.toPowerSeries, characterised by coeff_coeff_toPowerSeries: the coefficient at m of the coefficient of Xⁿ of the image is the coefficient of Xⁿ of the coefficient at m of the argument. It is always injective, and for a finite monoid M it is an isomorphism MonoidAlgebra.powerSeriesAlgEquiv. For an infinite M and a nontrivial A it is not surjective: a power series whose coefficients are supported on infinitely many elements of M altogether is not in the image, since an element of A⟦X⟧[M] involves only finitely many elements of M.

The finite case writes the ring ℤ_p⟦X⟧[C] attached to a finite group C as the power-series ring ℤ_p[C]⟦X⟧ over the group ring ℤ_p[C]; this is how the completed group algebra of a product C × ℤ_p becomes a power-series ring over ℤ_p[C].

Main declarations

• MonoidAlgebra.toPowerSeries R A M: the R-algebra homomorphism A⟦X⟧[M] →ₐ[R] A[M]⟦X⟧, with coeff_coeff_toPowerSeries and toPowerSeries_injective.
• MonoidAlgebra.powerSeriesAlgEquiv R A M: the isomorphism A⟦X⟧[M] ≃ₐ[R] A[M]⟦X⟧ for finite M.
• MonoidAlgebra.map_singleOneRingHom_dvd_iff: for finite M, a power series with coefficients in A divides ψ ∈ A[M]⟦X⟧ exactly when it divides, in A⟦X⟧, the coefficient at every m ∈ M of the element of A⟦X⟧[M] corresponding to ψ.

noncomputable def MonoidAlgebra.toPowerSeries (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] : MonoidAlgebra (PowerSeries A) M →ₐ[R] PowerSeries (MonoidAlgebra A M)

The R-algebra homomorphism A⟦X⟧[M] →ₐ[R] A[M]⟦X⟧ collecting the coefficients of Xⁿ: the coefficient at m of the coefficient of Xⁿ of the image of x is the coefficient of Xⁿ of the coefficient at m of x (coeff_coeff_toPowerSeries). It is injective, and bijective for finite M (powerSeriesAlgEquiv).

Equations

• MonoidAlgebra.toPowerSeries R A M = MonoidAlgebra.liftNCAlgHom (PowerSeries.mapAlgHom MonoidAlgebra.singleOneAlgHom) ((↑PowerSeries.C).comp (MonoidAlgebra.of A M)) ⋯

theorem MonoidAlgebra.toPowerSeries_single (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] (m : M) (φ : PowerSeries A) : (toPowerSeries R A M) (single m φ) = (PowerSeries.mapAlgHom singleOneAlgHom) φ * PowerSeries.C (single m 1)

On the monomial φ · m, the map to power series over A[M] is the power series φ with coefficients placed at 1, times the constant m.

@[simp]

theorem MonoidAlgebra.coeff_coeff_toPowerSeries (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] (x : MonoidAlgebra (PowerSeries A) M) (n : ℕ) (m : M) : ((PowerSeries.coeff n) ((toPowerSeries R A M) x)).coeff m = (PowerSeries.coeff n) (x.coeff m)

The characteristic property of toPowerSeries: the coefficient at m of the coefficient of Xⁿ of the image is the coefficient of Xⁿ of the coefficient at m.

@[simp]

theorem MonoidAlgebra.toPowerSeries_single_C (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] (m : M) (a : A) : (toPowerSeries R A M) (single m (PowerSeries.C a)) = PowerSeries.C (single m a)

The map to power series over A[M] sends the constant monomial a · m to the constant power series a · m.

@[simp]

theorem MonoidAlgebra.toPowerSeries_single_one_X (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] : (toPowerSeries R A M) (single 1 PowerSeries.X) = PowerSeries.X

The map to power series over A[M] sends X, placed at 1 ∈ M, to X.

theorem MonoidAlgebra.toPowerSeries_single_one (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] (φ : PowerSeries A) : (toPowerSeries R A M) (single 1 φ) = (PowerSeries.map singleOneRingHom) φ

The map to power series over A[M] sends the power series φ, placed at 1 ∈ M, to φ with its coefficients read in A[M] along singleOneRingHom.

theorem MonoidAlgebra.toPowerSeries_injective (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] : Function.Injective ⇑(toPowerSeries R A M)

The map A⟦X⟧[M] → A[M]⟦X⟧ is injective, for every monoid M: it determines all the coefficients of its argument (coeff_coeff_toPowerSeries).

theorem MonoidAlgebra.toPowerSeries_surjective (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] [Finite M] : Function.Surjective ⇑(toPowerSeries R A M)

The map A⟦X⟧[M] → A[M]⟦X⟧ is surjective when M is finite: a power series over A[M] is the image of the monoid algebra element whose coefficient at m is the power series of the coefficients at m, which is finitely supported in m because M is finite.

noncomputable def MonoidAlgebra.powerSeriesAlgEquiv (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] [Finite M] : MonoidAlgebra (PowerSeries A) M ≃ₐ[R] PowerSeries (MonoidAlgebra A M)

Power series over the monoid algebra of a finite monoid. For a finite monoid M, the monoid algebra of M over A⟦X⟧ is the power-series ring over the monoid algebra A[M], by collecting the coefficients of Xⁿ (toPowerSeries).

Equations

• MonoidAlgebra.powerSeriesAlgEquiv R A M = AlgEquiv.ofBijective (MonoidAlgebra.toPowerSeries R A M) ⋯

@[simp]

theorem MonoidAlgebra.coe_powerSeriesAlgEquiv (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] [Finite M] : ⇑(powerSeriesAlgEquiv R A M) = ⇑(toPowerSeries R A M)

@[simp]

theorem MonoidAlgebra.coeff_coeff_powerSeriesAlgEquiv_symm (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] [Finite M] (ψ : PowerSeries (MonoidAlgebra A M)) (m : M) (n : ℕ) : (PowerSeries.coeff n) (((powerSeriesAlgEquiv R A M).symm ψ).coeff m) = ((PowerSeries.coeff n) ψ).coeff m

The inverse of powerSeriesAlgEquiv reads the coefficients back: the coefficient of Xⁿ of the coefficient at m of the inverse image of ψ is the coefficient at m of the coefficient of Xⁿ of ψ.

@[simp]

theorem MonoidAlgebra.powerSeriesAlgEquiv_symm_C_single (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] [Finite M] (m : M) (a : A) : (powerSeriesAlgEquiv R A M).symm (PowerSeries.C (single m a)) = single m (PowerSeries.C a)

The inverse of powerSeriesAlgEquiv sends the constant power series a · m to the constant monomial a · m.

@[simp]

theorem MonoidAlgebra.powerSeriesAlgEquiv_symm_X (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] [Finite M] : (powerSeriesAlgEquiv R A M).symm PowerSeries.X = single 1 PowerSeries.X

The inverse of powerSeriesAlgEquiv sends X to X, placed at 1 ∈ M.

theorem MonoidAlgebra.map_singleOneRingHom_dvd_iff (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] (M : Type u_3) [Monoid M] [Finite M] (φ : PowerSeries A) (ψ : PowerSeries (MonoidAlgebra A M)) : (PowerSeries.map singleOneRingHom) φ ∣ ψ ↔ ∀ (m : M), φ ∣ ((powerSeriesAlgEquiv R A M).symm ψ).coeff m

Divisibility by a power series with coefficients in A. For φ ∈ A⟦X⟧ and ψ ∈ A[M]⟦X⟧, with M finite, φ read in A[M]⟦X⟧ divides ψ exactly when it divides, in A⟦X⟧, the coefficient at every m ∈ M of the element of A⟦X⟧[M] corresponding to ψ: the multiples of φ are the elements all of whose M-coefficients are multiples of φ.