From 3979b1c2aecbcb295b4d23c2abc7fe68fba4406f Mon Sep 17 00:00:00 2001 From: Aleksey Salkutsan Date: Sat, 25 Jul 2026 15:10:51 +0200 Subject: [PATCH] berkovich: add universe-controlled affinoid point model --- Rigid.lean | 1 + Rigid/Berkovich/AffinoidPoint.lean | 65 ++++++++++++++++++++++++++++++ Rigid/Development.lean | 47 ++++++++++++++++++++- 3 files changed, 111 insertions(+), 2 deletions(-) create mode 100644 Rigid/Berkovich/AffinoidPoint.lean diff --git a/Rigid.lean b/Rigid.lean index 2d3e20f..c15e48a 100644 --- a/Rigid.lean +++ b/Rigid.lean @@ -29,6 +29,7 @@ import Rigid.AffinoidSpectrum.RationalBasis import Rigid.AffinoidSpectrum.RationalCover import Rigid.AffinoidSpectrum.RationalRefinement import Rigid.AffinoidSpectrum.Restriction +import Rigid.Berkovich.AffinoidPoint import Rigid.Berkovich.AffinoidDomain import Rigid.Berkovich.CompletedResidue import Rigid.Berkovich.CompletedResidueFunctoriality diff --git a/Rigid/Berkovich/AffinoidPoint.lean b/Rigid/Berkovich/AffinoidPoint.lean new file mode 100644 index 0000000..5a16906 --- /dev/null +++ b/Rigid/Berkovich/AffinoidPoint.lean @@ -0,0 +1,65 @@ +import Mathlib.Topology.Category.TopCat.ULift +import Rigid.AffinoidAlgebra.ResidueNorm +import Rigid.Berkovich.RelativeSpectrum + +set_option linter.style.header false + +/-! +# Universe-controlled affinoid Berkovich point models + +This file packages the relative Berkovich spectrum of a strict affinoid algebra as a topological +space in the next universe. It contains only the point-set model; no structure sheaf or global +Berkovich-space structure is asserted here. +-/ + +universe u + +namespace Rigid +namespace AffinoidPoint + +variable (K : Type u) [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K] + +/-- The relative Berkovich spectrum associated with an explicit affinoid presentation, lifted by +one universe with its topology transported canonically along `ULift`. -/ +noncomputable def topCatOfPresentation {A : Type u} [CommRing A] [Algebra K A] + (P : AffinoidPresentation K A) : TopCat.{u + 1} := + letI : NormedCommRing A := + residueNormedCommRing K A P.n P.ideal P.equiv + letI : NormedAlgebra K A := + residueNormedAlgebra K A P.n P.ideal P.equiv + TopCat.of (ULift.{u + 1, u} (BerkovichSpectrumOver K A)) + +/-- The relative Berkovich spectrum, lifted by one universe with its topology transported +canonically along `ULift`. -/ +noncomputable def topCat {A : Type u} [CommRing A] [Algebra K A] + (hA : IsAffinoidAlgebra K A) : TopCat.{u + 1} := + topCatOfPresentation K hA.presentation + +/-- The lifted point model of an explicit affinoid presentation is canonically homeomorphic to +its relative Berkovich spectrum. -/ +noncomputable def homeomorphOfPresentation {A : Type u} [CommRing A] [Algebra K A] + (P : AffinoidPresentation K A) : + letI : NormedCommRing A := + residueNormedCommRing K A P.n P.ideal P.equiv + letI : NormedAlgebra K A := + residueNormedAlgebra K A P.n P.ideal P.equiv + topCatOfPresentation K P ≃ₜ BerkovichSpectrumOver K A := by + letI : NormedCommRing A := + residueNormedCommRing K A P.n P.ideal P.equiv + letI : NormedAlgebra K A := + residueNormedAlgebra K A P.n P.ideal P.equiv + exact Homeomorph.ulift + +/-- The lifted affinoid point model is canonically homeomorphic to the relative Berkovich +spectrum equipped with the residue norm from the chosen affinoid presentation. -/ +noncomputable def homeomorph {A : Type u} [CommRing A] [Algebra K A] + (hA : IsAffinoidAlgebra K A) : + letI : NormedCommRing A := + residueNormedCommRing K A hA.presentation.n hA.presentation.ideal hA.presentation.equiv + letI : NormedAlgebra K A := + residueNormedAlgebra K A hA.presentation.n hA.presentation.ideal hA.presentation.equiv + topCat K hA ≃ₜ BerkovichSpectrumOver K A := by + exact homeomorphOfPresentation K hA.presentation + +end AffinoidPoint +end Rigid diff --git a/Rigid/Development.lean b/Rigid/Development.lean index 5cece2a..5342d6f 100644 --- a/Rigid/Development.lean +++ b/Rigid/Development.lean @@ -3,6 +3,7 @@ import Rigid.AffinoidAlgebra.AutomaticContinuity import Rigid.AffinoidAlgebra.BanachRealization import Rigid.AffinoidAlgebra.Basic import Rigid.AffinoidAlgebra.MaximalSpectrum +import Rigid.Berkovich.AffinoidPoint import Rigid.Berkovich.Nonempty import Rigid.Berkovich.RelativeSpectrum import Rigid.Berkovich.RelativeNonempty @@ -2492,14 +2493,56 @@ theorem isHausdorff_iff_of_iso {X Y : BerkovichSpace K} (e : X ≅ Y) : /-- A universe-controlled point space for an affinoid Berkovich spectrum. -/ noncomputable def affinoidPointTopCat {A : Type u} [CommRing A] [Algebra K A] - (_hA : IsAffinoidAlgebra K A) : TopCat.{u + 1} := sorry + (_hA : IsAffinoidAlgebra K A) : TopCat.{u + 1} := + Rigid.AffinoidPoint.topCatOfPresentation K + { n := _hA.presentation.n, ideal := _hA.presentation.ideal, equiv := _hA.presentation.equiv } + +private noncomputable def berkovichSpectrumOverHomeomorphRigid + {A : Type u} [NormedCommRing A] [NormedAlgebra K A] [CompleteSpace A] + [IsUltrametricDist A] : + BerkovichSpectrumOver K A ≃ₜ Rigid.BerkovichSpectrumOver K A where + toFun x := + { toBerkovichSpectrum := + ⟨x.toBerkovichSpectrum.seminorm, x.toBerkovichSpectrum.le_norm'⟩ + map_algebraMap' := x.map_algebraMap' } + invFun x := + { toBerkovichSpectrum := + ⟨x.toBerkovichSpectrum.seminorm, x.toBerkovichSpectrum.le_norm'⟩ + map_algebraMap' := x.map_algebraMap' } + left_inv := by intro x; cases x; rfl + right_inv := by intro x; cases x; rfl + continuous_toFun := + (Rigid.BerkovichSpectrumOver.continuous_iff_eval K A).2 fun a ↦ + BerkovichSpectrumOver.continuous_eval K A a + continuous_invFun := + (BerkovichSpectrumOver.continuous_iff_eval K A).2 fun a ↦ + Rigid.BerkovichSpectrumOver.continuous_eval K A a /-- The universe-controlled point space is homeomorphic to the relative Berkovich spectrum. -/ noncomputable def affinoidPointHomeomorph {A : Type u} [CommRing A] [Algebra K A] (hA : IsAffinoidAlgebra K A) : letI : NormedCommRing A := hA.presentation.residueNormedCommRing K A letI : NormedAlgebra K A := hA.presentation.residueNormedAlgebra K A - affinoidPointTopCat K hA ≃ₜ BerkovichSpectrumOver K A := sorry + affinoidPointTopCat K hA ≃ₜ BerkovichSpectrumOver K A := + by + letI : NormedCommRing A := hA.presentation.residueNormedCommRing K A + letI : NormedAlgebra K A := hA.presentation.residueNormedAlgebra K A + letI : CompleteSpace A := hA.presentation.residueCompleteSpace K A + letI : IsUltrametricDist A := hA.presentation.residueIsUltrametricDist K A + change @Homeomorph + (Rigid.AffinoidPoint.topCatOfPresentation K + { n := hA.presentation.n, ideal := hA.presentation.ideal, + equiv := hA.presentation.equiv }) + (BerkovichSpectrumOver K A) + (Rigid.AffinoidPoint.topCatOfPresentation K + { n := hA.presentation.n, ideal := hA.presentation.ideal, + equiv := hA.presentation.equiv }).str + (berkovichSpectrumOverTopologicalSpace K A) + exact + (Rigid.AffinoidPoint.homeomorphOfPresentation K + { n := hA.presentation.n, ideal := hA.presentation.ideal, + equiv := hA.presentation.equiv }).trans + (berkovichSpectrumOverHomeomorphRigid K (A := A)).symm /-- The analytic structure sheaf on an affinoid Berkovich spectrum. -/ noncomputable def affinoidStructureSheaf {A : Type u} [CommRing A] [Algebra K A]