Construct universe-controlled affinoid Berkovich point model

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

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

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]