There are way too many objects in diffgeo, all of them subtly connected. Here I catalogue all of the ones I have run across:

§ Manifold

A manifold $M$ of dimension $n$ is a topological space. So, there is a topological structure $T$ on $M$. There is also an Atlas , which is a family of Chart s that satisfy some properties.

§ Chart

A chart is a pair $(O \in T , cm: O -> \mathbb R^n$. The $O$ is an open set of the manifold, and $cm$ ("chart for "m") is a continuous mapping from $O$ to $\mathbb R^n$ under the subspace topology for $U$ and the standard topology for $\mathbb R^n$.

§ Atlas

An Atlas is a collection of Chart s such that the charts cover the manifold, and the charts are pairwise compatible. That is, $A = \{ (U_i, \phi_i) \}$, such that $\cup{i} U_i = M$, and $\phi_j \circ phi_i^{-1}$ is smooth.

§ Differentiable map

$f: M \to N$ be a mapping from an $m$ dimensional manifold to an $n$ dimensional manifold. Let $frep = cn \circ f \circ cm^{-1}: \mathbb R^m -> \mathbb R^n$ where $cm: M \to \mathbb R^m$ is a chart for $M$, $cn: N \to \mathbb R^n$ is a chart for $N$. $frep$ is $f$ represented in local coordinates. If $frep$ is smooth for all choices of $cm, cn$, then $f$ is a differentiable map from $M$ to $N$.

§ Curve:

Let $I$ be an open interval of $\mathbb R$ which includes the point 0. A Curve is a differentiable map $C: (a, b) \to M$ where $a < 0 < b$.

§ Function: (I hate this term, I prefer something like Valuation):

A differentiable mapping from $M$ to $R$.

§ Directional derivative of a function f(m): M -> R with respect to a curve c(t): I -> M, denoted as c[f].

Let g(t) = (f . c)(t) :: I -c-> M -f-> R = I -> R. This this is the value dg/dt(t0) = (d (f . c) / dt) (0).

§ Tangent vector at a point p:

On a m dimensional manifold M, a tangent vector at a point p is an equivalence class of curves that have c(0) = p, such that c1(t) ~ c2(t) iff :

• For a (all) charts (O, ch) such that c1(0) ∈ O, d/dt (ch . c1: R -> R^m) = d/dt (ch . c2: R -> R^m).

That is, they have equal derivatives.

§ Tangent space( TpM):

The set of all tangent vectors at a point p forms a vector space TpM. We prove this by creating a bijection from every curve to a vector R^n.

Let (U, ch: U -> R) be a chart around the point p, where p ∈ U ⊆ M. Now, the bijection is defined as:

forward: (I -> M) -> R^nforward(c) = d/dt (c . ch)reverse: R^n -> (I -> M)reverse(v)(t) = ch^-1 (tv)

§ Cotangent space( TpM*): dual space of the tangent space / Space of all linear functions from TpM to R.

• Associated to every function f, there is a cotangent vector, colorfully called df. The definition is df: TpM -> R, df(c: I -> M) = c[f]. That is, given a curve c, we take the directional derivative of the function falong the curve c. We need to prove that this is constant for all vectors in the equivalence class and blah.

§ Pushforward push(f): TpM -> TpN

Given a curve c: I -> M, the pushforward is the curve f . c : I -> N. This extends to the equivalence classes and provides us a way to move curves in M to curves in N, and thus gives us a mapping from the tangent spaces.

This satisfies the identity:

push(f)(v)[g] === v[g . f]

§ Pullback pull(f): TpN* -> TpM*

Given a linear functional wn : TpN -> R, the pullback is defined as wn . push(f) : TpM -> R.

This satisfies the identity:

(pull wn)(v) === wn (push v)(pull (wn : TpN->R): TpM->R) (v : TpM) : R  = (wn: TpN->R) (push (v: TpM): TpN) : R

§ Lie derivation

§ Lie derivation as lie bracket