SUO: Re: IFF LOT Glossary
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Robert,
I return to a point near the beginning
of this thread to see if I've learned
anything in the meantime that will
help me to untangle it in my head.
| Recall that for any function
|
| f : A --> B
|
| from set A to set B, there is a function
|
| fib(f) : B --> pow(A)
|
| called the "fiber of f" which given any element b in B returns the subset
|
| fib(f) = {a in A | f(a) = b}
|
| of all elements of A that map to b.
|
| Here, fib(f)(b) is called "the f-fiber over b".
|
| RK: http://suo.ieee.org/email/msg10123.html
Looks like a typo that should be:
fib(f)(b) = = {a in A | f(a) = b}
JA: For a small example, let's say we have the following function f : X -> Y.
0 1 2 3 4 5 6 7 8 9
o o o o o o o o o o X
| \ | / \ \ | | \ /
| \ | / \ \ | | \ /
| \ | / \ \ | | \ f
| \ | / \ \ | | / \
v vvv v vv v v v
o o o o o o o o o o Y
0 1 2 3 4 5 6 7 8 9
I am used to saying that the inverse relation of f evaluated at y in Y,
brutally asciified as (f^(-1))(y), is the "fiber of f at y", so that is
familiar enough, "up to idiom-morphisms". Gloss fib(f)(y) as f^(-1)(y).
So fib(f) = f^(-1) is the 2-adic relation that is inverse or converse to f.
Well, not exactly, but via the obvious isomorphism, f^(-1) c Y x X being
the "same information" as fib(f) : Y -> Pow(X). Reading f backupwards:
0 1 2 3 4 5 6 7 8 9
o o o o o o o o o o X
^ ^ ^ ^ ^ ^ ^ ^ ^ ^
| \ | / \ \ | | \ /
| \ | / \ \ | | \ f^(-1)
| \ | / \ \ | | / \
| \|/ \ \| | / \
o o o o o o o o o o Y
0 1 2 3 4 5 6 7 8 9
This becomes fib(f) : Y -> Pow(X), which looks like this:
{0} { } {1,2,3} { } { } {4} {5,6} {7} {9} {8}
o o o o o o o o o o Pow(X)
^ ^ ^ ^ ^ ^ ^ ^ ^ ^
| | | | | | | | | |
| | | | | | | | | | fib(f)
| | | | | | | | | |
| | | | | | | | | |
o o o o o o o o o o Y
0 1 2 3 4 5 6 7 8 9
The important thing in all this fiber business is the formation of classes in the
functional domain X, where the elements of each class are equivalent in some sense
or another, here, quite literally getting "equal values" under the function f, that
one accordingly regards as classifying the domain elements by their functional value.
Further, in the case of a genuine (total) function, the equivalence classes partition
the functional domain X in the very way that any equivalence relation on X x X would do.
| We extend this terminology to categories in place of sets
| and functors in place of functions. There is a functor
|
| base : Theory --> Language
|
| from the category of theories to the category of languages.
|
| Consider the object function
|
| obj(base) : obj(Language) --> obj(Theory)
|
| of the base functor. Given any theory, this returns the underlying base FOL
| language consisting of the sets of relation, function and sort symbols used
| in the axioms and relational arities of the theory. The "base language fiber"
| refers to the "fiber of obj(base)"; that is, to the fiber of the function
| fib(obj(base)). For any language L in obj(Language), this returns the
| subclass
|
| fib(obj(base))(L) = {T in obj(Theory) | obj(base)(T) = L}
|
| of all theories of whose underlying base language is L.
| Here, fib(obj(base))(L), or fib(base)(L) for short, is
| called "the base fiber over L". This is the underlying
| set of the lattice of theories over L: LOT(L) = fib(base)(L).
|
| The morphic aspect of the base functor also comes into this picture.
| First of all, when the lattice of theories LOT(L) is regarded as part
| of the category of theories, there is a morphism g : T1 --> T2 between
| two theories in LOT(L) precisely when base(g) L --> L is the identity
| and T1 >= T2 in the lattice entailment order (T2 entails any axiom of T1).
| Secondly, for any morphism of languages f : L1 --> L2 in the category of
| languages, there are direct and inverse image functions
|
| dir(f) : LOT(L1) --> LOT(L2)
| inv(f) : LOT(L2) --> LOT(L1)
|
| that are adjoint monotonic functions. These are important for
| moving theories around, as the following paragraph indicates.
|
| A *diagram of theories* is the IFF representation for
| either an "unpopulated modular object-level ontology"
| or a "library of modules". Using the base functor,
| every diagram of theories T has an underlying base
| diagram of languages L = base(T). Take the colimit
| col(L) of this base diagram. Then the colimit of the
| diagram of theories col(T) is the direct image (flow)
| dir(inj_n) along the base diagram colimit injections
| followed by the meet in LOT(col(L)), the lattice of
| theories over col(L). Moreover, using the direct
| image (flow) dir(inj_n) moves the theories in T to
| the lattice of theories LOT(col(L)). Also, recall
| that we defined the notions of "monocosmic" and
| "polycosmic" in terms of the colimit of theories.
|
| RK: http://suo.ieee.org/email/msg10123.html
Nope, not there yet. I will have to go back
and see if I can pull through a ZOL analogue.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o