Documentation

TauCeti.Geometry.Diffeology.PlotOn

Plots on subsets of Cartesian spaces #

This file defines when a map from a Cartesian space to a diffeological space is a plot on a subset of its domain: its composite with every smooth map into the subset is a plot. On open subsets this is the usual local notion of a plot, and it does not require the map to extend to a plot on the whole Cartesian space.

source
def TauCeti.Diffeology.IsPlotOn {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} (u : Set (EuclideanSpace ℝ (Fin n))) (p : EuclideanSpace ℝ (Fin n) → X) :
Prop

A map defined on a subset of a Cartesian space is a plot on that subset if its composite with every smooth map having image in the subset is a globally defined plot.

For an open subset, this is the usual local notion of a diffeological plot.

Instances For
    source
    theorem TauCeti.Diffeology.isPlotOn_iff {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → X} :
    IsPlotOn u p ↔ ∀ {m : ℕ} (f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)), Set.MapsTo f Set.univ u → ContDiff ℝ (↑⊤) f → Diffeology.IsPlot (p ∘ f)

    A map is a plot on a subset exactly when its composite with every smooth map having image in the subset is a plot.

    source
    theorem TauCeti.Diffeology.IsPlotOn.isPlot_comp {X : Type u_1} [DiffeologicalSpace X] {n m : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → X} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)} (hp : IsPlotOn u p) (hfu : Set.MapsTo f Set.univ u) (hf : ContDiff ℝ (↑⊤) f) :
    Diffeology.IsPlot (p ∘ f)

    Composing a plot on a subset with a smooth map into that subset gives a plot.

    source
    theorem TauCeti.Diffeology.isPlotOn_of_isPlot {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} (hp : Diffeology.IsPlot p) (u : Set (EuclideanSpace ℝ (Fin n))) :
    IsPlotOn u p

    Globally defined plots are plots on every subset.

    source
    theorem TauCeti.Diffeology.IsPlotOn.congr {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {p p' : EuclideanSpace ℝ (Fin n) → X} (hp : IsPlotOn u p) (hpp' : Set.EqOn p p' u) :
    IsPlotOn u p'

    Being a plot on a subset depends only on the restriction to that subset.

    source
    theorem TauCeti.Diffeology.IsPlotOn.mono {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {u v : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → X} (hp : IsPlotOn u p) (hvu : v ⊆ u) :
    IsPlotOn v p

    A plot on a set remains a plot on a smaller set.

    source
    theorem TauCeti.Diffeology.isPlotOn_const {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} (u : Set (EuclideanSpace ℝ (Fin n))) (x : X) :
    IsPlotOn u fun (x_1 : EuclideanSpace ℝ (Fin n)) => x

    Constant maps are plots on every subset.

    source
    theorem TauCeti.Diffeology.IsPlotOn.isPlot {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} (hp : IsPlotOn Set.univ p) :
    Diffeology.IsPlot p

    A plot on all of Cartesian space is a plot.

    source
    @[simp]
    theorem TauCeti.Diffeology.isPlotOn_univ_iff {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X} :
    IsPlotOn Set.univ p ↔ Diffeology.IsPlot p

    Being a plot on all of Cartesian space is equivalent to being a globally defined plot.

    source
    theorem TauCeti.Diffeology.IsPlotOn.comp_contDiffOn {X : Type u_1} [DiffeologicalSpace X] {n m : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {v : Set (EuclideanSpace ℝ (Fin m))} {p : EuclideanSpace ℝ (Fin n) → X} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)} (hp : IsPlotOn u p) (hf : ContDiffOn ℝ (↑⊤) f v) (hfu : Set.MapsTo f v u) :
    IsPlotOn v (p ∘ f)

    Plots on subsets are stable under smooth reparametrization on subsets.

    source
    theorem TauCeti.Diffeology.IsPlotOn.dSmooth_comp {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → X} {f : X → Y} (hp : IsPlotOn u p) (hf : Diffeology.DSmooth f) :
    IsPlotOn u (f ∘ p)

    Plots on subsets are stable under postcomposition with smooth maps.

    source
    theorem TauCeti.Diffeology.isPlotOn_of_locally {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → X} (hp : ∀ z ∈ u, ∃ (v : Set (EuclideanSpace ℝ (Fin n))), IsOpen v ∧ z ∈ v ∧ IsPlotOn v p) :
    IsPlotOn u p

    A map that is a plot on an open neighborhood of each point of a subset is a plot on that subset.

    source
    theorem TauCeti.Diffeology.IsPlotOn.continuousOn {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → X} (hp : IsPlotOn u p) (hu : IsOpen u) :
    ContinuousOn p u

    A plot on an open subset is continuous on that subset for the D-topology.