Category of diffeological spaces

The category of diffeological spaces and smooth maps. Adapted from Mathlib.Topology.Category.TopCat.Basic.

Main definitions / results:

• DiffSp: the category of diffeological spaces and smooth maps.
• forget DiffSp: the forgetful functor DiffSp ⥤ Type, provided through a ConcreteCategory-instance on DiffSp.
• DiffSp.discrete, DiffSp.indiscrete: the functors Type ⥤ DiffSp giving each type the discrete/indiscrete diffeology.
• DiffSp.discreteForgetAdj, DiffSp.forgetIndiscreteAdj: the adjunctions discrete ⊣ forget ⊣ indiscrete.
• DiffSp.dTop, DiffSp.diffToDeltaGenerated, DiffSp.topToDiff, DiffSp.deltaGeneratedToDiff: the functors between DiffSp, DeltaGenerated and TopCat given by the D-topology and continuous diffeology.
• DiffSp.dTopAdj, DiffSp.dTopAdj': the adjunctions between those.
• DiffSp.hasLimits, DiffSp.hasColimits: DiffSp is complete and cocomplete.
• DiffSp.forgetPreservesLimits, DiffSp.forgetPreservesColimits: the forgetful functor DiffSp ⥤ Type preserves limits and colimits.

structure DiffSp : Type (u + 1)

The category of diffeological spaces.

• carrier : Type u
• str : DiffeologicalSpace ↑self

instance DiffSp.instCoeSortType : CoeSort DiffSp (Type u)

Equations

• DiffSp.instCoeSortType = { coe := DiffSp.carrier }

@[reducible, inline]

abbrev DiffSp.of (X : Type u) [DiffeologicalSpace X] : DiffSp

The object in DiffSp associated to a type equipped with the appropriate typeclasses. This is the preferred way to construct a term of DiffSp.

Equations

• DiffSp.of X = { carrier := X, str := inst✝ }

theorem DiffSp.coe_of (X : Type u) [DiffeologicalSpace X] : ↑(of X) = X

theorem DiffSp.of_carrier (X : DiffSp) : of ↑X = X

structure DiffSp.Hom (X Y : DiffSp) : Type u

The type of morphisms in DiffSp.

• hom' : DSmoothMap ↑X ↑Y

  The underlying DSmoothMap.

theorem DiffSp.Hom.ext_iff {X Y : DiffSp} {x y : X.Hom Y} : x = y ↔ x.hom' = y.hom'

theorem DiffSp.Hom.ext {X Y : DiffSp} {x y : X.Hom Y} (hom' : x.hom' = y.hom') : x = y

instance DiffSp.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} DiffSp

Equations

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

instance DiffSp.instConcreteCategoryDSmoothMapCarrier : CategoryTheory.ConcreteCategory DiffSp fun (X Y : DiffSp) => DSmoothMap ↑X ↑Y

Equations

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

@[reducible, inline]

abbrev DiffSp.Hom.hom {X Y : DiffSp} (f : X.Hom Y) : DSmoothMap ↑X ↑Y

Turn a morphism in DiffSp back into a DSmoothMap.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev DiffSp.ofHom {X Y : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : DSmoothMap X Y) : of X ⟶ of Y

Typecheck a DSmoothMap as a morphism in DiffSp.

Equations

• DiffSp.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def DiffSp.Hom.Simps.hom (X Y : DiffSp) (f : X.Hom Y) : DSmoothMap ↑X ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• DiffSp.Hom.Simps.hom X Y f = f.hom

@[simp]

theorem DiffSp.hom_id (X : DiffSp) : Hom.hom (CategoryTheory.CategoryStruct.id X) = DSmoothMap.id ↑X

@[simp]

theorem DiffSp.id_app (X : DiffSp) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem DiffSp.coe_id (X : DiffSp) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem DiffSp.hom_comp {X Y Z : DiffSp} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

@[simp]

theorem DiffSp.comp_app {X Y Z : DiffSp} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

@[simp]

theorem DiffSp.coe_comp {X Y Z : DiffSp} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem DiffSp.hom_ext {X Y : DiffSp} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem DiffSp.hom_ext_iff {X Y : DiffSp} {f g : X ⟶ Y} : f = g ↔ Hom.hom f = Hom.hom g

theorem DiffSp.ext {X Y : DiffSp} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem DiffSp.ext_iff {X Y : DiffSp} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

@[simp]

theorem DiffSp.hom_ofHom {X Y : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : DSmoothMap X Y) : Hom.hom (ofHom f) = f

@[simp]

theorem DiffSp.ofHom_hom {X Y : DiffSp} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem DiffSp.ofHom_id {X : Type u} [DiffeologicalSpace X] : ofHom (DSmoothMap.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem DiffSp.ofHom_comp {X Y Z : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (f : DSmoothMap X Y) (g : DSmoothMap Y Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem DiffSp.ofHom_apply {X Y : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : DSmoothMap X Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem DiffSp.hom_inv_id_apply {X Y : DiffSp} (f : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom f.inv) ((CategoryTheory.ConcreteCategory.hom f.hom) x) = x

theorem DiffSp.inv_hom_id_apply {X Y : DiffSp} (f : X ≅ Y) (y : ↑Y) : (CategoryTheory.ConcreteCategory.hom f.hom) ((CategoryTheory.ConcreteCategory.hom f.inv) y) = y

def DiffSp.homEquivDSmoothMap {X Y : DiffSp} : (X ⟶ Y) ≃ DSmoothMap ↑X ↑Y

Equations

• DiffSp.homEquivDSmoothMap = { toFun := DiffSp.Hom.hom, invFun := DiffSp.ofHom, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem DiffSp.homEquivDSmoothMap_apply {X Y : DiffSp} (f : X.Hom Y) : homEquivDSmoothMap f = f.hom

@[simp]

theorem DiffSp.homEquivDSmoothMap_symm_apply_hom {X Y : DiffSp} (f : DSmoothMap ↑X ↑Y) : Hom.hom (homEquivDSmoothMap.symm f) = f

@[simp]

theorem DiffSp.coe_of_of {X Y : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f : DSmoothMap X Y} {x : (CategoryTheory.forget DiffSp).obj (of X)} : (ofHom f) x = f x

Replace a function coercion for a morphism DiffSp.of X ⟶ DiffSp.of Y with the definitionally equal function coercion for a smooth map DSmoothMap X Y.

instance DiffSp.inhabited : Inhabited DiffSp

Equations

• DiffSp.inhabited = { default := DiffSp.of Empty }

def DiffSp.discrete : CategoryTheory.Functor (Type u) DiffSp

The functor equipping each type with the discrete diffeology.

Equations

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

def DiffSp.indiscrete : CategoryTheory.Functor (Type u) DiffSp

The functor equipping each type with the indiscrete diffeology.

Equations

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

def DiffSp.discreteForgetAdj : discrete ⊣ CategoryTheory.forget DiffSp

Adjunction discrete ⊣ forget, adapted from Mathlib.Topology.Category.TopCat.Adjunctions.

Equations

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

@[simp]

theorem DiffSp.discreteForgetAdj_counit : discreteForgetAdj.counit = { app := fun (X : DiffSp) => { hom' := { toFun := id, dsmooth := ⋯ } }, naturality := discreteForgetAdj._proof_3 }

@[simp]

theorem DiffSp.discreteForgetAdj_unit : discreteForgetAdj.unit = { app := fun (X : Type u) => id, naturality := discreteForgetAdj._proof_1 }

def DiffSp.forgetIndiscreteAdj : CategoryTheory.forget DiffSp ⊣ indiscrete

Adjunction forget ⊣ indiscrete, adapted from Mathlib.Topology.Category.TopCat.Adjunctions.

Equations

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

@[simp]

theorem DiffSp.forgetIndiscreteAdj_unit : forgetIndiscreteAdj.unit = { app := fun (X : DiffSp) => { hom' := { toFun := id, dsmooth := ⋯ } }, naturality := forgetIndiscreteAdj._proof_2 }

@[simp]

theorem DiffSp.forgetIndiscreteAdj_counit : forgetIndiscreteAdj.counit = { app := fun (X : Type u) => id, naturality := forgetIndiscreteAdj._proof_3 }

instance DiffSp.instIsRightAdjointForget : (CategoryTheory.forget DiffSp).IsRightAdjoint

instance DiffSp.instIsLeftAdjointForget : (CategoryTheory.forget DiffSp).IsLeftAdjoint

def DiffSp.dTop : CategoryTheory.Functor DiffSp TopCat

The functor sending each diffeological spaces to its D-topology.

Equations

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

def DiffSp.diffToDeltaGenerated : CategoryTheory.Functor DiffSp DeltaGenerated

The functor sending each diffeological space to its D-topology, as a delta-generated space.

Equations

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

def DiffSp.topToDiff : CategoryTheory.Functor TopCat DiffSp

The functor equipping each topological space with the continuous diffeology.

Equations

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

def DiffSp.deltaGeneratedToDiff : CategoryTheory.Functor DeltaGenerated DiffSp

The functor equipping each delta-generated space with the continuous diffeology.

Equations

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

def DiffSp.dTopAdj : dTop ⊣ topToDiff

Adjunction between the D-topology and continuous diffeology as functors between DiffSp and TopCat.

Equations

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

def DiffSp.dTopAdj' : diffToDeltaGenerated ⊣ deltaGeneratedToDiff

Adjunction between the D-topology and continuous diffeology as functors between DiffSp and DeltaGenerated.

Equations

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

instance DiffSp.instIsLeftAdjointTopCatDTop : dTop.IsLeftAdjoint

The D-topology functor DiffSp ⥤ TopCat is a left-adjoint.

instance DiffSp.instIsLeftAdjointDeltaGeneratedDiffToDeltaGenerated : diffToDeltaGenerated.IsLeftAdjoint

The D-topology functor DiffSp ⥤ DeltaGenerated is a left-adjoint.

Limits and colimits

The category of diffeological spaces is complete and cocomplete, and the forgetful functor preserves all limits and colimits. Adapted from Mathlib.Topology.Category.TopCat.Limits.

def DiffSp.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J DiffSp) : CategoryTheory.Limits.Cone F

A specific choice of limit cone for any F : J ⥤ DiffSp.

Equations

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

def DiffSp.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J DiffSp) : CategoryTheory.Limits.IsLimit (limitCone F)

DiffSp.limitCone F is actually a limit cone for the given F : J ⥤ DiffSp.

Equations

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

instance DiffSp.hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} DiffSp

instance DiffSp.hasLimits : CategoryTheory.Limits.HasLimits DiffSp

DiffSp has all limits, i.e. it is complete.

instance DiffSp.forgetPreservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget DiffSp)

instance DiffSp.forgetPreservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget DiffSp)

The forgetful functor DiffSp ⥤ Type preserves all limits.

def DiffSp.coconePtOfCoconeForget {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J DiffSp} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget DiffSp))) : Type u

Given a functor F : J ⥤ DiffSp and a cocone c : Cocone (F ⋙ forget) of the underlying cocone of types, this is the type c.pt with the infimum of the diffeologies that are coinduced by the maps c.ι.app j.

Equations

• DiffSp.coconePtOfCoconeForget c = c.pt

instance DiffSp.diffeologicalSpaceCoconePtOfCoconeForget {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J DiffSp} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget DiffSp))) : DiffeologicalSpace (coconePtOfCoconeForget c)

Equations

• DiffSp.diffeologicalSpaceCoconePtOfCoconeForget c = ⨆ (j : J), DiffeologicalSpace.coinduced (c.ι.app j) (F.obj j).str

def DiffSp.coconeOfCoconeForget {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J DiffSp} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget DiffSp))) : CategoryTheory.Limits.Cocone F

Given a functor F : J ⥤ DiffSp and a cocone c : Cocone (F ⋙ forget) of the underlying cocone of types, this is a cocone for F whose point is c.pt with the infimum of the coinduced diffeologies by the maps c.ι.app j.

Equations

• DiffSp.coconeOfCoconeForget c = { pt := DiffSp.of (DiffSp.coconePtOfCoconeForget c), ι := { app := fun (j : J) => DiffSp.ofHom { toFun := c.ι.app j, dsmooth := ⋯ }, naturality := ⋯ } }

@[simp]

theorem DiffSp.coconeOfCoconeForget_pt {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J DiffSp} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget DiffSp))) : (coconeOfCoconeForget c).pt = of (coconePtOfCoconeForget c)

@[simp]

theorem DiffSp.coconeOfCoconeForget_ι_app {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J DiffSp} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget DiffSp))) (j : J) : (coconeOfCoconeForget c).ι.app j = ofHom { toFun := c.ι.app j, dsmooth := ⋯ }

def DiffSp.isColimitCoconeOfForget {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J DiffSp} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget DiffSp))) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (coconeOfCoconeForget c)

Given a functor F : J ⥤ DiffSp and a cocone c : Cocone (F ⋙ forget) of the underlying cocone of types, the colimit of F is c.pt equipped with the supremum of the coinduced diffeologies by the maps c.ι.app j.

Equations

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

instance DiffSp.hasColimitsOfSize : CategoryTheory.Limits.HasColimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} DiffSp

instance DiffSp.hasColimits : CategoryTheory.Limits.HasColimits DiffSp

DiffSp has all colimits, i.e. it is cocomplete.

instance DiffSp.forgetPreservesColimitsOfSize : CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget DiffSp)

instance DiffSp.forgetPreservesColimits : CategoryTheory.Limits.PreservesColimits (CategoryTheory.forget DiffSp)

The forgetful functor DiffSp ⥤ Type preserves all colimits.

Products

Products in DiffSp are given by the usual products of spaces. Adapted from Mathlib.CategoryTheory.Limits.Shapes.Types.

def DiffSp.binaryProductCone (X Y : DiffSp) : CategoryTheory.Limits.BinaryFan X Y

The product space X × Y as a cone.

Equations

• X.binaryProductCone Y = CategoryTheory.Limits.BinaryFan.mk { hom' := { toFun := Prod.fst, dsmooth := ⋯ } } { hom' := { toFun := Prod.snd, dsmooth := ⋯ } }

def DiffSp.binaryProductLimit (X Y : DiffSp) : CategoryTheory.Limits.IsLimit (X.binaryProductCone Y)

DiffSp.binaryProductCone X Y is actually a limiting cone.

Equations

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

def DiffSp.binaryProductFunctor : CategoryTheory.Functor DiffSp (CategoryTheory.Functor DiffSp DiffSp)

The functor taking X, Y to the product space X × Y.

Equations

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

noncomputable def DiffSp.binaryProductIsoProd : binaryProductFunctor ≅ CategoryTheory.Limits.prod.functor

The explicit products we defined are naturally isomorphic to the products coming from the HasLimits instance on DiffSp. This is needed because the HasLimits instance only stores proof that all limits exist, not the explicit constructions, so the products derived from it are picked with the axiom of choice.

Equations

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

def DiffSp.terminalCone : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty DiffSp)

The one-point space as a cone.

Equations

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

def DiffSp.terminalCodeIsLimit : CategoryTheory.Limits.IsLimit terminalCone

DiffSp.terminalCone is actually limiting.

Equations

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

instance DiffSp.instCartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory DiffSp

Equations

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

noncomputable instance DiffSp.cartesianClosed : CategoryTheory.CartesianClosed DiffSp

DiffSp is cartesian-closed.

Equations

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