Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Algebraic geometry #1095

Closed
mzeuner opened this issue Feb 1, 2024 · 2 comments
Closed

Algebraic geometry #1095

mzeuner opened this issue Feb 1, 2024 · 2 comments

Comments

@mzeuner
Copy link
Contributor

mzeuner commented Feb 1, 2024

By now, the library has quite a bit of stuff on (constructive) algebraic geometry, but it is spread out.
The stuff based on the lattice theoretic approach of Coquand, Lombardy and Schuster is in Cubical.Algebra.ZariskiLattice, whereas the functor of points approach is developed in Cubical.Categories.Instances.ZFunctors.

I would suggest to make a folder Cubical.AlgebraicGeometry that itself contains to folders for the two approaches currently (partly) formalized and move everything algebraic geometry related there.

Does that sound like a reasonable idea?
@mzeuner mzeuner mentioned this issue Feb 1, 2024
Merged
@mortberg
Copy link
Collaborator

mortberg commented Feb 1, 2024

Yes, that would be great

@mzeuner mzeuner mentioned this issue Feb 6, 2024
Closed
@mortberg
Copy link
Collaborator

Has this been fixed now?

@mzeuner mzeuner closed this as completed May 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@mortberg @mzeuner