localizations of commutative rings

[Alizter]

In this PR we introduce localizations of commutative rings. This is based on a formalization of the Zariski topology I started back in 2020, but I think the localization is of independent interest.

FTR there is no good generalization of localization for noncommutative rings so I've stuck to commutative rings.

We begin by defining the notion of a multiplicative subset of a ring and give a few examples. We then define the underlying type of a ring localized with respect to a multiplicative subset as a quotient type of fractions. This generalises the field of fractions construction.

The rest of the work consists of showing that we have a commutative ring structure and that we have the expected recursion principle.

Along the way, we introduce various ring lemmas of general use.

[Alizter]

I've added an induciton princple for rng_localization and a lemma for proving uniquness of morphsims out of the localization type. I believe this confirms we have the correct universal property.

[jdchristensen]

By slightly generalizing isinvertible_unique (which incidentally makes it easier to state) and making the proof of isinvertible_inverse_elem compute better, we get that inverse_elem_inverse_elem is definitionally true and equiv_path_inverse_elem has a three line proof. I'll also handle the TODO I added, but wanted it as a separate commit, to make it clear what changed.

[jdchristensen]

I still have more to review, and it might be a couple more days before I get to it.

[Alizter]

The idea here is to show that a certain precomposition map is an equivalence as we do for other kinds of localizations. The LHS should be the hom from the localized ring to another ring T and the RHS should be S-inverting maps. The categories are a little awkward to describe however so I haven't been able to state this. We also would make this an equivalence of groupoids since otherwise funext would be introduced.

[jdchristensen]

As an aside, it would be great to have some "reflection" tools in Coq-HoTT that let us quickly solve all of these goals involving group and ring laws. I heard that the Cubical Agda library has recently added such things, and of course there's lots of work of this nature done in Coq. I wonder if any of it can be easily imported into Coq-HoTT?

[jdchristensen]

Ok, I've finished my review. The only things left to resolve are the naming and whether to add ind2 results to handle the repeated idiom.

[jdchristensen]

Nice, I like how that simplified things!

[Alizter]

I pushed some further cleanups for uses of Quotient_ind2/3 and Quotient_rec2.

[Alizter]

As an aside, it would be great to have some "reflection" tools in Coq-HoTT that let us quickly solve all of these goals involving group and ring laws. I heard that the Cubical Agda library has recently added such things, and of course there's lots of work of this nature done in Coq. I wonder if any of it can be easily imported into Coq-HoTT?

We have some ring reflection tactics already in the library. Though it is from mathclasses so I don't know how easy it would be to get working with the main algebra library. Coq also has its own ring tactics that can solve polynomial expressions in semirings. I don't know if it relies on the stdlib in anyway, but it would be interesting to see if we can adapt its usage here. I'll create an issue.

The key detail with adapting the ring tacitcs is to produce a normalization/reification procedure for semiring expressions together with proofs of correctness. mathcomp also adapts the ring tactic in a custom way, here is their code: https://github.com/math-comp/algebra-tactics/blob/master/theories/common.v