finsetoid

Stream: Is there code for X?

[Nicholas Tan]

I see that we have defined setoid that works on arbitrary sets but do we have anything for finsets ? Specifically, the classes of an equivalence relation (src/data/setoid/partition.lean) has type set (set a) whereas I wish it had type finset (finset a) .

If there is a way to generalize finsets as sets (with restrictions), I would be happy too.

Edit: perhaps set.to_finset

[Yakov Pechersky]

You want the other direction. And yes, all finsets are coercible to sets. If you have a (s : finset X), you can just write (s : set X)

[Nicholas Tan]

The problem is that setoid currently lifts it for me, which I don't want
def orbits [fintype α] [fintype G] : finset (finset α) := setoid.classes (orbit_rel G α)
(gives error)
def orbits [fintype α] [fintype G] : set (set α) := setoid.classes (orbit_rel G α)
(no error, but I need the finiteness)
def orbits [fintype α] [fintype G] : finset (set α) := set.to_finset (setoid.classes (orbit_rel G α))
(not computable, depends on classical.prop_decidable)

[Yakov Pechersky]

What do you hope to use the finset for? Do you have decidable_eq on alpha and G?

[Yakov Pechersky]

Do you care about computability?

[Nicholas Tan]

I would like to show that the sum of the sizes of the classes of an equivalence relation over a set is the same as the cardinality of the set itself.

[Nicholas Tan]

but i cant use $\Sigma$ because setoid.classes is not a finset

[Kevin Buzzard]

Then use finsum

[Eric Wieser]

And docs#nat.card instead of finset.card

[Adam Topaz]

If you don't care about computability, here's a sorry you could try to fill in

import data.setoid.partition
import data.fintype.basic
import algebra.big_operators

noncomputable theory

open_locale classical big_operators

variables {α : Type*} [fintype α] (S : setoid α)

example : ∑ s in S.classes.to_finset, (s : set α).to_finset.card = fintype.card α := sorry

[Adam Topaz]

(This is if you don't care about computability, since I've opened the classical locale)

[Yakov Pechersky]

I agree with Adam. You can just use set.to_finset since you're working over fintypes. I think the classical won't even be necessary if you also require decidable_eq alpha. Because, if I understand correctly, orbit should have a decidability instance in that case. Or you could write that simple algorithm.

[Yaël Dillies]

FYI Bhavik and I are using finpartition α for finset (set α).. It's not yet in mathlib.