English
The application of the continuousLinearMap pretrivialization to a fiber element is given by composing the coordinatewise maps with the appropriate linear maps on the base fibres.
Русский
Применение претривиализации continuousLinearMap к элементу фибры задаётся композицией координатных отображений с линейными отображениями на фибрах основания.
LaTeX
$$$ (continuousLinearMap σ e_1 e_2) p = \\langle p.1, (e_2.continuousLinearMapAt 𝕜_2 p.1) \\circ (p.2 \\circ (e_1.symmL 𝕜_1 p.1)) \\rangle $$$
Lean4
theorem continuousOn_continuousLinearMapCoordChange [RingHomIsometric σ] [VectorBundle 𝕜₁ F₁ E₁] [VectorBundle 𝕜₂ F₂ E₂]
[MemTrivializationAtlas e₁] [MemTrivializationAtlas e₁'] [MemTrivializationAtlas e₂] [MemTrivializationAtlas e₂'] :
ContinuousOn (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂')
(e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)) :=
by
have h₁ := (compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)).continuous
have h₂ := (ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)).continuous
have h₃ := continuousOn_coordChange 𝕜₁ e₁' e₁
have h₄ := continuousOn_coordChange 𝕜₂ e₂ e₂'
refine ((h₁.comp_continuousOn (h₄.mono ?_)).clm_comp (h₂.comp_continuousOn (h₃.mono ?_))).congr ?_
· mfld_set_tac
· mfld_set_tac
· intro b _
ext L v
dsimp [continuousLinearMapCoordChange]
