English
The base set of the continuous LinearMap pretrivialization equals the intersection of the base sets of the component trivializations.
Русский
База множества непрерывного линейного отображения в предтривиализации равна пересечению базовых множеств компонентных тривиализаций.
LaTeX
$$$ (e_1.continuousLinearMap σ e_2).baseSet = e_1.baseSet \\cap e_2.baseSet $$$
Lean4
/-- Given trivializations `e₁`, `e₂` for vector bundles `E₁`, `E₂` over a base `B`,
`Pretrivialization.continuousLinearMap σ 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. -/
def continuousLinearMap : Pretrivialization (F₁ →SL[σ] F₂) (π (F₁ →SL[σ] F₂)(fun x ↦ E₁ x →SL[σ] E₂ x))
where
toFun p := ⟨p.1, .comp (e₂.continuousLinearMapAt 𝕜₂ p.1) (p.2.comp (e₁.symmL 𝕜₁ p.1))⟩
invFun p := ⟨p.1, .comp (e₂.symmL 𝕜₂ p.1) (p.2.comp (e₁.continuousLinearMapAt 𝕜₁ p.1))⟩
source := Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet)
target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ
map_source' := fun ⟨_, _⟩ h ↦ ⟨h, Set.mem_univ _⟩
map_target' := fun ⟨_, _⟩ h ↦ h.1
left_inv' := fun ⟨x, L⟩ ⟨h₁, h₂⟩ ↦ by
simp only [TotalSpace.mk_inj]
ext (v : E₁ x)
dsimp only [comp_apply]
rw [Trivialization.symmL_continuousLinearMapAt, Trivialization.symmL_continuousLinearMapAt]
exacts [h₁, h₂]
right_inv' := fun ⟨x, f⟩ ⟨⟨h₁, h₂⟩, _⟩ ↦ by
simp only [Prod.mk_right_inj]
ext v
dsimp only [comp_apply]
rw [Trivialization.continuousLinearMapAt_symmL, Trivialization.continuousLinearMapAt_symmL]
exacts [h₁, h₂]
open_target := (e₁.open_baseSet.inter e₂.open_baseSet).prod isOpen_univ
baseSet := e₁.baseSet ∩ e₂.baseSet
open_baseSet := e₁.open_baseSet.inter e₂.open_baseSet
source_eq := rfl
target_eq := rfl
proj_toFun _ _ := rfl
