Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added the explicit definition at localization of a commutative ring
sorry, I should have put this into localization of a ring. Done so now and added the definition by quotienting an ideal to localization of a commutative ring.
There is already entry commutative localization.
Kevin Buzzard takes the issue of the identity between $R[1/f][1/g]$ and $R[1/f g]$ as a problem for type theory.
Say I wanted to show that for a ring, $R$, a set of its elements, $S$, and a partition of $S$ into $S_1$ and $S_2$, that $R[S]^{-1}$ and $(R[S_1]^{-1})[S_2]^{-1}$ are ’canonically’ identical, is this really a problem for HoTT?
I think there is only one way to find out, namely to try it :-), and I hope to do it over the next couple of days (in Cubical Agda).
Good! Let us know how you get on.
It seems Voevodsky worked on localization:
To test the applicability of Univalent Foundations to actual formalization of mathematics I wrote a library of formalized mathematics for Coq which developed abstract algebra up to the construction of localization of commutative rings.
Gabriel-Zisman localization in formalized mathematics has been studied by Carlos Simpson.
1 to 7 of 7