OAI/AlgebraicGeometry/SurfaceCones.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Kummer surfaces and completed surface cones
The constructions in OpenAI's A Complete Local Domain without a Small Cohen–Macaulay Module (2026) describe an explicit Kummer surface, its graded cone and its completion. The associated coherent sheaves carry duality, Cartier lattice filtrations and canonical-form calculations.
This file declares nothing itself. It gathers the 3 imports below, so a file that imports it gets all of them.