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 : M → Type u_12)
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
:
Type (max u_12 u_6)
- toFun : (x : M) → V x
- contMDiff_toFun : ContMDiff I (ModelWithCorners.prod I (modelWithCornersSelf 𝕜 F)) n fun x => Bundle.TotalSpace.mk' F x (ContMDiffSection.toFun s x)
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 : M → Type 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 : M → Type u_12}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
:
FunLike (ContMDiffSection I F n V) M 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 : M → Type 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 : M → Type u_12}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
(s : ContMDiffSection I F n V)
:
ContMDiff I (ModelWithCorners.prod I (modelWithCornersSelf 𝕜 F)) n fun x => Bundle.TotalSpace.mk' F x (↑s x)
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 : M → Type u_12}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
(s : ContMDiffSection I F ⊤ V)
:
Smooth I (ModelWithCorners.prod I (modelWithCornersSelf 𝕜 F)) fun x => Bundle.TotalSpace.mk' F x (↑s x)
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 : M → Type u_12}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
(s : ContMDiffSection I F n V)
(hn : 1 ≤ n)
:
MDifferentiable I (ModelWithCorners.prod I (modelWithCornersSelf 𝕜 F)) fun x => Bundle.TotalSpace.mk' F x (↑s x)
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 : M → Type u_12}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
(s : ContMDiffSection I F ⊤ V)
:
MDifferentiable I (ModelWithCorners.prod I (modelWithCornersSelf 𝕜 F)) fun x => Bundle.TotalSpace.mk' F x (↑s x)
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 : M → Type u_12}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
(s : ContMDiffSection I F ⊤ V)
{x : M}
:
MDifferentiableAt I (ModelWithCorners.prod I (modelWithCornersSelf 𝕜 F)) (fun x => Bundle.TotalSpace.mk' F x (↑s x)) x
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 : M → Type 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 : M → Type 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 : M → Type 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 : M → Type 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]
:
Add (ContMDiffSection I F n 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 : M → Type 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)
:
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 : M → Type 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]
:
Sub (ContMDiffSection I F n 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 : M → Type 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)
:
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 : M → Type 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]
:
Zero (ContMDiffSection I F n 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 : M → Type 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]
:
Inhabited (ContMDiffSection I F n 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 : M → Type 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 : M → Type 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 : M → Type 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)
:
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 : M → Type 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]
:
Neg (ContMDiffSection I F n 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 : M → Type 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)
:
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 : M → Type 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_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 : M → Type 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 : ℕ)
:
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 : M → Type 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_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 : M → Type 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 : ℤ)
:
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 : M → Type 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]
:
AddCommGroup (ContMDiffSection I F n 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 : M → Type 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 : M → Type 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)