Restricted series in two families of variables #
For positive polyradii c on σ and d on τ, a power series in σ ⊕ τ is restricted at the
polyradii Sum.elim c d exactly when, viewed through MvPowerSeries.sumAlgEquiv as a
power series in σ over power series in τ, each coefficient is restricted at d and the
Gauss norms of these coefficients make the series restricted at c. This identifies
R{X/c, Y/d} ≅ R{Y/d}{X/c}
as normed rings, with the Gauss norms on both sides. Unlike
MvPowerSeries.restrictedOptionEquiv, which separates a single variable into a univariate
series, both families of variables are arbitrary. Arbitrary radii are needed to present
restricted series over a quotient of a ring of restricted series, as in Kedlaya's proof that the
interval rings of the Fargues–Fontaine curve are strongly noetherian.
Main results #
TauCeti.MvPowerSeries.isRestricted_coeff_sumAlgEquiv: the coefficients inσof a restricted series inσ ⊕ τare restricted series inτ.TauCeti.MvPowerSeries.restrictedSumEquiv: the ring isomorphismR{X/c, Y/d} ≃+* R{Y/d}{X/c}, andTauCeti.MvPowerSeries.restrictedSumAlgEquiv: the same map as an algebra isomorphism over every algebraSof coefficients.TauCeti.MvPowerSeries.coeff_coeff_restrictedSumEquivandTauCeti.MvPowerSeries.coeff_restrictedSumEquiv_symm: its coefficients.TauCeti.MvPowerSeries.norm_restrictedSumEquivandTauCeti.MvPowerSeries.isometry_restrictedSumEquiv: it preserves the Gauss norms.TauCeti.MvPowerSeries.map_subtype_restrictedSumEquiv: on the underlying formal series it isMvPowerSeries.sumAlgEquiv.TauCeti.MvPowerSeries.restrictedSumEquiv_X_inl,TauCeti.MvPowerSeries.restrictedSumEquiv_X_inrandTauCeti.MvPowerSeries.restrictedSumEquiv_polynomialToRestricted: its values on the variables and on polynomials.TauCeti.MvPowerSeries.restrictedSumAssocandTauCeti.MvPowerSeries.map_restrictedSumEquiv_restrictedSumAssoc: reassociating three families of variables, and the associativity of iteration.TauCeti.MvPowerSeries.restrictedSumCongrandTauCeti.MvPowerSeries.coe_restrictedSumEquiv_restrictedSumCongr: renaming each family of variables, and the compatibility of iteration with these renamings.
Its compatibility with bounded coefficient maps is
TauCeti.MvPowerSeries.coe_restrictedSumEquiv_restrictedMap, in
TauCeti.RingTheory.MvPowerSeries.TateAlgebra.Map.
References #
- Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.1.
- K. S. Kedlaya, Noetherian properties of Fargues–Fontaine curves, IMRN 2016, no. 8, 2544–2567; arXiv:1410.5160v3, Theorem 4.10 and Remark 4.11.
Each coefficient of a restricted series in σ ⊕ τ, viewed as a series in σ over series in
τ, is restricted.
Restricted series in σ ⊕ τ are restricted series in σ over restricted series in τ.
For positive polyradii c and d, this is the ring isomorphism R{X/c, Y/d} ≃+* R{Y/d}{X/c}
induced by MvPowerSeries.sumAlgEquiv. No completeness of R and no finiteness of σ
or τ is needed.
Instances For
The coefficients of restrictedSumEquiv: the coefficient of yᵇ in the coefficient of xᵃ
of the image of f is the coefficient of xᵃ yᵇ in f.
The coefficients of the inverse of restrictedSumEquiv: the coefficient of xᵃ yᵇ is the
coefficient of yᵇ in the coefficient of xᵃ.
restrictedSumEquiv sends constants to constants: the constant r in σ ⊕ τ goes to the
constant series in σ whose value is the constant r in τ.
Iteration of restricted series as an algebra isomorphism: over every algebra S of
coefficients, restrictedSumEquiv is an S-algebra isomorphism R{X/c, Y/d} ≃ₐ[S] R{Y/d}{X/c}.
Instances For
restrictedSumAlgEquiv has the same underlying map as restrictedSumEquiv.
restrictedSumEquiv preserves the Gauss norms.
restrictedSumEquiv is an isometry for the Gauss norms.
On the underlying formal series, restrictedSumEquiv is MvPowerSeries.sumAlgEquiv.
restrictedSumEquiv sends a variable of the first family to the corresponding variable.
restrictedSumEquiv sends a variable of the second family to the corresponding constant.
restrictedSumEquiv is compatible with the polynomial inclusions: a polynomial in σ ⊕ τ goes
to the polynomial in σ whose coefficients are its coefficients in τ, read through
MvPolynomial.sumAlgEquiv.
Renaming and reassociating the families of variables #
Reassociating three families of variables. Renaming along Equiv.sumAssoc is an
R-algebra isomorphism R{(X, Y)/(c, d), Z/ρ} ≃ R{X/c, (Y, Z)/(d, ρ)}, preserving the Gauss
norms.
Instances For
restrictedSumAssoc renames the underlying series along Equiv.sumAssoc.
restrictedSumAssoc preserves the Gauss norms.
restrictedSumAssoc is an isometry for the Gauss norms.
Iteration is associative. Separating the last family Z from R{X/c, Y/d, Z/ρ} and then
Y from the remaining outer family (X, Y), over the coefficient ring R{Z/ρ}, gives the same
series in X over R{Z/ρ}{Y/d} as reassociating, separating (Y, Z) and then separating Z
coefficientwise.
Renaming each family of variables. For e₁ : σ' ≃ σ and e₂ : τ' ≃ τ, renaming along
Equiv.sumCongr e₁ e₂ is an R-algebra isomorphism R{X'/(c ∘ e₁), Y'/(d ∘ e₂)} ≃ R{X/c, Y/d},
preserving the Gauss norms.
Instances For
restrictedSumCongr renames the underlying series along Equiv.sumCongr.
restrictedSumCongr preserves the Gauss norms.
restrictedSumCongr is an isometry for the Gauss norms.
Iteration commutes with renaming. Renaming both families and then separating Y is
separating Y' first, renaming the coefficients along e₂ and then the outer variables along
e₁.