# Documentation

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

# Smooth sections #

In this file we define the type ContMDiffSection of n times continuously differentiable sections of a smooth vector bundle over a manifold M and prove that it's a module.

structure ContMDiffSection {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] (F : Type u_11) [] (n : ℕ∞) (V : MType u_12) [] [(x : M) → TopologicalSpace (V x)] [] :
Type (max u_12 u_6)
• toFun : (x : M) → V x
• contMDiff_toFun : ContMDiff I () n fun x =>

Bundled n times continuously differentiable sections of a vector bundle.

Instances For
@[reducible]
def SmoothSection {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] (F : Type u_11) [] (V : MType u_12) [] [(x : M) → TopologicalSpace (V x)] [] :
Type (max u_12 u_6)

Bundled smooth sections of a vector bundle.

Instances For
Instances For
instance ContMDiffSection.instFunLikeContMDiffSection {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → TopologicalSpace (V x)] [] :
@[simp]
theorem ContMDiffSection.coeFn_mk {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → TopologicalSpace (V x)] [] (s : (x : M) → V x) (hs : ContMDiff I () n fun x => { proj := x, snd := s x }) :
{ toFun := s, contMDiff_toFun := hs } = s
theorem ContMDiffSection.contMDiff {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → TopologicalSpace (V x)] [] (s : ContMDiffSection I F n V) :
ContMDiff I () n fun x => Bundle.TotalSpace.mk' F x (s x)
theorem ContMDiffSection.smooth {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {V : MType u_12} [] [(x : M) → TopologicalSpace (V x)] [] (s : ) :
Smooth I () fun x => Bundle.TotalSpace.mk' F x (s x)
theorem ContMDiffSection.mdifferentiable' {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → TopologicalSpace (V x)] [] (s : ContMDiffSection I F n V) (hn : 1 n) :
MDifferentiable I () fun x => Bundle.TotalSpace.mk' F x (s x)
theorem ContMDiffSection.mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {V : MType u_12} [] [(x : M) → TopologicalSpace (V x)] [] (s : ) :
MDifferentiable I () fun x => Bundle.TotalSpace.mk' F x (s x)
theorem ContMDiffSection.mdifferentiableAt {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {V : MType u_12} [] [(x : M) → TopologicalSpace (V x)] [] (s : ) {x : M} :
MDifferentiableAt I () (fun x => Bundle.TotalSpace.mk' F x (s x)) x
theorem ContMDiffSection.coe_inj {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → TopologicalSpace (V x)] [] ⦃s : ContMDiffSection I F n V ⦃t : ContMDiffSection I F n V (h : s = t) :
s = t
theorem ContMDiffSection.coe_injective {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → TopologicalSpace (V x)] [] :
Function.Injective FunLike.coe
theorem ContMDiffSection.ext {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → TopologicalSpace (V x)] [] {s : ContMDiffSection I F n V} {t : ContMDiffSection I F n V} (h : ∀ (x : M), s x = t x) :
s = t
instance ContMDiffSection.instAdd {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
@[simp]
theorem ContMDiffSection.coe_add {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) (t : ContMDiffSection I F n V) :
↑(s + t) = s + t
instance ContMDiffSection.instSub {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
@[simp]
theorem ContMDiffSection.coe_sub {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) (t : ContMDiffSection I F n V) :
↑(s - t) = s - t
instance ContMDiffSection.instZero {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
instance ContMDiffSection.inhabited {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
@[simp]
theorem ContMDiffSection.coe_zero {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
0 = 0
instance ContMDiffSection.instSMul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
SMul 𝕜 (ContMDiffSection I F n V)
@[simp]
theorem ContMDiffSection.coe_smul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] (r : 𝕜) (s : ContMDiffSection I F n V) :
↑(r s) = r s
instance ContMDiffSection.instNeg {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
@[simp]
theorem ContMDiffSection.coe_neg {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) :
↑(-s) = -s
instance ContMDiffSection.instNSMul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
@[simp]
theorem ContMDiffSection.coe_nsmul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) (k : ) :
↑(k s) = k s
instance ContMDiffSection.instZSMul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
@[simp]
theorem ContMDiffSection.coe_zsmul {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V) (z : ) :
↑(z s) = z s
instance ContMDiffSection.instAddCommGroup {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
def ContMDiffSection.coeAddHom {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] (I : ) {M : Type u_6} [] [] (F : Type u_11) [] (n : ℕ∞) (V : MType u_12) [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
ContMDiffSection I F n V →+ (x : M) → V x

The additive morphism from smooth sections to dependent maps.

Instances For
instance ContMDiffSection.instModule {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_4} [] {I : } {M : Type u_6} [] [] {F : Type u_11} [] {n : ℕ∞} {V : MType u_12} [] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [] [VectorBundle 𝕜 F V] :
Module 𝕜 (ContMDiffSection I F n V)