Documentation

Orbifolds.Diffeology.TangentSpace

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: #

TODO: #

def DiffeologicalSpace.pointedPlots {X : Type u} [DiffeologicalSpace X] (x : X) :
Set ((n : ) × (Eucl nX))

The set of all plots in X that send 0 to x.

Equations
Instances For

    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
    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
          theorem InternalTangentSpace.lof_comp_apply {X : Type u} [DiffeologicalSpace X] {x : X} (p : (DiffeologicalSpace.pointedPlots x)) {m : } {f : Eucl mEucl (↑p).fst} (hf : ContDiff (↑) f) (hf' : f 0 = 0) (v : Eucl m) :
          (lof m, (↑p).snd f, ) v = (lof p) ((fderiv f 0) v)
          theorem InternalTangentSpace.lof_comp {X : Type u} [DiffeologicalSpace X] {x : X} (p : (DiffeologicalSpace.pointedPlots x)) {m : } {f : Eucl mEucl (↑p).fst} (hf : ContDiff (↑) f) (hf' : f 0 = 0) :
          lof m, (↑p).snd f, = lof p ∘ₗ (fderiv f 0)
          def DiffeologicalSpace.pointedPlots_map {X Y : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f : XY} (hf : DSmooth f) (x : X) :
          (pointedPlots x)(pointedPlots (f x))

          Transports plots from x to f x for any smooth map f.

          Equations
          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
                theorem preInternalTangentMap_comp {X Y Z : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : XY} {g : YZ} (hf : DSmooth f) (hg : DSmooth g) (x : X) :
                theorem internalTangentMap_comp {X Y Z : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : XY} {g : YZ} (hf : DSmooth f) (hg : DSmooth g) (x : X) :

                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.
                Instances For