Compactly supported smooth bundle sections #
The support of a bundle section is the closure of its nonzero locus, not the support of its
map into the total space: the zero vector varies with the base point. We define this closed
support on native ContMDiffSection, the submodules of sections supported in a prescribed set,
and their compactly supported submodule. The latter is the directed supremum of the
fixed-compact stages. These are algebraic carriers; no topology on section spaces is installed
here.
Smooth scalar multiplication preserves support and compact support. A compactly supported scalar function localizes even a section without compact support, and a cutoff equal to one on the support acts as the identity. These operations provide the support stages and localizations used in test sections and their inductive-limit topologies.
The smoothness of multiplication is supplied by Mathlib's ContMDiff.smul_section.
def
ContMDiffSection.tsupport
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → Zero (V x)]
(s : ContMDiffSection I F n V)
:
Set M
The closed support of a section: the closure of its nonzero locus in the base.
Instances For
theorem
ContMDiffSection.tsupport_def
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → Zero (V x)]
(s : ContMDiffSection I F n V)
:
The closed support is the closure of the fibrewise nonzero locus.
theorem
ContMDiffSection.isClosed_tsupport
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → Zero (V x)]
(s : ContMDiffSection I F n V)
:
The closed support is closed in the base.
theorem
ContMDiffSection.eq_zero_of_notMem_tsupport
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → Zero (V x)]
(s : ContMDiffSection I F n V)
{x : M}
(hx : x ∉ s.tsupport)
:
A section vanishes off its closed support.
theorem
ContMDiffSection.tsupport_subset_iff
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → Zero (V x)]
{s : ContMDiffSection I F n V}
{K : Set M}
(hK : IsClosed K)
:
Containment of closed support in a closed set is equivalent to vanishing outside it.
@[simp]
theorem
ContMDiffSection.tsupport_zero
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
:
@[simp]
theorem
ContMDiffSection.tsupport_eq_empty_iff
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{s : ContMDiffSection I F n V}
:
theorem
ContMDiffSection.tsupport_add_subset
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(s t : ContMDiffSection I F n V)
:
Addition cannot enlarge support beyond the union of the two supports.
theorem
ContMDiffSection.tsupport_smul_subset
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(c : 𝕜)
(s : ContMDiffSection I F n V)
:
Constant scalar multiplication does not enlarge support.
theorem
ContMDiffSection.tsupport_smul
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(c : 𝕜)
(s : ContMDiffSection I F n V)
(hc : c ≠ 0)
:
Multiplication by a nonzero scalar preserves closed support.
def
ContMDiffSection.supportedIn
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
[TopologicalSpace M]
[ChartedSpace H M]
(F : Type u_5)
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(n : WithTop ℕ∞)
(V : M → Type u_6)
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(K : Set M)
:
Submodule 𝕜 (ContMDiffSection I F n V)
The submodule of native smooth sections whose closed support lies in K.
Instances For
@[simp]
theorem
ContMDiffSection.mem_supportedIn
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{K : Set M}
{s : ContMDiffSection I F n V}
:
theorem
ContMDiffSection.supportedIn_mono
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{K L : Set M}
(h : K ⊆ L)
:
The fixed-support stages increase with the supporting set.
@[simp]
theorem
ContMDiffSection.supportedIn_empty
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
:
@[simp]
theorem
ContMDiffSection.supportedIn_univ
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
:
@[simp]
theorem
ContMDiffSection.supportedIn_inter
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(K L : Set M)
:
def
ContMDiffSection.compactlySupported
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
[TopologicalSpace M]
[ChartedSpace H M]
(F : Type u_5)
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(n : WithTop ℕ∞)
(V : M → Type u_6)
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
:
Submodule 𝕜 (ContMDiffSection I F n V)
The submodule of native smooth sections with compact closed support. Its subtype is the algebraic compact-test carrier, before a test-space topology is chosen.
Instances For
@[simp]
theorem
ContMDiffSection.mem_compactlySupported
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{s : ContMDiffSection I F n V}
:
theorem
ContMDiffSection.supportedIn_le_compactlySupported
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{K : Set M}
(hK : IsCompact K)
:
A section supported in a compact set has compact support.
theorem
ContMDiffSection.mem_compactlySupported_iff
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
{s : ContMDiffSection I F n V}
:
Every compactly supported section belongs to a fixed-compact stage.
theorem
ContMDiffSection.directed_supportedIn
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
:
Directed (fun (x1 x2 : Submodule 𝕜 (ContMDiffSection I F n V)) => x1 ≤ x2) fun (K : TopologicalSpace.Compacts M) =>
supportedIn I F n V ↑K
Fixed-compact support stages form a directed family, using union of compact sets.
theorem
ContMDiffSection.iSup_supportedIn
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
:
The compactly supported submodule is exactly the supremum of its fixed-compact stages. This is an algebraic statement, not an assertion about a final topology.
@[simp]
theorem
ContMDiffSection.compactlySupported_eq_top
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
[CompactSpace M]
:
On a compact base every smooth section has compact support.
def
ContMDiffSection.smulLinearMap
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
:
Multiplication of sections by a smooth scalar function as a linear map.
Instances For
@[instance_reducible]
instance
ContMDiffSection.instSMulContMDiffMap
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
:
SMul (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n) (ContMDiffSection I F n V)
Scalar-valued C^n functions act on C^n sections by pointwise multiplication.
@[simp]
theorem
ContMDiffSection.smul_apply
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
(s : ContMDiffSection I F n V)
(x : M)
:
Evaluation of smooth-function multiplication is fibrewise scalar multiplication.
@[simp]
theorem
ContMDiffSection.smulLinearMap_eq_smul
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
(s : ContMDiffSection I F n V)
:
The scalar-localization linear map agrees with smooth-function multiplication.
theorem
ContMDiffSection.tsupport_smul_function_subset
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
(s : ContMDiffSection I F n V)
:
(f • s).tsupport ⊆ _root_.tsupport ⇑f ∩ s.tsupport
Scalar localization is supported in both the scalar support and the section support.
theorem
ContMDiffSection.smul_function_mem_supportedIn
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
{s : ContMDiffSection I F n V}
{K : Set M}
(hs : s ∈ supportedIn I F n V K)
:
Smooth multiplication preserves each fixed-support stage.
theorem
ContMDiffSection.smul_function_mem_compactlySupported
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
{s : ContMDiffSection I F n V}
(hs : s ∈ compactlySupported I F n V)
:
Smooth multiplication preserves compact support of the section.
theorem
ContMDiffSection.smul_function_mem_compactlySupported_of_hasCompactSupport
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
(hf : HasCompactSupport ⇑f)
(s : ContMDiffSection I F n V)
:
A compactly supported smooth scalar function localizes any smooth section to compact support, even when the original section is not compactly supported.
theorem
ContMDiffSection.smul_function_eq_self
{𝕜 : Type u_1}
{E : Type u_2}
{H : Type u_3}
{M : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
[TopologicalSpace M]
[ChartedSpace H M]
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{V : M → Type u_6}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : M) → TopologicalSpace (V x)]
[FiberBundle F V]
[(x : M) → AddCommGroup (V x)]
[(x : M) → Module 𝕜 (V x)]
[VectorBundle 𝕜 F V]
(f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 n)
(s : ContMDiffSection I F n V)
(hf : Set.EqOn (⇑f) 1 s.tsupport)
:
A cutoff equal to one on a section's closed support leaves that section unchanged.