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)
:
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)
:
noncomputable def
MvPowerSeries.truncTotalAlgHom
(σ : Type u_3)
(R : Type u_4)
[Finite σ]
[CommRing 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.
Instances For
@[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
Instances For
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)
:
theorem
MvPowerSeries.toAdicCompletion_coe
{σ : Type u_1}
{R : Type u_2}
[CommRing R]
[Finite σ]
(p : MvPolynomial σ R)
:
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)))
Instances For
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.
Instances For
@[simp]
theorem
MvPowerSeries.toAdicCompletionAlgEquiv_apply
{σ : Type u_1}
{R : Type u_2}
[CommRing R]
[Finite σ]
(p : MvPowerSeries σ R)
:
@[simp]
theorem
MvPowerSeries.toAdicCompletionAlgEquiv_symm_apply
{σ : Type u_1}
{R : Type u_2}
[CommRing R]
[Finite σ]
(x : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
:
noncomputable def
PowerSeries.toMvPowerSeries
{R : Type u_1}
{σ : Type u_2}
[CommSemiring R]
(i : σ)
:
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
Instances For
theorem
PowerSeries.toMvPowerSeries_apply
{R : Type u_1}
{σ : Type u_2}
[CommSemiring R]
{f : PowerSeries R}
(i : σ)
:
@[simp]
theorem
PowerSeries.toMvPowerSeries_C
{R : Type u_1}
{σ : Type u_2}
[CommSemiring R]
(i : σ)
(r : R)
:
@[simp]
theorem
PowerSeries.toMvPowerSeries_injective
{R : Type u_1}
{σ : Type u_2}
[CommSemiring R]
(i : σ)
:
theorem
PowerSeries.toMvPowerSeries_inj
{R : Type u_1}
{σ : Type u_2}
[CommSemiring R]
(i : σ)
{p q : PowerSeries R}
:
theorem
PowerSeries.toMvPowerSeries_eq_subst
{σ : Type u_2}
{R : Type u_4}
[CommRing R]
{f : PowerSeries R}
{i : σ}
:
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)
:
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)
:
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 : σ)
:
@[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)
: