fin (s.card) finset equiv

Stream: Is there code for X?

[Wrenna Robson]

Do we already have this? (Should be an MWE.)

namespace finset
open fintype
noncomputable def fin_equiv {α : Type*} (s : finset α) : fin (s.card) ≃ s :=
equiv_of_card_eq ((card_coe s) ▸ card_fin _)
end finset

To be clear, I know about fintype.fin_equiv. But I specifically want fin (s.card) and not fin (fintype.card s). What I want is an injective function from fin (s.card) to s, and this seems the best way to get it.

[Wrenna Robson]

Alternatively you could have:

namespace finset
open fintype
noncomputable def equiv_fin {α : Type*} (s : finset α) : s ≃ fin (s.card) :=
equiv_of_card_eq (eq.trans (card_coe s) (card_fin _).symm)
end finset

[Violeta Hernández]

Would be nice to have MW imports too

[Wrenna Robson]

oh, bother.

[Wrenna Robson]

I've just closed my lean, I didn't think I was using any of my imports.

[Violeta Hernández]

Doesn't work without imports, so I have to figure out what to import

[Violeta Hernández]

Ah, import data.fintype.card does it

[Wrenna Robson]

Right, yes.

[Violeta Hernández]

This seems alright to me

[Violeta Hernández]

I was expecting fintype.card s and s.card to be def-eq, but it doesn't seem to be the case

[Wrenna Robson]

Yeah, that's the issue I was running into for why I wanted this for convenience.

[Violeta Hernández]

If it doesn't exist already, which it doesn't seem to, then it should totally be PR'd

[Wrenna Robson]

Cool - I'm meant to give a presentation in two hours which I haven't written yet so I'm just doing that first. If you feel like it you can PR it in the meantime ;)

[Wrenna Robson]

Do you think my fin_equiv or equiv_fin is better? Even though it's fin_equiv I want more, I feel like in a PR finset.equiv_fin to match fintype.equiv_fin would be better.

[Wrenna Robson]

You could also have a finset.equiv_of_card_eq, I guess.

[Wrenna Robson]

Why isn't fintype.card s and s.card defeq, I wonder.

[Violeta Hernández]

I prefer fin_equiv out of the general principle of having a simpler RHS

[Wrenna Robson]

Yes, that's how I feel.

[Wrenna Robson]

Maybe we should flip fintype.equiv_fin.

[Violeta Hernández]

docs#fintype.equiv_fin

[Wrenna Robson]

(Which is the corresponding theorem for fintypes.)

[Violeta Hernández]

I guess there is one exception to that principle of a simpler RHS: when your lemma is meant to expand an expression rather than simplify it

[Violeta Hernández]

I guess you can sort of argue that's happening here?

[Wrenna Robson]

Aye. I mean in my context what I want is embeddings from fin blah to the thing... because i'm sort of thinking of this as "labelling things with fin n".

[Violeta Hernández]

Surely there's few circumstances when you'll want to turn fin (fintype.card α) into α, but many where you'll want to do the opposite

[Violeta Hernández]

So yeah, on second thought, equiv_fin is the better one

[Wrenna Robson]

Like what this correspond to, basically, is: "Let s be a finite set of size n. Suppose x_0, x_1, ..., x_(n-1) are the elements of s. Then..."

[Wrenna Robson]

And that is implicitly taking fin (card s) to s.

[Wrenna Robson]

I mean possibly the answer is "even though it would just be an application of symmetry, have both".

[Oliver Nash]

Ages ago, I wanted something like this. I think this was the thread

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Enumerating.20a.20finite.20subset

[Violeta Hernández]

I feel like there's little circumstances where you want names for both sides of an equiv

[Wrenna Robson]

Yes.

[Violeta Hernández]

Because, unless that equiv is incredibly well-behaved (something like a cast between type synonyms), you lose easy access to a lot of theorems about an equivalence and its inverse

[Wrenna Robson]

@Oliver Nash A similar situation to me. It is curious that we have finset.order_iso_of_fin but not the one that doesn't have a requirement for linear_order.

[Wrenna Robson]

list.nodup.nth_le_equiv has fin-first

[Oliver Nash]

Indeed. I’m afraid I’m on a phone on plane at the moment so I can’t say much but I do recall that I persuaded myself that I didn’t really want what I thought I wanted.

[Wrenna Robson]

Unfortunately I do want such an embedding, having tried my best to avoid it.

[Violeta Hernández]

Wrenna Robson said:

Oliver Nash A similar situation to me. It is curious that we have finset.order_iso_of_fin but not the one that doesn't have a requirement for linear_order.

I feel like most people's mental model of an ordered relation is a partial order, or sometimes just a linear order haha

[Violeta Hernández]

That would explain the odd missing generalizations you find now and then

[Wrenna Robson]

Well ideally you don't want an order at all.

[Wrenna Robson]

Like there is in some sense an order induced

[Wrenna Robson]

But it is arbitrary, or at least should be.

[Wrenna Robson]

Sometimes you want to choose it though

[Kyle Miller]

@Wrenna Robson A bit shorter:

noncomputable def equiv_fin {α : Type*} (s : finset α) : s ≃ fin (s.card) :=
fintype.equiv_fin_of_card_eq (fintype.card_coe _)

[Kyle Miller]

Wrenna Robson said:

Why isn't fintype.card s and s.card defeq, I wonder.

That's a good question. I'm not sure if it can be made to be defeq -- to make a fintype instance you need a finset that enumerates all the elements of s coerced to a type, and currently it uses s.attach to do so:

example {α : Type*} (s : finset α) : fintype.card s = s.attach.card := rfl

[Violeta Hernández]

So really, this boils down to asking why finset.univ : finset s isn't def-eq to s

[Yaël Dillies]

That doesn't typecheck, right?

[Violeta Hernández]

Oh, yeah

[Violeta Hernández]

Well, there's the answer, isn't it?

[Violeta Hernández]

fintype.card s is defined as (finset.univ : finset s).card while s.card is just that

[Violeta Hernández]

Which makes sense I think

[Kyle Miller]

Still, I wonder if there's some trick where you can make fintype.card s reduce to s.card. The problem right now is that attach is a map operation over the underlying list, and that doesn't preserve the length definitionally.

[Violeta Hernández]

btw note s.attach is def-eq to (finset.univ : finset s)

[Violeta Hernández]

And finset.univ is def-eq to fintype.elems

[Kyle Miller]

Yes, finset.univ : finset s is defeq to s.attach because of docs#finset.fintype_coe_sort, which defines the fintype s instance.

[Violeta Hernández]

So really, I think the issue is that fintype.elems s isn't def-eq to s, which it can't reasonably be because they aren't of the same type

[Violeta Hernández]

It doesn't seem reasonable to define fintype.card s as anything other than (fintype.elems s).card

[Kyle Miller]

Sure, that's the proximal issue, but there still might be some trick so that (fintype.elems s).card reduces to s.card by using something other than s.attach. Neither of us can think of anything, but that doesn't mean that there isn't something that would work in place of s.attach.

[Kyle Miller]

It seems unlikely, but I'm not willing to say it's impossible here.

[Kyle Miller]

One solution would be to extend fintype to include a card field so you can get definitional control over it.

meta def tactic_rfl : tactic unit := `[exact rfl]

class fintype' (α : Type*) :=
(elems [] : finset α)
(complete : ∀ x : α, x ∈ elems)
(card : ℕ := elems.card)
(card_eq : card = elems.card . tactic_rfl) -- just so the default case automatically goes through

[Eric Wieser]

If you want to go down that route, you could also have card be a member of finsets, multisets, or even lists

[Kyle Miller]

This seems it could easily lead to "fun." Imagine getting to use the finset.reset_card lemma to reset the internal card field to the card of its multiset, after spending some time wondering why you weren't able to rw with some other lemma.

[Wrenna Robson]

Kyle Miller said:

Wrenna Robson A bit shorter:

noncomputable def equiv_fin {α : Type*} (s : finset α) : s ≃ fin (s.card) :=
fintype.equiv_fin_of_card_eq (fintype.card_coe _)

Very nice.

[Wrenna Robson]

Still not quite sure why all the lemmas like this for list e.g. list.nodup.nth_le_equiv have the fin on the left, but all these are on the right for fintype.

[Wrenna Robson]

Like you'd think they'd all be the same.

[Wrenna Robson]

Would you want a finset.trunc_equiv_fin as well? The computable version.

[Wrenna Robson]

Violeta Hernández said:

So really, I think the issue is that fintype.elems s isn't def-eq to s, which it can't reasonably be because they aren't of the same type

Oh, because one is a finset s and the other is finset \alph or whatever?

[Kyle Miller]

Wrenna Robson said:

Would you want a finset.trunc_equiv_fin as well? The computable version.

I'd say "no" unless you're using it. How much would having finset.equiv_fin simplify your work, by the way? I'm wondering if (equiv_fin_of_card_eq (card_coe _)).symm (assuming open fintype) is already short enough of a name for what you're doing.

[Kyle Miller]

(The trunc_equiv_fin definition is used extremely rarely in mathlib -- only 3 legitimate uses outside fintype/basic -- which is why I suggest not including finset.trunc_equiv_fin. I just made #15076 and #15077 to remove the uses that were in a computation-free and classical context so don't need to be computable.)

[Wrenna Robson]

Yeah, I wasn't sure why it existed. finset.equiv_fin wouldn't simplify things a lot but it would make like one line less unwieldy.

[Kyle Miller]

@Wrenna Robson I'm sort of ambivalent about finset.equiv_fin, but even though it's just a composition of two things, may as well add it since it makes it easier to find this particular equivalence.

I think new definitions usually need some sort of justification since there's a cognitive cost to adding definitions to mathlib, and these are some justifications that come to mind:

• It's a common expression and will save on repetition.
• It chooses a canonical way of stating something (a nexus for a concept).
• There is theory surrounding it.

It's worth considering that not everything needs an explicit name, and sometimes the body of a definition might be about the same length as the name of the definition itself (so it can be its own name, so to speak).

However, for this equivalence, I suspect that anyone who uses it only really cares that the equivalence exists, and it's a more convenient writing it this way than having it be a lemma proving nonempty (s ≃ fin s.card).

[Kyle Miller]

By the way, here's one of the uses of trunc_equiv_fin: https://github.com/leanprover-community/mathlib/blob/eb852609e908d661c0e31c94fa3fff6d113b9d6e/src/group_theory/perm/sign.lean#L427

It's an auxiliary function for computing the sign of a permutation, and since it's computable you can #eval the sign function if you wanted to.

[Wrenna Robson]

I mean really I even only care that there's an embedding from fin n to s where s.card = n: it's literally just the "we can label the finset" concept.

[Wrenna Robson]

What file should this be in? Feels like I can't put it in the finset bit of data.fintype.basic because that is before the fintype version which it makes sense to use

[Wrenna Robson]

See #15080

[Wrenna Robson]

@Kyle Miller fyi