Derivation bundle #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define the derivations at a point of a manifold on the algebra of smooth fuctions. Moreover, we define the differential of a function in terms of derivations.
The content of this file is not meant to be regarded as an alternative definition to the current tangent bundle but rather as a purely algebraic theory that provides a purely algebraic definition of the Lie algebra for a Lie group.
@[protected, instance]
def
smooth_functions_algebra
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_4)
[topological_space M]
[charted_space H M] :
algebra 𝕜 (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤)
Equations
@[protected, instance]
def
smooth_functions_tower
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_4)
[topological_space M]
[charted_space H M] :
is_scalar_tower 𝕜 (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤) (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤)
@[nolint]
def
pointed_smooth_map
(𝕜 : Type u_1)
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
(M : Type u_4)
[topological_space M]
[charted_space H M]
(n : ℕ∞)
(x : M) :
Type (max u_4 u_1)
Type synonym, introduced to put a different has_smul action on C^n⟮I, M; 𝕜⟯
which is defined as f • r = f(x) * r.
Equations
- pointed_smooth_map 𝕜 I M n x = cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 n
Instances for pointed_smooth_map
@[protected, instance]
def
pointed_smooth_map.fun_like
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M} :
fun_like (pointed_smooth_map 𝕜 I M ⊤ x) M (λ (_x : M), 𝕜)
Equations
@[protected, instance]
def
pointed_smooth_map.comm_ring
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M} :
comm_ring (pointed_smooth_map 𝕜 I M ⊤ x)
Equations
@[protected, instance]
def
pointed_smooth_map.algebra
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M} :
algebra 𝕜 (pointed_smooth_map 𝕜 I M ⊤ x)
Equations
@[protected, instance]
def
pointed_smooth_map.inhabited
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M} :
inhabited (pointed_smooth_map 𝕜 I M ⊤ x)
Equations
- pointed_smooth_map.inhabited I = {default := 0}
@[protected, instance]
def
pointed_smooth_map.cont_mdiff_map.algebra
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M} :
algebra (pointed_smooth_map 𝕜 I M ⊤ x) (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤)
Equations
@[protected, instance]
def
pointed_smooth_map.cont_mdiff_map.is_scalar_tower
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M} :
is_scalar_tower 𝕜 (pointed_smooth_map 𝕜 I M ⊤ x) (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤)
@[protected, instance]
def
pointed_smooth_map.eval_algebra
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{x : M} :
algebra (pointed_smooth_map 𝕜 I M ⊤ x) 𝕜
smooth_map.eval_ring_hom gives rise to an algebra structure of C^∞⟮I, M; 𝕜⟯ on 𝕜.
Equations
def
pointed_smooth_map.eval
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
(x : M) :
cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤ →ₐ[pointed_smooth_map 𝕜 I M ⊤ x] 𝕜
With the eval_algebra algebra structure evaluation is actually an algebra morphism.
Equations
- pointed_smooth_map.eval x = algebra.of_id (pointed_smooth_map 𝕜 I M ⊤ x) 𝕜
theorem
pointed_smooth_map.smul_def
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
(x : M)
(f : pointed_smooth_map 𝕜 I M ⊤ x)
(k : 𝕜) :
@[protected, instance]
def
pointed_smooth_map.is_scalar_tower
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
(x : M) :
is_scalar_tower 𝕜 (pointed_smooth_map 𝕜 I M ⊤ x) 𝕜
@[reducible]
def
point_derivation
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
(x : M) :
Type (max u_4 u_1)
The derivations at a point of a manifold. Some regard this as a possible definition of the tangent space
Equations
- point_derivation I x = derivation 𝕜 (pointed_smooth_map 𝕜 I M ⊤ x) 𝕜
def
smooth_function.eval_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
(I : model_with_corners 𝕜 E H)
{M : Type u_4}
[topological_space M]
[charted_space H M]
(x : M) :
cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤ →ₗ[pointed_smooth_map 𝕜 I M ⊤ x] 𝕜
Evaluation at a point gives rise to a C^∞⟮I, M; 𝕜⟯-linear map between C^∞⟮I, M; 𝕜⟯ and 𝕜.
Equations
def
derivation.eval_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
(x : M) :
derivation 𝕜 (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤) (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤) →ₗ[𝕜] point_derivation I x
The evaluation at a point as a linear map.
Equations
theorem
derivation.eval_at_apply
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
(X : derivation 𝕜 (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤) (cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤))
(f : cont_mdiff_map I (model_with_corners_self 𝕜 𝕜) M 𝕜 ⊤)
(x : M) :
def
hfdifferential
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : cont_mdiff_map I I' M M' ⊤}
{x : M}
{y : M'}
(h : ⇑f x = y) :
point_derivation I x →ₗ[𝕜] point_derivation I' y
The heterogeneous differential as a linear map. Instead of taking a function as an argument this
differential takes h : f x = y. It is particularly handy to deal with situations where the points
on where it has to be evaluated are equal but not definitionally equal.
Equations
- hfdifferential h = {to_fun := λ (v : point_derivation I x), derivation.mk' {to_fun := λ (g : pointed_smooth_map 𝕜 I' M' ⊤ y), ⇑v (cont_mdiff_map.comp g f), map_add' := _, map_smul' := _} _, map_add' := _, map_smul' := _}
def
fdifferential
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : cont_mdiff_map I I' M M' ⊤)
(x : M) :
point_derivation I x →ₗ[𝕜] point_derivation I' (⇑f x)
The homogeneous differential as a linear map.
Equations
- fdifferential f x = hfdifferential _
@[simp]
theorem
apply_fdifferential
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
(f : cont_mdiff_map I I' M M' ⊤)
{x : M}
(v : point_derivation I x)
(g : cont_mdiff_map I' (model_with_corners_self 𝕜 𝕜) M' 𝕜 ⊤) :
@[simp]
theorem
apply_hfdifferential
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{M' : Type u_7}
[topological_space M']
[charted_space H' M']
{f : cont_mdiff_map I I' M M' ⊤}
{x : M}
{y : M'}
(h : ⇑f x = y)
(v : point_derivation I x)
(g : cont_mdiff_map I' (model_with_corners_self 𝕜 𝕜) M' 𝕜 ⊤) :
⇑(⇑(hfdifferential h) v) g = ⇑(⇑(fdifferential f x) v) g
@[simp]
theorem
fdifferential_comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{H : Type u_3}
[topological_space H]
{I : model_with_corners 𝕜 E H}
{M : Type u_4}
[topological_space M]
[charted_space H M]
{E' : Type u_5}
[normed_add_comm_group E']
[normed_space 𝕜 E']
{H' : Type u_6}
[topological_space H']
{I' : model_with_corners 𝕜 E' H'}
{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'']
(g : cont_mdiff_map I' I'' M' M'' ⊤)
(f : cont_mdiff_map I I' M M' ⊤)
(x : M) :
fdifferential (g.comp f) x = (fdifferential g (⇑f x)).comp (fdifferential f x)