Dagger algebras

Let K be an ultrametric normed field. A K-dagger algebra is a commutative K-algebra A admitting a surjective K-algebra homomorphism W_n ↠ A from the Monsky–Washnitzer algebra W_n = K⟨X₁, …, Xₙ⟩† of overconvergent power series, equivalently A ≅ W_n ⧸ I for an ideal I. Dagger algebras are to Grosse-Klönne's dagger spaces what affinoid algebras are to rigid spaces. Like TauCeti.IsAffinoidAlgebra, the predicate is algebraic: it fixes neither a norm nor a topology on A, and it includes nonreduced algebras and the zero algebra.

Every element a of a dagger algebra over a complete field has bounded spectrum in the following sense: 1 + c • a is a unit for every sufficiently small scalar c. Over a nontrivially normed field this rules out the polynomial ring K[X], whose element 1 + c • X is a unit only for c = 0; so a dagger algebra is not merely a finitely generated K-algebra.

Main definitions

• TauCeti.Dagger.IsDaggerAlgebra K A: A is a quotient of some W_n.
• TauCeti.Dagger.presentationDim K A: the least number of variables of a presentation W_n ↠ A, and TauCeti.Dagger.presentation K A: a chosen presentation in that many variables.

Main results

• TauCeti.Dagger.IsDaggerAlgebra.of_surjective: surjective images, in particular quotients (TauCeti.Dagger.IsDaggerAlgebra.quotient), of dagger algebras are dagger algebras.
• TauCeti.Dagger.isDaggerAlgebra_iff_exists_ideal: A is a dagger algebra iff it is isomorphic to W_n ⧸ I for some n and some ideal I.
• TauCeti.Dagger.IsDaggerAlgebra.of_surjective_washnitzerAlgebra: a quotient of the Monsky–Washnitzer algebra in any finite type of variables is a dagger algebra.
• TauCeti.Dagger.presentationDim_eq_zero_iff: a dagger algebra has a presentation in zero variables iff it is spanned by the scalars; so K has presentation dimension 0 and W_1 has presentation dimension 1.
• TauCeti.Dagger.IsDaggerAlgebra.eventually_isUnit_one_add_smul: in a dagger algebra over a complete field, 1 + c • a is a unit for all c near 0, and TauCeti.Dagger.not_isDaggerAlgebra_polynomial: over a complete nontrivially normed field, K[X] is not a dagger algebra.

References

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

class TauCeti.Dagger.IsDaggerAlgebra (K : Type u_1) [NormedField K] [IsUltrametricDist K] (A : Type u_2) [CommRing A] [Algebra K A] : Prop

A K-dagger algebra is a commutative K-algebra which is a quotient of the Monsky–Washnitzer algebra W_n = K⟨X₁, …, Xₙ⟩† for some n.

• exists_surjective : ∃ (n : ℕ) (φ : ↥(Dagger.washnitzerAlgebra (Fin n) K) →ₐ[K] A), Function.Surjective ⇑φ

theorem TauCeti.Dagger.IsDaggerAlgebra.of_surjective {K : Type u_1} [NormedField K] [IsUltrametricDist K] {A : Type u_2} [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] {B : Type u_3} [CommRing B] [Algebra K B] (f : A →ₐ[K] B) (hf : Function.Surjective ⇑f) : IsDaggerAlgebra K B

A surjective image of a dagger algebra is a dagger algebra.

instance TauCeti.Dagger.IsDaggerAlgebra.quotient {K : Type u_1} [NormedField K] [IsUltrametricDist K] {A : Type u_2} [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] (I : Ideal A) : IsDaggerAlgebra K (A ⧸ I)

A quotient of a dagger algebra is a dagger algebra.

theorem TauCeti.Dagger.IsDaggerAlgebra.of_surjective_washnitzerAlgebra {K : Type u_1} [NormedField K] [IsUltrametricDist K] {A : Type u_2} [CommRing A] [Algebra K A] {σ : Type u_3} [Finite σ] (φ : ↥(Dagger.washnitzerAlgebra σ K) →ₐ[K] A) (hφ : Function.Surjective ⇑φ) : IsDaggerAlgebra K A

A quotient of the Monsky–Washnitzer algebra in finitely many variables is a dagger algebra.

instance TauCeti.Dagger.IsDaggerAlgebra.washnitzerAlgebra {K : Type u_1} [NormedField K] [IsUltrametricDist K] {σ : Type u_3} [Finite σ] : IsDaggerAlgebra K ↥(Dagger.washnitzerAlgebra σ K)

The Monsky–Washnitzer algebra in finitely many variables is a dagger algebra.

instance TauCeti.Dagger.IsDaggerAlgebra.self (K : Type u_1) [NormedField K] [IsUltrametricDist K] : IsDaggerAlgebra K K

The coefficient field is a dagger algebra, presented by the constant coefficient W_0 → K.

theorem TauCeti.Dagger.isDaggerAlgebra_iff_exists_ideal {K : Type u_1} [NormedField K] [IsUltrametricDist K] {A : Type u_2} [CommRing A] [Algebra K A] : IsDaggerAlgebra K A ↔ ∃ (n : ℕ) (I : Ideal ↥(washnitzerAlgebra (Fin n) K)), Nonempty ((↥(washnitzerAlgebra (Fin n) K) ⧸ I) ≃ₐ[K] A)

The presentation criterion. A K-algebra is a dagger algebra iff it is isomorphic to a quotient W_n ⧸ I of a Monsky–Washnitzer algebra.

noncomputable def TauCeti.Dagger.presentationDim (K : Type u_1) [NormedField K] [IsUltrametricDist K] (A : Type u_2) [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] : ℕ

The presentation dimension of a dagger algebra A: the least n for which there is a surjection W_n ↠ A. It is not the Krull dimension: the dual numbers K[ε] ⧸ (ε²) have Krull dimension 0 but need one variable.

noncomputable def TauCeti.Dagger.presentation (K : Type u_1) [NormedField K] [IsUltrametricDist K] (A : Type u_2) [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] : ↥(washnitzerAlgebra (Fin (presentationDim K A)) K) →ₐ[K] A

A chosen presentation W_n ↠ A in the least possible number n = presentationDim K A of variables.

theorem TauCeti.Dagger.presentation_surjective (K : Type u_1) [NormedField K] [IsUltrametricDist K] (A : Type u_2) [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] : Function.Surjective ⇑(presentation K A)

The chosen presentation is surjective.

theorem TauCeti.Dagger.presentationDim_le {K : Type u_1} [NormedField K] [IsUltrametricDist K] {A : Type u_2} [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] {n : ℕ} (φ : ↥(washnitzerAlgebra (Fin n) K) →ₐ[K] A) (hφ : Function.Surjective ⇑φ) : presentationDim K A ≤ n

Any presentation W_n ↠ A has at least presentationDim K A variables.

theorem TauCeti.Dagger.presentationDim_eq_zero_iff {K : Type u_1} [NormedField K] [IsUltrametricDist K] {A : Type u_2} [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] : presentationDim K A = 0 ↔ Function.Surjective ⇑(algebraMap K A)

Dagger algebras of presentation dimension zero. A dagger algebra has a presentation in zero variables iff every element is a scalar.

@[simp]

theorem TauCeti.Dagger.presentationDim_self (K : Type u_1) [NormedField K] [IsUltrametricDist K] : presentationDim K K = 0

The coefficient field has a presentation in zero variables.

@[simp]

theorem TauCeti.Dagger.presentationDim_washnitzerAlgebra_fin_one (K : Type u_1) [NormedField K] [IsUltrametricDist K] : presentationDim K ↥(washnitzerAlgebra (Fin 1) K) = 1

The Monsky–Washnitzer algebra W_1 in one variable needs exactly one variable: the variable X is not a scalar.

theorem TauCeti.Dagger.IsDaggerAlgebra.eventually_isUnit_one_add_smul {K : Type u_1} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A] [Algebra K A] [IsDaggerAlgebra K A] (a : A) : ∀ᶠ (c : K) in nhds 0, IsUnit (1 + c • a)

Elements of dagger algebras have bounded spectrum. Over a complete ultrametric normed field, for every element a of a dagger algebra, 1 + c • a is a unit for all scalars c near 0.

theorem TauCeti.Dagger.not_isDaggerAlgebra_polynomial {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] : ¬IsDaggerAlgebra K (Polynomial K)

The polynomial ring is not a dagger algebra. Over a complete nontrivially normed ultrametric field, 1 + c • X is a unit of K[X] only for c = 0, so K[X] is not a quotient of any Monsky–Washnitzer algebra.