Substitutions in the Monsky–Washnitzer algebra

Let R be an ultrametric normed commutative ring with ‖1‖ = 1, and let a s be polynomials in the variables τ, indexed by finitely many s : σ, without constant term and with all coefficients of norm at most 1. Formal substitution X s ↦ a s then carries overconvergent series to overconvergent series: if f is restricted at a radius ρ > 1 and the a s have total degree at most A, the substitution is restricted at ρ ^ (1 / (A + 1)) > 1. It is therefore an R-algebra homomorphism R⟨X⟩† → R⟨Y⟩† of Monsky–Washnitzer algebras, compatible with the corresponding homomorphism of Tate algebras, and two mutually inverse substitutions give an isomorphism.

Main definitions

• TauCeti.Dagger.washnitzerAlgebra.subst: substitution of unit-ball polynomials without constant term, as an R-algebra homomorphism of Monsky–Washnitzer algebras.
• TauCeti.Dagger.washnitzerAlgebra.substEquiv: the isomorphism given by two mutually inverse substitutions.

Main results

• TauCeti.Dagger.subst_mem_washnitzerAlgebra: substitution of unit-ball polynomials without constant term preserves overconvergence.
• TauCeti.Dagger.washnitzerAlgebra.subst_X and TauCeti.Dagger.washnitzerAlgebra.subst_ofMvPolynomial: the substitution on variables and on polynomials.
• TauCeti.Dagger.washnitzerAlgebra.toTate_subst: compatibility with the substitutions of the Tate algebra.

References

• E. Grosse-Klönne, Rigid analytic spaces with overconvergent structure sheaf, J. reine angew. Math. 519 (2000), §1.3 (iv).

theorem TauCeti.Dagger.subst_mem_washnitzerAlgebra {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] {a : σ → MvPolynomial τ R} (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) {f : MvPowerSeries σ R} (hf : f ∈ washnitzerAlgebra σ R) : MvPowerSeries.subst (fun (s : σ) => ↑(a s)) f ∈ washnitzerAlgebra τ R

Substitution preserves overconvergence. Substituting finitely many polynomials without constant term, whose coefficients have norm at most 1, into an overconvergent series gives an overconvergent series.

noncomputable def TauCeti.Dagger.washnitzerAlgebra.subst {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) : ↥(washnitzerAlgebra σ R) →ₐ[R] ↥(washnitzerAlgebra τ R)

Substitution of unit-ball polynomials as a map of Monsky–Washnitzer algebras. Substituting polynomials without constant term whose coefficients have norm at most 1 is an R-algebra homomorphism R⟨X⟩† → R⟨Y⟩†.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.coe_subst {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) (f : ↥(washnitzerAlgebra σ R)) : ↑((subst a ha₀ ha₁) f) = MvPowerSeries.subst (fun (s : σ) => ↑(a s)) ↑f

The map of Monsky–Washnitzer algebras is Mathlib's formal substitution.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.subst_X {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) (s : σ) : (subst a ha₀ ha₁) (X σ R s) = (ofMvPolynomial τ R) (a s)

Substitution sends the variable Xₛ to the polynomial a s.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.subst_ofMvPolynomial {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) (p : MvPolynomial σ R) : (subst a ha₀ ha₁) ((ofMvPolynomial σ R) p) = (ofMvPolynomial τ R) ((MvPolynomial.aeval a) p)

Substitution sends a polynomial p to the polynomial p(a).

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.toTate_subst {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) (f : ↥(washnitzerAlgebra σ R)) : (toTate τ R) ((subst a ha₀ ha₁) f) = (MvPowerSeries.restrictedSubst a ha₀ ha₁) ((toTate σ R) f)

Substitution commutes with the inclusions into the Tate algebras.

noncomputable def TauCeti.Dagger.washnitzerAlgebra.substEquiv {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R) (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0) (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1) (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s) (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) : ↥(washnitzerAlgebra σ R) ≃ₐ[R] ↥(washnitzerAlgebra τ R)

Isomorphisms of Monsky–Washnitzer algebras from inverse substitutions. If two families of unit-ball polynomials without constant term are inverse to each other under substitution, the substitutions are mutually inverse R-algebra isomorphisms R⟨X⟩† ≃ R⟨Y⟩†.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.coe_substEquiv {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R) (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0) (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1) (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s) (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) (f : ↥(washnitzerAlgebra σ R)) : ↑((substEquiv a ha₀ ha₁ b hb₀ hb₁ hab hba) f) = MvPowerSeries.subst (fun (s : σ) => ↑(a s)) ↑f

The isomorphism of Monsky–Washnitzer algebras is the substitution of a.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.coe_substEquiv_symm {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R) (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0) (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1) (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s) (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) (f : ↥(washnitzerAlgebra τ R)) : ↑((substEquiv a ha₀ ha₁ b hb₀ hb₁ hab hba).symm f) = MvPowerSeries.subst (fun (t : τ) => ↑(b t)) ↑f

The inverse isomorphism of Monsky–Washnitzer algebras is the substitution of b.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.substEquiv_X {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R) (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0) (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1) (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s) (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) (s : σ) : (substEquiv a ha₀ ha₁ b hb₀ hb₁ hab hba) (X σ R s) = (ofMvPolynomial τ R) (a s)

The isomorphism of Monsky–Washnitzer algebras sends the variable Xₛ to a s.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.substEquiv_symm_X {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R) (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0) (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1) (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s) (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) (t : τ) : (substEquiv a ha₀ ha₁ b hb₀ hb₁ hab hba).symm (X τ R t) = (ofMvPolynomial σ R) (b t)

The inverse isomorphism of Monsky–Washnitzer algebras sends the variable Xₜ to b t.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.toTate_substEquiv {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R) (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0) (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1) (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s) (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) (f : ↥(washnitzerAlgebra σ R)) : (toTate τ R) ((substEquiv a ha₀ ha₁ b hb₀ hb₁ hab hba) f) = (MvPowerSeries.restrictedSubstEquiv a ha₀ ha₁ b hb₀ hb₁ hab hba) ((toTate σ R) f)

The isomorphism of Monsky–Washnitzer algebras is the restriction of the isomorphism of Tate algebras given by the same substitutions.