Formal smooth sets are one possible model of the Kock-Lawvere axioms
of synthetic differential geometry.
This talk will explain the toposes of smooth sets and formal smooth sets.
A smooth set is a sheaf on the site with objects
{ℝⁿ | n∈ℕ}
and all smooth maps as morhpisms.
This is a site with the Grothendieck topology
generated by good open covers, i.e. it is a collection of
open subset inclusions {Uᵢ → ℝⁿ} such that all non-empty finite intersections
are diffeomorphic to ℝⁿ. Sheaves on this site are called smooth sets.
Formal smooth sets are sheaves on an extension of this site.
The goals are:
There is an article on synthetic PDEs by Urs Schreiber and Igor Khavkine which introduces and uses this topos.
Depending on demand, this talk might also cover the differential cohesive structure of this topos and its higher variant,
which is expected to provide a model for differential cohesive HoTT as it is used by David Jaz Myers in the articles:
This talk will also introduce constructive reasoning.
The main slogan/feature of higher toposes is, that any cohomology theory can be expressed using hom-spaces and truncation in some higher topos.
Since HoTT is known to interpret in higher toposes, this yields an easy way to define cohomology internally:
Hⁿ(X,ℱ):≡∥ (x : X) → K(ℱₓ,n) ∥₀
Since this implies Hⁿ(X,ℱ)=πₖ((x : X) → K(ℱₓ,n+k)), exact sequences can be constructed using the long exact sequence for homotopy fibers F → E → B:
… → πₖ₊₁(B) → πₖ(F) → πₖ(E) → πₖ(B) → πₖ₋₁(F) → …