# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeNov 25th 2013

added the explicit definition at localization of a commutative ring

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeNov 25th 2013

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.

• CommentRowNumber3.
• CommentAuthorzskoda
• CommentTimeNov 25th 2013

There is already entry commutative localization.

• CommentRowNumber4.
• CommentAuthorDavid_Corfield
• CommentTimeJun 9th 2020

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?

1. 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).

• CommentRowNumber6.
• CommentAuthorDavid_Corfield
• CommentTimeJun 17th 2020

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.

• CommentRowNumber7.
• CommentAuthorzskoda
• CommentTimeJun 17th 2020

Gabriel-Zisman localization in formalized mathematics has been studied by Carlos Simpson.