Bundled smooth maps

Defines the type DSmoothMap X Y of smooth maps between diffeological spaces.

This file contains only very basic API; more advanced constructions are done in CatDG.Diffeology.Constructions.

Adapted from Mathlib.Topology.ContinuousMap.Def and Mathlib.Topology.ContinuousMap.Basic.

TODO

• move this into a folder together with CatDG.Diffeology.Algebra.DSmoothMap and the relevant constructions from CatDG.Diffeology.Constructions.
• maybe introduce a notation like C∞(X, Y) or X →C∞ Y for DSmoothMap X Y?

structure DSmoothMap (X : Type u_1) (Y : Type u_2) [DiffeologicalSpace X] [DiffeologicalSpace Y] : Type (max u_1 u_2)

The type of bundled smooth maps between diffeological spaces X and Y.

• toFun : X → Y

  The map X → Y.

• dsmooth : DSmooth self.toFun

  The map X → Y is smooth.

class DSmoothMapClass (F : Type u_1) (X : outParam (Type u_2)) (Y : outParam (Type u_3)) [DiffeologicalSpace X] [DiffeologicalSpace Y] [FunLike F X Y] : Prop

DSmoothMapClass F X Y states that F is a type of smooth maps X → Y.

• map_dsmooth (f : F) : DSmooth ⇑f

  Smoothness.

def DSmoothMapClass.toDSmoothMap {F : Type u_1} {X : Type u_2} {Y : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [FunLike F X Y] [DSmoothMapClass F X Y] (f : F) : DSmoothMap X Y

Coerce a bundled morphism with a DSmoothMapClass instance to a DSmoothMap.

Equations

• ↑f = { toFun := ⇑f, dsmooth := ⋯ }

instance DSmoothMapClass.instCoeTCDSmoothMap {F : Type u_1} {X : Type u_2} {Y : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [FunLike F X Y] [DSmoothMapClass F X Y] : CoeTC F (DSmoothMap X Y)

Equations

• DSmoothMapClass.instCoeTCDSmoothMap = { coe := DSmoothMapClass.toDSmoothMap }

instance DSmoothMap.instFunLike {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] : FunLike (DSmoothMap X Y) X Y

Equations

• DSmoothMap.instFunLike = { coe := DSmoothMap.toFun, coe_injective' := ⋯ }

instance DSmoothMap.instDSmoothMapClass {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] : DSmoothMapClass (DSmoothMap X Y) X Y

@[simp]

theorem DSmoothMap.toFun_eq_coe {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f : DSmoothMap X Y} : f.toFun = ⇑f

instance DSmoothMap.instCanLiftForallCoeDSmooth {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] : CanLift (X → Y) (DSmoothMap X Y) DFunLike.coe DSmooth

def DSmoothMap.Simps.apply {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : DSmoothMap X Y) : X → Y

See note [custom simps projection].

Equations

• DSmoothMap.Simps.apply f = ⇑f

@[simp]

theorem DSmoothMap.coe_coe {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {F : Type u_5} [FunLike F X Y] [DSmoothMapClass F X Y] (f : F) : ⇑↑f = ⇑f

theorem DSmoothMap.coe_apply {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {F : Type u_5} [FunLike F X Y] [DSmoothMapClass F X Y] (f : F) (x : X) : ↑f x = f x

theorem DSmoothMap.ext {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f g : DSmoothMap X Y} (h : ∀ (x : X), f x = g x) : f = g

theorem DSmoothMap.ext_iff {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f g : DSmoothMap X Y} : f = g ↔ ∀ (x : X), f x = g x

theorem DSmoothMap.coe_injective {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] : Function.Injective DFunLike.coe

@[simp]

theorem DSmoothMap.coe_mk {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : X → Y) (hf : DSmooth f) : ⇑{ toFun := f, dsmooth := hf } = f

def DSmoothMap.id (X : Type u_1) [DiffeologicalSpace X] : DSmoothMap X X

The identity as a smooth map.

Equations

• DSmoothMap.id X = { toFun := id, dsmooth := ⋯ }

@[simp]

theorem DSmoothMap.coe_id (X : Type u_1) [DiffeologicalSpace X] : ⇑(DSmoothMap.id X) = id

@[simp]

theorem DSmoothMap.id_apply {X : Type u_1} [DiffeologicalSpace X] (x : X) : (DSmoothMap.id X) x = x

def DSmoothMap.const (X : Type u_1) {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (y : Y) : DSmoothMap X Y

The constant map as a continuous map.

Equations

• DSmoothMap.const X y = { toFun := fun (x : X) => y, dsmooth := ⋯ }

@[simp]

theorem DSmoothMap.coe_const (X : Type u_1) {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {y : Y} : ⇑(const X y) = Function.const X y

@[simp]

theorem DSmoothMap.const_apply {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (y : Y) (x : X) : (const X y) x = y

instance DSmoothMap.instInhabited {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [Inhabited Y] : Inhabited (DSmoothMap X Y)

Equations

• DSmoothMap.instInhabited = { default := DSmoothMap.const X default }

instance DSmoothMap.instUnique {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [Unique Y] : Unique (DSmoothMap X Y)

Equations

• DSmoothMap.instUnique = { toInhabited := DSmoothMap.instInhabited, uniq := ⋯ }

instance DSmoothMap.instNontrivialOfNonempty {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [Nonempty X] [Nontrivial Y] : Nontrivial (DSmoothMap X Y)

def DSmoothMap.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (f : DSmoothMap Y Z) (g : DSmoothMap X Y) : DSmoothMap X Z

The composition of continuous maps, as a continuous map.

Equations

• f.comp g = { toFun := ⇑f ∘ ⇑g, dsmooth := ⋯ }

@[simp]

theorem DSmoothMap.coe_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (f : DSmoothMap Y Z) (g : DSmoothMap X Y) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem DSmoothMap.comp_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (f : DSmoothMap Y Z) (g : DSmoothMap X Y) (x : X) : (f.comp g) x = f (g x)

@[simp]

theorem DSmoothMap.comp_assoc {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] [DiffeologicalSpace W] (f : DSmoothMap Z W) (g : DSmoothMap Y Z) (h : DSmoothMap X Y) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem DSmoothMap.id_comp {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : DSmoothMap X Y) : (DSmoothMap.id Y).comp f = f

@[simp]

theorem DSmoothMap.comp_id {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : DSmoothMap X Y) : f.comp (DSmoothMap.id X) = f

@[simp]

theorem DSmoothMap.const_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (z : Z) (f : DSmoothMap X Y) : (const Y z).comp f = const X z

@[simp]

theorem DSmoothMap.comp_const {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (f : DSmoothMap Y Z) (y : Y) : f.comp (const X y) = const X (f y)

@[simp]

theorem DSmoothMap.cancel_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f₁ f₂ : DSmoothMap Y Z} {g : DSmoothMap X Y} (hg : Function.Surjective ⇑g) : f₁.comp g = f₂.comp g ↔ f₁ = f₂

@[simp]

theorem DSmoothMap.cancel_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : DSmoothMap Y Z} {g₁ g₂ : DSmoothMap X Y} (hf : Function.Injective ⇑f) : f.comp g₁ = f.comp g₂ ↔ g₁ = g₂