Synthetic Differential Geometry

Synthetic_differential_geometry.txt

The text for the video	

https://youtu.be/utJjFMWWq2Y


# Set Definitions and auxiliary function
R ... a commutative ring
Below, use the field variable name k_g for k_g : R.
Below, use the function variable name g for g : R → R.

D_n := {x ∈ R | x^n · x = 0}
0 ∈ D_n

D_1 := {x ∈ R | x^2 = 0}
Below, use the field variable name ɛ for ɛ : D_1.

# Axiom (simple version)
∀g. ∃!k_g. ∀ɛ. g(ɛ) = g(0) + k_g · ɛ

# Non-existence of ɛ apart from 0.
∀g. ∀ɛ. g(ɛ)^2 = (g(0) + 2 · k_g · ɛ) · g(0)
∀g. ∀ɛ. g(0) = 0 → g(ɛ)^2 = 0


nonZero(x) := 0 if (x = 0), 1 if (x ≠ 0)

Assume this is a function
nonZero : R → R
(as implies by LEM)

Then
∀ɛ. nonZero(ɛ)^2 = 0
∀ɛ. (ɛ ≠ 0) → nonZero(ɛ)^2 = 1
∀ɛ. (ɛ ≠ 0) → 0 = 1
∀ɛ. ¬(ɛ ≠ 0)
¬∃ɛ. ɛ ≠ 0

## Implications of LEM
With LEM, nonZero is indeed a function

∀ɛ. (ɛ = 0 ∨ ɛ ≠ 0) → ɛ = 0

I.e., this LEM principle allows for only one semantics of the theory, D={0}.

## Inverses in R
Constructively, there's no ɛ for which we can decide ɛ ≠ 0.
(see refs)

Consider the usual field axiom "nonzero => invertible."

Not being able to establish ≠ means we can't prove such things,
i.e. prove
  ∃(ɛ^-1 ∈ R). ɛ · ɛ^-1 = 1

## Every function is differentiable.
In the sense that
f(x) = k(x - a) → f(a + ɛ) = f(a) + d_k_a · ɛ
f(x) = k(x - a) → f(a + ɛ) - f(a) = d_k_a · ɛ

And, as a matter of fact, f'(x) must be this unique d_k_a.

## Tangent bundle
This gives a synthetic theory such that tangent bundles are realized as
T(M) = D -> M
T(M) = M^D
of tangent vectors and a projection to their base given as v(0), so that there's
p : M^D -> M
p(v) := v(0)

Since D is a sub-object in R, this makes for a nice/compact presentation.
The theory can be expressed in nice nice universal properties.

# Models of the theory
The category of manifolds embed into C^∞Rng^op.

The synthetic logic of tangent bundles has a model as internal logic of the
topos given by the sheaves on the Grothendieck topology on C^∞Rng^op.

# References
https://ncatlab.org/nlab/show/synthetic+differential+geometry

https://en.wikipedia.org/wiki/Synthetic_differential_geometry
See links therein.
https://en.wikipedia.org/wiki/Dual_number
https://en.wikipedia.org/wiki/Smooth_infinitesimal_analysis
https://en.wikipedia.org/wiki/Categorical_logic
https://en.wikipedia.org/wiki/Topos

https://users-math.au.dk/~kock/sdg99.pdf
https://www.fuw.edu.pl/~kostecki/sdg.pdf
http://home.sandiego.edu/~shulman/papers/sdg-pizza-seminar.pdf
http://www.acsu.buffalo.edu/~wlawvere/SDG_Outline.pdf
https://www.math.ru.nl/~landsman/scriptieTim.pdf

https://mathoverflow.net/questions/186851/synthetic-vs-classical-differential-geometry