Constructions of diffeological spaces #
This file gives some concrete constructions like products and coproducts of
diffeological spaces. General limits and colimits are found in
Orbifolds.Diffeology.DiffSp.
Mostly based on Mathlib.Topology.Constructions.
TODO #
- binary disjoint unions
- arbitrary disjoint unions
- more API on arbitrary products
Equations
instance
instDiffeologicalSpaceProd
{X : Type u_1}
{Y : Type u_2}
[dX : DiffeologicalSpace X]
[dY : DiffeologicalSpace Y]
:
DiffeologicalSpace (X × Y)
instance
Pi.diffeologicalSpace
{ι : Type u_1}
{Y : ι → Type u_2}
[D : (i : ι) → DiffeologicalSpace (Y i)]
:
DiffeologicalSpace ((i : ι) → Y i)
Equations
- Pi.diffeologicalSpace = ⨅ (i : ι), DiffeologicalSpace.induced (fun (x : (i : ι) → Y i) => x i) (D i)
Additive, Multiplicative #
The diffeology on those type synonyms is inherited without change.
Equations
Equations
Order dual #
The diffeology on this type synonym is inherited without change.
Equations
theorem
IsOpen.isOpenInduction_subtype_val
{X : Type u_1}
[DiffeologicalSpace X]
{s : Set X}
(hs : IsOpen s)
:
theorem
IsOpen.isOpenInduction_subtype_val'
{X : Type u_1}
[DiffeologicalSpace X]
{s : Set X}
[TopologicalSpace X]
[DTopCompatible X]
(hs : IsOpen s)
:
theorem
IsDInducing.of_codRestrict
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
{t : Set Y}
(ht : ∀ (x : X), f x ∈ t)
(hf : IsDInducing (Set.codRestrict f t ht))
:
theorem
IsInduction.of_codRestrict
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
{t : Set Y}
(ht : ∀ (x : X), f x ∈ t)
(hf : IsInduction (Set.codRestrict f t ht))
:
theorem
DSmooth.subtype_val
{X : Type u_1}
[DiffeologicalSpace X]
{p : X → Prop}
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : Y → Subtype p}
(hf : DSmooth f)
:
DSmooth fun (x : Y) => ↑(f x)
theorem
DSmooth.subtype_mk
{X : Type u_1}
[DiffeologicalSpace X]
{p : X → Prop}
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : Y → X}
(hf : DSmooth f)
(hp : ∀ (x : Y), p (f x))
:
DSmooth fun (x : Y) => ⟨f x, ⋯⟩
theorem
DSmooth.subtype_map
{X : Type u_1}
[DiffeologicalSpace X]
{p : X → Prop}
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
(h : DSmooth f)
{q : Y → Prop}
(hpq : ∀ (x : X), p x → q (f x))
:
DSmooth (Subtype.map f hpq)
theorem
IsOpen.isOpenInduction_inclusion
{X : Type u_1}
[DiffeologicalSpace X]
{s t : Set X}
(hs : IsOpen s)
(h : s ⊆ t)
:
theorem
IsOpen.isOpenInduction_inclusion'
{X : Type u_1}
[DiffeologicalSpace X]
[TopologicalSpace X]
[DTopCompatible X]
{s t : Set X}
(hs : IsOpen s)
(h : s ⊆ t)
:
theorem
dsmooth_inclusion
{X : Type u_1}
[DiffeologicalSpace X]
{s t : Set X}
(h : s ⊆ t)
:
DSmooth (Set.inclusion h)
theorem
DSmooth.codRestrict
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
{s : Set Y}
(hf : DSmooth f)
(hs : ∀ (a : X), f a ∈ s)
:
DSmooth (Set.codRestrict f s hs)
theorem
DSmooth.restrict
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
{s : Set X}
{t : Set Y}
(h1 : Set.MapsTo f s t)
(h2 : DSmooth f)
:
DSmooth (Set.MapsTo.restrict f s t h1)
theorem
DSmooth.restrictPreimage
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
{s : Set Y}
(h : DSmooth f)
:
DSmooth (s.restrictPreimage f)
theorem
IsDInducing.codRestrict
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
(hf : IsDInducing f)
{s : Set Y}
(hs : ∀ (x : X), f x ∈ s)
:
IsDInducing (Set.codRestrict f s hs)
theorem
IsInduction.codRestrict
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
(hf : IsInduction f)
{s : Set Y}
(hs : ∀ (x : X), f x ∈ s)
:
IsInduction (Set.codRestrict f s hs)
theorem
IsOpenInduction.codRestrict
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
(hf : IsOpenInduction f)
{s : Set Y}
(hs : ∀ (x : X), f x ∈ s)
:
IsOpenInduction (Set.codRestrict f s hs)
theorem
IsDInducing.restrict
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
(hf : IsDInducing f)
{s : Set X}
{t : Set Y}
(hf' : Set.MapsTo f s t)
:
IsDInducing (Set.MapsTo.restrict f s t hf')
theorem
IsInduction.restrict
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
(hf : IsInduction f)
{s : Set X}
{t : Set Y}
(hf' : Set.MapsTo f s t)
:
IsInduction (Set.MapsTo.restrict f s t hf')
theorem
IsOpenInduction.restrict
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
(hf : IsOpenInduction f)
{s : Set X}
{t : Set Y}
(hs : IsOpen s)
(hf' : Set.MapsTo f s t)
:
IsOpenInduction (Set.MapsTo.restrict f s t hf')
theorem
IsOpenInduction.restrict'
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
[TopologicalSpace X]
[DTopCompatible X]
{f : X → Y}
(hf : IsOpenInduction f)
{s : Set X}
{t : Set Y}
(hs : IsOpen s)
(hf' : Set.MapsTo f s t)
:
IsOpenInduction (Set.MapsTo.restrict f s t hf')
theorem
ContDiffOn.dsmooth_restrict
{X : Type u_1}
[DiffeologicalSpace X]
{s : Set X}
{Y : Type u_2}
[DiffeologicalSpace Y]
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[ContDiffCompatible X]
[NormedAddCommGroup Y]
[NormedSpace ℝ Y]
[ContDiffCompatible Y]
{f : X → Y}
(hf : ContDiffOn ℝ (↑⊤) f s)
:
theorem
IsOpen.dsmooth_iff_contDiffOn
{X : Type u_1}
[DiffeologicalSpace X]
{s : Set X}
{Y : Type u_2}
[DiffeologicalSpace Y]
[NormedAddCommGroup X]
[InnerProductSpace ℝ X]
[ContDiffCompatible X]
[FiniteDimensional ℝ X]
[NormedAddCommGroup Y]
[NormedSpace ℝ Y]
[ContDiffCompatible Y]
{f : X → Y}
(hs : IsOpen s)
:
On an open subset, a function is smooth in the usual sense iff it is smooth diffeologically.
theorem
IsOpenMap.subtype_mk
{X : Type u_3}
{Y : Type u_4}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{f : Y → X}
(hf : IsOpenMap f)
(hfs : ∀ (x : Y), f x ∈ s)
:
IsOpenMap fun (x : Y) => ⟨f x, ⋯⟩
theorem
IsOpen.isOpenMap_subtype_map
{X : Type u_3}
{Y : Type u_4}
[TopologicalSpace X]
[TopologicalSpace Y]
{s : Set X}
{t : Set Y}
{f : X → Y}
(hs : IsOpen s)
(hf : IsOpenMap f)
(hst : ∀ (x : X), s x → t (f x))
:
IsOpenMap (Subtype.map f hst)
theorem
IsOpen.isOpenMap_inclusion
{X : Type u_3}
[TopologicalSpace X]
{s t : Set X}
(hs : IsOpen s)
(h : s ⊆ t)
:
theorem
IsOpenMap.codRestrict
{X : Type u_3}
{Y : Type u_4}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
{s : Set Y}
(hf : IsOpenMap f)
(hs : ∀ (a : X), f a ∈ s)
:
IsOpenMap (Set.codRestrict f s hs)
theorem
IsOpen.dTopCompatible
{X : Type u_1}
[DiffeologicalSpace X]
{s : Set X}
[TopologicalSpace X]
[DTopCompatible X]
(hs : IsOpen s)
:
On open subsets, the D-topology and subspace topology agree.
instance
instDTopCompatibleElemOfFactIsOpen
{X : Type u_1}
[DiffeologicalSpace X]
{s : Set X}
[TopologicalSpace X]
[DTopCompatible X]
[h : Fact (IsOpen s)]
:
instance
instDTopCompatibleSubtypeMemOpens
{X : Type u_1}
[DiffeologicalSpace X]
[TopologicalSpace X]
[DTopCompatible X]
{u : TopologicalSpace.Opens X}
:
theorem
dsmooth_iff'
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
:
Smoothness can also be characterised as preserving smooth maps u → X for open u.
theorem
dsmooth_iff_locally_dsmooth
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
:
theorem
IsLocallyConstant.dsmooth
{X : Type u_1}
[DiffeologicalSpace X]
{Y : Type u_2}
[DiffeologicalSpace Y]
{f : X → Y}
(hf : IsLocallyConstant f)
:
DSmooth f
Any D-locally constant map is smooth.
The indiscrete diffeology is the one for which every map is a plot.
The discrete diffeologoy is the only diffeology whose D-topology is discrete. Note that the corresponding statement for indiscrete spaces is false.
theorem
dsmooth_top_iff_indiscrete_range
{X : Type u_1}
{Y : Type u_2}
{dY : DiffeologicalSpace Y}
{f : X → Y}
:
A map from an indiscrete space is smooth iff its range is indiscrete. Note that this can't be characterised purely topologically, since it might be the case that all involved D-topologies are indiscrete but the diffeologies are not.
theorem
dsmooth_bot_iff_isLocallyConstant
{X : Type u_1}
{Y : Type u_2}
{dX : DiffeologicalSpace X}
{f : X → Y}
:
A map to an discrete space is smooth iff it is D-locally constant.
theorem
isPlot_coinduced_iff
{X : Type u_1}
{Y : Type u_2}
{dX : DiffeologicalSpace X}
{f : X → Y}
{n : ℕ}
{p : Eucl n → Y}
:
A map is a plot in the coinduced diffeology iff it is constant or lifts locally.
theorem
Function.Surjective.isPlot_coinduced_iff
{X : Type u_1}
{Y : Type u_2}
{dX : DiffeologicalSpace X}
{f : X → Y}
(hf : Surjective f)
{n : ℕ}
{p : Eucl n → Y}
:
For surjective functions, the plots of the coinduced diffeology are precicely those that locally lift.
theorem
dTop_eq_iSup_coinduced
{X : Type u_1}
[dX : DiffeologicalSpace X]
:
DTop = ⨆ (p : (n : ℕ) × ↑(DiffeologicalSpace.plots n)), TopologicalSpace.coinduced (↑p.snd) inferInstance
The D-topology is coinduced by all plots.
theorem
coinduced_sigma
{ι Y : Type u}
{X : ι → Type v}
[tX : (i : ι) → TopologicalSpace (X i)]
(f : (i : ι) → X i → Y)
:
TopologicalSpace.coinduced (fun (x : (i : ι) × X i) => f x.fst x.snd) inferInstance = ⨆ (i : ι), TopologicalSpace.coinduced (f i) inferInstance
The topology coinduced by a map out of a sigma type is the surpremum of the topologies
coinduced by its components.
Maybe should go into mathlib? A similar induced_to_pi is already there.
theorem
dTop_eq_coinduced
{X : Type u_1}
[dX : DiffeologicalSpace X]
:
DTop = TopologicalSpace.coinduced (fun (x : (p : (n : ℕ) × ↑(DiffeologicalSpace.plots n)) × Eucl p.fst) => ↑x.fst.snd x.snd)
inferInstance
The D-topology is coinduced by the sum of all plots.
The D-topology is always delta-generated.
instance
instDeltaGeneratedSpaceOfDTopCompatible
{X : Type u_1}
[DiffeologicalSpace X]
[TopologicalSpace X]
[DTopCompatible X]
:
Diffeological spaces are always delta-generated when equipped with the D-topology.
theorem
isDCoinducing_quot_mk
{X : Type u_1}
[DiffeologicalSpace X]
{r : X → X → Prop}
:
IsDCoinducing (Quot.mk r)
theorem
isSubduction_quot_mk
{X : Type u_1}
[DiffeologicalSpace X]
{r : X → X → Prop}
:
IsSubduction (Quot.mk r)
theorem
dsmooth_quot_lift
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
{r : X → X → Prop}
{f : X → Y}
(hr : ∀ (a b : X), r a b → f a = f b)
(h : DSmooth f)
:
theorem
DSmooth.quotient_lift
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
{s : Setoid X}
{f : X → Y}
(h : DSmooth f)
(hs : ∀ (a b : X), a ≈ b → f a = f b)
:
DSmooth (Quotient.lift f hs)
theorem
DSmooth.quotient_liftOn'
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
{s : Setoid X}
{f : X → Y}
(h : DSmooth f)
(hs : ∀ (a b : X), s a b → f a = f b)
:
theorem
DSmooth.quotient_map'
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
{s : Setoid X}
{t : Setoid Y}
{f : X → Y}
(hf : DSmooth f)
(H : Relator.LiftFun (⇑s) (⇑t) f f)
:
DSmooth (Quotient.map' f H)
theorem
isPlot_quot_iff
{X : Type u_1}
[DiffeologicalSpace X]
{r : X → X → Prop}
{n : ℕ}
{p : Eucl n → Quot r}
:
The plots of the quotient diffeology are precicely those that locally lift to plots.
theorem
isPlot_quotient_iff
{X : Type u_1}
[DiffeologicalSpace X]
{s : Setoid X}
{n : ℕ}
{p : Eucl n → Quotient s}
:
The plots of the quotient diffeology are precicely those that locally lift to plots.
instance
instDTopCompatibleQuot
{X : Type u_1}
[DiffeologicalSpace X]
{r : X → X → Prop}
[TopologicalSpace X]
[DTopCompatible X]
:
DTopCompatible (Quot r)
instance
instDTopCompatibleQuotient
{X : Type u_1}
[DiffeologicalSpace X]
{s : Setoid X}
[TopologicalSpace X]
[DTopCompatible X]
:
@[simp]
theorem
dsmooth_prod_mk
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X → Y}
{g : X → Z}
:
theorem
DSmooth.fst
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X → Y × Z}
(hf : DSmooth f)
:
DSmooth fun (x : X) => (f x).1
theorem
DSmooth.fst'
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X → Z}
(hf : DSmooth f)
:
theorem
DSmooth.snd
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X → Y × Z}
(hf : DSmooth f)
:
DSmooth fun (x : X) => (f x).2
theorem
DSmooth.snd'
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : Y → Z}
(hf : DSmooth f)
:
theorem
DSmooth.prod_mk
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : Z → X}
{g : Z → Y}
(hf : DSmooth f)
(hg : DSmooth g)
:
theorem
DSmooth.Prod.mk
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
(x : X)
:
theorem
DSmooth.Prod.mk_left
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
(y : Y)
:
theorem
DSmooth.comp₂
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{W : Type u_4}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
[DiffeologicalSpace W]
{g : X × Y → Z}
(hg : DSmooth g)
{e : W → X}
(he : DSmooth e)
{f : W → Y}
(hf : DSmooth f)
:
theorem
DSmooth.comp₃
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{W : Type u_4}
{ε : Type u_5}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
[DiffeologicalSpace W]
[DiffeologicalSpace ε]
{g : X × Y × Z → ε}
(hg : DSmooth g)
{e : W → X}
(he : DSmooth e)
{f : W → Y}
(hf : DSmooth f)
{k : W → Z}
(hk : DSmooth k)
:
theorem
DSmooth.comp₄
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{W : Type u_4}
{ε : Type u_5}
{ζ : Type u_6}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
[DiffeologicalSpace W]
[DiffeologicalSpace ε]
[DiffeologicalSpace ζ]
{g : X × Y × Z × ζ → ε}
(hg : DSmooth g)
{e : W → X}
(he : DSmooth e)
{f : W → Y}
(hf : DSmooth f)
{k : W → Z}
(hk : DSmooth k)
{l : W → ζ}
(hl : DSmooth l)
:
theorem
DSmooth.prod_map
{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 : Z → X}
{g : W → Y}
(hf : DSmooth f)
(hg : DSmooth g)
:
theorem
dsmooth_inf_dom_left₂
{X : Type u_7}
{Y : Type u_8}
{Z : Type u_9}
{f : X → Y → Z}
{dX dX' : DiffeologicalSpace X}
{dY dY' : DiffeologicalSpace Y}
{dZ : DiffeologicalSpace Z}
(h : DSmooth fun (p : X × Y) => f p.1 p.2)
:
A version of dsmooth_inf_dom_left for binary functions
theorem
dsmooth_inf_dom_right₂
{X : Type u_7}
{Y : Type u_8}
{Z : Type u_9}
{f : X → Y → Z}
{dX dX' : DiffeologicalSpace X}
{dY dY' : DiffeologicalSpace Y}
{dZ : DiffeologicalSpace Z}
(h : DSmooth fun (p : X × Y) => f p.1 p.2)
:
A version of dsmooth_inf_dom_right for binary functions
theorem
dsmooth_sInf_dom₂
{X : Type u_7}
{Y : Type u_8}
{Z : Type u_9}
{f : X → Y → Z}
{DX : Set (DiffeologicalSpace X)}
{DY : Set (DiffeologicalSpace Y)}
{tX : DiffeologicalSpace X}
{tY : DiffeologicalSpace Y}
{tc : DiffeologicalSpace Z}
(hX : tX ∈ DX)
(hY : tY ∈ DY)
(hf : DSmooth fun (p : X × Y) => f p.1 p.2)
:
A version of dsmooth_sInf_dom for binary functions
theorem
DSmooth.uncurry_left
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X → Y → Z}
(x : X)
(h : DSmooth (Function.uncurry f))
:
DSmooth (f x)
theorem
DSmooth.uncurry_right
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X → Y → Z}
(y : Y)
(h : DSmooth (Function.uncurry f))
:
DSmooth fun (a : X) => f a y
theorem
dsmooth_curry
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{g : X × Y → Z}
(x : X)
(h : DSmooth g)
:
DSmooth (Function.curry g x)
theorem
DSmooth.curry_left
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X × Y → Z}
(hf : DSmooth f)
{y : Y}
:
Smooth functions on products are smooth in their first argument
theorem
DSmooth.along_fst
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X × Y → Z}
(hf : DSmooth f)
{y : Y}
:
Alias of DSmooth.curry_left.
Smooth functions on products are smooth in their first argument
theorem
DSmooth.curry_right
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X × Y → Z}
(hf : DSmooth f)
{x : X}
:
Smooth functions on products are smooth in their second argument
theorem
DSmooth.along_snd
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X × Y → Z}
(hf : DSmooth f)
{x : X}
:
Alias of DSmooth.curry_right.
Smooth functions on products are smooth in their second argument
theorem
isSubduction_fst
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[Nonempty Y]
:
The first projection in a product of diffeological spaces is a subduction.
theorem
isSubduction_snd
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[Nonempty X]
:
The second projection in a product of diffeological spaces is a subduction.
theorem
DiffeologicalSpace.prod_induced_induced
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
{W : Type u_4}
[DiffeologicalSpace Y]
[DiffeologicalSpace W]
(f : X → Y)
(g : Z → W)
:
A product of induced diffeologies is induced by the product map.
theorem
DiffeologicalSpace.coinduced_prod_le
{X : Type u_7}
{Y : Type u_8}
{Z : Type u_9}
{W : Type u_10}
[dX : DiffeologicalSpace X]
[dZ : DiffeologicalSpace Z]
(f : X → Y)
(g : Z → W)
:
coinduced (fun (p : X × Z) => (f p.1, g p.2)) instDiffeologicalSpaceProd ≤ instDiffeologicalSpaceProd
The diffeology coinduced by a product map is at least as fine as the product of the coinduced diffelogies. Note that equality only holds when both maps are surjective.
theorem
DiffeologicalSpace.prod_coinduced_coinduced
{X : Type u_7}
{Y : Type u_8}
{Z : Type u_9}
{W : Type u_10}
[dX : DiffeologicalSpace X]
[dZ : DiffeologicalSpace Z]
{f : X → Y}
{g : Z → W}
(hf : Function.Surjective f)
(hg : Function.Surjective g)
:
instDiffeologicalSpaceProd = coinduced (fun (p : X × Z) => (f p.1, g p.2)) instDiffeologicalSpaceProd
A product of coinduced diffeologies is coinduced by the product map, if both maps are surjective.
theorem
IsDInducing.prod_map
{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 : X → Y}
{g : Z → W}
(hf : IsDInducing f)
(hg : IsDInducing g)
:
IsDInducing (Prod.map f g)
theorem
IsInduction.prod_map
{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 : X → Y}
{g : Z → W}
(hf : IsInduction f)
(hg : IsInduction g)
:
IsInduction (Prod.map f g)
theorem
IsSubduction.prod_map
{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 : X → Y}
{g : Z → W}
(hf : IsSubduction f)
(hg : IsSubduction g)
:
IsSubduction (Prod.map f g)
@[simp]
theorem
isDInducing_const_prod
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{x : X}
{f : Y → Z}
:
@[simp]
theorem
isInduction_const_prod
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{x : X}
{f : Y → Z}
:
@[simp]
theorem
isDInducing_prod_const
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{y : Y}
{f : X → Z}
:
@[simp]
theorem
isInduction_prod_const
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{y : Y}
{f : X → Z}
:
theorem
isInduction_graph
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
{f : X → Y}
(hf : DSmooth f)
:
IsInduction fun (x : X) => (x, f x)
theorem
isInduction_prod_mk
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
(x : X)
:
IsInduction (Prod.mk x)
theorem
isInduction_prod_mk_left
{X : Type u_1}
[DiffeologicalSpace X]
(y : X)
:
IsInduction fun (x : X) => (x, y)
instance
instReflexiveDiffeologicalSpaceProd
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[hX : ReflexiveDiffeologicalSpace X]
[hY : ReflexiveDiffeologicalSpace Y]
:
ReflexiveDiffeologicalSpace (X × Y)
Products of reflexive diffeological spaces are reflexive.
instance
instContDiffCompatibleProd
{X : Type u_7}
{Y : Type u_8}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
[DiffeologicalSpace X]
[ContDiffCompatible X]
[NormedAddCommGroup Y]
[NormedSpace ℝ Y]
[DiffeologicalSpace Y]
[ContDiffCompatible Y]
:
ContDiffCompatible (X × Y)
Products of normed spaces are compatible with the product diffeology.
theorem
dTop_prod_le_prod_dTop
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
:
The D-topology of the product diffeology is at least as fine as the product of the D-topologies.
theorem
Topology.IsQuotientMap.id_prod
{X : Type u_7}
{Y : Type u_8}
{Z : Type u_9}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[LocallyCompactSpace X]
{f : Y → Z}
(hf : IsQuotientMap f)
:
IsQuotientMap (Prod.map id f)
For locally compact spaces X, the product functor X × - takes quotient maps to quotient
maps. Note that surjectivity is actually required here - coinducing maps do not necessarily
get taken to coinducing maps.
Adapted from
https://dantopology.wordpress.com/2023/04/21/the-product-of-the-identity-map-and-a-quotient-map/.
TODO: give an explicit description of the coinduced topology without assuming surjectivity
TODO: give an explicit description even without local compactness, using deltaGenerated
TODO: maybe move to mathlib?
theorem
Topology.IsQuotientMap.prod_id
{X : Type u_7}
{Y : Type u_8}
{Z : Type u_9}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[LocallyCompactSpace Z]
{f : X → Y}
(hf : IsQuotientMap f)
:
IsQuotientMap (Prod.map f id)
Analogous to QuotientMap.id_prod.
theorem
Topology.IsQuotientMap.sigma_map
{ι : Type u_7}
{ι' : Type u_8}
{X : ι → Type u_9}
{Y : ι' → Type u_10}
[(i : ι) → TopologicalSpace (X i)]
[(i : ι') → TopologicalSpace (Y i)]
{f₁ : ι → ι'}
{f₂ : (i : ι) → X i → Y (f₁ i)}
(h₁ : Function.Surjective f₁)
(h₂ : ∀ (i : ι), IsQuotientMap (f₂ i))
:
IsQuotientMap (Sigma.map f₁ f₂)
Equivalent of Function.Surjective.sigma_map for quotient maps.
TODO: move to mathlib.
theorem
coinduced_sigma'
{ι : Type u_7}
{Y : Type u_8}
{X : ι → Type v}
[tX : (i : ι) → TopologicalSpace (X i)]
(f : (i : ι) × X i → Y)
:
TopologicalSpace.coinduced f inferInstance = ⨆ (i : ι), TopologicalSpace.coinduced (fun (x : X i) => f ⟨i, x⟩) inferInstance
theorem
dTop_prod_eq_prod_dTop_of_locallyCompact_left
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[LocallyCompactSpace X]
:
For locally compact diffeological spaces, the D-topology commutes with products. This is not true in general, because the product topology might not be delta-generated; however, according to a remark in https://arxiv.org/abs/1302.2935 it should be always true if one takes the product in the category of delta-generated spaces instead of in Top. TODO: work this all out more generally
theorem
dTop_prod_eq_prod_dTop_of_locallyCompact_right
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[LocallyCompactSpace Y]
:
Version of dTop_prod_eq_prod_dTop_of_locallyCompact_left where the second factor
is assumed to be locally compact instead of the first one.
theorem
dsmooth_pi_iff
{ι : Type u_1}
{Y : ι → Type u_2}
[(i : ι) → DiffeologicalSpace (Y i)]
{X : Type u_3}
[DiffeologicalSpace X]
{f : X → (i : ι) → Y i}
:
theorem
dsmooth_pi
{ι : Type u_1}
{Y : ι → Type u_2}
[(i : ι) → DiffeologicalSpace (Y i)]
{X : Type u_3}
[DiffeologicalSpace X]
{f : X → (i : ι) → Y i}
(h : ∀ (i : ι), DSmooth fun (a : X) => f a i)
:
DSmooth f
theorem
dsmooth_apply
{ι : Type u_1}
{Y : ι → Type u_2}
[(i : ι) → DiffeologicalSpace (Y i)]
(i : ι)
:
DSmooth fun (p : (i : ι) → Y i) => p i
instance
instDTopCompatibleForallOfFintypeOfLocallyCompactSpace
{ι : Type u_1}
{Y : ι → Type u_2}
[(i : ι) → DiffeologicalSpace (Y i)]
[Fintype ι]
[(i : ι) → TopologicalSpace (Y i)]
[∀ (i : ι), LocallyCompactSpace (Y i)]
[∀ (i : ι), DTopCompatible (Y i)]
:
DTopCompatible ((i : ι) → Y i)
instance
instContDiffCompatibleForall
{ι : Type u_4}
[Fintype ι]
{Y : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (Y i)]
[(i : ι) → NormedSpace ℝ (Y i)]
[(i : ι) → DiffeologicalSpace (Y i)]
[∀ (i : ι), ContDiffCompatible (Y i)]
:
ContDiffCompatible ((i : ι) → Y i)
instance
DSmoothMap.diffeologicalSpace
{X : Type u_4}
{Y : Type u_5}
[dX : DiffeologicalSpace X]
[dY : DiffeologicalSpace Y]
:
DiffeologicalSpace (DSmoothMap X Y)
The functional diffeology on the space DSmoothMap X Y of smooth maps X → Y.
Equations
- One or more equations did not get rendered due to their size.
theorem
DSmoothMap.isPlot_iff
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
{n : ℕ}
{p : Eucl n → DSmoothMap X Y}
:
theorem
DSmoothMap.dsmooth_iff
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
{f : X → DSmoothMap Y Z}
:
A map f : X → DSmoothMap Y Z is smooth iff the corresponding map X × Y → Z is.
theorem
DSmoothMap.dsmooth_eval
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
:
DSmooth fun (p : DSmoothMap X Y × X) => p.1 p.2
The evaluation map DSmoothMap X Y × X → Y is smooth.
theorem
DSmoothMap.dsmooth_comp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
:
DSmooth fun (x : DSmoothMap Y Z × DSmoothMap X Y) => x.1.comp x.2
The composition map DSmoothMap Y Z × DSmoothMap X Y → DSmoothMap X Z is smooth.
def
DSmoothMap.coev
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
(y : Y)
:
DSmoothMap X (Y × X)
The coevaluation map Y → DSmoothMap X (Y × X).
Equations
- DSmoothMap.coev y = { toFun := fun (x : X) => (y, x), dsmooth := ⋯ }
Instances For
theorem
DSmoothMap.dsmooth_coev
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
:
The coevaluation map is smooth.
def
DSmoothMap.curry
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
(f : DSmoothMap (X × Y) Z)
:
DSmoothMap X (DSmoothMap Y Z)
The currying map DSmoothMap (X × Y) Z → DSmoothMap X (DSmoothMap Y Z)
Equations
- f.curry = { toFun := fun (x : X) => { toFun := Function.curry (⇑f) x, dsmooth := ⋯ }, dsmooth := ⋯ }
Instances For
theorem
DSmoothMap.dsmooth_curry
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
:
The currying map is smooth.
def
DSmoothMap.uncurry
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
(f : DSmoothMap X (DSmoothMap Y Z))
:
DSmoothMap (X × Y) Z
The uncurrying map DSmoothMap X (DSmoothMap Y Z) → DSmoothMap (X × Y) Z.
Instances For
theorem
DSmoothMap.dsmooth_uncurry
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
:
The uncurrying map is smooth.
def
DSmoothMap.fst
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
:
DSmoothMap (X × Y) X
The projection X × Y → X as a DSmoothMap.
Equations
- DSmoothMap.fst = { toFun := Prod.fst, dsmooth := ⋯ }
Instances For
def
DSmoothMap.snd
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
:
DSmoothMap (X × Y) Y
The projection X × Y → Y as a DSmoothMap.
Equations
- DSmoothMap.snd = { toFun := Prod.snd, dsmooth := ⋯ }
Instances For
def
DSmoothMap.prodMk
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[DiffeologicalSpace Z]
(f : DSmoothMap X Y)
(g : DSmoothMap X Z)
:
DSmoothMap X (Y × Z)
The continuous map X → Y × Z corresponding to two maps X → Y, X → Z.
Instances For
def
DSmoothMap.equivFnOfDiscrete
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[TopologicalSpace X]
[DiscreteTopology X]
[DTopCompatible X]
:
The equivalence between smooth functions X → Y and plain functions when X is discrete.
TODO: replace the topological assumptions with [DiscreteDiffeology X] once that is defined.
Equations
- DSmoothMap.equivFnOfDiscrete = { toFun := fun (f : DSmoothMap X Y) => ⇑f, invFun := fun (f : X → Y) => { toFun := f, dsmooth := ⋯ }, left_inv := ⋯, right_inv := ⋯ }
Instances For
def
DSmoothMap.equivFnOfUnique
{X : Type u_1}
{Y : Type u_2}
[DiffeologicalSpace X]
[DiffeologicalSpace Y]
[Unique X]
[TopologicalSpace X]
[DTopCompatible X]
:
The equivalence between smooth functions X → Y and Y when X is discrete.
TODO: remove topological assumptions.
TODO: DDiffeomorph variants of these two constructions.