Internal tangent spaces #
This file defines internal tangent spaces on diffeological spaces following
https://arxiv.org/abs/1411.5425; concretely, the tangent space at x
is implemented as
a quotient of the direct sum of the domains of all plots sending 0
to x
.
For this to be actually useful we will need to show that this agrees with the usual tangent spaces of vector spaces and manifolds, which we have yet to do.
Main definitions / results: #
PreInternalTangentSpace x
: the direct sum of the domains of all plots sending0
tox
.InternalTangentSpace x
: the internal tangent space atx
.internalTangentMap f x
: the tangent map off
atx
iff
is (globally) smooth, and0
otherwise.internalTangentMap_id
,internalTangentMap_comp
: lemmas showing that this is functorial.
TODO: #
- namespace and shorten names of
InternalTangentSpace
andinternalTangentMap
, maybe find some good abbreviations - tangent spaces of discrete / indiscrete spaces
- tangent spaces of open subspaces
- tangent spaces of vector spaces
- tangent spaces of manifolds
- tangent maps of constant maps
- tangent maps of maps between vector spaces / manifolds
The direct sum of the domains of all pointed plots to x
.
The actual internal tangent space is obtained as a quotient from this.
Equations
- PreInternalTangentSpace x = DirectSum ↑(DiffeologicalSpace.pointedPlots x) fun (p : ↑(DiffeologicalSpace.pointedPlots x)) => Eucl (↑p).fst
Instances For
Equations
- PreInternalTangentSpace.lof p = DirectSum.lof ℝ (↑(DiffeologicalSpace.pointedPlots x)) (fun (p : ↑(DiffeologicalSpace.pointedPlots x)) => Eucl (↑p).fst) p
Instances For
The internal tangent space of X
at x
, implemented here as the quotient of
PreInternalTangentSpace x
by the subspace generated by some relations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical linear map from the domain of any pointed plot into the tangent space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Transports plots from x
to f x
for any smooth map f
.
Equations
- DiffeologicalSpace.pointedPlots_map hf x p = ⟨⟨(↑p).fst, f ∘ (↑p).snd⟩, ⋯⟩
Instances For
The map PreInternalTangentSpace x →ₗ[ℝ] PreInternalTangentSpace (f x)
that
descents to the actual tangent map. Defined as 0
when f
isn't smooth.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The internal tangent map of f
at x
when f
is smooth, and 0
otherwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical isomorphism between the internal tangent space of a diffeological vector spaces and the vector space itself.
TODO: fill in the sorries for injectivity and bijectivity. This probably requires getting a nicer
form of the equivalence relation that PreInternalTangentSpace
is quotiented by specifically for
diffeological vector spaces (or additive groups, if that is enough?).
Equations
- One or more equations did not get rendered due to their size.