Puzzle 43: The way I would define the pushforward \\(f_!(P)\\) of a partition \\(P\\) is by first using \\(f_!: P(X)\to P(Y) \\) to push forward each part of P, getting a family of subsets of \\(Y\\), and then taking the finest partition \\(Q\\) of \\(Y\\) such that each subset in the family is contained in one of \\(Q\\)'s parts.

On the level of equivalence relations, it would look like this: Given an equivalence relation \\(\approx\\) on \\(X\\), first define \\(y_1\sim y_2\\) in \\(Y\\) by \\(y_1\sim y_2\iff \\) (there exist \\(x_1\mapsto y_1\\) and \\(x_2\mapsto y_2\\) such that \\(x_1\approx x_2\\) in \\(X\\)). This relation \\(\sim\\) is always symmetric, but generally not transitive, and is not even reflexive if \\(f:X\to Y\\) is not surjective. So make \\(\sim\\) into an equivalence relation on \\(Y\\) by generously adding everything it's missing: declare \\(y\approx y'\\) iff there is a chain of elements \\(y_0,\dots,y_n\\) in \\(Y\\) such that \\(y = y_0\sim y_1\sim\ldots\sim y_n=y'\\).

Each step in this construction is monotone with respect to fineness: if \\(x_1\approx x_2\\) implies \\(x_1\approx' x_2\\), then \\(y_1\sim y_2\\) implies \\(y_1\sim' y_2\\) and \\(y_1\approx y_2\\) implies \\(y_1\approx' y_2\\). So we've produced a monotone map of posets \\(f_! : \mathcal{E}(X)\to \mathcal{E}(Y)\\).

On the level of equivalence relations, it would look like this: Given an equivalence relation \\(\approx\\) on \\(X\\), first define \\(y_1\sim y_2\\) in \\(Y\\) by \\(y_1\sim y_2\iff \\) (there exist \\(x_1\mapsto y_1\\) and \\(x_2\mapsto y_2\\) such that \\(x_1\approx x_2\\) in \\(X\\)). This relation \\(\sim\\) is always symmetric, but generally not transitive, and is not even reflexive if \\(f:X\to Y\\) is not surjective. So make \\(\sim\\) into an equivalence relation on \\(Y\\) by generously adding everything it's missing: declare \\(y\approx y'\\) iff there is a chain of elements \\(y_0,\dots,y_n\\) in \\(Y\\) such that \\(y = y_0\sim y_1\sim\ldots\sim y_n=y'\\).

Each step in this construction is monotone with respect to fineness: if \\(x_1\approx x_2\\) implies \\(x_1\approx' x_2\\), then \\(y_1\sim y_2\\) implies \\(y_1\sim' y_2\\) and \\(y_1\approx y_2\\) implies \\(y_1\approx' y_2\\). So we've produced a monotone map of posets \\(f_! : \mathcal{E}(X)\to \mathcal{E}(Y)\\).