Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2407.17362 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
Tabla de Contenidos:
- We investigate two constructive approaches to defining quasi-compact and quasi-separated schemes (qcqs-schemes), namely qcqs-schemes as locally ringed lattices and as functors from rings to sets. We work in Homotopy Type Theory and Univalent Foundations, but reason informally. The main result is a constructive and univalent proof that the two definitions coincide, giving an equivalence between the respective categories of qcqs-schemes.