The completion of a nonnegatively graded algebra along its grading

Let A = ⨁ₙ Aₙ be an ℕ-graded algebra over a commutative semiring R, given internally by 𝒜 : ℕ → Submodule R A with GradedAlgebra 𝒜. Its completion along the grading is the algebra of formal series ∑ₙ aₙ with aₙ ∈ Aₙ, multiplied by the Cauchy product. It is the completion of A for the descending filtration ⨁_{m ≥ n} Aₘ, for instance the length-adic completion of a path algebra with respect to its path-length grading.

This file realizes that completion as the subalgebra TauCeti.gradedCompletion 𝒜 of the formal power series PowerSeries A whose coefficient of index n lies in Aₙ: the Cauchy product of power series is exactly the multiplication of such formal sums, so no separate ring structure has to be built. The comparison map from A sends an element to the power series of its homogeneous components; it is injective, and its image consists of the series with finitely many nonzero coefficients.

Main definitions

• TauCeti.gradedCompletion: the completion of A along 𝒜, as a subalgebra of PowerSeries A.
• TauCeti.gradedComponentSeries: the power series of homogeneous components of an element of A, an algebra homomorphism A →ₐ[R] PowerSeries A.
• TauCeti.toGradedCompletion: the comparison map A →ₐ[R] gradedCompletion 𝒜.

Main results

• TauCeti.mem_gradedCompletion_iff: a power series lies in the completion exactly when its n-th coefficient is homogeneous of degree n.
• TauCeti.coeff_gradedComponentSeries: the n-th coefficient of the series of components is the degree-n component.
• TauCeti.gradedComponentSeries_injective and TauCeti.toGradedCompletion_injective: the comparison map is injective.
• TauCeti.mem_range_gradedComponentSeries_iff and TauCeti.mem_range_toGradedCompletion_iff: the image of A in its completion consists of the series with finitely many nonzero coefficients.

References

• B. Keller, Deformed Calabi--Yau completions, Section 6, for the completion of a graded path algebra with respect to path length.

The completion

def TauCeti.gradedCompletion {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : Subalgebra R (PowerSeries A)

The completion of a nonnegatively graded algebra along its grading: the subalgebra of formal power series over A whose coefficient of index n is homogeneous of degree n. Its elements are the formal sums ∑ₙ aₙ with aₙ ∈ 𝒜 n, multiplied by the Cauchy product.

Equations

• TauCeti.gradedCompletion 𝒜 = { carrier := {f : PowerSeries A | ∀ (n : ℕ), (PowerSeries.coeff n) f ∈ 𝒜 n}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_gradedCompletion_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : PowerSeries A} : f ∈ gradedCompletion 𝒜 ↔ ∀ (n : ℕ), (PowerSeries.coeff n) f ∈ 𝒜 n

A power series lies in the completion exactly when its n-th coefficient is homogeneous of degree n.

The series of homogeneous components

def TauCeti.gradedComponentSeries {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : A →ₐ[R] PowerSeries A

The power series of homogeneous components of an element of a nonnegatively graded algebra: the coefficient of index n is the degree-n component. It is an algebra homomorphism, because the degree-n component of a product is the Cauchy product of the components of the factors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coeff_gradedComponentSeries {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (a : A) (n : ℕ) : (PowerSeries.coeff n) ((gradedComponentSeries 𝒜) a) = ↑(((DirectSum.decompose 𝒜) a) n)

The n-th coefficient of the series of homogeneous components is the degree-n component.

theorem TauCeti.gradedComponentSeries_of_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {n : ℕ} {a : A} (ha : a ∈ 𝒜 n) : (gradedComponentSeries 𝒜) a = (PowerSeries.monomial n) a

The series of components of a homogeneous element of degree n is the monomial of that element in index n.

theorem TauCeti.gradedComponentSeries_injective {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : Function.Injective ⇑(gradedComponentSeries 𝒜)

An element is determined by the series of its homogeneous components.

theorem TauCeti.mem_range_gradedComponentSeries_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : PowerSeries A} : f ∈ (gradedComponentSeries 𝒜).range ↔ (∀ (n : ℕ), (PowerSeries.coeff n) f ∈ 𝒜 n) ∧ (Function.support fun (n : ℕ) => (PowerSeries.coeff n) f).Finite

The series of homogeneous components of elements of A are exactly the series with homogeneous coefficients and finitely many nonzero coefficients.

The comparison map

theorem TauCeti.gradedComponentSeries_mem_gradedCompletion {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (a : A) : (gradedComponentSeries 𝒜) a ∈ gradedCompletion 𝒜

The series of homogeneous components lies in the completion.

noncomputable def TauCeti.toGradedCompletion {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : A →ₐ[R] ↥(gradedCompletion 𝒜)

The comparison map from a nonnegatively graded algebra to its completion, sending an element to the series of its homogeneous components.

Equations

• TauCeti.toGradedCompletion 𝒜 = (TauCeti.gradedComponentSeries 𝒜).codRestrict (TauCeti.gradedCompletion 𝒜) ⋯

@[simp]

theorem TauCeti.coe_toGradedCompletion_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (a : A) : ↑((toGradedCompletion 𝒜) a) = (gradedComponentSeries 𝒜) a

theorem TauCeti.toGradedCompletion_injective {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : Function.Injective ⇑(toGradedCompletion 𝒜)

The comparison map is injective: a graded algebra embeds in its completion.

theorem TauCeti.mem_range_toGradedCompletion_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : ↥(gradedCompletion 𝒜)} : f ∈ (toGradedCompletion 𝒜).range ↔ (Function.support fun (n : ℕ) => (PowerSeries.coeff n) ↑f).Finite

The image of the comparison map consists of the series with finitely many nonzero coefficients.