Finite Relations

For collections, I want the notion finite to have its orthodox meaning; but I intend to examine what notions applicable to relations in general may collapse down to this special case for collections. In particular, where the right and left equivalences of a relation have finitely many equivalence classes, I consider the relation finite.

I'll describe a relation, r, as finite precisely if it may be factorised via some collection, A, for which {monic (A:f|A)} = {mapping (A|g:A)}. A relation g is a mapping iff g relates a to c and b to c implies a=b; a relation f is monic iff f relates c to a and c to b implies a=b. Factorising r via A means finding some relations u, v for which r = u&on;A&on;v; given that A is a collection, this is just (:u:A)&on;v aka u&on;(A:v:). When r itself is a collection, r is finite becomes synonymous with {monic (r:f|r)} = {mapping (r|f:r)}, though I have yet to prove that.

Note that, for instance, {naturals} isn't finite: successor is monic ({naturals}:|{naturals}) but, although it is a mapping, it isn't ({naturals}|:{naturals}) because empty, in {naturals}, isn't in (|successor:).

I need to prove:

• collection, A, is finite iff {monic (A:|A)} = {mapping (A|:A)}, i.e. factorising via such a collection implies being one.
• empty is finite (easy)
• any intersection of finites is finite
• successor(finite) is finite (indeed, in fact, finite&unite;finite is finite)

much of which I have addressed, at least for collections, in the past.

The assertion | makes

Time to look at: describe a relation r as finite iff {monic (r:m|r)} = {mapping (r|f:r)} then try to decide what | was saying ... The two given collections are one another's images under reverse; so anything I say for f, read as said for reverse(m) likewise. (:x←x:f) must subsume (r:x←x:), for the familiar case's sake. when (:r|) is a non-trivial equivalence, I don't mind each of its equivalence classes being infinite, provided there's only finitely many classes ; for that to work, (r|f:r) has to assert that each (|f:{x}) is subsumed by an equivalence class of (:r|), or possibly, with f = (r|f:r), just that (:r|) subsumes (|f:) ; the latter is a weaker condition