Induced/coinduced diffeologies and inductions/subductions

In large parts based on Mathlib.Topology.Order.

@[implicit_reducible]

def DiffeologicalSpace.induced {X : Type u_1} {Y : Type u_2} (f : X → Y) (dY : DiffeologicalSpace Y) : DiffeologicalSpace X

The coarsest diffeology on X such that f : X → Y is smooth, also known as the pullback diffeology.

Equations

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

@[implicit_reducible]

def DiffeologicalSpace.coinduced {X : Type u_1} {Y : Type u_2} (f : X → Y) (dX : DiffeologicalSpace X) : DiffeologicalSpace Y

The finest diffeology on Y such that f : X → Y is smooth, also known as the pushforward diffeology. While this is just the infimum of all diffeologies that make f smooth, we use a slightly more involved construction to make the D-topology defeq to the coinduced topology.

Equations

• DiffeologicalSpace.coinduced f dX = (sInf {d : DiffeologicalSpace Y | DSmooth f}).withDTopology (TopologicalSpace.coinduced f DTop) ⋯

theorem isPlot_induced_iff {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {f : X → Y} {n : ℕ} {p : Eucl n → X} : IsPlot p ↔ IsPlot (f ∘ p)

theorem DSmooth.le_induced {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {f : X → Y} (hf : DSmooth f) : dX ≤ DiffeologicalSpace.induced f dY

theorem dsmooth_iff_le_induced {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {f : X → Y} : DSmooth f ↔ dX ≤ DiffeologicalSpace.induced f dY

theorem DiffeologicalSpace.coinduced_eq_sInf {X : Type u_1} {Y : Type u_2} {f : X → Y} {dX : DiffeologicalSpace X} : coinduced f dX = sInf {d : DiffeologicalSpace Y | DSmooth f}

The coinduced diffeology is the infimum of all diffeologies that make f smooth.

theorem DSmooth.coinduced_le {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {f : X → Y} (hf : DSmooth f) : DiffeologicalSpace.coinduced f dX ≤ dY

theorem dsmooth_iff_coinduced_le {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {f : X → Y} : DSmooth f ↔ DiffeologicalSpace.coinduced f dX ≤ dY

theorem DiffeologicalSpace.coinduced_eq_generateFrom {X : Type u_4} {Y : Type u_5} [dX : DiffeologicalSpace X] {f : X → Y} : coinduced f dX = generateFrom {p : (n : ℕ) × (Eucl n → Y) | ∃ (q : Eucl p.fst → X), IsPlot q ∧ p.snd = f ∘ q}

The diffeology coinduced by f : X → Y is generated by all plots of the form f ∘ p for plots p in X.

theorem dTop_coinduced_comm {X : Type u_4} {Y : Type u_5} {dX : DiffeologicalSpace X} {f : X → Y} : DTop = TopologicalSpace.coinduced f DTop

The D-topology of the coinduced diffeology agrees with the coinduced topology.

theorem DiffeologicalSpace.coinduced_le_iff_le_induced {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {f : X → Y} : coinduced f dX ≤ dY ↔ dX ≤ induced f dY

theorem DiffeologicalSpace.gc_coinduced_induced {X : Type u_1} {Y : Type u_2} (f : X → Y) : GaloisConnection (coinduced f) (induced f)

theorem DiffeologicalSpace.induced_mono {X : Type u_1} {Y : Type u_2} {f : X → Y} {d₁ d₂ : DiffeologicalSpace Y} (h : d₁ ≤ d₂) : induced f d₁ ≤ induced f d₂

theorem DiffeologicalSpace.coinduced_mono {X : Type u_1} {Y : Type u_2} {f : X → Y} {d₁ d₂ : DiffeologicalSpace X} (h : d₁ ≤ d₂) : coinduced f d₁ ≤ coinduced f d₂

@[simp]

theorem DiffeologicalSpace.induced_top {X : Type u_1} {Y : Type u_2} {f : X → Y} : induced f ⊤ = ⊤

@[simp]

theorem DiffeologicalSpace.induced_inf {X : Type u_1} {Y : Type u_2} {d₁ d₂ : DiffeologicalSpace Y} {f : X → Y} : induced f (d₁ ⊓ d₂) = induced f d₁ ⊓ induced f d₂

@[simp]

theorem DiffeologicalSpace.induced_iInf {X : Type u_1} {Y : Type u_2} {ι : Sort u_4} {d : ι → DiffeologicalSpace Y} {f : X → Y} : induced f (⨅ (i : ι), d i) = ⨅ (i : ι), induced f (d i)

@[simp]

theorem DiffeologicalSpace.coinduced_bot {X : Type u_1} {Y : Type u_2} {f : X → Y} : coinduced f ⊥ = ⊥

@[simp]

theorem DiffeologicalSpace.coinduced_sup {X : Type u_1} {Y : Type u_2} {d₁ d₂ : DiffeologicalSpace X} {f : X → Y} : coinduced f (d₁ ⊔ d₂) = coinduced f d₁ ⊔ coinduced f d₂

@[simp]

theorem DiffeologicalSpace.coinduced_iSup {X : Type u_1} {Y : Type u_2} {ι : Sort u_4} {d : ι → DiffeologicalSpace X} {f : X → Y} : coinduced f (⨆ (i : ι), d i) = ⨆ (i : ι), coinduced f (d i)

theorem DiffeologicalSpace.induced_id {X : Type u_1} {dX : DiffeologicalSpace X} : induced id dX = dX

theorem DiffeologicalSpace.induced_compose {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {dZ : DiffeologicalSpace Z} {f : X → Y} {g : Y → Z} : induced f (induced g dZ) = induced (g ∘ f) dZ

theorem DiffeologicalSpace.induced_const {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {y : Y} : induced (fun (x : X) => y) dY = ⊤

theorem DiffeologicalSpace.coinduced_id {X : Type u_1} {dX : DiffeologicalSpace X} : coinduced id dX = dX

theorem DiffeologicalSpace.coinduced_compose {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {dX : DiffeologicalSpace X} {f : X → Y} {g : Y → Z} : coinduced g (coinduced f dX) = coinduced (g ∘ f) dX

theorem DiffeologicalSpace.coinduced_const {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {y : Y} : coinduced (fun (x : X) => y) dX = ⊥

theorem Equiv.induced_diffeology_symm {X : Type u_1} {Y : Type u_2} (e : X ≃ Y) : DiffeologicalSpace.induced ⇑e.symm = DiffeologicalSpace.coinduced ⇑e

theorem Equiv.coinduced_diffeology_symm {X : Type u_1} {Y : Type u_2} (e : X ≃ Y) : DiffeologicalSpace.coinduced ⇑e.symm = DiffeologicalSpace.induced ⇑e

theorem dsmooth_generateFrom_iff {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {g : Set ((n : ℕ) × (Eucl n → X))} {f : X → Y} : DSmooth f ↔ ∀ (n : ℕ) (p : Eucl n → X), ⟨n, p⟩ ∈ g → IsPlot (f ∘ p)

theorem dsmooth_induced_dom {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {f : X → Y} : DSmooth f

theorem dsmooth_induced_rng {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {dY : DiffeologicalSpace Y} {dZ : DiffeologicalSpace Z} {f : X → Y} {g : Z → X} : DSmooth g ↔ DSmooth (f ∘ g)

theorem dsmooth_coinduced_rng {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {f : X → Y} : DSmooth f

theorem dsmooth_coinduced_dom {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {dX : DiffeologicalSpace X} {dZ : DiffeologicalSpace Z} {f : X → Y} {g : Y → Z} : DSmooth g ↔ DSmooth (g ∘ f)

theorem dsmooth_le_dom {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {dX' : DiffeologicalSpace X} {f : X → Y} (h : dX' ≤ dX) : DSmooth f → DSmooth f

theorem dsmooth_le_rng {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY dY' : DiffeologicalSpace Y} {f : X → Y} (h : dY ≤ dY') : DSmooth f → DSmooth f

theorem dsmooth_sup_dom {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {dX' : DiffeologicalSpace X} {f : X → Y} : DSmooth f ↔ DSmooth f ∧ DSmooth f

theorem dsmooth_sup_rng_left {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY dY' : DiffeologicalSpace Y} {f : X → Y} : DSmooth f → DSmooth f

theorem dsmooth_sup_rng_right {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY dY' : DiffeologicalSpace Y} {f : X → Y} : DSmooth f → DSmooth f

theorem dsmooth_sSup_dom {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {f : X → Y} {D : Set (DiffeologicalSpace X)} : DSmooth f ↔ ∀ d ∈ D, DSmooth f

theorem dsmooth_sSup_rng {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {f : X → Y} {D : Set (DiffeologicalSpace Y)} (h : dY ∈ D) (hf : DSmooth f) : DSmooth f

theorem dsmooth_iSup_dom {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {f : X → Y} {ι : Type u_4} {D : ι → DiffeologicalSpace X} : DSmooth f ↔ ∀ (i : ι), DSmooth f

theorem dsmooth_iSup_rng {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {f : X → Y} {ι : Type u_4} {D : ι → DiffeologicalSpace Y} {i : ι} (h : DSmooth f) : DSmooth f

theorem dsmooth_inf_rng {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY dY' : DiffeologicalSpace Y} {f : X → Y} : DSmooth f ↔ DSmooth f ∧ DSmooth f

theorem dsmooth_inf_dom_left {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {dX' : DiffeologicalSpace X} {f : X → Y} : DSmooth f → DSmooth f

theorem dsmooth_inf_dom_right {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {dX' : DiffeologicalSpace X} {f : X → Y} : DSmooth f → DSmooth f

theorem dsmooth_sInf_dom {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {dY : DiffeologicalSpace Y} {f : X → Y} {D : Set (DiffeologicalSpace X)} (h : dX ∈ D) : DSmooth f → DSmooth f

theorem dsmooth_sInf_rng {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {f : X → Y} {D : Set (DiffeologicalSpace Y)} : DSmooth f ↔ ∀ d ∈ D, DSmooth f

theorem dsmooth_iInf_dom {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {f : X → Y} {ι : Type u_4} {D : ι → DiffeologicalSpace X} {i : ι} : DSmooth f → DSmooth f

theorem dsmooth_iInf_rng {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {f : X → Y} {ι : Type u_4} {D : ι → DiffeologicalSpace Y} : DSmooth f ↔ ∀ (i : ι), DSmooth f

theorem dsmooth_bot {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {f : X → Y} : DSmooth f

theorem dsmooth_top {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {f : X → Y} : DSmooth f

theorem dsmooth_id_iff_le {X : Type u_1} {dX dX' : DiffeologicalSpace X} : DSmooth id ↔ dX ≤ dX'

theorem dsmooth_id_of_le {X : Type u_1} {dX dX' : DiffeologicalSpace X} (h : dX ≤ dX') : DSmooth id

theorem dTop_induced_le_induced_dTop {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {f : X → Y} : DTop ≤ TopologicalSpace.induced f DTop

The D-topology of the induced diffeology is always at least as fine as the induced topology.

theorem dTop_induced_comm {X : Type u_4} {Y : Type u_5} {dY : DiffeologicalSpace Y} {f : X → Y} (hf : IsOpen (Set.range f)) : DTop = TopologicalSpace.induced f DTop

For functions whose range is D-open, the D-topology of the induced diffeology agrees with the induced topology.

structure IsDInducing {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] (f : X → Y) : Prop

We call a map "D-inducing" (short for diffeologically inducing) if its domain carries the diffeology induced by it. This doesn't seem to appear in the literature, but we introduce it as a weaker version of inductions for situations where injectivity isn't actually needed.

This is analogous to inducing maps in topology, whereas inductions are analagous to embeddings.

• eq_induced : dX = DiffeologicalSpace.induced f dY

theorem isDInducing_iff {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] (f : X → Y) : IsDInducing f ↔ dX = DiffeologicalSpace.induced f dY

structure IsInduction {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] (f : X → Y) extends IsDInducing f : Prop

An induction is a map between diffeological spaces that is both inducing and injective. This is analogous to embeddings in topology.

• eq_induced : dX = DiffeologicalSpace.induced f dY
• injective : Function.Injective f

theorem isInduction_iff {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] (f : X → Y) : IsInduction f ↔ IsDInducing f ∧ Function.Injective f

structure IsDCoinducing {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] (f : X → Y) : Prop

We call a map "D-coinducing" (short for diffeologically coinducing) if its codomain carries the diffeology coinduced by it. This doesn't seem to appear in the literature, but we introduce it as a weaker version of subductions for situations where surjectivity isn't actually needed.

This is analogous to coinducing maps in topology, whereas subductions are analagous to quotient maps.

• eq_coinduced : dY = DiffeologicalSpace.coinduced f dX

theorem isDCoinducing_iff {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] (f : X → Y) : IsDCoinducing f ↔ dY = DiffeologicalSpace.coinduced f dX

structure IsSubduction {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] (f : X → Y) extends IsDCoinducing f : Prop

A subduction is a map between diffeological spaces that is both coinducing and surjective. This is analogous to quotient maps in topology.

• eq_coinduced : dY = DiffeologicalSpace.coinduced f dX
• surjective : Function.Surjective f

theorem isSubduction_iff {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] (f : X → Y) : IsSubduction f ↔ IsDCoinducing f ∧ Function.Surjective f

def IsDInducing_of : Lean.ParserDescr

Equations

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

def IsDCoinducing_of : Lean.ParserDescr

Equations

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

def IsInduction_of : Lean.ParserDescr

Equations

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

def IsSubduction_of : Lean.ParserDescr

Equations

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

theorem isDInducing_induced {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {f : X → Y} : IsDInducing f

theorem isDCoinducing_coinduced {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {f : X → Y} : IsDCoinducing f

theorem Function.Injective.isInduction_induced {X : Type u_1} {Y : Type u_2} {dY : DiffeologicalSpace Y} {f : X → Y} (hf : Injective f) : IsInduction f

theorem Function.Surjective.isSubduction_coinduced {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} {f : X → Y} (hf : Surjective f) : IsSubduction f

theorem IsDInducing.dsmooth {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} (hf : IsDInducing f) : DSmooth f

theorem IsDCoinducing.dsmooth {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} (hf : IsDCoinducing f) : DSmooth f

theorem isDInducing_id {X : Type u_1} [dX : DiffeologicalSpace X] : IsDInducing id

theorem isInduction_id {X : Type u_1} [dX : DiffeologicalSpace X] : IsInduction id

theorem IsDInducing.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsDInducing g) (hf : IsDInducing f) : IsDInducing (g ∘ f)

theorem IsInduction.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsInduction g) (hf : IsInduction f) : IsInduction (g ∘ f)

theorem IsDInducing.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsDInducing g) (hf : IsDInducing f) : IsDInducing fun (x : X) => g (f x)

theorem IsInduction.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsInduction g) (hf : IsInduction f) : IsInduction fun (x : X) => g (f x)

theorem IsDInducing.of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsDInducing g) (h : IsDInducing (g ∘ f)) : IsDInducing f

theorem IsInduction.of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsInduction g) (h : IsInduction (g ∘ f)) : IsInduction f

theorem IsDInducing.of_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsDInducing g) : IsDInducing (g ∘ f) ↔ IsDInducing f

theorem IsInduction.of_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsInduction g) : IsInduction (g ∘ f) ↔ IsInduction f

theorem IsDInducing.of_comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : DSmooth f) (hg : DSmooth g) (h : IsDInducing (g ∘ f)) : IsDInducing f

theorem IsInduction.of_comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : DSmooth f) (hg : DSmooth g) (h : IsInduction (g ∘ f)) : IsInduction f

theorem isDCoinducing_id {X : Type u_1} [dX : DiffeologicalSpace X] : IsDCoinducing id

theorem isSubduction_id {X : Type u_1} [dX : DiffeologicalSpace X] : IsSubduction id

theorem IsDCoinducing.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsDCoinducing g) (hf : IsDCoinducing f) : IsDCoinducing (g ∘ f)

theorem IsSubduction.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsSubduction g) (hf : IsSubduction f) : IsSubduction (g ∘ f)

theorem IsDCoinducing.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsDCoinducing g) (hf : IsDCoinducing f) : IsDCoinducing fun (x : X) => g (f x)

theorem IsSubduction.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsSubduction g) (hf : IsSubduction f) : IsSubduction fun (x : X) => g (f x)

theorem IsDCoinducing.of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : IsDCoinducing f) (h : IsDCoinducing (g ∘ f)) : IsDCoinducing g

theorem IsSubduction.of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : IsSubduction f) (h : IsSubduction (g ∘ f)) : IsSubduction g

theorem IsDCoinducing.of_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : IsDCoinducing f) : IsDCoinducing (g ∘ f) ↔ IsDCoinducing g

theorem IsSubduction.of_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : IsSubduction f) : IsSubduction (g ∘ f) ↔ IsSubduction g

theorem IsDCoinducing.of_comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : DSmooth f) (hg : DSmooth g) (h : IsDCoinducing (g ∘ f)) : IsDCoinducing g

theorem IsSubduction.of_comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : DSmooth f) (hg : DSmooth g) (h : IsSubduction (g ∘ f)) : IsSubduction g

theorem IsDInducing.dsmooth_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsDInducing g) : DSmooth f ↔ DSmooth (g ∘ f)

theorem IsDInducing.isPlot_iff {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} {n : ℕ} {p : Eucl n → X} (hf : IsDInducing f) : IsPlot p ↔ IsPlot (f ∘ p)

theorem IsDCoinducing.dsmooth_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : IsDCoinducing f) : DSmooth g ↔ DSmooth (g ∘ f)

theorem Function.LeftInverse.isInduction {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} {g : Y → X} (h : LeftInverse f g) (hf : DSmooth f) (hg : DSmooth g) : IsInduction g

theorem Function.LeftInverse.isSubduction {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} {g : Y → X} (h : LeftInverse f g) (hf : DSmooth f) (hg : DSmooth g) : IsSubduction f

structure IsOpenInduction {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] (f : X → Y) extends IsInduction f : Prop

An open induction is an induction that is also an open map with respect to the D-topologies. What makes this an especially interesting notion compared to e.g. closed inductions is that while inductions are not always embeddings, open inductions are always open embeddings; furthermore, inductions are open iff their range is open. In comparison, an induction whose range is closed can still be both not an embedding and not a closed map.

• eq_induced : dX = DiffeologicalSpace.induced f dY
• injective : Function.Injective f
• isOpenMap : IsOpenMap f

theorem isOpenInduction_iff {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] (f : X → Y) : IsOpenInduction f ↔ IsInduction f ∧ IsOpenMap f

theorem IsOpenInduction.isOpenMap' {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [TopologicalSpace X] [DTopCompatible X] [TopologicalSpace Y] [DTopCompatible Y] {f : X → Y} (hf : IsOpenInduction f) : IsOpenMap f

theorem IsOpenInduction.isEmbedding {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} (hf : IsOpenInduction f) : Topology.IsEmbedding f

theorem IsOpenInduction.isEmbedding' {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [TopologicalSpace X] [DTopCompatible X] [TopologicalSpace Y] [DTopCompatible Y] {f : X → Y} (hf : IsOpenInduction f) : Topology.IsEmbedding f

theorem IsOpenInduction.isOpen_range {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} (hf : IsOpenInduction f) : IsOpen (Set.range f)

theorem IsOpenInduction.isOpen_range' {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [TopologicalSpace Y] [DTopCompatible Y] {f : X → Y} (hf : IsOpenInduction f) : IsOpen (Set.range f)

theorem IsOpenInduction.isOpenEmbedding {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} (hf : IsOpenInduction f) : Topology.IsOpenEmbedding f

theorem IsOpenInduction.isOpenEmbedding' {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [TopologicalSpace X] [DTopCompatible X] [TopologicalSpace Y] [DTopCompatible Y] {f : X → Y} (hf : IsOpenInduction f) : Topology.IsOpenEmbedding f

theorem IsInduction.isOpenInduction_of_isOpen_range {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} (hf : IsInduction f) (hf' : IsOpen (Set.range f)) : IsOpenInduction f

theorem IsInduction.isOpenInduction_of_isOpen_range' {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [TopologicalSpace Y] [DTopCompatible Y] {f : X → Y} (hf : IsInduction f) (hf' : IsOpen (Set.range f)) : IsOpenInduction f

theorem isOpenInduction_iff_isInduction_and_isOpen_range {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} : IsOpenInduction f ↔ IsInduction f ∧ IsOpen (Set.range f)

theorem isOpenInduction_iff_isInduction_and_isOpen_range' {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [TopologicalSpace Y] [DTopCompatible Y] {f : X → Y} : IsOpenInduction f ↔ IsInduction f ∧ IsOpen (Set.range f)

theorem IsInduction.isOpenInduction_of_surjective {X : Type u_1} {Y : Type u_2} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] {f : X → Y} (hf : IsInduction f) (hf' : Function.Surjective f) : IsOpenInduction f

theorem isOpenInduction_id {X : Type u_1} [dX : DiffeologicalSpace X] : IsOpenInduction id

theorem IsOpenInduction.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsOpenInduction g) (hf : IsOpenInduction f) : IsOpenInduction (g ∘ f)

theorem IsOpenInduction.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsOpenInduction g) (hf : IsOpenInduction f) : IsOpenInduction fun (x : X) => g (f x)

theorem IsOpenInduction.of_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsOpenInduction g) (h : IsOpenInduction (g ∘ f)) : IsOpenInduction f

theorem IsOpenInduction.of_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsOpenInduction g) : IsOpenInduction (g ∘ f) ↔ IsOpenInduction f

theorem IsOpenInduction.of_comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [dZ : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : IsInduction g) (h : IsOpenInduction (g ∘ f)) : IsOpenInduction f