Derivatives of overconvergent power series

Over an ultrametric normed commutative ring R, the Hasse derivative

∂^d (∑ₘ aₘ Xᵐ) = ∑ₘ (∏ⱼ (mⱼ + dⱼ choose dⱼ)) aₘ₊d Xᵐ

preserves restrictedness at every positive radius, with the Cauchy estimate ρᵈ ‖∂^d f‖_ρ ≤ ‖f‖_ρ for the Gauss norms (MvPowerSeries.IsRestricted.hasseDeriv, MvPowerSeries.norm_restrictedHasseDeriv_le). Since this holds at each radius ρ > 1 separately, Hasse derivatives, and in particular the partial derivatives ∂/∂Xᵢ = ∂^(eᵢ), preserve the Monsky–Washnitzer algebra W = R⟨X⟩† of overconvergent series. Only natural-number multiples of coefficients occur, so no assumption on the characteristic is needed. The identity k! • ∂^(k eᵢ) = (∂/∂Xᵢ)^[k] holds over every R; when k! is invertible in R it exhibits ∂^(k eᵢ) as (∂/∂Xᵢ)ᵏ / k!, but in characteristic p this division is not available for k ≥ p while ∂^(k eᵢ) still is.

The partial derivatives are packaged as R-derivations of W. They are the derivations through which the differential dg = ∑ᵢ (∂g/∂Xᵢ) dXᵢ of the overconvergent de Rham complex is written. The Hasse derivatives ∂^d are R-linear endomorphisms of W satisfying k! • ∂^(k eᵢ) = (∂/∂Xᵢ)^[k], and they remain available in characteristic p.

Main definitions

• TauCeti.Dagger.washnitzerAlgebra.hasseDeriv d: the d-th Hasse derivative, an R-linear endomorphism of W.
• TauCeti.Dagger.washnitzerAlgebra.pderiv i: the partial derivative ∂/∂Xᵢ, an R-derivation of W.

Main results

• TauCeti.Dagger.hasseDeriv_mem_washnitzerAlgebra and TauCeti.Dagger.pderiv_mem_washnitzerAlgebra: Hasse and partial derivatives of overconvergent series are overconvergent.
• TauCeti.Dagger.washnitzerAlgebra.toTate_hasseDeriv and TauCeti.Dagger.washnitzerAlgebra.norm_toTate_hasseDeriv_le: the inclusion into the Tate algebra intertwines the Hasse derivatives, which do not increase the Gauss norm.
• TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_mul: the Leibniz rule ∂^d (f g) = ∑_{a + b = d} ∂^a f · ∂^b g, and TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_comp: the composition rule, from which TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_comm shows that Hasse derivatives commute.
• TauCeti.Dagger.washnitzerAlgebra.factorial_smul_hasseDeriv_single: k! • ∂^(k eᵢ) f = (∂/∂Xᵢ)^[k] f.
• TauCeti.Dagger.washnitzerAlgebra.pderiv_X: ∂Xⱼ/∂Xᵢ = δᵢⱼ, and TauCeti.Dagger.washnitzerAlgebra.pderiv_ofMvPolynomial: on polynomials the partial derivatives are the polynomial ones.
• TauCeti.Dagger.washnitzerAlgebra.pderiv_primitive: over a field of characteristic zero, ∂/∂Xᵢ is a left inverse of the termwise primitive in Xᵢ.
• TauCeti.Dagger.washnitzerAlgebra.derivation_ext: over a complete ultrametric field, two derivations of W in finitely many variables into a finite module agreeing on the variables are equal.

References

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

theorem TauCeti.Dagger.hasseDeriv_mem_washnitzerAlgebra {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {f : MvPowerSeries σ R} (hf : f ∈ washnitzerAlgebra σ R) (d : σ →₀ ℕ) : (MvPowerSeries.hasseDeriv d) f ∈ washnitzerAlgebra σ R

Hasse derivatives of overconvergent series are overconvergent. See MvPowerSeries.IsRestricted.hasseDeriv for the radius-by-radius version.

theorem TauCeti.Dagger.pderiv_mem_washnitzerAlgebra {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {f : MvPowerSeries σ R} (hf : f ∈ washnitzerAlgebra σ R) (i : σ) : (MvPowerSeries.pderiv i) f ∈ washnitzerAlgebra σ R

Partial derivatives of overconvergent series are overconvergent.

noncomputable def TauCeti.Dagger.washnitzerAlgebra.hasseDeriv (σ : Type u_1) (R : Type u_2) [NormedCommRing R] [IsUltrametricDist R] (d : σ →₀ ℕ) : ↥(washnitzerAlgebra σ R) →ₗ[R] ↥(washnitzerAlgebra σ R)

The d-th Hasse derivative ∂^d, as an R-linear endomorphism of the Monsky–Washnitzer algebra.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.coe_hasseDeriv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (d : σ →₀ ℕ) (f : ↥(washnitzerAlgebra σ R)) : ↑((hasseDeriv σ R d) f) = (MvPowerSeries.hasseDeriv d) ↑f

The Hasse derivative in W is the Hasse derivative of the underlying series.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_zero {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] : hasseDeriv σ R 0 = LinearMap.id

The Hasse derivative of order zero is the identity.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_one {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {d : σ →₀ ℕ} (hd : d ≠ 0) : (hasseDeriv σ R d) 1 = 0

Every Hasse derivative of positive order kills the constant 1 of W.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_algebraMap {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {d : σ →₀ ℕ} (hd : d ≠ 0) (a : R) : (hasseDeriv σ R d) ((algebraMap R ↥(washnitzerAlgebra σ R)) a) = 0

Every Hasse derivative of positive order kills the constants of W.

noncomputable def TauCeti.Dagger.washnitzerAlgebra.pderiv (σ : Type u_1) (R : Type u_2) [NormedCommRing R] [IsUltrametricDist R] (i : σ) : Derivation R ↥(washnitzerAlgebra σ R) ↥(washnitzerAlgebra σ R)

The partial derivative ∂/∂Xᵢ, as an R-derivation of the Monsky–Washnitzer algebra.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.coe_pderiv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (i : σ) (f : ↥(washnitzerAlgebra σ R)) : ↑((pderiv σ R i) f) = (MvPowerSeries.pderiv i) ↑f

The partial derivative in W is the partial derivative of the underlying series.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_single_one {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (i : σ) (f : ↥(washnitzerAlgebra σ R)) : (hasseDeriv σ R (Finsupp.single i 1)) f = (pderiv σ R i) f

The first Hasse derivative in Xᵢ is the partial derivative in Xᵢ.

theorem TauCeti.Dagger.washnitzerAlgebra.factorial_smul_hasseDeriv_single {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (i : σ) (k : ℕ) (f : ↥(washnitzerAlgebra σ R)) : k.factorial • (hasseDeriv σ R (Finsupp.single i k)) f = (⇑(pderiv σ R i))^[k] f

k! times the Hasse derivative ∂^(k eᵢ) is the k-th iterated partial derivative in Xᵢ: k! • ∂^(k eᵢ) f = (∂/∂Xᵢ)^[k] f.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.pderiv_hasseDeriv_single {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (i : σ) (k : ℕ) (f : ↥(washnitzerAlgebra σ R)) : (pderiv σ R i) ((hasseDeriv σ R (Finsupp.single i k)) f) = (k + 1) • (hasseDeriv σ R (Finsupp.single i (k + 1))) f

Differentiating ∂^(k eᵢ) f in Xᵢ gives (k + 1) ∂^((k + 1) eᵢ) f in W.

theorem TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_mul {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [DecidableEq σ] (d : σ →₀ ℕ) (f g : ↥(washnitzerAlgebra σ R)) : (hasseDeriv σ R d) (f * g) = ∑ x ∈ Finset.antidiagonal d, (hasseDeriv σ R x.1) f * (hasseDeriv σ R x.2) g

The Leibniz rule for Hasse derivatives in W: ∂^d (f g) = ∑_{a + b = d} ∂^a f · ∂^b g.

theorem TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_comp {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (a b : σ →₀ ℕ) : hasseDeriv σ R a ∘ₗ hasseDeriv σ R b = (a.prod fun (j : σ) (k : ℕ) => (k + b j).choose k) • hasseDeriv σ R (a + b)

The composition rule for Hasse derivatives in W: ∂^a ∘ ∂^b = (∏ⱼ (aⱼ + bⱼ choose aⱼ)) • ∂^(a + b).

theorem TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_comm {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (a b : σ →₀ ℕ) : hasseDeriv σ R a ∘ₗ hasseDeriv σ R b = hasseDeriv σ R b ∘ₗ hasseDeriv σ R a

Hasse derivatives in W commute: ∂^a ∘ ∂^b = ∂^b ∘ ∂^a.

theorem TauCeti.Dagger.washnitzerAlgebra.pderiv_comm {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (i j : σ) (f : ↥(washnitzerAlgebra σ R)) : (pderiv σ R i) ((pderiv σ R j) f) = (pderiv σ R j) ((pderiv σ R i) f)

Partial derivatives of overconvergent series commute.

theorem TauCeti.Dagger.washnitzerAlgebra.forall_pderiv_eq_zero_iff {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [HasUniqueDiv R] (g : ↥(washnitzerAlgebra σ R)) : (∀ (i : σ), (pderiv σ R i) g = 0) ↔ ∃ (c : R), (algebraMap R ↥(washnitzerAlgebra σ R)) c = g

Over a torsion-free coefficient ring, an overconvergent function has all partial derivatives zero exactly when it is a scalar. This also holds for an infinite variable type.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.hasseDeriv_ofMvPolynomial {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (d : σ →₀ ℕ) (p : MvPolynomial σ R) : (hasseDeriv σ R d) ((ofMvPolynomial σ R) p) = (ofMvPolynomial σ R) ((MvPolynomial.hasseDeriv d) p)

Hasse derivatives of polynomials in W are the polynomial Hasse derivatives.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.pderiv_ofMvPolynomial {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (i : σ) (p : MvPolynomial σ R) : (pderiv σ R i) ((ofMvPolynomial σ R) p) = (ofMvPolynomial σ R) ((MvPolynomial.pderiv i) p)

Partial derivatives of polynomials in W are the polynomial partial derivatives.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.pderiv_X_self {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (i : σ) : (pderiv σ R i) (X σ R i) = 1

The partial derivative of Xᵢ in Xᵢ is 1.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.pderiv_X_of_ne {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {i j : σ} (h : j ≠ i) : (pderiv σ R i) (X σ R j) = 0

The partial derivative of Xⱼ in Xᵢ is 0 for j ≠ i.

theorem TauCeti.Dagger.washnitzerAlgebra.pderiv_X {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [DecidableEq σ] (i j : σ) : (pderiv σ R i) (X σ R j) = Pi.single i 1 j

The partial derivatives of the variables: ∂Xⱼ/∂Xᵢ = δᵢⱼ.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.toTate_hasseDeriv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (d : σ →₀ ℕ) (f : ↥(washnitzerAlgebra σ R)) : (toTate σ R) ((hasseDeriv σ R d) f) = (MvPowerSeries.restrictedHasseDeriv d) ((toTate σ R) f)

The inclusion into the Tate algebra intertwines the Hasse derivatives of W and of the unit-radius Tate algebra.

theorem TauCeti.Dagger.washnitzerAlgebra.norm_toTate_hasseDeriv_le {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (d : σ →₀ ℕ) (f : ↥(washnitzerAlgebra σ R)) : ‖(toTate σ R) ((hasseDeriv σ R d) f)‖ ≤ ‖(toTate σ R) f‖

The Cauchy estimate at unit radius: Hasse derivatives do not increase the Gauss norm of an overconvergent series.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.pderiv_primitive {σ : Type u_3} {K : Type u_4} [NormedField K] [IsUltrametricDist K] [CharZero K] (i : σ) (f : ↥(washnitzerAlgebra σ K)) : (pderiv σ K i) ((primitive σ K i) f) = f

The derivative of the primitive: in W, ∂/∂Xᵢ (∫ f dXᵢ) = f.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.pderiv_primitive_of_ne {σ : Type u_3} {K : Type u_4} [NormedField K] [IsUltrametricDist K] [CharZero K] {i j : σ} (hij : i ≠ j) (f : ↥(washnitzerAlgebra σ K)) : (pderiv σ K j) ((primitive σ K i) f) = (primitive σ K i) ((pderiv σ K j) f)

Differentiation in another variable commutes with termwise integration in W.

theorem TauCeti.Dagger.washnitzerAlgebra.derivation_ext {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_4} [Finite σ] {M : Type u_5} [AddCommGroup M] [Module (↥(washnitzerAlgebra σ K)) M] [Module K M] [Module.Finite (↥(washnitzerAlgebra σ K)) M] {D₁ D₂ : Derivation K (↥(washnitzerAlgebra σ K)) M} (h : ∀ (i : σ), D₁ (X σ K i) = D₂ (X σ K i)) : D₁ = D₂

Derivations into finite modules are determined by the variables. Two K-derivations of the Monsky–Washnitzer algebra in finitely many variables into a finite module are equal as soon as they agree on the variables.