The universal property of Gauss-normed Tate algebras at power-bounded arguments

Let R be an ultrametric normed commutative ring and S a complete Hausdorff nonarchimedean commutative ring, for instance a complete ultrametric normed ring. Let φ : R →+* S be continuous, and let b₁, …, bₖ ∈ S be power-bounded. Then there is exactly one continuous ring homomorphism ψ : R⟨X₁, …, Xₖ⟩ → S on the Gauss-normed ring of unit-radius restricted series with ψ (C r) = φ r and ψ (Xᵢ) = bᵢ.

This is Wedhorn's Proposition 5.50, TauCeti.Huber.existsUnique_continuous_ringHom_weightedRestrictedSubring, carried along the identity comparison TauCeti.Huber.restrictedMvPowerSeriesGaussEquiv between the Huber model and the Gauss-normed model, which is continuous in both directions. Unlike MvPowerSeries.restrictedEval₂, neither ‖φ r‖ ≤ ‖r‖ nor ‖bᵢ‖ ≤ 1 is assumed. Power-boundedness is TauCeti.Huber.IsPowerBounded for the topology of S: for a normed S the powers of bᵢ stay bounded, while bᵢ itself may have norm larger than one.

Main definitions

• TauCeti.MvPowerSeries.restrictedLift: the continuous ring homomorphism R⟨X₁, …, Xₖ⟩ →+* S extending φ and sending Xᵢ to bᵢ.
• TauCeti.MvPowerSeries.restrictedRename: for complete R and f : Fin m → Fin k, the R-algebra map R⟨X₁, …, Xₘ⟩ →ₐ[R] R⟨X₁, …, Xₖ⟩ sending Xᵢ to X_{f i}.

Main results

• TauCeti.MvPowerSeries.isPowerBounded_X: each variable Xᵢ is power-bounded.
• TauCeti.MvPowerSeries.isRestricted_subring_ringHom_ext_of_continuous: continuous ring homomorphisms out of R⟨X₁, …, Xₖ⟩ agreeing on constants and variables are equal.
• TauCeti.MvPowerSeries.restrictedLift_unique: restrictedLift is the only such continuous extension.
• TauCeti.MvPowerSeries.existsUnique_continuous_ringHom_isRestricted_subring: the universal property.
• TauCeti.MvPowerSeries.restrictedRename_id, TauCeti.MvPowerSeries.restrictedRename_comp: renaming along the identity is the identity, and successive renamings compose.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Proposition 5.50.
• S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis, §1.4.

theorem TauCeti.MvPowerSeries.isRestricted_subring_ringHom_ext_of_continuous {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {T : Type u_2} [Semiring T] [TopologicalSpace T] [T2Space T] {ψ₁ ψ₂ : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1) →+* T} (h₁ : Continuous ⇑ψ₁) (h₂ : Continuous ⇑ψ₂) (hC : ∀ (r : R), ψ₁ ((algebraMap R ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)) r) = ψ₂ ((algebraMap R ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)) r)) (hX : ∀ (i : Fin k), ψ₁ ⟨MvPowerSeries.X i, ⋯⟩ = ψ₂ ⟨MvPowerSeries.X i, ⋯⟩) : ψ₁ = ψ₂

Continuous ring homomorphisms out of R⟨X₁, …, Xₖ⟩ are determined by the constants and the variables. Two continuous ring homomorphisms into a Hausdorff ring that agree on every constant and on every Xᵢ are equal.

theorem TauCeti.MvPowerSeries.isPowerBounded_X {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] (i : Fin k) : Huber.IsPowerBounded ⟨MvPowerSeries.X i, ⋯⟩

Each variable Xᵢ of the Gauss-normed algebra R⟨X₁, …, Xₖ⟩ is power-bounded.

noncomputable def TauCeti.MvPowerSeries.restrictedLift {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {S : Type u_2} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [NonarchimedeanRing S] [CompleteSpace S] [T3Space S] {φ : R →+* S} (hφ : Continuous ⇑φ) {b : Fin k → S} (hb : ∀ (i : Fin k), Huber.IsPowerBounded (b i)) : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1) →+* S

The extension of φ to R⟨X₁, …, Xₖ⟩ sending each Xᵢ to bᵢ, for a continuous ring homomorphism φ : R →+* S into a complete Hausdorff nonarchimedean ring and power-bounded b₁, …, bₖ ∈ S. It is Wedhorn's evaluation homomorphism TauCeti.Huber.weightedEvalHom, carried along the Gauss comparison TauCeti.Huber.restrictedMvPowerSeriesGaussEquiv.

theorem TauCeti.MvPowerSeries.continuous_restrictedLift {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {S : Type u_2} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [NonarchimedeanRing S] [CompleteSpace S] [T3Space S] {φ : R →+* S} (hφ : Continuous ⇑φ) {b : Fin k → S} (hb : ∀ (i : Fin k), Huber.IsPowerBounded (b i)) : Continuous ⇑(restrictedLift hφ hb)

restrictedLift is continuous.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedLift_algebraMap {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {S : Type u_2} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [NonarchimedeanRing S] [CompleteSpace S] [T3Space S] {φ : R →+* S} (hφ : Continuous ⇑φ) {b : Fin k → S} (hb : ∀ (i : Fin k), Huber.IsPowerBounded (b i)) (r : R) : (restrictedLift hφ hb) ((algebraMap R ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)) r) = φ r

restrictedLift extends φ on constants.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedLift_X {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {S : Type u_2} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [NonarchimedeanRing S] [CompleteSpace S] [T3Space S] {φ : R →+* S} (hφ : Continuous ⇑φ) {b : Fin k → S} (hb : ∀ (i : Fin k), Huber.IsPowerBounded (b i)) (i : Fin k) : (restrictedLift hφ hb) ⟨MvPowerSeries.X i, ⋯⟩ = b i

restrictedLift sends each variable Xᵢ to bᵢ.

theorem TauCeti.MvPowerSeries.restrictedLift_unique {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {S : Type u_2} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [NonarchimedeanRing S] [CompleteSpace S] [T3Space S] {φ : R →+* S} (hφ : Continuous ⇑φ) {b : Fin k → S} (hb : ∀ (i : Fin k), Huber.IsPowerBounded (b i)) {ψ : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1) →+* S} (hψ : Continuous ⇑ψ) (hC : ∀ (r : R), ψ ((algebraMap R ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)) r) = φ r) (hX : ∀ (i : Fin k), ψ ⟨MvPowerSeries.X i, ⋯⟩ = b i) : ψ = restrictedLift hφ hb

restrictedLift is the only continuous ring homomorphism extending φ on constants and sending each Xᵢ to bᵢ.

theorem TauCeti.MvPowerSeries.existsUnique_continuous_ringHom_isRestricted_subring {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {S : Type u_2} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [NonarchimedeanRing S] [CompleteSpace S] [T3Space S] {φ : R →+* S} (hφ : Continuous ⇑φ) {b : Fin k → S} (hb : ∀ (i : Fin k), Huber.IsPowerBounded (b i)) : ∃! ψ : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1) →+* S, Continuous ⇑ψ ∧ (∀ (r : R), ψ ((algebraMap R ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)) r) = φ r) ∧ ∀ (i : Fin k), ψ ⟨MvPowerSeries.X i, ⋯⟩ = b i

The universal property of R⟨X₁, …, Xₖ⟩ at power-bounded arguments. For a continuous ring homomorphism φ : R →+* S into a complete Hausdorff nonarchimedean ring and power-bounded b₁, …, bₖ ∈ S, there is exactly one continuous ring homomorphism out of the Gauss-normed unit-radius restricted series that extends φ on constants and sends each Xᵢ to bᵢ, namely TauCeti.MvPowerSeries.restrictedLift.

noncomputable def TauCeti.MvPowerSeries.restrictedRename {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] {m : ℕ} (f : Fin m → Fin k) : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin m) => 1) →ₐ[R] ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)

Renaming the variables of restricted series. For a complete ultrametric normed ring R and f : Fin m → Fin k, this is the R-algebra map R⟨X₁, …, Xₘ⟩ → R⟨X₁, …, Xₖ⟩ sending each Xᵢ to X_{f i}, the extension TauCeti.MvPowerSeries.restrictedLift of the constant-series embedding. The map f need not be injective.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedRename_X {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] {m : ℕ} (f : Fin m → Fin k) (i : Fin m) : (restrictedRename f) ⟨MvPowerSeries.X i, ⋯⟩ = ⟨MvPowerSeries.X (f i), ⋯⟩

restrictedRename f sends each variable Xᵢ to X_{f i}.

theorem TauCeti.MvPowerSeries.continuous_restrictedRename {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] {m : ℕ} (f : Fin m → Fin k) : Continuous ⇑(restrictedRename f)

restrictedRename f is continuous.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedRename_id {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] : restrictedRename id = AlgHom.id R ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)

Renaming along the identity is the identity.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedRename_comp {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] {m n : ℕ} (g : Fin k → Fin n) (f : Fin m → Fin k) : (restrictedRename g).comp (restrictedRename f) = restrictedRename (g ∘ f)

Successive renamings compose: renaming along f and then g is renaming along g ∘ f.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedRename_restrictedRename {k : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] {m n : ℕ} (g : Fin k → Fin n) (f : Fin m → Fin k) (x : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin m) => 1)) : (restrictedRename g) ((restrictedRename f) x) = (restrictedRename (g ∘ f)) x

Applying restrictedRename f and then restrictedRename g is renaming along g ∘ f.