Documentation

TauCeti.RingTheory.MvPowerSeries.TateAlgebra.Eval

Evaluating restricted power series at bounded arguments #

Let R and S be ultrametric normed commutative rings, with S complete, let φ : R →+* S not increase norms, and let a : Fin k → S satisfy ‖a i‖ ≤ c i for a polyradius c. For a series f = ∑ₜ fₜ Xᵗ restricted at c, the monomial values satisfy

‖φ(fₜ) aᵗ‖ ≤ ‖fₜ‖ cᵗ → 0,

so they are summable in S, and their sum f(a) defines a ring homomorphism R{X/c} → S with C r ↦ φ r and X i ↦ a i. It does not increase norms, and it is the only continuous ring homomorphism with these values on constants and variables, because the polynomials are dense in R{X/c}. This is the universal property of the Tate algebra R{X/c} among complete ultrametric normed rings, at arguments whose norms reach the real radii c i.

The value f(a) is the sum TauCeti.Huber.weightedEval φ a f of the evaluation of weighted restricted series in Huber's sense (Wedhorn, Proposition 5.50), and additivity and the Cauchy product formula are TauCeti.Huber.weightedEval_add_of_summable and TauCeti.Huber.weightedEval_mul_of_summable; what is new here is the summability, from the Gauss norm. Huber's weights are subsets of R, so they reach only radii that are norms of elements of R, and Mathlib's MvPowerSeries.eval₂ evaluates only at topologically nilpotent arguments. Arbitrary real radii are what present rings of convergent functions on annuli as quotients of Tate algebras, as in Kedlaya's Lemma 4.9 for the interval rings of the Fargues–Fontaine curve.

Main definitions #

Main results #

References #

source
theorem MvPowerSeries.IsRestricted.tendsto_weightedEvalTerm {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) {f : MvPowerSeries (Fin k) R} (hf : IsRestricted c f) :
Filter.Tendsto (TauCeti.Huber.weightedEvalTerm φ a f) Filter.cofinite (nhds 0)

The monomial values of a restricted series at a bounded argument tend to zero.

source
theorem MvPowerSeries.IsRestricted.summable_weightedEvalTerm {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) {f : MvPowerSeries (Fin k) R} (hf : IsRestricted c f) :
Summable (TauCeti.Huber.weightedEvalTerm φ a f)

The monomial values of a restricted series at a bounded argument are summable.

source
noncomputable def MvPowerSeries.restrictedEval₂ {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] [IsUltrametricDist R] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) :
↥(IsRestricted.subring c) →+* S

Evaluation of restricted power series at bounded arguments. For a norm-nonincreasing φ : R →+* S into a complete ultrametric normed ring and arguments a i of norm at most c i, the ring homomorphism R{X/c} → S sending f = ∑ₜ fₜ Xᵗ to f(a) = ∑ₜ φ(fₜ) aᵗ, that is, TauCeti.Huber.weightedEval φ a f.

Instances For
    source
    theorem MvPowerSeries.restrictedEval₂_apply {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] [IsUltrametricDist R] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) (f : ↥(IsRestricted.subring c)) :
    (restrictedEval₂ φ a hφ ha) f = TauCeti.Huber.weightedEval φ a ↑f

    The evaluation f(a) is TauCeti.Huber.weightedEval φ a f.

    source
    theorem MvPowerSeries.hasSum_restrictedEval₂ {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] [IsUltrametricDist R] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) (f : ↥(IsRestricted.subring c)) :
    HasSum (TauCeti.Huber.weightedEvalTerm φ a ↑f) ((restrictedEval₂ φ a hφ ha) f)

    The evaluation f(a) is the sum of the monomial values φ(fₜ) aᵗ.

    source
    @[simp]
    theorem MvPowerSeries.restrictedEval₂_monomial {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] [IsUltrametricDist R] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) (t : Fin k →₀ ℕ) (r : R) :
    (restrictedEval₂ φ a hφ ha) ⟨(monomial t) r, ⋯⟩ = φ r * ∏ i : Fin k, a i ^ t i

    The evaluation of a monomial r Xᵗ is φ(r) aᵗ.

    source
    @[simp]
    theorem MvPowerSeries.restrictedEval₂_algebraMap {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] [IsUltrametricDist R] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) (r : R) :
    (restrictedEval₂ φ a hφ ha) ((algebraMap R ↥(IsRestricted.subring c)) r) = φ r

    Evaluation extends φ on constants.

    source
    @[simp]
    theorem MvPowerSeries.restrictedEval₂_X {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] [IsUltrametricDist R] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) (i : Fin k) :
    (restrictedEval₂ φ a hφ ha) ⟨X i, ⋯⟩ = a i

    Evaluation sends the variable X i to a i.

    source
    @[simp]
    theorem MvPowerSeries.restrictedEval₂_polynomial {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] [IsUltrametricDist R] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) (p : MvPolynomial (Fin k) R) :
    (restrictedEval₂ φ a hφ ha) ⟨↑p, ⋯⟩ = MvPolynomial.eval₂ φ a p

    Evaluation extends polynomial evaluation: the value of a polynomial p at a is MvPolynomial.eval₂ φ a p.

    source
    theorem MvPowerSeries.norm_restrictedEval₂_le {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] [IsUltrametricDist R] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) [∀ (i : Fin k), Fact (0 < c i)] (f : ↥(IsRestricted.subring c)) :
    ‖(restrictedEval₂ φ a hφ ha) f‖ ≤ ‖f‖

    Evaluation does not increase the Gauss norm: ‖f(a)‖ ≤ ‖f‖.

    source
    theorem MvPowerSeries.continuous_restrictedEval₂ {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] [IsUltrametricDist R] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) [∀ (i : Fin k), Fact (0 < c i)] :
    Continuous ⇑(restrictedEval₂ φ a hφ ha)

    Evaluation is 1-Lipschitz for the Gauss norm, hence continuous.

    source
    theorem MvPowerSeries.eq_restrictedEval₂ {k : ℕ} {R : Type u_1} {S : Type u_2} [NormedCommRing R] [NormedCommRing S] {c : Fin k → ℝ} (φ : R →+* S) (a : Fin k → S) [IsUltrametricDist S] [CompleteSpace S] [IsUltrametricDist R] (hφ : ∀ (r : R), ‖φ r‖ ≤ ‖r‖) (ha : ∀ (i : Fin k), ‖a i‖ ≤ c i) [∀ (i : Fin k), Fact (0 < c i)] (ψ : ↥(IsRestricted.subring c) →+* S) (hψ : Continuous ⇑ψ) (hC : ∀ (r : R), ψ ((algebraMap R ↥(IsRestricted.subring c)) r) = φ r) (hX : ∀ (i : Fin k), ψ ⟨X i, ⋯⟩ = a i) :
    ψ = restrictedEval₂ φ a hφ ha

    Uniqueness of evaluation: a continuous ring homomorphism R{X/c} → S that extends φ on constants and sends each X i to a i is the evaluation f ↦ f(a).