Bundled smooth embeddings #
Mathlib provides the predicate Manifold.IsSmoothEmbedding I J n f, saying that a map between
manifolds is a C^n immersion and a topological embedding, but it does not bundle maps satisfying
that predicate. This file adds the small bundled type needed by the geometric-topology roadmap's
first-class geometric knot/link presentations: a smooth presentation is a smooth embedding of the
circle into an ambient manifold, and later files should traffic in the embedding as data rather
than in a bare function plus detached hypotheses.
The file deliberately stays at the general manifold level. The roadmap's circle presentations are special cases of this type, while the same bundled smooth embeddings are also the right inputs for later tubular-neighbourhood and surgery interfaces.
Main definitions #
TauCeti.SmoothEmbedding I J n M N: bundledC^nsmooth embeddingsM → N.TauCeti.SmoothEmbedding.toContinuousMap: the underlying continuous map, implemented through Mathlib's genericContinuousMapClasscoercion.TauCeti.SmoothEmbedding.ofIsSmoothEmbedding: bundle a map satisfying Mathlib'sManifold.IsSmoothEmbeddingpredicate.TauCeti.SmoothEmbedding.id: the identity smooth embedding.TauCeti.SmoothEmbedding.ofOpens: the inclusion of an open subset as a smooth embedding.TauCeti.SmoothEmbedding.prodMap: the product of two bundled smooth embeddings.TauCeti.SmoothEmbedding.sumInl/sumInr: the coproduct inclusions as smooth embeddings.
The construction is a thin wrapper around Mathlib's
Manifold.IsSmoothEmbedding API, especially IsSmoothEmbedding.id, of_opens, prodMap,
sumInl, and sumInr.
structure
TauCeti.SmoothEmbedding
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
(I : ModelWithCorners 𝕜 E H)
(J : ModelWithCorners 𝕜 E' H')
(n : WithTop ℕ∞)
(M : Type u_14)
[TopologicalSpace M]
[ChartedSpace H M]
(N : Type u_15)
[TopologicalSpace N]
[ChartedSpace H' N]
:
Type (max u_14 u_15)
A bundled C^n smooth embedding between manifolds.
This is a bundled ContMDiffMap whose underlying function satisfies Mathlib's
Manifold.IsSmoothEmbedding: it is both a C^n immersion and a topological embedding.
- toContMDiffMap : ContMDiffMap I J M N n
The underlying bundled smooth map.
- isSmoothEmbedding_toFun : Manifold.IsSmoothEmbedding I J n ⇑self.toContMDiffMap
The underlying map is a smooth embedding in Mathlib's predicate sense.
Instances For
@[instance_reducible]
instance
TauCeti.SmoothEmbedding.instFunLike
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
:
FunLike (SmoothEmbedding I J n M N) M N
Equations
- TauCeti.SmoothEmbedding.instFunLike = { coe := fun (f : TauCeti.SmoothEmbedding I J n M N) => ⇑f.toContMDiffMap, coe_injective := ⋯ }
instance
TauCeti.SmoothEmbedding.instContinuousMapClass
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
:
ContinuousMapClass (SmoothEmbedding I J n M N) M N
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_toContMDiffMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
:
The bundled C^n map underlying a smooth embedding.
@[reducible, inline]
abbrev
TauCeti.SmoothEmbedding.toContinuousMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
:
The continuous map underlying a bundled smooth embedding.
Equations
- f.toContinuousMap = ↑f
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.toContinuousMap_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
(x : M)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_toContinuousMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
:
theorem
TauCeti.SmoothEmbedding.toContinuousMap_injective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
:
The underlying continuous map determines a bundled smooth embedding.
theorem
TauCeti.SmoothEmbedding.toContinuousMap_inj
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
:
theorem
TauCeti.SmoothEmbedding.contMDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
:
ContMDiff I J n ⇑f
A bundled smooth embedding is a C^n map.
theorem
TauCeti.SmoothEmbedding.isSmoothEmbedding
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
:
Manifold.IsSmoothEmbedding I J n ⇑f
A bundled smooth embedding satisfies Mathlib's smooth-embedding predicate.
theorem
TauCeti.SmoothEmbedding.isImmersion
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
:
Manifold.IsImmersion I J n ⇑f
A bundled smooth embedding is an immersion.
theorem
TauCeti.SmoothEmbedding.isEmbedding
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : SmoothEmbedding I J n M N)
:
A bundled smooth embedding is a topological embedding.
def
TauCeti.SmoothEmbedding.ofIsSmoothEmbedding
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : M → N)
(hf : Manifold.IsSmoothEmbedding I J n f)
:
SmoothEmbedding I J n M N
Bundle a map satisfying Mathlib's smooth-embedding predicate as a smooth embedding.
Equations
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_ofIsSmoothEmbedding
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : M → N)
(hf : Manifold.IsSmoothEmbedding I J n f)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.ofIsSmoothEmbedding_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(f : M → N)
(hf : Manifold.IsSmoothEmbedding I J n f)
(x : M)
:
theorem
TauCeti.SmoothEmbedding.ext
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
(h : ∀ (x : M), f x = g x)
:
Two smooth embeddings are equal when their underlying functions are pointwise equal.
theorem
TauCeti.SmoothEmbedding.ext_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
{f g : SmoothEmbedding I J n M N}
:
def
TauCeti.SmoothEmbedding.id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
[IsManifold I n M]
:
SmoothEmbedding I I n M M
The identity map as a bundled smooth embedding.
Equations
- TauCeti.SmoothEmbedding.id = { toContMDiffMap := ContMDiffMap.id, isSmoothEmbedding_toFun := ⋯ }
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.id_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
[IsManifold I n M]
(x : M)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
[IsManifold I n M]
:
def
TauCeti.SmoothEmbedding.ofOpens
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
[IsManifold I n M]
(s : TopologicalSpace.Opens M)
:
SmoothEmbedding I I n (↥s) M
The inclusion of an open subset of a manifold as a bundled smooth embedding.
Equations
- TauCeti.SmoothEmbedding.ofOpens s = { toContMDiffMap := ⟨Subtype.val, ⋯⟩, isSmoothEmbedding_toFun := ⋯ }
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.ofOpens_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
[IsManifold I n M]
(s : TopologicalSpace.Opens M)
(x : ↥s)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_ofOpens
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
[IsManifold I n M]
(s : TopologicalSpace.Opens M)
:
def
TauCeti.SmoothEmbedding.prodMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{F' : Type u_5}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{G : Type u_8}
[TopologicalSpace G]
{G' : Type u_9}
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{I' : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{M' : Type u_12}
[TopologicalSpace M']
[ChartedSpace G M']
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
[IsManifold I' n M']
[IsManifold J' n N']
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' n M' N')
:
SmoothEmbedding (I.prod I') (J.prod J') n (M × M') (N × N')
The product of two bundled smooth embeddings.
Equations
- f.prodMap g = { toContMDiffMap := (f.toContMDiffMap.comp ContMDiffMap.fst).prodMk (g.toContMDiffMap.comp ContMDiffMap.snd), isSmoothEmbedding_toFun := ⋯ }
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.prodMap_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{F' : Type u_5}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{G : Type u_8}
[TopologicalSpace G]
{G' : Type u_9}
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{I' : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{M' : Type u_12}
[TopologicalSpace M']
[ChartedSpace G M']
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
[IsManifold I' n M']
[IsManifold J' n N']
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' n M' N')
(x : M × M')
:
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_prodMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{F' : Type u_5}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{G : Type u_8}
[TopologicalSpace G]
{G' : Type u_9}
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{I' : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{M' : Type u_12}
[TopologicalSpace M']
[ChartedSpace G M']
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
[IsManifold I' n M']
[IsManifold J' n N']
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' n M' N')
:
@[simp]
theorem
TauCeti.SmoothEmbedding.toContinuousMap_prodMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{F' : Type u_5}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{H : Type u_6}
[TopologicalSpace H]
{H' : Type u_7}
[TopologicalSpace H']
{G : Type u_8}
[TopologicalSpace G]
{G' : Type u_9}
[TopologicalSpace G']
{I : ModelWithCorners 𝕜 E H}
{J : ModelWithCorners 𝕜 E' H'}
{I' : ModelWithCorners 𝕜 F G}
{J' : ModelWithCorners 𝕜 F' G'}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_11}
[TopologicalSpace N]
[ChartedSpace H' N]
{M' : Type u_12}
[TopologicalSpace M']
[ChartedSpace G M']
{N' : Type u_13}
[TopologicalSpace N']
[ChartedSpace G' N']
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
[IsManifold I' n M']
[IsManifold J' n N']
(f : SmoothEmbedding I J n M N)
(g : SmoothEmbedding I' J' n M' N')
:
The underlying continuous map of a product of smooth embeddings is the product of the underlying continuous maps.
def
TauCeti.SmoothEmbedding.sumInl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{M₂ : Type u_14}
[TopologicalSpace M₂]
[ChartedSpace H M₂]
[IsManifold I n M]
[IsManifold I n M₂]
:
SmoothEmbedding I I n M (M ⊕ M₂)
The left coproduct inclusion as a bundled smooth embedding.
Equations
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.sumInl_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{M₂ : Type u_14}
[TopologicalSpace M₂]
[ChartedSpace H M₂]
[IsManifold I n M]
[IsManifold I n M₂]
(x : M)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_sumInl
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{M₂ : Type u_14}
[TopologicalSpace M₂]
[ChartedSpace H M₂]
[IsManifold I n M]
[IsManifold I n M₂]
:
def
TauCeti.SmoothEmbedding.sumInr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{M₂ : Type u_14}
[TopologicalSpace M₂]
[ChartedSpace H M₂]
[IsManifold I n M]
[IsManifold I n M₂]
:
SmoothEmbedding I I n M₂ (M ⊕ M₂)
The right coproduct inclusion as a bundled smooth embedding.
Equations
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.sumInr_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{M₂ : Type u_14}
[TopologicalSpace M₂]
[ChartedSpace H M₂]
[IsManifold I n M]
[IsManifold I n M₂]
(x : M₂)
:
@[simp]
theorem
TauCeti.SmoothEmbedding.coe_sumInr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_10}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
{M₂ : Type u_14}
[TopologicalSpace M₂]
[ChartedSpace H M₂]
[IsManifold I n M]
[IsManifold I n M₂]
: