Equivalences related to power series rings

This file establishes a number of equivalences related to power series rings and is patterned after Mathlib/Algebra/MvPolynomial/Equiv.lean.

• MvPowerSeries.isEmptyEquiv : The isomorphism between multivariable power series in no variables and the ground ring.

• MvPowerSeries.optionEquivLeft : The isomorphism between multivariable power series in Option σ and power series with coefficients in MvPowerSeries σ R.

• MvPowerSeries.finSuccEquiv : The isomorphism between multivariable power series in Fin (n + 1) and power series over multivariable power series in Fin n.

• 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.

noncomputable def MvPowerSeries.isEmptyEquiv (σ : Type u_1) (R : Type u_2) [CommSemiring R] [IsEmpty σ] : MvPowerSeries σ R ≃ₐ[R] R

The isomorphism between multivariable power series in no variables and the ground ring.

Equations

• MvPowerSeries.isEmptyEquiv σ R = { toFun := (↑↑MvPowerSeries.constantCoeff).toFun, invFun := ⇑MvPowerSeries.C, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem MvPowerSeries.isEmptyEquiv_symm_apply (σ : Type u_1) (R : Type u_2) [CommSemiring R] [IsEmpty σ] (a : R) : (isEmptyEquiv σ R).symm a = C a

@[simp]

theorem MvPowerSeries.isEmptyEquiv_apply (σ : Type u_1) (R : Type u_2) [CommSemiring R] [IsEmpty σ] (a✝ : MvPowerSeries σ R) : (isEmptyEquiv σ R) a✝ = constantCoeff a✝

noncomputable def MvPowerSeries.optionEquivLeft (σ : Type u_1) (R : Type u_2) [CommSemiring R] : MvPowerSeries (Option σ) R ≃ₐ[R] PowerSeries (MvPowerSeries σ R)

The algebra isomorphism between multivariable power series in Option σ and power series with coefficients in MvPowerSeries σ R.

Equations

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

theorem MvPowerSeries.coeff_coeff_optionEquivLeft {σ : Type u_1} {R : Type u_2} [CommSemiring R] (p : MvPowerSeries (Option σ) R) (n : ℕ) (x : σ →₀ ℕ) : (coeff x) ((PowerSeries.coeff n) ((optionEquivLeft σ R) p)) = (coeff (Finsupp.optionElim n x)) p

theorem MvPowerSeries.optionEquivLeft_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : Option σ →₀ ℕ) (r : R) : (optionEquivLeft σ R) ((monomial x) r) = (PowerSeries.monomial (x none)) ((monomial x.some) r)

@[simp]

theorem MvPowerSeries.optionEquivLeft_X_some {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) : (optionEquivLeft σ R) (X (some i)) = PowerSeries.C (X i)

@[simp]

theorem MvPowerSeries.optionEquivLeft_X_none {σ : Type u_1} {R : Type u_2} [CommSemiring R] : (optionEquivLeft σ R) (X none) = PowerSeries.X

@[simp]

theorem MvPowerSeries.optionEquivLeft_C {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : R) : (optionEquivLeft σ R) (C r) = PowerSeries.C (C r)

noncomputable def MvPowerSeries.finSuccEquiv (R : Type u_2) [CommSemiring R] (n : ℕ) : MvPowerSeries (Fin (n + 1)) R ≃ₐ[R] PowerSeries (MvPowerSeries (Fin n) R)

The algebra isomorphism between multivariable power series in Fin (n + 1) and power series over multivariable power series in Fin n.

Equations

• MvPowerSeries.finSuccEquiv R n = (MvPowerSeries.renameEquiv R (finSuccEquiv n)).trans (MvPowerSeries.optionEquivLeft (Fin n) R)

theorem MvPowerSeries.coeff_coeff_finSuccEquiv {R : Type u_2} [CommSemiring R] {n : ℕ} (p : MvPowerSeries (Fin (n + 1)) R) {k : ℕ} {x : Fin n →₀ ℕ} : (coeff x) ((PowerSeries.coeff k) ((finSuccEquiv R n) p)) = (coeff (Finsupp.cons k x)) p

@[simp]

theorem MvPowerSeries.finSuccEquiv_X_zero {R : Type u_2} [CommSemiring R] {n : ℕ} : (finSuccEquiv R n) (X 0) = PowerSeries.X

@[simp]

theorem MvPowerSeries.finSuccEquiv_X_succ {R : Type u_2} [CommSemiring R] {n : ℕ} (j : Fin n) : (finSuccEquiv R n) (X j.succ) = PowerSeries.C (X j)

@[simp]

theorem MvPowerSeries.finSuccEquiv_C {R : Type u_2} [CommSemiring R] {n : ℕ} (r : R) : (finSuccEquiv R n) (C r) = PowerSeries.C (C r)

theorem MvPowerSeries.finSuccEquiv_comp_C {R : Type u_2} [CommSemiring R] {n : ℕ} : (finSuccEquiv R n).symm.toRingEquiv.toRingHom.comp (PowerSeries.C.comp C) = C

instance MvPowerSeries.isNoetherianRing {σ : Type u_1} (S : Type u_3) [CommRing S] [IsNoetherianRing S] [Finite σ] : IsNoetherianRing (MvPowerSeries σ S)

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 m) p - (truncTotal 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 n) (p * q) - (truncTotal n) p * (truncTotal 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 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 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 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

noncomputable def PowerSeries.toMvPowerSeries {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) : PowerSeries R →ₐ[R] MvPowerSeries σ R

Given a power series p : R⟦X⟧ and an index i, we may view it as a multivariate power series toMvPowerSeries i p : MvPowerSeries σ R.

Equations

• PowerSeries.toMvPowerSeries i = MvPowerSeries.rename fun (x : Unit) => i

theorem PowerSeries.toMvPowerSeries_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] {f : PowerSeries R} (i : σ) : (toMvPowerSeries i) f = (MvPowerSeries.rename fun (x : Unit) => i) f

@[simp]

theorem PowerSeries.toMvPowerSeries_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (r : R) : (toMvPowerSeries i) (C r) = MvPowerSeries.C r

@[simp]

theorem PowerSeries.toMvPowerSeries_X {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) : (toMvPowerSeries i) X = MvPowerSeries.X i

theorem PowerSeries.toMvPowerSeries_injective {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) : Function.Injective ⇑(toMvPowerSeries i)

theorem PowerSeries.toMvPowerSeries_inj {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) {p q : PowerSeries R} : (toMvPowerSeries i) p = (toMvPowerSeries i) q ↔ p = q

theorem PowerSeries.toMvPowerSeries_eq_subst {σ : Type u_2} {R : Type u_4} [CommRing R] {f : PowerSeries R} {i : σ} : (toMvPowerSeries i) f = subst (MvPowerSeries.X i) f

theorem PowerSeries.subst_toMvPowerSeries {σ : Type u_2} {τ : Type u_3} {R : Type u_4} [CommRing R] {f : PowerSeries R} {i : σ} {a : σ → MvPowerSeries τ R} (ha : MvPowerSeries.HasSubst a) : MvPowerSeries.subst a ((toMvPowerSeries i) f) = subst (a i) f

theorem PowerSeries.toMvPowerSeries_coeff_eq_zero {σ : Type u_2} {R : Type u_4} [CommRing R] {f : PowerSeries R} {i : σ} {d : σ →₀ ℕ} (hd : d i = 0) (hf : constantCoeff f = 0) : (MvPowerSeries.coeff d) ((toMvPowerSeries i) f) = 0

theorem MvPowerSeries.HasSubst.toMvPowerSeries {σ : Type u_2} {R : Type u_4} [CommRing R] {f : PowerSeries R} (hf : PowerSeries.constantCoeff f = 0) : HasSubst fun (x : σ) => (PowerSeries.toMvPowerSeries x) f

@[simp]

theorem MvPowerSeries.rename_comp_toMvPowerSeries {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] (f : σ → τ) [Filter.TendstoCofinite f] (a : σ) : (rename f).comp (PowerSeries.toMvPowerSeries a) = PowerSeries.toMvPowerSeries (f a)

@[simp]

theorem MvPowerSeries.rename_toMvPowerSeries {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [CommSemiring R] (f : σ → τ) [Filter.TendstoCofinite f] (a : σ) (p : PowerSeries R) : (rename f) ((PowerSeries.toMvPowerSeries a) p) = (PowerSeries.toMvPowerSeries (f a)) p