Skip to content

Define rigid admissible sites and G-ringed spaces - #42

Merged
dagurtomas merged 10 commits into
dagurtomas:mainfrom
katobungen:rigid_codex_23Jul
Jul 23, 2026
Merged

Define rigid admissible sites and G-ringed spaces#42
dagurtomas merged 10 commits into
dagurtomas:mainfrom
katobungen:rigid_codex_23Jul

Conversation

@katobungen

Copy link
Copy Markdown
Contributor

Summary

  • define admissible G-sites via pretopologies and their generated Grothendieck topologies
  • define G-ringed and G-locally ringed spaces with sheaf-valued structure sheaves and colimit stalks
  • define continuous morphisms and their induced local stalk maps
  • add rigid-space saturation axioms and admissible affinoid atlases following Chapters 4–5
  • keep the implementation split into focused production modules with direct root imports

Closes #35.

Verification

  • ./scripts/check_root_imports.sh
  • ./scripts/check_challenge_development.sh
  • lake build Rigid

Yoaskay and others added 10 commits July 23, 2026 08:12
Model the ordinary K-locally-ringed layer as locally ringed spaces over the universe lift of Spec K. Reuse mathlib for the faithful forgetful functor, point maps, sections, stalks, and germs, and correct the global Berkovich comparator universes to contain this core.
# Conflicts:
#	Rigid/RigidSpace/AdmissibleSite.lean
#	Rigid/RigidSpace/CanonicalTopology.lean
#	Rigid/RigidSpace/Morphism.lean
@dagurtomas
dagurtomas merged commit e5ecd52 into dagurtomas:main Jul 23, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Build reusable G-site/G-ringed infrastructure and its rigid instantiation

3 participants