Topos Theory
Introduction
===============================================================================
There are plenty of ways to learn topos.
One can check Baez's introduction.
Baez : http://math.ucr.edu/home/baez/topos.html
\pagebreak
Topos
=============================================================================
Effective Topos
------------------------------------------------------------------------------
Effective Topos is an elementary topos which is not a grothendieck topos.
Effective Topos : https://ncatlab.org/nlab/show/effective+topos
Topos and LEM
------------------------------------------------------------------------------
A sheaf is said to be a type which behaves in the same way under any situation, or under where any axiom is assumed. So, we cannot say a sheaf type is decidable under some situation and it is not decidable in another situation.
We could connect sheaf and LEM in this way.
Topos mainly takes place in presheaves. And we make them into sheaves in order to do mathematics on them; i.e. to handle objects(types) like real numbers in a coherent way. Sheaves are Grothendieck Topoi.
When we do mathematics on presheaves like in Homotopy Type Theory (HoTT),
we need to handle real numbers, hence, we need to double negate sheafificate dedekind-cut real numbers.
This is the same idea with that double nagated intuitionistic logic is classical logic.
Topos as Variety
------------------------------------------------------------------------------
The Category of Varieties $ \mathscr{Bar} $
- varieties: p,q,r, (p,q), (p,r), (q,r), (p,q,r), ....
- morphisms: inclusion maps, projection maps, ...
* `a variety` means `a set of irreducible varieties` i.e. `a set of prime ideals`
* `a program` is `a path in a variety`
Topos as Set of rules
------------------------------------------------------------------------------
- set of rules: {p}, {q}, {r}, {p,q}, {p,r}, {q,r}, {p,q,r}, ...
- morphisms: inclusion maps, projection maps
- inclusion map:
- projection map: injectiveness is assured. f:{p,q} -> p
~~~
`a set of rules` means `a programming language`
`a derivation tree` in it means `a program` in that
the path of `a derivation tree` is `a program`
~~~
\pagebreak
Geometric Morphism
===============================================================================
For a topos morphism $f:X\to Y$,
a `geometric morphism` is the pair $(f_*,f^*)$ of `direct image`$f_*$ and `inverse image` $f^*$
where
* `direct image` ( cofibration ) $f_* := \exists_f$ := $f \circ -$
* `inverse image` $f^* : \mathscr{O}(Y) \to \mathscr{O}(X)$ is a pullback of $f : X \to Y$
* (i.e. bring Y's structure to X and apply to it)
* `inverse image * direct image == id`
\pagebreak
SGL
===============================================================================
Category of Functors
------------------------------------------------------------------------------
Sheaves of Sets
------------------------------------------------------------------------------
Grothendieck Topologies and Sheaves
------------------------------------------------------------------------------
\pagebreak
Elementary Topoi
------------------------------------------------------------------------------
### Definition of Topos
* `elementary topoi`
* `char m` ( charcteristic map of m / classifying map)
### Exponential
* every topos has exponential
### Direct image
* `direct image` ( cofibration ) $\exists_f$ := $f \circ -$
* `inverse image` $f^* : \mathscr{O}(Y) \to \mathscr{O}(X)$ is a pullback of $f : X \to Y$
* (i.e. bring Y's structure to X and apply to it)
* `inverse image * direct image == id`
### Monads
* in a topos every monic arrow is an equalizer
### The construction of colimits
* `power set functor is a monad (p181)`
* `topos has all finite colimits (p184)`
### Factorization and Images
* In a topos, every arrow $f$ has an image $m$ and factors as $f=me$, with $e$ epi.
* If $f=me$ and $f'=m'e'$ with $m,m'$ monic and $e,e'$ epi, then each map of the arrow $f$ to the arrow $f'$ extends to a unique map of $m,e$ to $m',e'$.
* subobjects of a topos is a lattice.
* for $k:A \to B$, pullback $k^{-1}:Sub(B)\to Sub(A)$ has left adjoint $\exists_k$
* In a topos $\mathscr{E}$, the lattice $Sub(\mathbb{1}) \simeq Open(\mathscr{E}/B)$
### The Slice Category as a topos
* For any object $B$ in a Topos $\mathscr{E}$, slice category $\mathscr{E}/B$ is a Topos.
* For $k^*:\mathscr{E}/B\to\mathscr{E}/A$, it has left adjoint and right adjoint $\exists_k\dashv k^* \dashv\forall_k$ .
* An arrow to initial object $k:A\to 0$ is an isomorphism.
* Every arrow from initial object $0$ is monic.
* The join of disjoint subobjects is their coproduct.
* for $m_i : S_i \rightarrowtail B$, the induced map $m:\bigsqcup S_i \to B$ is monic.
### Lattice and Heyting Algebra Objects in a topos
The following theorems are equivalent:
* (External) For any object $A$ in a topos $\mathscr{E}$, the poset $Sub(A)$ has the structure of a `Heyting Algebra`
* (Internal) For any object $A$ in a topos $\mathscr{E}$, the power object $\mathscr{P}(A)$ is an `internal Heyting Algebra` (where $\Omega := \mathscr{P}(1)$)
### The Beck-Chevalley Condition
* Beck-Chevalley Condition as defined as : $g^{-1}(\exists_f U) = \exists_{pb(f)}( pb(g)^{-1}(U))$
* (where $pb(f)$ denotes for `pullback` of f)
* (External) : $\exists_f \dashv f^{-1} \dashv \forall_f : Sub(A)\to Sub(B)$
* (Internal) : $\Sigma_f \dashv f^{*} \dashv \Pi_f : \mathscr{E}/A \to \mathscr{E}/B$
### Injective Objects
* In any Topos $\mathscr{E}$, the subobject classifier $\Omega$ is `injective`.
* If $C$ is an object in a topos, then $\mathscr{P}(C)$ is `injective`.
* Any object $C$ in a topos has a monomorphism to an `injective object`.
* The pushout of a `monic` along arbitrary map is `monic`.
* for monos $m_i : S_i \rightarrowtail B_i$, the induced map $m:\bigsqcup S_i \to \bigsqcup B_i$ is monic.
Basic Constructions of Topoi
------------------------------------------------------------------------------
### Lawvere-Tierney Topologies
* The sieves on a Grothendieck topology gives a Lawvere-Tierney Topology
### Sheaves
* For a topos $\mathscr{E}$ and Lawvere-Tierney topology $j$, $Sh_j(\mathscr{E})$ is a topos.
### The Associated Sheaf Functors
* The inclusion $\mathbb{a}: \mathscr{E} \rightarrowtail Sh_j(\mathscr{E})$ is `left exact`.
*