Cantor-Schröder-Bernstein, redux

[jamesmckinna]

Currently, we have in Data.Fin.Properties

cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} →
                            Injective _≡_ _≡_ f → Injective _≡_ _≡_ g →
                            m ≡ n

but nowhere do we followup on this to prove the 'real' result, namely that

cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} →
                            Injective _≡_ _≡_ f → Injective _≡_ _≡_ g →
                            Permutation m n

ie that there is an isomorphism between Fin m and Fin n, indeed we could/should have this as a consequence of the yet stronger

cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} →
                            Injective _≡_ _≡_ f → Injective _≡_ _≡_ g →
                            Inverseᵇ f g

So: we should refactor to tidy all this up!

[JacquesCarette]

Yes, we should. If you don't around to it, I might get one of my two (new!) summer students to do it.

I don't see how the third is stronger than the second? I'm probably mis-remembering definitions.

[jamesmckinna]

@JacquesCarette writes:

I don't see how the third is stronger than the second? I'm probably mis-remembering definitions.

The second (via Inverse/_↔_) asserts the bundled existence of some f and g which are inverse, whereas the third asserts that the supplied f and g are in fact the required witnesses...

[Taneb]

cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} →
                            Injective _≡_ _≡_ f → Injective _≡_ _≡_ g →
                            Inverseᵇ f g

This particular definition is too strong: it's in fact false. Here's a counterexample:

f : Fin 2 → Fin 2
f x = x

finj : Injective _≡_ _≡_ f
finj p = p

g : Fin 2 → Fin 2
g zero = suc zero
g (suc zero) = zero

ginj : Injective _≡_ _≡_ g
ginj {zero} {zero} refl = refl
ginj {zero} {suc zero} ()
ginj {suc zero} {suc zero} refl = refl

¬fginverse : ¬ Inverseᵇ _≡_ _≡_ f g
¬fginverse (p , _) with () ← p {zero} refl

[jamesmckinna]

Ugh! Oops! Thanks @Taneb What about the second version? (and then: for me, or @JacquesCarette 's student(s), what is the relationship between f, g and the bundled witnesses? Martin Hofmann had a formalisation (in LEGO?) of the back-and-forth argument for CSB way back in the 1990s... will try to dig it out).

[MatthewDaggitt]

The second one is fine because Permutation m n -> m = n -> and so there's a trivial permutation of `id`. However, it's not very interesting?

…

On Fri, Jun 6, 2025 at 2:17 PM jamesmckinna ***@***.***> wrote: *jamesmckinna* left a comment (agda/agda-stdlib#2728) <#2728 (comment)> Ugh! Oops! Thanks @Taneb <https://github.com/Taneb> What about the second version? (and then: for me, or @JacquesCarette <https://github.com/JacquesCarette> 's student(s), what is the relationship f, g and the bundled witnesses? Martin Hofman had a formalisation (in LEGO?) of the back-and-forth argument for CSB way back in the 1990s... will try to dig it out) — Reply to this email directly, view it on GitHub <#2728 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAP26EQ5YWBE5LF53MOC5VD3CEXATAVCNFSM6AAAAAB6WSFCZ2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDSNBYGIYTQOBUGM> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[jamesmckinna]

@MatthewDaggitt indeed, and that's why the 'interesting' version (with the first version following as a consequence of Permutation m n → m ≡ n) should try to relate the actual witnesses to the supplied f and g... and I was stupidly hasty to assume that they alone would suffice... when the back-and-forth argument is more subtle than that!

[JacquesCarette]

For the 'interesting' version, I doubt you'll be able to get away without saying (essentially) that they are inverses. There are n! choices that an injective function can make, and its companion has to make (in reverse) the exact same ones.

[Taneb]

1. the theorem is most interesting in the classical case where it works on infinite sets, and is the easiest way to get any bijection between them
2. on finite sets, an interesting property is that the resulting h is at each point either equal to f or to g^-1
3. do we have a case where we'd want to use (some variant of) this theorem?

[jamesmckinna]

@Taneb thanks for the feedback. To your points:

3. The case I had had in mind was precisely to refactor the existing proof in Data.Fin.Properties to go via the stronger theorem and Data.Fin.Permutation.↔⇒≡... which may be no more than window dressing, but still.
4. Agreed, and the paper proof I've more or less got working makes this clear, as well as developing a bit more infrastructure in Data.Fin.Properties to sharpen ¬∀⟶∃¬-smallest there.
5. Also agreed, so the real interest is in comparing a direct inductive proof for Fin, and the classical proof (esp. the one based on Knaster-Tarski). Of interest here is that using Relation.Nullary.Decidable.via-injection we do have access to classical methods, on the assumption that one of the arbitrary infinite sets A or B carries a IsDecEquivalence structure, because then they both do... and of course each Fin n satisfies this condition.

For DecSetoids, I think it is also separately interesting that they support an operation to 'subtract'/detach any single element, and more generally a finite subset (enumerated by some Fin n), and this operation is the basis for the inductive construction I've been developing.

So I think there is a contribution to be made here!