§ Subobject classifiers of , or precosheaf of
§ Subobject classifier in
- Start with . This has as objects . The subobjects are of the form:
S0 -> S1
X0 -> X1
- we can identify with a subset of , and with a subset of .
- The diagram commuting implies that . This means that , or that .
- Thus, we have that .
- We define the subobject classifier as having values , where is interpreted as "is a subobject" (is true), and is interpreted as "delay" (ie, will be a subobject in the next timestep).
- An element will be classified as .
- An element will be classified as , since it lands in in one timestep.
- An element will be classified as , since it lands in after infinite timesteps (ie, never).
- We can alternatively think of , since it takes "two timesteps", but the second timestep is never materialized.
§ Proof that this is the subobject classifier
- We formally define the subobject classifier as , where , .
- The map is , , , .
- Informally, the map can be said to be given by .
- We call it "force" since it forces a layer of delay.
- We define the bijection between subobjects and classification maps as follows: Let be the least index such that . Then have . See that by the square, this determines for all larger :
X0 ---Χ[f]0--> Ω0
X1 - Χ[f]1- -> Ο1
[to be determined]
§ Why does not have subobject classifier
- The objects in this category are sequences of sets .
- We claim this category