Ring homomorphism from the integers to the rationals

[andreasabel]

I was looking for the definition of the ring homomorphism ZtoQ : Z -> Q with proofs that the ring operations are preserved, but did not find such. If this exists already, please let me know where to find it.
Otherwise, would an implementation of this component be welcome?
If there already ideas/expectations where this should live and how it should look like, please let me know.

[jamesmckinna]

One thing the library has long been missing is a systematic treatment of Free structures/bundles, and in this case, characterising the integers as the free Ring on the empty set of generators ... and hence a (unique!) homomorphism from Z to any Ring... be it Q or anything else.

[andreasabel]

Digging a bit deeper, I also did not find a ring homos between the rationals and the unnormalized ones.

One thing the library has long been missing is a systematic treatment of Free structures/bundles, and in this case, characterising the integers as the free Ring on the empty set of generators ... and hence a (unique!) homomorphism from Z to any Ring... be it Q or anything else.

I suppose a free ring of level l is a ring R plus a an index set G : Set l and a map gen : G -> R. Those should maybe be bundled together as a "Collection" Sigma (G : Set l). G -> R. (A collection could be represented as the denotation of a container with a single shape, but this seems like an overkill.)

For now, I would however stick to the ground and do a direct implementation of the Z->Qu homo. The free construction can always be added later and replace the direct implementation, should an application demand for it.

[jamesmckinna]

Digging a bit deeper, I also did not find a ring homos between the rationals and the unnormalized ones.

See: #2113

One thing the library has long been missing is a systematic treatment of Free structures/bundles, and in this case, characterising the integers as the free Ring on the empty set of generators ... and hence a (unique!) homomorphism from Z to any Ring... be it Q or anything else.

I suppose a free ring of level l is a ring R plus a an index set G : Set l and a map gen : G -> R. Those should maybe be bundled together as a "Collection" Sigma (G : Set l). G -> R. (A collection could be represented as the denotation of a container with a single shape, but this seems like an overkill.)

See also: #1962 #2539

For now, I would however stick to the ground and do a direct implementation of the Z->Qu homo. The free construction can always be added later and replace the direct implementation, should an application demand for it.

It's an interesting design problem. In the interests of 'making progress', some might favour incremental concrete constructions ('bottom-up' development), but I think here that there is a clear need for a more 'top-down' approach.

While I wouldn't stand in the way of any contribution in this space, I might suggest that your design at least be alive to/align with the wider prospectus envisioned in the above issues.

[Taneb]

Data.Rational.Properties has a ring monomorphism from ℚ to ℚᵘ. It's not hard to show that this extends to an isomorphism:

toℚᵘ-isRingIsomorphism-+-* : IsRingIsomorphism +-*-rawRing ℚᵘ.+-*-rawRing toℚᵘ
toℚᵘ-isRingIsomorphism-+-* = record
  { isRingMonomorphism = toℚᵘ-isRingMonomorphism-+-*
  ; surjective = λ y → fromℚᵘ y , λ eq → ℚᵘ.≃-trans (ℚᵘ.≃-reflexive (cong toℚᵘ eq)) (toℚᵘ-fromℚᵘ y)
  }

I had thought that we had a proof somewhere that isomorphisms are invertible, but now I can't find it. If we did have that, we could use it to easily get the other direction, and then we can compose that with a ring monomorphism from ℤ to ℚᵘ (I tried to implement that while on a train yesterday - showing addition is homomorphic is the only tricky bit)

[Taneb]

Related to @jamesmckinna's point, we can show that ℤ is the initial ring, and get this homomorphism "for free", probably easier than showing it's a free ring. But I'm worried that that would be operationally worse than defining it directly and concretely, if we're not careful.