## Downcasing CategoriesQuick index:
- 1. DNC for Categories
- 2. Downcasing categorical diagrams (in general)
- 3. Why we want to allow pseudopoints
- 4. Quantifiers, categorically
1. DNC for Categories ===================== 2. Downcasing categorical diagrams (in general) =============================================== One day I realized that the same notation that I was using for sets did also work - with no changes in the syntax, only in the semantics - for categories. Here's a comparison; in the second situation, at the right, \catC is an arbitrary category. A is a set | A is an object of \catC, A∈|\catC| B is a set | B is an object of \catC, B∈|\catC| | A ---> B (a function) | A ---> B (a morphism) a |--> b (a function) | a |--> b (a morphism) | A is the space of `a's | Now: B is the space of `b's | ``an `a''' is an abuse of language A = E[a] | ``a `b''' is an abuse of language B = E[b] | `a|->b' has semantics - it's a morphism - | but `a' and `b' have no semantics An `a' is a point of A, | a `b' is a point of B, | `a's and `b's are not points in this case, a∈A, b∈B. | just ``pseudopoints'', and pseudopoints | don't need to exist - they may be just | syntactical devices | | To enforce the distinction we say | ``object of'' instead of ``space of'' | and we write O[·] instead of E[·] | | A is the objects of `a's | B is the objects of `b's | A = O[a] | B = O[b] Note: it's almost impossible to understand this is the general case without examples... L 3. Why we want to allow pseudopoints ==================================== For example, for subobjects. Implications can be seen as inclusions. ∀a∈A.P(a)⊃Q(a) {a∈A|P(a)} \subset {a∈A|Q(a)} Categorically, {a|P(a)} ------> {a|Q(a)} /{a|P(a)}\ /{a|Q(a)}\ v v | v | | v | | | | | | ---> | | | v v | v | | v | A -------------> A \ A / \ A / This is a morphism between two objects of Set^>->, where Set^>-> is the category of monic arrows between objects of Set. Set^>-> is also called Sub(Set) - the category of subojects of Set. Notational trick: /{a|P(a)}\ /{a|Q(a)}\ | v | | v | {a||P(a)} ---> {a||Q(a)} := | | | ---> | | | | v | | v | \ A / \ A / The `|' in {a|P(a)} is called the ``such that'' bar; we're doubling it to represent subobjects. We downcase that into: a||P(a) |-> a||Q(a) this morphism - in Set^>-> is not just a mapping of points... in fact, it's two morphisms in Set - a|P(a) |-> a|Q(a) and a|->a - plus the information that the square below commutes: a|P(a) |---> a|Q(a) / / | | v v a |--------> a More generally: b:=b(a) a|P(a) |-------> b|Q(b) / / | | v b:=b(a) v a |------------> b a||P(a) |-> b||Q(b) means ∀a.P(a)⊃Q(b(a)). Note the use of a bit of ``physicist's notation'' here - in the presence of a function f = a|->b the value of b can be seen as a function of a, and a physicist would write b=f(a) or b=b(a)... we will prefer b=b(a) to avoid using new letters, and the dictionary will translate such expressions (atrocities!) into something mathematically sound. 4. Quantifiers, categorically ============================= In Set^>-> the functors that quantify over a variable are adjoints to ``weakening functors'' that add a dummy variable to the domain: {a,b||P(a,b)} |---> {a||∃b.P(a,b)} P(a,b) ===> ∃b.P(a,b) | | - - | <-> | | <-> | v v v v {a,b||Q(a)} <------| {a||Q(a)} Q(a) <====== Q(a) | | - - | <-> | | <-> | v v v v {a,b||R(a,b)} |---> {a||∀b.R(a,b)} R(a,b) ===> ∀b.R(a,b) A×B ----------------> A a,b |------> a These functors do not operate on the whole of Set^>-> - they go from one ``fiber'' of Set^>-> to another. The best way to formalize this is via /fibrations/; Set^>-> is a fibration over Set. A fibration is composed of: an ``entire category'' Set^>-> a ``base category'' Set a ``projection functor'' Cod: Set^>-> -> Set and enough ``cartesian liftings''. (?!?!?! - next slide) In our diagrams we will not usually draw the projection functors. Instead we will just draw the objects of the entire category over their projections - and we will often omit the part of their names that can be recovered from the projections. In the diagram above we wrote just `Q(a)', not `a||Q(a)'. |