Stream: new members
Topic: complete lattice of setoids
Amelia Livingston (Sep 03 2019 at 22:42):
Hi! I've written a small file of results about setoids that were generalisations of things I've written about congruence relations.
It's at https://github.com/leanprover-community/mathlib/blob/setoid_complete_lattice/src/data/setoid.lean and it's got stuff like the complete lattice of setoids on a type, results about the inductively defined equivalence closure of a binary relation,
eqv_gen, and the analogues of some isomorphism theorems for quotients of arbitrary types.
I'd like to try and make it PR-able if it's deemed useful.
I'm assuming there's a reason there's no coercion from
setoid α to
α → α → Prop; is
def r' (r : setoid α) := @setoid.r _ r
a sensible alternative if I want to easily talk about different setoids on the same type?
I'd like to add to the file if there's more that should be there, and I realise it might be better off without the lemmas about kernels, split into sections and put in existing appropriate files.
Bryan Gin-ge Chen (Sep 03 2019 at 23:18):
the complete lattice of setoids on a type,
Johannes suggested adding that here, and I would happily close that PR in favor of something built off what you're putting together.
Floris van Doorn (Sep 04 2019 at 02:24):
For the latest Proving for Fun problem set we also had different setoids on a single type. I think it's very welcome to have better support for that. I would maybe call it
setoid.rel instead of
Johan Commelin (Sep 04 2019 at 06:01):
+1 from me. Projection notation to the win! @Amelia Livingston With the suggestion of Floris, we would be able to type
foo.rel to access the relation, for
foo : setoid X.
Amelia Livingston (Sep 04 2019 at 09:24):
@Bryan Gin-ge Chen brilliant, thanks so much for the link! I'll incorporate what's in the partitions file into mine.
rel would definitely be better!
Amelia Livingston (Sep 13 2019 at 11:27):
I've incorporated the partitions file into mine following the advice on the partitions PR and the tutorial thread; as such there's not much infrastructure for working with partitions instead of setoids and I haven't made them a separate structure. I also haven't assumed a partition doesn't contain the empty set until it's needed in theorems (so the docstrings aren't strictly precise).
I was working on showing the Bell numbers are the number of possible partitions of a finite set until I found @Neil Strickland's done this here in a neat and computationally efficient way. If it's okay with him I could try and write an adaptation of that compatible with my file at some point, but it's long and I'm trying to get round to PR'ing some other stuff before term starts. I left in a couple of lemmas about my Bell number function, not sure they should be there.
Last updated: May 12 2021 at 05:19 UTC