mathlib3documentation

geometry.manifold.vector_bundle.smooth_section

Smooth sections #

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_section of n times continuously differentiable sections of a smooth vector bundle over a manifold M and prove that it's a module.

structure cont_mdiff_section {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ M] (F : Type u_11) [ F] (n : ℕ∞) (V : M Type u_12) [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
Type (max u_12 u_6)
• to_fun : Π (x : M), V x
• cont_mdiff_to_fun : (I.prod F)) n (λ (x : M), {proj := x, snd := self.to_fun x})

Bundled n times continuously differentiable sections of a vector bundle.

Instances for cont_mdiff_section
@[reducible]
def smooth_section {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} (I : H) {M : Type u_6} [ M] (F : Type u_11) [ F] (V : M Type u_12) [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
Type (max u_12 u_6)

Bundled smooth sections of a vector bundle.

Equations
• V = V
@[protected, instance]
def cont_mdiff_section.has_coe_to_fun {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
has_coe_to_fun n V) (λ (s : n V), Π (x : M), V x)
Equations
@[simp]
theorem cont_mdiff_section.coe_fn_mk {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s : Π (x : M), V x) (hs : (I.prod F)) n (λ (x : M), {proj := x, snd := s x})) :
@[protected]
theorem cont_mdiff_section.cont_mdiff {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s : n V) :
(I.prod F)) n (λ (x : M), {proj := x, snd := s x})
@[protected]
theorem cont_mdiff_section.smooth {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s : V) :
(I.prod F)) (λ (x : M), {proj := x, snd := s x})
@[protected]
theorem cont_mdiff_section.mdifferentiable' {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s : n V) (hn : 1 n) :
(I.prod F)) (λ (x : M), {proj := x, snd := s x})
@[protected]
theorem cont_mdiff_section.mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s : V) :
(I.prod F)) (λ (x : M), {proj := x, snd := s x})
@[protected]
theorem cont_mdiff_section.mdifferentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s : V) {x : M} :
(I.prod F)) (λ (x : M), {proj := x, snd := s x}) x
theorem cont_mdiff_section.coe_inj {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] ⦃s t : n V⦄ (h : s = t) :
s = t
theorem cont_mdiff_section.coe_injective {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
@[ext]
theorem cont_mdiff_section.ext {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] {s t : n V} (h : (x : M), s x = t x) :
s = t
@[protected, instance]
def cont_mdiff_section.has_add {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
Equations
@[simp]
theorem cont_mdiff_section.coe_add {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s t : n V) :
(s + t) = s + t
@[protected, instance]
def cont_mdiff_section.has_sub {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
has_sub n V)
Equations
@[simp]
theorem cont_mdiff_section.coe_sub {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s t : n V) :
(s - t) = s - t
@[protected, instance]
def cont_mdiff_section.has_zero {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
Equations
@[protected, instance]
def cont_mdiff_section.inhabited {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
Equations
@[simp]
theorem cont_mdiff_section.coe_zero {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
0 = 0
@[protected, instance]
def cont_mdiff_section.has_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
n V)
Equations
@[simp]
theorem cont_mdiff_section.coe_smul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (r : 𝕜) (s : n V) :
(r s) = r s
@[protected, instance]
def cont_mdiff_section.has_neg {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
has_neg n V)
Equations
@[simp]
theorem cont_mdiff_section.coe_neg {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s : n V) :
@[protected, instance]
def cont_mdiff_section.has_nsmul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
n V)
Equations
@[simp]
theorem cont_mdiff_section.coe_nsmul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s : n V) (k : ) :
(k s) = k s
@[protected, instance]
def cont_mdiff_section.has_zsmul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
n V)
Equations
@[simp]
theorem cont_mdiff_section.coe_zsmul {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] (s : n V) (z : ) :
(z s) = z s
@[protected, instance]
def cont_mdiff_section.add_comm_group {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_4} {I : H} {M : Type u_6} [ M] {F : Type u_11} [ F] {n : ℕ∞} {V : M Type u_12} [Π (x : M), add_comm_group (V x)] [Π (x : M), (V x)] [Π (x : M), topological_space (V x)] [ V] [ V] [ I] :
Equations