Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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]R[1/f][1/g] and R[1/fg]R[1/f g] as a problem for type theory.

    Say I wanted to show that for a ring, RR, a set of its elements, SS, and a partition of SS into S 1S_1 and S 2S_2, that R[S] 1R[S]^{-1} and (R[S 1] 1)[S 2] 1(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.