Quotient norms and the topology of affinoid algebras

A Tate presentation π : K⟨X₁, …, Xₙ⟩ → A of an affinoid algebra gives the residue algebra K⟨X₁, …, Xₙ⟩ ⧸ ker π its quotient Gauss norm, a complete ultrametric algebra norm (the instances are assembled in TauCeti.RingTheory.MvPowerSeries.TateAlgebra.ClosedIdeal). This file proves that the resulting topology does not depend on the presentation, and more generally that the topology of an affinoid algebra carrying any complete ultrametric algebra norm is determined by its algebra structure.

All statements follow from automatic continuity, TauCeti.IsAffinoidAlgebra.continuous_algHom, and the Banach open mapping theorem. Equivalent norms need not be equal or isometric.

Main results

• TauCeti.IsAffinoidAlgebra.isOpenQuotientMap: a surjective algebra homomorphism from a noetherian ultrametric Banach algebra onto a completely normed affinoid algebra is an open quotient map, so the target carries the quotient topology.
• TauCeti.IsAffinoidAlgebra.quotientKerContinuousAlgEquiv: for such a surjection f : A → B, the first isomorphism theorem A ⧸ ker f ≃ B is a homeomorphism.
• TauCeti.IsAffinoidAlgebra.toContinuousAlgEquiv: every algebra isomorphism between completely normed affinoid algebras is a homeomorphism; in particular complete ultrametric algebra norms on an affinoid algebra are equivalent.
• TauCeti.IsAffinoidAlgebra.presentationContinuousAlgEquiv: two Tate presentations of the same algebra give homeomorphic residue algebras for their quotient Gauss norms.
• TauCeti.IsAffinoidAlgebra.residueNormedCommRing: every affinoid algebra carries a complete ultrametric algebra norm, transported from the residue algebra of a chosen Tate presentation.

References

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

theorem TauCeti.IsAffinoidAlgebra.isOpenQuotientMap {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] [IsNoetherianRing A] (hB : IsAffinoidAlgebra K B) (f : A →ₐ[K] B) (hf : Function.Surjective ⇑f) : IsOpenQuotientMap ⇑f

A surjective algebra homomorphism from a noetherian ultrametric Banach algebra onto a completely normed affinoid algebra is an open quotient map, so the target carries the quotient topology induced by the homomorphism.

noncomputable def TauCeti.IsAffinoidAlgebra.quotientKerContinuousAlgEquiv {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] [IsNoetherianRing A] (hB : IsAffinoidAlgebra K B) (f : A →ₐ[K] B) (hf : Function.Surjective ⇑f) : (A ⧸ RingHom.ker f) ≃A[K] B

For a surjective algebra homomorphism f from a noetherian ultrametric Banach algebra onto a completely normed affinoid algebra, the algebraic first isomorphism theorem A ⧸ ker f ≃ B is a homeomorphism for the quotient topology on A ⧸ ker f. This is ContinuousAlgHom.quotientKerEquivOfSurjective applied to f, which is automatically continuous.

@[simp]

theorem TauCeti.IsAffinoidAlgebra.quotientKerContinuousAlgEquiv_mk {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] [IsNoetherianRing A] (hB : IsAffinoidAlgebra K B) (f : A →ₐ[K] B) (hf : Function.Surjective ⇑f) (a : A) : (hB.quotientKerContinuousAlgEquiv f hf) ((Ideal.Quotient.mk (RingHom.ker f)) a) = f a

The first isomorphism theorem sends the class of a to f a.

@[simp]

theorem TauCeti.IsAffinoidAlgebra.toAlgEquiv_quotientKerContinuousAlgEquiv {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] [IsNoetherianRing A] (hB : IsAffinoidAlgebra K B) (f : A →ₐ[K] B) (hf : Function.Surjective ⇑f) : (hB.quotientKerContinuousAlgEquiv f hf).toAlgEquiv = Ideal.quotientKerAlgEquivOfSurjective hf

The underlying algebra isomorphism is the algebraic first isomorphism theorem.

noncomputable def TauCeti.IsAffinoidAlgebra.toContinuousAlgEquiv {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) (e : A ≃ₐ[K] B) : A ≃A[K] B

Equivalence of complete affinoid norms. An algebra isomorphism between completely normed affinoid algebras is a homeomorphism, whatever complete ultrametric algebra norms they carry. Applied to two such norms on one algebra, this says that they define the same topology.

@[simp]

theorem TauCeti.IsAffinoidAlgebra.coe_toContinuousAlgEquiv {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) (e : A ≃ₐ[K] B) : ⇑(hB.toContinuousAlgEquiv e) = ⇑e

The homeomorphism attached to an algebra isomorphism has the same underlying function.

@[simp]

theorem TauCeti.IsAffinoidAlgebra.toAlgEquiv_toContinuousAlgEquiv {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] (hB : IsAffinoidAlgebra K B) (e : A ≃ₐ[K] B) : (hB.toContinuousAlgEquiv e).toAlgEquiv = e

The homeomorphism attached to an algebra isomorphism has that isomorphism as its underlying algebra isomorphism.

noncomputable def TauCeti.IsAffinoidAlgebra.presentationContinuousAlgEquiv {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_4} {τ : Type u_5} [Finite σ] [Finite τ] {C : Type u_6} [CommRing C] [Algebra K C] (π₁ : ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) →ₐ[K] C) (hπ₁ : Function.Surjective ⇑π₁) (π₂ : ↥(MvPowerSeries.IsRestricted.subring fun (x : τ) => 1) →ₐ[K] C) (hπ₂ : Function.Surjective ⇑π₂) : (↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) ⧸ RingHom.ker π₁) ≃A[K] ↥(MvPowerSeries.IsRestricted.subring fun (x : τ) => 1) ⧸ RingHom.ker π₂

Independence of presentation. Two Tate presentations of the same algebra give residue algebras whose quotient Gauss norms define the same topology: the canonical algebra isomorphism between them, compatible with both presentations, is a homeomorphism.

@[simp]

theorem TauCeti.IsAffinoidAlgebra.kerLiftAlg_presentationContinuousAlgEquiv {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {σ : Type u_4} {τ : Type u_5} [Finite σ] [Finite τ] {C : Type u_6} [CommRing C] [Algebra K C] (π₁ : ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) →ₐ[K] C) (hπ₁ : Function.Surjective ⇑π₁) (π₂ : ↥(MvPowerSeries.IsRestricted.subring fun (x : τ) => 1) →ₐ[K] C) (hπ₂ : Function.Surjective ⇑π₂) (x : ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) ⧸ RingHom.ker π₁) : (Ideal.kerLiftAlg π₂) ((presentationContinuousAlgEquiv π₁ hπ₁ π₂ hπ₂) x) = (Ideal.kerLiftAlg π₁) x

The presentation comparison is characterized by compatibility with both presentations.

noncomputable def TauCeti.IsAffinoidAlgebra.residueAlgEquiv {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] {D : Type u_4} [CommRing D] [Algebra K D] (hD : IsAffinoidAlgebra K D) : D ≃ₐ[K] ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin ⋯.choose) => 1) ⧸ RingHom.ker ⋯.choose

The isomorphism of an affinoid algebra D with the residue algebra K⟨X₁, …, Xₙ⟩ ⧸ ker π of a chosen Tate presentation π : K⟨X₁, …, Xₙ⟩ → D.

@[reducible, inline]

noncomputable abbrev TauCeti.IsAffinoidAlgebra.residueNormedCommRing {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {D : Type u_4} [CommRing D] [Algebra K D] (hD : IsAffinoidAlgebra K D) : NormedCommRing D

The residue norm on an affinoid algebra. The norm ‖x‖ = ‖residueAlgEquiv hD x‖ on D, transported from the quotient Gauss norm of a chosen Tate presentation. It is a complete ultrametric K-algebra norm (TauCeti.IsAffinoidAlgebra.residueNormedAlgebra, TauCeti.IsAffinoidAlgebra.isUltrametricDist_residueNormedCommRing, TauCeti.IsAffinoidAlgebra.completeSpace_residueNormedCommRing). It is not an instance, since it depends on the chosen presentation; all such norms define the same topology (TauCeti.IsAffinoidAlgebra.toContinuousAlgEquiv).

@[reducible, inline]

noncomputable abbrev TauCeti.IsAffinoidAlgebra.residueNormedAlgebra {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {D : Type u_4} [CommRing D] [Algebra K D] (hD : IsAffinoidAlgebra K D) : NormedAlgebra K D

The residue norm TauCeti.IsAffinoidAlgebra.residueNormedCommRing is a K-algebra norm.

theorem TauCeti.IsAffinoidAlgebra.norm_residueAlgEquiv {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {D : Type u_4} [CommRing D] [Algebra K D] (hD : IsAffinoidAlgebra K D) (x : D) : ‖hD.residueAlgEquiv x‖ = ‖x‖

TauCeti.IsAffinoidAlgebra.residueAlgEquiv preserves the residue norm.

theorem TauCeti.IsAffinoidAlgebra.isUltrametricDist_residueNormedCommRing {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {D : Type u_4} [CommRing D] [Algebra K D] (hD : IsAffinoidAlgebra K D) : IsUltrametricDist D

The residue norm on an affinoid algebra is ultrametric.

theorem TauCeti.IsAffinoidAlgebra.completeSpace_residueNormedCommRing {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {D : Type u_4} [CommRing D] [Algebra K D] (hD : IsAffinoidAlgebra K D) : CompleteSpace D

An affinoid algebra is complete for its residue norm.