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 sending 0 to x.
• InternalTangentSpace x: the internal tangent space at x.
• internalTangentMap f x: the tangent map of f at x if f is (globally) smooth, and 0 otherwise.
• internalTangentMap_id, internalTangentMap_comp: lemmas showing that this is functorial.

TODO:

• namespace and shorten names of InternalTangentSpace and internalTangentMap, 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

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

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

Equations

• DiffeologicalSpace.pointedPlots x = {p : (n : ℕ) × (Eucl n → X) | IsPlot p.snd ∧ p.snd 0 = x}

def PreInternalTangentSpace {X : Type u} [DiffeologicalSpace X] (x : X) : Type u

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

instance instAddCommGroupPreInternalTangentSpace {X : Type u} [DiffeologicalSpace X] {x : X} : AddCommGroup (PreInternalTangentSpace x)

Equations

• instAddCommGroupPreInternalTangentSpace = id inferInstance

instance instModuleRealPreInternalTangentSpace {X : Type u} [DiffeologicalSpace X] {x : X} : Module ℝ (PreInternalTangentSpace x)

Equations

• instModuleRealPreInternalTangentSpace = id inferInstance

@[reducible, inline]

abbrev PreInternalTangentSpace.lof {X : Type u} [DiffeologicalSpace X] {x : X} (p : ↑(DiffeologicalSpace.pointedPlots x)) : Eucl (↑p).fst →ₗ[ℝ] PreInternalTangentSpace x

Equations

• PreInternalTangentSpace.lof p = DirectSum.lof ℝ (↑(DiffeologicalSpace.pointedPlots x)) (fun (p : ↑(DiffeologicalSpace.pointedPlots x)) => Eucl (↑p).fst) p

def InternalTangentSpace {X : Type u} [DiffeologicalSpace X] (x : X) : Type u

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.

instance instAddCommGroupInternalTangentSpace {X : Type u} [DiffeologicalSpace X] {x : X} : AddCommGroup (InternalTangentSpace x)

Equations

• instAddCommGroupInternalTangentSpace = id inferInstance

instance instModuleRealInternalTangentSpace {X : Type u} [DiffeologicalSpace X] {x : X} : Module ℝ (InternalTangentSpace x)

Equations

• instModuleRealInternalTangentSpace = id inferInstance

def InternalTangentSpace.lof {X : Type u} [DiffeologicalSpace X] {x : X} (p : ↑(DiffeologicalSpace.pointedPlots x)) : Eucl (↑p).fst →ₗ[ℝ] InternalTangentSpace x

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.

theorem InternalTangentSpace.lof_comp_apply {X : Type u} [DiffeologicalSpace X] {x : X} (p : ↑(DiffeologicalSpace.pointedPlots x)) {m : ℕ} {f : Eucl m → Eucl (↑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 m → Eucl (↑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 : X → Y} (hf : DSmooth f) (x : X) : ↑(pointedPlots x) → ↑(pointedPlots (f x))

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

Equations

• DiffeologicalSpace.pointedPlots_map hf x p = ⟨⟨(↑p).fst, f ∘ (↑p).snd⟩, ⋯⟩

def preInternalTangentMap {X Y : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : X → Y) (x : X) : PreInternalTangentSpace x →ₗ[ℝ] PreInternalTangentSpace (f x)

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.

def internalTangentMap {X Y : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : X → Y) (x : X) : InternalTangentSpace x →ₗ[ℝ] InternalTangentSpace (f x)

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.

@[simp]

theorem pointedPlots_map_id {X : Type u} [DiffeologicalSpace X] (x : X) : DiffeologicalSpace.pointedPlots_map ⋯ x = id

theorem pointedPlots_map_comp {X Y Z : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : DSmooth f) (hg : DSmooth g) (x : X) : DiffeologicalSpace.pointedPlots_map ⋯ x = DiffeologicalSpace.pointedPlots_map hg (f x) ∘ DiffeologicalSpace.pointedPlots_map hf x

@[simp]

theorem preInternalTangentMap_id {X : Type u} [DiffeologicalSpace X] (x : X) : preInternalTangentMap id x = LinearMap.id

theorem preInternalTangentMap_comp {X Y Z : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : DSmooth f) (hg : DSmooth g) (x : X) : preInternalTangentMap (g ∘ f) x = preInternalTangentMap g (f x) ∘ₗ preInternalTangentMap f x

@[simp]

theorem internalTangentMap_id {X : Type u} [DiffeologicalSpace X] (x : X) : internalTangentMap id x = LinearMap.id

theorem internalTangentMap_comp {X Y Z : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : DSmooth f) (hg : DSmooth g) (x : X) : internalTangentMap (g ∘ f) x = internalTangentMap g (f x) ∘ₗ internalTangentMap f x

def vectorSpaceToInternalTangentSpace {X : Type u} [DiffeologicalSpace X] [AddCommGroup X] [Module ℝ X] [DiffeologicalAddGroup X] [DSmoothSMul ℝ X] (x : X) : X →ₗ[ℝ] InternalTangentSpace x

The canonical map from a diffeological vector space to its internal tangent space at a point x, sending any vector v to the internal tangent vector represented by the path t ↦ x + t • v.

Equations

• One or more equations did not get rendered due to their size.

theorem vectorSpaceToInternalTangentSpace_injective {X : Type u} [DiffeologicalSpace X] [AddCommGroup X] [Module ℝ X] [IsFineDiffeology ℝ X] {x : X} : Function.Injective ⇑(vectorSpaceToInternalTangentSpace x)

The canonical map from a fine diffeological vector space to its internal tangent space at a point is injective.

Note that this isn't the case for arbitrary diffeological vector spaces, because e.g. any vector space becomes a diffeological vector space with the coarse diffeology but internal tangent spaces of coarse spaces are all trivial.

theorem vectorSpaceToInternalTangentSpace_surjective {X : Type u} [DiffeologicalSpace X] [AddCommGroup X] [Module ℝ X] [IsFineDiffeology ℝ X] {x : X} : Function.Surjective ⇑(vectorSpaceToInternalTangentSpace x)

The canonical map from a fine diffeological vector space to its internal tangent space at a point is surjective.

I don't yet know whether this holds more generally for all diffeological vector spaces, but wouldn't bet on it.

def InternalTangentSpaceVectorSpaceEquivSelf {X : Type u} [DiffeologicalSpace X] [AddCommGroup X] [Module ℝ X] [IsFineDiffeology ℝ X] (x : X) : InternalTangentSpace x ≃ₗ[ℝ] X

The canonical isomorphism between the internal tangent space of a fine diffeological vector space and the vector space itself, given in the backwards direction by vectorSpaceToInternalTangentSpace.

Equations

• InternalTangentSpaceVectorSpaceEquivSelf x = (LinearEquiv.ofBijective (vectorSpaceToInternalTangentSpace x) ⋯).symm