Restricted series over an affinoid algebra

Let A be an affinoid algebra over a complete nonarchimedean field K, carrying a complete ultrametric algebra norm, and let A⟨X₁, …, Xₘ⟩ be the Gauss-normed ring of unit-radius restricted series over A. This file proves that A⟨X₁, …, Xₘ⟩ is again affinoid, and that K-algebra maps from it to a completely normed affinoid algebra B correspond to K-algebra maps A → B together with power-bounded images of the variables.

For a Tate presentation π : K⟨Y₁, …, Yₙ⟩ → A, automatic continuity makes π bounded and the open mapping theorem gives lifts of controlled norm. Applying π to coefficients is then a surjection K⟨Y⟩⟨X⟩ → A⟨X⟩ (TauCeti.MvPowerSeries.restrictedMap_surjective), and the iteration isomorphism K⟨X, Y⟩ ≅ K⟨Y⟩⟨X⟩ (TauCeti.MvPowerSeries.restrictedSumAlgEquiv) presents A⟨X⟩ as a quotient of the Tate algebra in m + n variables.

The universal property needs no continuity hypothesis: algebra homomorphisms from the noetherian Banach algebras A and A⟨X⟩ into a completely normed affinoid algebra are automatically continuous, so the continuous universal property TauCeti.MvPowerSeries.existsUnique_continuous_ringHom_isRestricted_subring applies. The images of the variables need only be power-bounded, not of norm at most one.

Main definitions

• TauCeti.IsAffinoidAlgebra.restrictedLift: the K-algebra map A⟨X₁, …, Xₘ⟩ →ₐ[K] B extending φ : A →ₐ[K] B and sending Xᵢ to a power-bounded bᵢ.

Main results

• TauCeti.IsAffinoidAlgebra.isRestricted_subring: A⟨X₁, …, Xₘ⟩ is affinoid.
• TauCeti.IsAffinoidAlgebra.algHom_ext_isRestricted_subring: K-algebra maps A⟨X₁, …, Xₘ⟩ → B agreeing on A and on the variables are equal.
• TauCeti.IsAffinoidAlgebra.continuous_algHom_quotient, TauCeti.IsAffinoidAlgebra.isPowerBounded_map_quotient_X: K-algebra maps A⟨X₁, …, Xₘ⟩ ⧸ L → B are continuous and send the variables to power-bounded elements.
• TauCeti.IsAffinoidAlgebra.existsUnique_algHom_isRestricted_subring: a K-algebra map φ : A → B into an affinoid algebra and power-bounded b₁, …, bₘ ∈ B extend uniquely to a K-algebra map A⟨X₁, …, Xₘ⟩ → B sending Xᵢ to bᵢ.

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §§1.4, 6.1.1 and 6.1.3.

theorem TauCeti.IsAffinoidAlgebra.isRestricted_subring {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {τ : Type u_3} [Finite τ] (hA : IsAffinoidAlgebra K A) : IsAffinoidAlgebra K ↥(MvPowerSeries.IsRestricted.subring fun (x : τ) => 1)

Restricted series over an affinoid algebra form an affinoid algebra. For an affinoid algebra A with a complete ultrametric algebra norm, the Gauss-normed algebra A⟨X₁, …, Xₘ⟩ of unit-radius restricted series is affinoid: a Tate presentation K⟨Y₁, …, Yₙ⟩ → A induces a presentation K⟨X₁, …, Xₘ, Y₁, …, Yₙ⟩ → A⟨X₁, …, Xₘ⟩.

theorem TauCeti.IsAffinoidAlgebra.algHom_ext_isRestricted_subring {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {k : ℕ} (hA : IsAffinoidAlgebra K A) {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) {ψ₁ ψ₂ : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1) →ₐ[K] B} (hC : ∀ (a : A), ψ₁ ((algebraMap A ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)) a) = ψ₂ ((algebraMap A ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)) a)) (hX : ∀ (i : Fin k), ψ₁ ⟨MvPowerSeries.X i, ⋯⟩ = ψ₂ ⟨MvPowerSeries.X i, ⋯⟩) : ψ₁ = ψ₂

K-algebra maps out of A⟨X₁, …, Xₖ⟩ are determined on A and the variables. Let A and B be affinoid algebras with complete ultrametric algebra norms. Two K-algebra maps A⟨X₁, …, Xₖ⟩ → B that agree on A and on every Xᵢ are equal. No continuity is assumed: it is automatic (TauCeti.IsAffinoidAlgebra.continuous_algHom).

theorem TauCeti.IsAffinoidAlgebra.continuous_algHom_quotient {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {k : ℕ} (hA : IsAffinoidAlgebra K A) {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) {L : Ideal ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)} (ψ : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1) ⧸ L →ₐ[K] B) : Continuous ⇑ψ

K-algebra maps out of a quotient of A⟨X₁, …, Xₖ⟩ are continuous. Let A and B be affinoid algebras with complete ultrametric algebra norms. Every K-algebra map A⟨X₁, …, Xₖ⟩ ⧸ L → B is continuous for the quotient topology.

theorem TauCeti.IsAffinoidAlgebra.isPowerBounded_map_quotient_X {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {k : ℕ} (hA : IsAffinoidAlgebra K A) {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) {L : Ideal ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)} (ψ : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1) ⧸ L →ₐ[K] B) (i : Fin k) : Huber.IsPowerBounded (ψ ((Ideal.Quotient.mk L) ⟨MvPowerSeries.X i, ⋯⟩))

K-algebra maps out of a quotient of A⟨X₁, …, Xₖ⟩ send the variables to power-bounded elements. Let A and B be affinoid algebras with complete ultrametric algebra norms. Every K-algebra map A⟨X₁, …, Xₖ⟩ ⧸ L → B sends the image of each Xᵢ to a power-bounded element.

noncomputable def TauCeti.IsAffinoidAlgebra.restrictedLift {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {k : ℕ} (hA : IsAffinoidAlgebra K A) {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) (φ : A →ₐ[K] B) {b : Fin k → B} (hb : ∀ (i : Fin k), Huber.IsPowerBounded (b i)) : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1) →ₐ[K] B

The extension of a K-algebra map φ : A → B to A⟨X₁, …, Xₖ⟩ sending each Xᵢ to bᵢ, for affinoid algebras A and B with complete ultrametric algebra norms and power-bounded b₁, …, bₖ ∈ B. It is the continuous extension TauCeti.MvPowerSeries.restrictedLift, which applies because φ is automatically continuous.

@[simp]

theorem TauCeti.IsAffinoidAlgebra.restrictedLift_algebraMap {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {k : ℕ} (hA : IsAffinoidAlgebra K A) {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) (φ : A →ₐ[K] B) {b : Fin k → B} (hb : ∀ (i : Fin k), Huber.IsPowerBounded (b i)) (a : A) : (hA.restrictedLift hB φ hb) ((algebraMap A ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)) a) = φ a

restrictedLift extends φ on A.

@[simp]

theorem TauCeti.IsAffinoidAlgebra.restrictedLift_X {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {k : ℕ} (hA : IsAffinoidAlgebra K A) {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) (φ : A →ₐ[K] B) {b : Fin k → B} (hb : ∀ (i : Fin k), Huber.IsPowerBounded (b i)) (i : Fin k) : (hA.restrictedLift hB φ hb) ⟨MvPowerSeries.X i, ⋯⟩ = b i

restrictedLift sends each variable Xᵢ to bᵢ.

theorem TauCeti.IsAffinoidAlgebra.existsUnique_algHom_isRestricted_subring {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {k : ℕ} (hA : IsAffinoidAlgebra K A) {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) (φ : A →ₐ[K] B) {b : Fin k → B} (hb : ∀ (i : Fin k), Huber.IsPowerBounded (b i)) : ∃! ψ : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1) →ₐ[K] B, (∀ (a : A), ψ ((algebraMap A ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin k) => 1)) a) = φ a) ∧ ∀ (i : Fin k), ψ ⟨MvPowerSeries.X i, ⋯⟩ = b i

The universal property of restricted series over an affinoid algebra. Let A and B be affinoid algebras with complete ultrametric algebra norms. A K-algebra map φ : A → B and power-bounded b₁, …, bₖ ∈ B extend to exactly one K-algebra map A⟨X₁, …, Xₖ⟩ → B sending each Xᵢ to bᵢ, namely TauCeti.IsAffinoidAlgebra.restrictedLift. It is continuous, as is every algebra map between such algebras (TauCeti.IsAffinoidAlgebra.continuous_algHom).