finset to list

Stream: Is there code for X?

[Kevin Buzzard]

1) Do we have a noncomputable finset X -> list X (a one-sided inverse of list.to_finset)? I can make it but if it's there already I'd rather use what's there. I was hoping to use #find to find it but I failed.

2) If X has decidable equality and a total ordering, do we have a computable finset X -> list X? Asking for a friend.

[Eric Wieser]

We have docs#finset.sort for 2)

[Eric Wieser]

As for 1, that's s.1.out I think (docs#finset.val, docs#quotient.out)

[Kevin Buzzard]

yes that was my construction for 1, I was just wondering if there was an API

[Eric Wieser]

I doubt there is, given there's not even API for m.out whenm : multiset X

[Kevin Buzzard]

as for 2 I've never looked at that file before! Thanks! This is for an MSc student who's been doing too much Agda

[Yakov Pechersky]

It begs the question, what's the list going to be used for?

[Reid Barton]

maybe printing it to the screen? :scream:

[Eric Wieser]

Well then 1) probably isn't an option

[Eric Wieser]

You need quot.unquot s.1 instead if you're trying to print

[Joseph Hua]

its for reconstructing multivariable polynomials over a field as (symbolic) sums of monomials in the terms in the language of rings. since it is symbolic (hence not having add_comm_monoid) i can't make sums using finset

[Eric Wieser]

i can't make sums using finset

Why not?

[Yakov Pechersky]

We defined a noncomm_sum for finset such that you can still sum when the underlying addition isn't commutative but in the finset it is.

[Yakov Pechersky]

Not sure why docs linkifier won't link it

[Eric Wieser]

I suspect the problem is that (add x y) = (add y x) is not true in Joseph's "symbolic" terms

[Yakov Pechersky]

Whatever the sum is over your extracted list, if you're going to be using it, you'll have to prove at some point that it didn't matter which list you extracted. Or am I misunderstanding something?

[Floris van Doorn]

Yakov is talking about docs#finset.noncomm_sum.

[Reid Barton]

Is this for a tactic or for some internal argument?

[Reid Barton]

e.g. if you're trying to prove an internal proposition like "for any polynomial $f \in R[x,y]$, there exists a term in the language of an $R$-algebra extended by two constant symbols $X$ and $Y$ that interprets to $f$ when we set $X = x$ and $Y = y$" then you don't need either 1) or 2)

[Kevin Buzzard]

I think that this will be one of the things @Joseph Hua wants except with n variables not 2

[Kevin Buzzard]

he wants to see how much of the model theory proof of Ax-Grothendieck is feasible before we both get stuck

[Joseph Hua]

because sums using finset require having add_comm_monoid on the type, I only have has_zero, has_add, has_neg, has_one, has_mul

[Kevin Buzzard]

Yes, we're really in a position where the sum is not well-defined, but it is well-defined up to associativity and commutativity, so when the term is evaluated in ring theory it will be well-defined.

[Adam Topaz]

You can probably avoid model theory and still reduce from $\mathbb{C}$ to $\overline{\mathbb{F}_p}$ by specializing along a maximal valuation of $\mathbb{C}$ (whose residue field must be the algebraic closure of a finite field). Does anyone know is such an argument along these lines has been written down?

[Eric Wieser]

If you take a quotient by the kernel of evaluation map, then your addition becomes commutative

[Eric Wieser]

But also if you're using polynomials in a single variable (as opposed to mv_polynomial which wasn't mentioned above) then there's an obvious ordering of monomials anyway, so .sorted is indeed a sensible choice.

[Kyle Miller]

Kevin Buzzard said:

1) Do we have a noncomputable finset X -> list X

docs#finset.to_list

[Kyle Miller]

Eric Wieser said:

I doubt there is, given there's not even API for m.out whenm : multiset X

It's called docs#multiset.to_list instead.

[Reid Barton]

I see there is also docs#finset.exists_list_nodup_eq which is the kind of approach I had in mind