Explaining Gabriel-Zisman localization to the computer
范畴论
2007-05-23 v1 代数几何
逻辑
摘要
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.
引用
@article{arxiv.math/0506471,
title = {Explaining Gabriel-Zisman localization to the computer},
author = {Carlos T. Simpson},
journal= {arXiv preprint arXiv:math/0506471},
year = {2007}
}