Documentation

TauCeti.RingTheory.Dagger.Distinguished

Distinguished overconvergent series #

Let R be an ultrametric normed commutative ring with ‖1‖ = 1. The triangular substitution Y ↦ Y, Xᵢ ↦ Xᵢ + Y ^ α i, with Y = X none, is an automorphism of the Monsky–Washnitzer algebra R⟨X, Y⟩†. Over a complete nonarchimedean field K, a suitable such automorphism makes any nonzero overconvergent series f distinguished in Y: written as a series in Y over the Tate algebra in the remaining variables, its image is distinguished of some degree s at radius 1, and its coefficient in degree s is a unit. This is the change of variables that precedes Weierstrass division and preparation in K⟨X, Y⟩†. The automorphism is the restriction of the corresponding automorphism of the Tate algebra, so the statement follows from the Tate algebra case TauCeti.MvPowerSeries.exists_restrictedTriangularEquiv_isDistinguished_isUnit.

Separating Y writes a series in W = K⟨X, Y⟩† as g = ∑ₘ gₘ Yᵐ with coefficients gₘ in the variables σ. At unit radius this is MvPowerSeries.restrictedOptionEquiv, and g is Y-distinguished of degree s when this series over the Tate algebra in σ is TauCeti.PowerSeries.IsDistinguished of degree s at radius 1 with a unit coefficient g_s.

Weierstrass division by such a g must stay inside W. It therefore has to take place over a ring of series restricted at some radius ρ > 1 in the variables σ, at some radius r > 1 in Y. Distinguishedness does not persist to a common radius ρ = r > 1: Y + X² is Y-distinguished of degree 1 at unit radius, but ‖X²‖_ρ = ρ² > ρ = ‖1‖_ρ ρ for all ρ > 1. This file proves that unequal radii work. For every g as above there are radii 1 < ρ ≤ r, as close to 1 as desired, such that g is restricted at r and ∑ₘ gₘ Yᵐ is distinguished of degree s at radius r over the series restricted at ρ, with g_s a unit there.

In one variable, distinguishedness of a fixed degree at unit radius persists to a radius strictly greater than one, over any ultrametric normed commutative ring.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.Dagger.washnitzerAlgebra.triangularEquiv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (α : σ → ℕ) (hα : ∀ (i : σ), α i ≠ 0) :
↥(washnitzerAlgebra (Option σ) R) ≃ₐ[R] ↥(washnitzerAlgebra (Option σ) R)

The triangular automorphism Y ↦ Y, Xᵢ ↦ Xᵢ + Y ^ α i of the Monsky–Washnitzer algebra in the variables Option σ, where Y is the variable none and the exponents α are positive. Its inverse is Xᵢ ↦ Xᵢ - Y ^ α i.

Instances For
    source
    @[simp]
    theorem TauCeti.Dagger.washnitzerAlgebra.triangularEquiv_X_none {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (α : σ → ℕ) (hα : ∀ (i : σ), α i ≠ 0) :
    (triangularEquiv α hα) (X (Option σ) R none) = X (Option σ) R none

    The triangular automorphism fixes the variable Y.

    source
    @[simp]
    theorem TauCeti.Dagger.washnitzerAlgebra.triangularEquiv_X_some {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (α : σ → ℕ) (hα : ∀ (i : σ), α i ≠ 0) (i : σ) :
    (triangularEquiv α hα) (X (Option σ) R (some i)) = X (Option σ) R (some i) + X (Option σ) R none ^ α i

    The triangular automorphism sends Xᵢ to Xᵢ + Y ^ α i.

    source
    @[simp]
    theorem TauCeti.Dagger.washnitzerAlgebra.triangularEquiv_symm_X_none {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (α : σ → ℕ) (hα : ∀ (i : σ), α i ≠ 0) :
    (triangularEquiv α hα).symm (X (Option σ) R none) = X (Option σ) R none

    The inverse triangular automorphism fixes the variable Y.

    source
    @[simp]
    theorem TauCeti.Dagger.washnitzerAlgebra.triangularEquiv_symm_X_some {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (α : σ → ℕ) (hα : ∀ (i : σ), α i ≠ 0) (i : σ) :
    (triangularEquiv α hα).symm (X (Option σ) R (some i)) = X (Option σ) R (some i) - X (Option σ) R none ^ α i

    The inverse triangular automorphism sends Xᵢ to Xᵢ - Y ^ α i.

    source
    @[simp]
    theorem TauCeti.Dagger.washnitzerAlgebra.toTate_triangularEquiv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (α : σ → ℕ) (hα : ∀ (i : σ), α i ≠ 0) (f : ↥(washnitzerAlgebra (Option σ) R)) :
    (toTate (Option σ) R) ((triangularEquiv α hα) f) = (MvPowerSeries.restrictedTriangularEquiv α hα) ((toTate (Option σ) R) f)

    The triangular automorphism of the Monsky–Washnitzer algebra is the restriction of the triangular automorphism of the Tate algebra.

    source
    @[simp]
    theorem TauCeti.Dagger.washnitzerAlgebra.norm_triangularEquiv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (α : σ → ℕ) (hα : ∀ (i : σ), α i ≠ 0) (f : ↥(washnitzerAlgebra (Option σ) R)) :
    ‖(triangularEquiv α hα) f‖ = ‖f‖

    The triangular automorphism preserves the Gauss norm.

    source
    theorem TauCeti.Dagger.washnitzerAlgebra.exists_triangularEquiv_isDistinguished_isUnit {σ : Type u_1} {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [Finite σ] (f : ↥(washnitzerAlgebra (Option σ) K)) (hf : f ≠ 0) :
    ∃ (α : σ → ℕ) (hα : ∀ (i : σ), α i ≠ 0) (s : ℕ), PowerSeries.IsDistinguished 1 s ↑(MvPowerSeries.restrictedOptionEquiv ((toTate (Option σ) K) ((triangularEquiv α hα) f))) ∧ IsUnit ((PowerSeries.coeff s) ↑(MvPowerSeries.restrictedOptionEquiv ((toTate (Option σ) K) ((triangularEquiv α hα) f))))

    Distinguishing automorphisms of Monsky–Washnitzer algebras. Over a complete nonarchimedean field K, every nonzero overconvergent series f in the variables Option σ, for finite σ, is carried by a triangular automorphism Y ↦ Y, Xᵢ ↦ Xᵢ + Y ^ α i of K⟨X, Y⟩† to a series which, as a restricted series in the variable Y = none over the Tate algebra in the variables σ, is distinguished of some degree s at radius 1 with a unit coefficient in degree s.

    source
    theorem TauCeti.Dagger.exists_isDistinguished_of_isDistinguished_one {R : Type u_4} [NormedCommRing R] [IsUltrametricDist R] {f : ↥(washnitzerAlgebra Unit R)} {s : ℕ} (hf : PowerSeries.IsDistinguished 1 s ↑f) {ρ₀ : ℝ} (hρ₀ : 1 < ρ₀) :
    ∃ ρ > 1, ρ ≤ ρ₀ ∧ PowerSeries.IsRestricted ρ ↑f ∧ PowerSeries.IsDistinguished ρ s ↑f

    A one-variable overconvergent series distinguished at radius one remains distinguished of the same degree at some radius greater than one, within any prescribed upper bound.

    source
    theorem TauCeti.Dagger.exists_isDistinguished_isUnit_of_isDistinguished_one {σ : Type u_1} {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {g : ↥(washnitzerAlgebra (Option σ) K)} {s : ℕ} (hg : PowerSeries.IsDistinguished 1 s ↑(MvPowerSeries.restrictedOptionEquiv ((washnitzerAlgebra.toTate (Option σ) K) g))) (hu : IsUnit ((PowerSeries.coeff s) ↑(MvPowerSeries.restrictedOptionEquiv ((washnitzerAlgebra.toTate (Option σ) K) g)))) {ρ₀ : ℝ} (hρ₀ : 1 < ρ₀) :
    ∃ (ρ : ℝ) (x : Fact (0 < ρ)) (r : ℝ), 1 < ρ ∧ ρ ≤ r ∧ r ≤ ρ₀ ∧ MvPowerSeries.IsRestricted (fun (x : Option σ) => r) ↑g ∧ ∃ (G : PowerSeries ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => ρ)), (∀ (m : ℕ), ↑((PowerSeries.coeff m) G) = (PowerSeries.coeff m) ((MvPowerSeries.optionEquivLeft σ K) ↑g)) ∧ PowerSeries.IsDistinguished r s G ∧ IsUnit ((PowerSeries.coeff s) G)

    Radius selection for distinguished overconvergent series. Let g be an overconvergent series in the variables Option σ which, as a series in Y = X none over the Tate algebra in the variables σ, is distinguished of degree s at radius 1 with a unit coefficient g_s. Then for every ρ₀ > 1 there are radii 1 < ρ ≤ r ≤ ρ₀ such that g is restricted at r, and its coefficient slices gₘ, which are restricted at ρ, form a series G = ∑ₘ gₘ Yᵐ over the series restricted at ρ that is distinguished of degree s at radius r, with g_s a unit.

    This is the radius selection behind Weierstrass division by g inside the Monsky–Washnitzer algebra. A single common radius ρ = r > 1 does not suffice in general.