Smooth bundled map #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define the type cont_mdiff_map of n times continuously differentiable
bundled maps.
def
cont_mdiff_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
(I : model_with_corners 𝕜 E H)
(I' : model_with_corners 𝕜 E' H')
(M : Type u_6)
[topological_space M]
[charted_space H M]
(M' : Type u_7)
[topological_space M']
[charted_space H' M']
(n : ℕ∞) :
Type (max u_6 u_7)
Bundled n times continuously differentiable maps.
Equations
- cont_mdiff_map I I' M M' n = {f // cont_mdiff I I' n f}
Instances for cont_mdiff_map
- cont_mdiff_map.fun_like
- cont_mdiff_map.continuous_map.has_coe
- cont_mdiff_map.continuous_map_class
- cont_mdiff_map.inhabited
- continuous_linear_map.has_coe_to_cont_mdiff_map
- diffeomorph.cont_mdiff_map.has_coe
- smooth_map.has_mul
- smooth_map.has_add
- smooth_map.has_one
- smooth_map.has_zero
- smooth_map.semigroup
- smooth_map.add_semigroup
- smooth_map.monoid
- smooth_map.add_monoid
- smooth_map.comm_monoid
- smooth_map.add_comm_monoid
- smooth_map.group
- smooth_map.add_group
- smooth_map.comm_group
- smooth_map.add_comm_group
- smooth_map.semiring
- smooth_map.ring
- smooth_map.comm_ring
- smooth_map.has_smul
- smooth_map.module
- smooth_map.algebra
- smooth_map.has_smul'
- smooth_map.module'
- smooth_functions_algebra
- smooth_functions_tower
- pointed_smooth_map.cont_mdiff_map.algebra
- pointed_smooth_map.cont_mdiff_map.is_scalar_tower
@[reducible]
def
smooth_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
(I : model_with_corners 𝕜 E H)
(I' : model_with_corners 𝕜 E' H')
(M : Type u_6)
[topological_space M]
[charted_space H M]
(M' : Type u_7)
[topological_space M']
[charted_space H' M'] :
Type (max u_6 u_7)
Bundled smooth maps.
Equations
- smooth_map I I' M M' = cont_mdiff_map I I' M M' ⊤
@[protected, instance]
def
cont_mdiff_map.fun_like
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞} :
fun_like (cont_mdiff_map I I' M M' n) M (λ (_x : M), M')
Equations
- cont_mdiff_map.fun_like = {coe := subtype.val (λ (f : M → M'), cont_mdiff I I' n f), coe_injective' := _}
@[protected]
theorem
cont_mdiff_map.cont_mdiff
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
(f : cont_mdiff_map I I' M M' n) :
cont_mdiff I I' n ⇑f
@[protected]
theorem
cont_mdiff_map.smooth
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : cont_mdiff_map I I' M M' ⊤) :
@[protected, instance]
def
cont_mdiff_map.continuous_map.has_coe
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞} :
has_coe (cont_mdiff_map I I' M M' n) C(M, M')
Equations
- cont_mdiff_map.continuous_map.has_coe = {coe := λ (f : cont_mdiff_map I I' M M' n), {to_fun := ⇑f, continuous_to_fun := _}}
@[simp]
theorem
cont_mdiff_map.coe_fn_mk
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
(f : M → M')
(hf : cont_mdiff I I' n f) :
theorem
cont_mdiff_map.coe_inj
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
⦃f g : cont_mdiff_map I I' M M' n⦄
(h : ⇑f = ⇑g) :
f = g
@[ext]
theorem
cont_mdiff_map.ext
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
{f g : cont_mdiff_map I I' M M' n}
(h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
@[protected, instance]
def
cont_mdiff_map.continuous_map_class
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞} :
continuous_map_class (cont_mdiff_map I I' M M' n) M M'
Equations
- cont_mdiff_map.continuous_map_class = {coe := λ (f : cont_mdiff_map I I' M M' n), ⇑f, coe_injective' := _, map_continuous := _}
def
cont_mdiff_map.id
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_4}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{n : ℕ∞} :
cont_mdiff_map I I M M n
The identity as a smooth map.
Equations
- cont_mdiff_map.id = ⟨id M, _⟩
def
cont_mdiff_map.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{n : ℕ∞}
(f : cont_mdiff_map I' I'' M' M'' n)
(g : cont_mdiff_map I I' M M' n) :
cont_mdiff_map I I'' M M'' n
The composition of smooth maps, as a smooth map.
@[simp]
theorem
cont_mdiff_map.comp_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{E'' : Type u_8}
[normed_add_comm_group E'']
[normed_space 𝕜 E'']
{H'' : Type u_9}
[topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type u_10}
[topological_space M'']
[charted_space H'' M'']
{n : ℕ∞}
(f : cont_mdiff_map I' I'' M' M'' n)
(g : cont_mdiff_map I I' M M' n)
(x : M) :
@[protected, instance]
def
cont_mdiff_map.inhabited
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
[inhabited M'] :
inhabited (cont_mdiff_map I I' M M' n)
Equations
- cont_mdiff_map.inhabited = {default := ⟨λ (_x : M), inhabited.default, _⟩}
def
cont_mdiff_map.const
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞}
(y : M') :
cont_mdiff_map I I' M M' n
Constant map as a smooth map
Equations
- cont_mdiff_map.const y = ⟨λ (x : M), y, _⟩
def
cont_mdiff_map.fst
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞} :
cont_mdiff_map (I.prod I') I (M × M') M n
The first projection of a product, as a smooth map.
Equations
- cont_mdiff_map.fst = ⟨prod.fst M', _⟩
def
cont_mdiff_map.snd
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{n : ℕ∞} :
cont_mdiff_map (I.prod I') I' (M × M') M' n
The second projection of a product, as a smooth map.
Equations
- cont_mdiff_map.snd = ⟨prod.snd M', _⟩
def
cont_mdiff_map.prod_mk
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H : Type u_4}
[topological_space H]
{H' : Type u_5}
[topological_space H']
{I : model_with_corners 𝕜 E H}
{I' : model_with_corners 𝕜 E' H'}
{M : Type u_6}
[topological_space M]
[charted_space H M]
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{F : Type u_11}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_12}
[topological_space G]
{J : model_with_corners 𝕜 F G}
{N : Type u_13}
[topological_space N]
[charted_space G N]
{n : ℕ∞}
(f : cont_mdiff_map J I N M n)
(g : cont_mdiff_map J I' N M' n) :
cont_mdiff_map J (I.prod I') N (M × M') n
Given two smooth maps f and g, this is the smooth map x ↦ (f x, g x).
@[protected, instance]
def
continuous_linear_map.has_coe_to_cont_mdiff_map
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{E' : Type u_3}
[normed_add_comm_group E']
[normed_space 𝕜 E']
(n : ℕ∞) :
has_coe (E →L[𝕜] E') (cont_mdiff_map (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' n)
Equations
- continuous_linear_map.has_coe_to_cont_mdiff_map n = {coe := λ (f : E →L[𝕜] E'), ⟨f.to_linear_map.to_fun, _⟩}