SUO: Re: IFF LOT Glossary
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Alright, this is what I need.
Let me see if I can stretch
a few neurons from point A
to point B and maybe draw
some maps as I go.
Robert E. Kent wrote:
>
> Jon,
>
> 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".
Yes, for a small example, let's say we have the following function f : A -> B.
0 1 2 3 4 5 6 7 8 9
o o o o o o o o o o A
| \ | / \ \ | | \ /
| \ | / \ \ | | \ /
| \ | / \ \ | | \ f
| \ | / \ \ | | / \
v vvv v vv v v v
o o o o o o o o o o B
0 1 2 3 4 5 6 7 8 9
I am used to saying that the inverse relation of f evaluated at b in B,
brutally asciified as (f^(-1))(b), is the "fiber of f at b", so that's
familiar enough, "up to idiom-morphisms". Gloss fib(f)(b) as f^(-1)(b).
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 B x A being
the "same information" as fib(f) : B -> Pow(A). Reading f backupwards:
0 1 2 3 4 5 6 7 8 9
o o o o o o o o o o A
^ ^ ^ ^ ^ ^ ^ ^ ^ ^
| \ | / \ \ | | \ /
| \ | / \ \ | | \ f^(-1)
| \ | / \ \ | | / \
| \|/ \ \| | / \
o o o o o o o o o o B
0 1 2 3 4 5 6 7 8 9
This becomes fib(f) : B -> Pow(A), 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(A)
^ ^ ^ ^ ^ ^ ^ ^ ^ ^
| | | | | | | | | |
| | | | | | | | | | fib(f)
| | | | | | | | | |
| | | | | | | | | |
o o o o o o o o o o B
0 1 2 3 4 5 6 7 8 9
So far so good, but man are my eyes tired.
Will try to work through the rest tomorrow.
Jon
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
> 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.
>
> Robert E. Kent
> rekent@ontologos.org
>
> ----- Original Message -----
> From: "Jon Awbrey" <jawbrey@oakland.edu>
> To: "Robert E. Kent" <rekent@ontologos.org>
> Cc: "SUO" <standard-upper-ontology@ieee.org>
> Sent: Thursday, June 26, 2003 12:45 PM
> Subject: Re: IFF LOT Glossary
>
> > o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
> >
> > hi robert,
> >
> > could you explain what you mean by "base language fiber".
> > i kind of know what a fiber is in simple situations.
> >
> > thanks,
> >
> > jon
> >
> > o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
> >
> > Robert E. Kent wrote:
> > >
> > > All,
> > >
> > > I have posted the PDF document "The IFF Glossary
> > > for the Lattice of Theories" at the address:
> > >
> > > http://suo.ieee.org/IFF/LOT-glossary.pdf.
> > >
> > > This graphically illustrates and briefly discusses the core
> > > functionality for both the truth concept lattice and the
> > > lattice of theories, two notions that are equivalent
> > > from the order-theoretic viewpoint. The lattice of
> > > theories is the base language fiber in the category
> > > of theories, whereas the truth concept lattice is
> > > the base language fiber in the category of
> > > closed theories.
> > >
> > > Please regard this as a mid-range report -- I am
> > > developing a new version of the theory namespace
> > > axiomatization that contains all of this. This
> > > will offer a baseline axiomatization in the IFF
> > > for the notions of a "lattice of theories" and
> > > a "library of modules".
> > >
> > > As always, all constructive comments are welcomed.
> > >
> > > Robert E. Kent
> > > rekent@ontologos.org
> >
> > o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o