English
The vector prebundle for continuous linear maps forms a fiber bundle with trivializations given by Pretrivialization.continuousLinearMap σ e1 e2.
Русский
Векторное предрасслоение для непрерывных линейных отображений образует фибробundle с тривиализациями, заданными Pretrivialization.continuousLinearMap σ e1 e2.
LaTeX
$$$ \\text{VectorPrebundle } 𝕜_2 (F_1 \\toSL[σ] F_2) (b \\mapsto E_1(b) \\toSL[σ] E_2(b))$$$
Lean4
/-- 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). -/
def vectorPrebundle : VectorPrebundle 𝕜₂ (F₁ →SL[σ] F₂) (fun x ↦ E₁ x →SL[σ] E₂ x)
where
pretrivializationAtlas :=
{e |
∃ (e₁ : Trivialization F₁ (π F₁ E₁)) (e₂ : Trivialization F₂ (π F₂ E₂)) (_ : MemTrivializationAtlas e₁) (_ :
MemTrivializationAtlas e₂), e = Pretrivialization.continuousLinearMap σ e₁ e₂}
pretrivialization_linear' := by
rintro _ ⟨e₁, he₁, e₂, he₂, rfl⟩
infer_instance
pretrivializationAt x := Pretrivialization.continuousLinearMap σ (trivializationAt F₁ E₁ x) (trivializationAt F₂ E₂ x)
mem_base_pretrivializationAt x := ⟨mem_baseSet_trivializationAt F₁ E₁ x, mem_baseSet_trivializationAt F₂ E₂ x⟩
pretrivialization_mem_atlas
x := ⟨trivializationAt F₁ E₁ x, trivializationAt F₂ E₂ x, inferInstance, inferInstance, rfl⟩
exists_coordChange := by
rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩ _ ⟨e₁', e₂', he₁', he₂', rfl⟩
exact
⟨continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂', continuousOn_continuousLinearMapCoordChange,
continuousLinearMapCoordChange_apply σ e₁ e₁' e₂ e₂'⟩
totalSpaceMk_isInducing := by
intro b
let L₁ : E₁ b ≃L[𝕜₁] F₁ :=
(trivializationAt F₁ E₁ b).continuousLinearEquivAt 𝕜₁ b (mem_baseSet_trivializationAt _ _ _)
let L₂ : E₂ b ≃L[𝕜₂] F₂ :=
(trivializationAt F₂ E₂ b).continuousLinearEquivAt 𝕜₂ b (mem_baseSet_trivializationAt _ _ _)
let φ : (E₁ b →SL[σ] E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
have : IsInducing fun x ↦ (b, φ x) := isInducing_const_prod.mpr φ.toHomeomorph.isInducing
convert this
ext f
dsimp [Pretrivialization.continuousLinearMap_apply]
rw [Trivialization.linearMapAt_def_of_mem _ (mem_baseSet_trivializationAt _ _ _)]
rfl
