The finset of numerators of a finite set of fractions.

Stream: Is there code for X?

[Yiming Fu]

Can we take the numerators of a finite set of fractions (as a finset)?
I only found docs#IsLocalizedModule.finsetIntegerMultiple.
Any help or clarification would be appreciated!

[Yury G. Kudryashov]

Do you have a #mwe?

[Yury G. Kudryashov]

E.g., are you talking about Rat or something more general?

[Kevin Buzzard]

So you want {1/2, 1/3} |-> {1}? Just use Finset.image on Rat.num?

[Yiming Fu]

Sorry for missing some details. I want to use it for a set of LocalizedModule or IsLocalizedModule.

[Yury G. Kudryashov]

If you have a function for the numerator, then you can use Finset.image.

[Yiming Fu]

Do you mean something like this?

import Mathlib

variable {R : Type*} [CommSemiring R] (S : Submonoid R)
variable {M M' : Type*} [AddCommMonoid M] [AddCommMonoid M']
variable [Module R M] [Module R M'] [DecidableEq M] (f : M →ₗ[R] M') [IsLocalizedModule S f]

noncomputable def getNumerator (x : M') : M :=
  (Classical.choose (IsLocalizedModule.surj S f x)).1

noncomputable def finsetNumerator (s : Finset M') : Finset M := Finset.image (getNumerator S f) s

[Yiming Fu]

If mathlib doesn’t have a better definition, I’ll just use this one.

[Yiming Fu]

Thank you all for your help — now I’ve learned how to use Finset.image.

[Eric Wieser]

It's not clear to me that getNumerator picks a particularly canonical numerator

[Eric Wieser]

IN particular, you might find that {1/2, 2/5} has numerators {2} if 1/2 ends up being treated as 2/4.

[Yiming Fu]

Well, that’s a problem. Let me think about how to choose the canonical numerator...

[Kevin Buzzard]

Mathematically you're not going to have a canonical numerator, even in the integral domain case. Having a canonical numerator is the same as having a canonical denominator in the integral domain case when M=R, and what you have instead is the ideal of denominators, which has no reason to be principal, so you don't even have a canonical numerator up to units in this generality.

[Eric Wieser]

Kevin, am I right in thinking this somehow featured in some Lean slides of yours long ago? I was expecting you to have something to say here :)

[Kevin Buzzard]

I don't know about slides, but mathematically the issue is that if $R$ is an integral domain with field of fractions $K$, and if $x\in K$ then you can consider $I:=\{d\in R\mid dx\in R\}$ and this is easily checked to be an ideal of $R$, but if $R$ is not a PID then you can say very little about it, let alone choose a canonical element of it.

[Kevin Buzzard]

Example: if $R=\Z[\sqrt{-5}]=\{a+b\sqrt{-5}\mid a,b\in\Z\}$ and $x=\frac{1+\sqrt{-5}}{2}$ then $I$ contains $2$ and $1-\sqrt{-5}$ so it's the nonprincipal ideal whose square is 2 and which generates the (nontrivial) class group of $R$.

[Kevin Buzzard]

In more elementary terms, $x=\frac{1+\sqrt{-5}}{2}=\frac{3}{1-\sqrt{-5}}$ and both these fractions are in "lowest terms" (in the sense that there are no common factors than you can cancel other than $\pm1$) but their numerators don't even differ by a unit.

[Kevin Buzzard]

What's going on here is that $6=2\times 3=(1+\sqrt{-5})(1-\sqrt{-5})$ is two distinct factorizations of $6$ into irreducibles (the ring is an integral domain but not a UFD).

[Kevin Buzzard]

Historically it was known since Euclid that the greatest common divisor of two integers was a linear combination of the integers (if the gcd of $a$ and $b$ is $d$ then there are integers $$\lambda$4 anad $\mu$ such that $d=\lambda a+\mu b$), so to try and "fix" this factorization of 6 you need some kind of gcd of 2 and $1+\sqrt{-5}$, and you can start looking for it by looking at the linear combinations $2\lambda +(1+\sqrt{-5})\mu)$ where $\lambda,\mu\in\Z[\sqrt{-5}]=:R$ (because that worked for $\Z$) and you're not sure which one to choose, so you let $I$ be the set of all of them, and then you realise that if $J$ is the analogous set for $3,1+\sqrt{-5}$ and $K$ for $3,1-\sqrt{-5}$ then $I^2=2R$ and $JK=3R$ and $IJ=(1+\sqrt{-5})R$ so now $6R=I^2JK$ and this factorization is unique, so these sets are behaving better than numbers, so they're like "ideal numbers" because things are factorizing uniquely again. Historically a lot of the basics of ring theory like ideals were invented in the mid-1800s by number theorists through the study of concrete subsets of the complexes, before abstract algebra was discovered around 1900.