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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_11) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ∞) (V : MType u_12) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] :
Type (max u_12 u_6)

Bundled n times continuously differentiable sections of a vector bundle.

Instances For
    @[reducible]
    def SmoothSection {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (F : Type u_11) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : MType u_12) [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F V] :
    Type (max u_12 u_6)

    Bundled smooth sections of a vector bundle.

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