English
Pullback can be pulled back along a map, yielding a new trivialization on the pullback bundle.
Русский
Pullback может быть подтянут вдоль отображения, образуя новую тривиализацию над тягой pullback.
LaTeX
$$$\mathrm{pullback}(e,f)$$$
Lean4
/-- A fiber bundle trivialization can be pulled back to a trivialization on the pullback bundle. -/
@[simps]
noncomputable def pullback (e : Trivialization F (π F E)) (f : K) : Trivialization F (π F((f : B' → B) *ᵖ E))
where
toFun z := (z.proj, (e (Pullback.lift f z)).2)
invFun y := @TotalSpace.mk _ F (f *ᵖ E) y.1 (e.symm (f y.1) y.2)
source := Pullback.lift f ⁻¹' e.source
baseSet := f ⁻¹' e.baseSet
target := (f ⁻¹' e.baseSet) ×ˢ univ
map_source' x
h := by
simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj] at h
simp_rw [prodMk_mem_set_prod_eq, mem_univ, and_true, mem_preimage, h]
map_target' y
h := by
rw [mem_prod, mem_preimage] at h
simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj, h.1]
left_inv' x
h := by
simp_rw [mem_preimage, e.mem_source, Pullback.lift_proj] at h
simp_rw [Pullback.lift, e.symm_apply_apply_mk h]
right_inv' x
h := by
simp_rw [mem_prod, mem_preimage, mem_univ, and_true] at h
simp_rw [Pullback.lift_mk, e.apply_mk_symm h]
open_source := by
simp_rw [e.source_eq, ← preimage_comp]
exact e.open_baseSet.preimage ((map_continuous f).comp <| Pullback.continuous_proj F E f)
open_target := ((map_continuous f).isOpen_preimage _ e.open_baseSet).prod isOpen_univ
open_baseSet := (map_continuous f).isOpen_preimage _ e.open_baseSet
continuousOn_toFun :=
(Pullback.continuous_proj F E f).continuousOn.prodMk
(continuous_snd.comp_continuousOn <| e.continuousOn.comp (Pullback.continuous_lift F E f).continuousOn Subset.rfl)
continuousOn_invFun :=
by
simp_rw [(inducing_pullbackTotalSpaceEmbedding F E f).continuousOn_iff, Function.comp_def,
pullbackTotalSpaceEmbedding]
exact
continuousOn_fst.prodMk
(e.continuousOn_symm.comp ((map_continuous f).prodMap continuous_id).continuousOn Subset.rfl)
source_eq := by
rw [e.source_eq]
rfl
target_eq := rfl
proj_toFun _ _ := rfl
