Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeNov 25th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexadded the explicit definition at _[[localization of a commutative ring]]_

   added the explicit definition at localization of a commutative ring

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeNov 25th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexsorry, 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]]_.

   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.

3. • CommentRowNumber3.
   • CommentAuthorzskoda
   • CommentTimeNov 25th 2013
   • PermaLink
   Author: zskoda
   Format: MarkdownItexThere is already entry [[commutative localization]].

   There is already entry commutative localization.

4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeJun 9th 2020
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexKevin Buzzard takes the issue of the identity between $R[1/f][1/g]$ and $R[1/f g]$ as a [problem for type theory](https://twitter.com/XenaProject/status/1270008346763038720). 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?

   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?

5. • CommentRowNumber5.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeJun 17th 2020
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexI 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).

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

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeJun 17th 2020
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexGood! Let us know how you get on. It [seems](https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_08_27_NUS.pdf) 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorzskoda
   • CommentTimeJun 17th 2020
   • PermaLink
   Author: zskoda
   Format: MarkdownItexGabriel-Zisman localization in formalized mathematics has been studied by [[Carlos Simpson]].

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