The vector bundle of continuous alternating multilinear maps #
We define the topological vector bundle of continuous alternating maps between two vector bundles over the same base.
Consider topological vector bundles with fibers E₁ x, E₂ x, x : B,
with model fibers F₁ and F₂, and a finite index type ι.
If F₁ and F₂ are normed spaces over a nontrivially normed field 𝕜,
then we define a vector bundle with fiber E₁ x [⋀^ι]→L[𝕜] E₂ x
with model fiber F₁ [⋀^ι]→L[𝕜] F₂.
The topology on the total space is constructed from the trivializations for E₁ and E₂ and the
norm-topology on the model fiber F₁ [⋀^ι]→L[𝕜] F₂ using the VectorPrebundle construction.
Continuous alternating map between fibers written in coordinates #
noncomputable def
ContinuousAlternatingMap.inCoordinates
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
{B₁ : Type u_3}
(F₁ : Type u_4)
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B₁ → Type u_5}
[(x : B₁) → AddCommGroup (E₁ x)]
[(x : B₁) → Module 𝕜 (E₁ x)]
[TopologicalSpace B₁]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B₁) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{B₂ : Type u_6}
(F₂ : Type u_7)
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B₂ → Type u_8}
[(x : B₂) → AddCommGroup (E₂ x)]
[(x : B₂) → Module 𝕜 (E₂ x)]
[TopologicalSpace B₂]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[(x : B₂) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
(x₀ x : B₁)
(y₀ y : B₂)
(ϕ : E₁ x [⋀^ι]→L[𝕜] E₂ y)
:
When ϕ is a continuous alternating map
between the fibers E₁ x and E₂ y of two vector bundles E and E',
ContinuousAlternatingMap.inCoordinates F E F' E' x₀ x y₀ y ϕ
is a coordinate change of this continuous linear map
w.r.t. the chart around x₀ and the chart around y₀.
It is defined by composing ϕ with appropriate coordinate changes
given by the vector bundles E₁ and E₂.
We use the operations Bundle.Trivialization.continuousLinearMapAt and
Bundle.Trivialization.symmL in the definition, instead of
Bundle.Trivialization.continuousLinearEquivAt, so that
ContinuousAlternatingMap.inCoordinates is defined everywhere.
See also ContinuousAlternatingMap.inCoordinates_eq.
This is the (second component of the) underlying function
of a trivialization of the bundle of continuous alternating maps,
see FiberBundle.trivializationAt_continuousAlternatingMap_apply.
However, note that ContinuousAlternatingMap.inCoordinates is
defined even when x and y live in different base sets.
Therefore, it is also convenient when working with the bundle of continuous alternating maps
between pulled back bundles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ContinuousAlternatingMap.inCoordinates_eq
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
{B₁ : Type u_3}
(F₁ : Type u_4)
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B₁ → Type u_5}
[(x : B₁) → AddCommGroup (E₁ x)]
[(x : B₁) → Module 𝕜 (E₁ x)]
[TopologicalSpace B₁]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B₁) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{B₂ : Type u_6}
(F₂ : Type u_7)
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B₂ → Type u_8}
[(x : B₂) → AddCommGroup (E₂ x)]
[(x : B₂) → Module 𝕜 (E₂ x)]
[TopologicalSpace B₂]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[(x : B₂) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
{x₀ x : B₁}
{y₀ y : B₂}
{ϕ : E₁ x [⋀^ι]→L[𝕜] E₂ y}
(hx : x ∈ (trivializationAt F₁ E₁ x₀).baseSet)
(hy : y ∈ (trivializationAt F₂ E₂ y₀).baseSet)
:
inCoordinates F₁ F₂ x₀ x y₀ y ϕ = ((↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₂ E₂ y₀) y hy)).compContinuousAlternatingMap
ϕ).compContinuousLinearMap
↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ x₀) x hx).symm
Rewrite ContinuousAlternatingMap.inCoordinates using continuous linear equivalences.
Pretrivialization of the bundle of continuous alternating maps #
noncomputable def
Bundle.Pretrivialization.continuousAlternatingMapCoordChange
(𝕜 : Type u_1)
(ι : Type u_2)
[NontriviallyNormedField 𝕜]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
(e₁ e₁' : Trivialization F₁ TotalSpace.proj)
(e₂ e₂' : Trivialization F₂ TotalSpace.proj)
[Trivialization.IsLinear 𝕜 e₁]
[Trivialization.IsLinear 𝕜 e₁']
[Trivialization.IsLinear 𝕜 e₂]
[Trivialization.IsLinear 𝕜 e₂']
(b : B)
:
Assume eᵢ and eᵢ' are trivializations of the bundles Eᵢ over base B with fiber Fᵢ
(i ∈ {1,2}), then Pretrivialization.continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂'
is the coordinate change function between the two induced (pre)trivializations
Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂
and Pretrivialization.continuousAlternatingMap 𝕜 ι e₁' e₂'
of the bundle of continuous alternating maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Bundle.Pretrivialization.continuousOn_continuousAlternatingMapCoordChange
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
{e₁ e₁' : Trivialization F₁ TotalSpace.proj}
{e₂ e₂' : Trivialization F₂ TotalSpace.proj}
[Finite ι]
[VectorBundle 𝕜 F₁ E₁]
[VectorBundle 𝕜 F₂ E₂]
[MemTrivializationAtlas e₁]
[MemTrivializationAtlas e₁']
[MemTrivializationAtlas e₂]
[MemTrivializationAtlas e₂']
:
ContinuousOn (continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂')
(e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
noncomputable def
Bundle.Pretrivialization.continuousAlternatingMap
(𝕜 : Type u_1)
(ι : Type u_2)
[NontriviallyNormedField 𝕜]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
(e₁ : Trivialization F₁ TotalSpace.proj)
(e₂ : Trivialization F₂ TotalSpace.proj)
[Trivialization.IsLinear 𝕜 e₁]
[Trivialization.IsLinear 𝕜 e₂]
:
Pretrivialization (F₁ [⋀^ι]→L[𝕜] F₂) TotalSpace.proj
Given trivializations e₁, e₂ for vector bundles E₁, E₂ over a base B,
Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂ is the induced pretrivialization for the
continuous σ-semilinear maps from E₁ to E₂. That is, the map which will later become a
trivialization, after the bundle of continuous semilinear maps is equipped with the right
topological vector bundle structure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
Bundle.Pretrivialization.continuousAlternatingMap.isLinear
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
{e₁ : Trivialization F₁ TotalSpace.proj}
{e₂ : Trivialization F₂ TotalSpace.proj}
[Trivialization.IsLinear 𝕜 e₁]
[Trivialization.IsLinear 𝕜 e₂]
[∀ (x : B), ContinuousAdd (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
:
Pretrivialization.IsLinear 𝕜 (continuousAlternatingMap 𝕜 ι e₁ e₂)
theorem
Bundle.Pretrivialization.continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
{e₁ : Trivialization F₁ TotalSpace.proj}
{e₂ : Trivialization F₂ TotalSpace.proj}
[Trivialization.IsLinear 𝕜 e₁]
[Trivialization.IsLinear 𝕜 e₂]
(p : TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) => E₁ x [⋀^ι]→L[𝕜] E₂ x)
:
↑(continuousAlternatingMap 𝕜 ι e₁ e₂) p = (p.proj, (Trivialization.continuousLinearMapAt 𝕜 e₂ p.proj).compContinuousAlternatingMap
(p.snd.compContinuousLinearMap (Trivialization.symmL 𝕜 e₁ p.proj)))
theorem
Bundle.Pretrivialization.continuousAlternatingMap_symm_apply
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
{e₁ : Trivialization F₁ TotalSpace.proj}
{e₂ : Trivialization F₂ TotalSpace.proj}
[Trivialization.IsLinear 𝕜 e₁]
[Trivialization.IsLinear 𝕜 e₂]
(p : B × F₁ [⋀^ι]→L[𝕜] F₂)
:
↑(continuousAlternatingMap 𝕜 ι e₁ e₂).symm p = { proj := p.1,
snd :=
(Trivialization.symmL 𝕜 e₂ p.1).compContinuousAlternatingMap
(p.2.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 e₁ p.1)) }
theorem
Bundle.Pretrivialization.continuousAlternatingMap_symm_apply'
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
{e₁ : Trivialization F₁ TotalSpace.proj}
{e₂ : Trivialization F₂ TotalSpace.proj}
[Trivialization.IsLinear 𝕜 e₁]
[Trivialization.IsLinear 𝕜 e₂]
{b : B}
(hb : b ∈ e₁.baseSet ∩ e₂.baseSet)
(L : F₁ [⋀^ι]→L[𝕜] F₂)
:
(continuousAlternatingMap 𝕜 ι e₁ e₂).symm b L = (Trivialization.symmL 𝕜 e₂ b).compContinuousAlternatingMap
(L.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 e₁ b))
theorem
Bundle.Pretrivialization.continuousAlternatingMapCoordChange_apply
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
{e₁ e₁' : Trivialization F₁ TotalSpace.proj}
{e₂ e₂' : Trivialization F₂ TotalSpace.proj}
[Trivialization.IsLinear 𝕜 e₁]
[Trivialization.IsLinear 𝕜 e₁']
[Trivialization.IsLinear 𝕜 e₂]
[Trivialization.IsLinear 𝕜 e₂']
(b : B)
(hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
(L : F₁ [⋀^ι]→L[𝕜] F₂)
:
(continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂' b) L = (↑(continuousAlternatingMap 𝕜 ι e₁' e₂') { proj := b, snd := (continuousAlternatingMap 𝕜 ι e₁ e₂).symm b L }).2
Vector (pre)bundle structure #
noncomputable def
Bundle.ContinuousAlternatingMap.vectorPrebundle
(𝕜 : Type u_1)
(ι : Type u_2)
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
(F₁ : Type u_4)
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
(E₁ : B → Type u_5)
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
(F₂ : Type u_6)
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
(E₂ : B → Type u_7)
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
:
The continuous σ-semilinear maps between two topological vector bundles form a
VectorPrebundle (this is an auxiliary construction for the
VectorBundle instance, in which the pretrivializations are collated but no topology
on the total space is yet provided).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[implicit_reducible]
noncomputable instance
Bundle.ContinuousAlternatingMap.instTopologicalSpaceTotalSpace
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
:
TopologicalSpace (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) => E₁ x [⋀^ι]→L[𝕜] E₂ x)
Topology on the total space of the continuous σ-semilinear maps between two "normable" vector
bundles over the same base.
@[implicit_reducible]
noncomputable instance
Bundle.ContinuousAlternatingMap.instFiberBundle
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
:
The continuous σ-semilinear maps between two vector bundles form a fiber bundle.
Equations
instance
Bundle.ContinuousAlternatingMap.instVectorBundle
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
:
The continuous σ-semilinear maps between two vector bundles form a vector bundle.
Trivialization of the bundle of continuous alternating maps #
noncomputable def
Bundle.Trivialization.continuousAlternatingMap
(𝕜 : Type u_1)
(ι : Type u_2)
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
(e₁ : Trivialization F₁ TotalSpace.proj)
(e₂ : Trivialization F₂ TotalSpace.proj)
[he₁ : MemTrivializationAtlas e₁]
[he₂ : MemTrivializationAtlas e₂]
:
Trivialization (F₁ [⋀^ι]→L[𝕜] F₂) TotalSpace.proj
Given trivializations e₁, e₂ in the atlas for vector bundles E₁, E₂ over a base B,
the induced trivialization for the continuous σ-semilinear maps from E₁ to E₂,
whose base set is e₁.baseSet ∩ e₂.baseSet.
Equations
Instances For
instance
Bundle.Trivialization.memTrivializationAtlas_continuousAlternatingMap
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
{e₁ : Trivialization F₁ TotalSpace.proj}
{e₂ : Trivialization F₂ TotalSpace.proj}
[he₁ : MemTrivializationAtlas e₁]
[he₂ : MemTrivializationAtlas e₂]
:
MemTrivializationAtlas (continuousAlternatingMap 𝕜 ι e₁ e₂)
@[simp]
theorem
Bundle.Trivialization.baseSet_continuousAlternatingMap
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
{e₁ : Trivialization F₁ TotalSpace.proj}
{e₂ : Trivialization F₂ TotalSpace.proj}
[he₁ : MemTrivializationAtlas e₁]
[he₂ : MemTrivializationAtlas e₂]
:
theorem
Bundle.Trivialization.continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
{e₁ : Trivialization F₁ TotalSpace.proj}
{e₂ : Trivialization F₂ TotalSpace.proj}
[he₁ : MemTrivializationAtlas e₁]
[he₂ : MemTrivializationAtlas e₂]
(p : TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) => E₁ x [⋀^ι]→L[𝕜] E₂ x)
:
↑(continuousAlternatingMap 𝕜 ι e₁ e₂) p = (p.proj, ((continuousLinearMapAt 𝕜 e₂ p.proj).compContinuousAlternatingMap p.snd).compContinuousLinearMap
(symmL 𝕜 e₁ p.proj))
Lemmas about trivializationAt for the bundle of continuous alternating maps #
theorem
FiberBundle.trivializationAt_continuousAlternatingMap
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
(x₀ : B)
:
trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂) (fun (x : B) => E₁ x [⋀^ι]→L[𝕜] E₂ x) x₀ = Bundle.Trivialization.continuousAlternatingMap 𝕜 ι (trivializationAt F₁ E₁ x₀) (trivializationAt F₂ E₂ x₀)
theorem
FiberBundle.trivializationAt_continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
(x₀ : B)
(x : Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) => E₁ x [⋀^ι]→L[𝕜] E₂ x)
:
@[simp]
theorem
FiberBundle.trivializationAt_continuousAlternatingMap_source
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
(x₀ : B)
:
(trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂) (fun (x : B) => E₁ x [⋀^ι]→L[𝕜] E₂ x) x₀).source = Bundle.TotalSpace.proj ⁻¹' ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet)
@[simp]
theorem
FiberBundle.trivializationAt_continuousAlternatingMap_target
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
(x₀ : B)
:
@[simp]
theorem
FiberBundle.trivializationAt_continuousAlternatingMap_baseSet
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
(x₀ : B)
:
(trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂) (fun (x : B) => E₁ x [⋀^ι]→L[𝕜] E₂ x) x₀).baseSet = (trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet
Continuity of maps to the total space of the bundle of continuous alternating maps #
theorem
continuousWithinAt_continuousAlternatingMap_bundle
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
{X : Type u_8}
[TopologicalSpace X]
{s : Set X}
{x₀ : X}
(f : X → Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) => E₁ x [⋀^ι]→L[𝕜] E₂ x)
:
ContinuousWithinAt f s x₀ ↔ ContinuousWithinAt (fun (x : X) => (f x).proj) s x₀ ∧ ContinuousWithinAt
(fun (x : X) =>
ContinuousAlternatingMap.inCoordinates F₁ F₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
s x₀
theorem
continuousAt_continuousAlternatingMap_bundle
{𝕜 : Type u_1}
{ι : Type u_2}
[NontriviallyNormedField 𝕜]
[Fintype ι]
{B : Type u_3}
[TopologicalSpace B]
{F₁ : Type u_4}
[NormedAddCommGroup F₁]
[NormedSpace 𝕜 F₁]
{E₁ : B → Type u_5}
[(x : B) → AddCommGroup (E₁ x)]
[(x : B) → Module 𝕜 (E₁ x)]
[TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
[(x : B) → TopologicalSpace (E₁ x)]
[FiberBundle F₁ E₁]
[VectorBundle 𝕜 F₁ E₁]
{F₂ : Type u_6}
[NormedAddCommGroup F₂]
[NormedSpace 𝕜 F₂]
{E₂ : B → Type u_7}
[(x : B) → AddCommGroup (E₂ x)]
[(x : B) → Module 𝕜 (E₂ x)]
[TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
[(x : B) → TopologicalSpace (E₂ x)]
[FiberBundle F₂ E₂]
[VectorBundle 𝕜 F₂ E₂]
[∀ (x : B), IsTopologicalAddGroup (E₂ x)]
[∀ (x : B), ContinuousSMul 𝕜 (E₂ x)]
{X : Type u_8}
[TopologicalSpace X]
{x₀ : X}
(f : X → Bundle.TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) => E₁ x [⋀^ι]→L[𝕜] E₂ x)
:
ContinuousAt f x₀ ↔ ContinuousAt (fun (x : X) => (f x).proj) x₀ ∧ ContinuousAt
(fun (x : X) =>
ContinuousAlternatingMap.inCoordinates F₁ F₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
x₀