Equivalences related to power series rings

This file establishes a number of equivalences related to power series rings.

• MvPowerSeries.toAdicCompletionAlgEquiv : the canonical isomorphism from multivariate power series to the adic completion of multivariate polynomials with respect to the ideal spanned by all variables when the index is finite.

theorem MvPowerSeries.truncTotal_sub_truncTotal_mem_pow_idealOfVars {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {l m n : ℕ} (h : l ≤ m) (h' : l ≤ n) (p : MvPowerSeries σ R) : (truncTotal R m) p - (truncTotal R n) p ∈ MvPolynomial.idealOfVars σ R ^ l

theorem MvPowerSeries.truncTotal_mul_sub_mul_truncTotal_mem_pow_idealOfVars {σ : Type u_1} {R : Type u_2} {n : ℕ} [CommRing R] [Finite σ] (p q : MvPowerSeries σ R) : (truncTotal R n) (p * q) - (truncTotal R n) p * (truncTotal R n) q ∈ MvPolynomial.idealOfVars σ R ^ n

noncomputable def MvPowerSeries.truncTotalAlgHom (σ : Type u_3) (R : Type u_4) [Finite σ] [CommRing R] (n : ℕ) : MvPowerSeries σ R →ₐ[MvPolynomial σ R] MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n

The canonical map induced by truncTotal from multivariate power series to the quotient ring of multivariate polynomials by the n-th power of the ideal spanned by all variables.

Equations

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

@[simp]

theorem MvPowerSeries.truncTotalAlgHom_apply (σ : Type u_3) (R : Type u_4) [Finite σ] [CommRing R] (n : ℕ) (p : MvPowerSeries σ R) : (truncTotalAlgHom σ R n) p = (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal R n) p)

noncomputable def MvPowerSeries.toAdicCompletion (σ : Type u_3) (R : Type u_4) [Finite σ] [CommRing R] : MvPowerSeries σ R →ₐ[MvPolynomial σ R] AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)

The canonical map from multivariate power series to the adic completion of multivariate polynomials with respect to the ideal spanned by all variables when the index is finite.

Equations

• MvPowerSeries.toAdicCompletion σ R = AdicCompletion.liftAlgHom (MvPolynomial.idealOfVars σ R) (MvPowerSeries.truncTotalAlgHom σ R) ⋯

theorem MvPowerSeries.toAdicCompletion_apply_eq_mk_truncTotal {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {n : ℕ} {p : MvPowerSeries σ R} : ↑((toAdicCompletion σ R) p) n = (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) ((truncTotal R n) p)

theorem MvPowerSeries.coeff_toAdicCompletion_val_apply_out {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {x : σ →₀ ℕ} {p : MvPowerSeries σ R} {n : ℕ} (hx : Finsupp.degree x < n) : MvPolynomial.coeff x (Quotient.out (↑((toAdicCompletion σ R) p) n)) = (coeff x) p

theorem MvPowerSeries.toAdicCompletion_coe {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] (p : MvPolynomial σ R) : (toAdicCompletion σ R) ↑p = (AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p

noncomputable def MvPowerSeries.toAdicCompletionInv (σ : Type u_3) (R : Type u_4) [CommRing R] (f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) : MvPowerSeries σ R

An inverse function of toAdicCompletion.

Equations

• MvPowerSeries.toAdicCompletionInv σ R f x = MvPolynomial.coeff x (Quotient.out (↑f (Finsupp.degree x + 1)))

theorem MvPowerSeries.coeff_toAdicCompletionInv {σ : Type u_1} {R : Type u_2} [CommRing R] {x : σ →₀ ℕ} {f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)} : (coeff x) (toAdicCompletionInv σ R f) = MvPolynomial.coeff x (Quotient.out (↑f (Finsupp.degree x + 1)))

theorem MvPowerSeries.mk_truncTotal_toAdicCompletionInv {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {n : ℕ} {f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)} : (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) ((truncTotal R n) (toAdicCompletionInv σ R f)) = ↑f n

noncomputable def MvPowerSeries.toAdicCompletionAlgEquiv (σ : Type u_3) (R : Type u_4) [Finite σ] [CommRing R] : MvPowerSeries σ R ≃ₐ[MvPolynomial σ R] AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)

The isomorphism from multivariate power series to the adic completion of multivariate polynomials with respect to the ideal spanned by all variables when the index is finite.

Equations

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

@[simp]

theorem MvPowerSeries.toAdicCompletionAlgEquiv_apply {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] (p : MvPowerSeries σ R) : (toAdicCompletionAlgEquiv σ R) p = (toAdicCompletion σ R) p

@[simp]

theorem MvPowerSeries.toAdicCompletionAlgEquiv_symm_apply {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] (x : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) : (toAdicCompletionAlgEquiv σ R).symm x = toAdicCompletionInv σ R x