Parent
Subtask of #21, split from draft PR #34. Comparator targets were added in d960950.
Goal
Construct a universe-controlled topological point model for an affinoid Berkovich spectrum.
Comparator targets
BerkovichSpace.affinoidPointTopCat
BerkovichSpace.affinoidPointHomeomorph
Scope
For a strict affinoid algebra in the ground-field universe, construct a TopCat.{u + 1} point space, likely by lifting the relative Berkovich spectrum and transporting its topology. Prove it homeomorphic to BerkovichSpectrumOver K A with the canonical residue norm and normed-algebra instances.
This issue deliberately excludes the structure sheaf and global Berkovich-space assembly.
Acceptance criteria
- No point-only object is presented as a completed Berkovich space.
- The topology is transported canonically and the universe levels match the comparator.
- Production files contain no
sorry.
- Focused, root-import, comparator, and full
Rigid builds pass.
Parent
Subtask of #21, split from draft PR #34. Comparator targets were added in
d960950.Goal
Construct a universe-controlled topological point model for an affinoid Berkovich spectrum.
Comparator targets
BerkovichSpace.affinoidPointTopCatBerkovichSpace.affinoidPointHomeomorphScope
For a strict affinoid algebra in the ground-field universe, construct a
TopCat.{u + 1}point space, likely by lifting the relative Berkovich spectrum and transporting its topology. Prove it homeomorphic toBerkovichSpectrumOver K Awith the canonical residue norm and normed-algebra instances.This issue deliberately excludes the structure sheaf and global Berkovich-space assembly.
Acceptance criteria
sorry.Rigidbuilds pass.