Explaining Gabriel-Zisman localization to the computer

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

This explains a computer formulation of Gabriel-Zisman localization of categories in the proof assistant Coq. It includes both the general localization construction with the proof of GZ's Lemma 1.2, as well as the construction using calculus of fractions. The proof files are bundled with the other preprint "Files for GZ localization" posted simultaneously.

Keywords

Category Theory, Algebraic Geometry, Logic

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/75564

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/math/0506471
 http://arxiv.org/abs/math/0506471

Collections

arXiv