Skip to content

Construct universe-controlled affinoid Berkovich point model - #45

Open
kernelpanic888 wants to merge 1 commit into
dagurtomas:mainfrom
kernelpanic888:codex/affinoid-point-universe-39
Open

Construct universe-controlled affinoid Berkovich point model#45
kernelpanic888 wants to merge 1 commit into
dagurtomas:mainfrom
kernelpanic888:codex/affinoid-point-universe-39

Conversation

@kernelpanic888

Copy link
Copy Markdown

Summary

  • add a production affinoid Berkovich point model using ULift
  • transport the existing topology canonically and expose Homeomorph.ulift
  • close the two comparator targets without changing Rigid/Challenge.lean

Closes #39

Scope boundary

This is only the affinoid point-set model. It does not define a structure sheaf or claim a completed Berkovich space.

Validation

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

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.

Construct the universe-controlled affinoid Berkovich point model

1 participant