English
For a fixed i, the local trivialization at a base point b is a bundle trivialization compatible with the core, using indexAt b to select the chart.
Русский
Для фиксированного индекса i локальная тривиализация в точке опорной основы является тривиализацией биндла, согласованной с ядром, с использованием indexAt b для выбора карты.
LaTeX
$$$\\text{localTrivAt}(b) := \\text{localTriv}(\\text{indexAt}(b))$$$
Lean4
/-- Extended version of the local trivialization of a fiber bundle constructed from core,
registering additionally in its type that it is a local bundle trivialization. -/
def localTriv (i : ι) : Trivialization F Z.proj
where
baseSet := Z.baseSet i
open_baseSet := Z.isOpen_baseSet i
source_eq := rfl
target_eq := rfl
proj_toFun p
_ := by
simp only [mfld_simps]
rfl
open_source := Z.open_source' i
open_target := (Z.isOpen_baseSet i).prod isOpen_univ
continuousOn_toFun := by
rw [continuousOn_open_iff (Z.open_source' i)]
intro s s_open
apply TopologicalSpace.GenerateOpen.basic
simp only [exists_prop, mem_iUnion, mem_singleton_iff]
exact ⟨i, s, s_open, rfl⟩
continuousOn_invFun := by
refine continuousOn_isOpen_of_generateFrom fun t ht ↦ ?_
simp only [exists_prop, mem_iUnion, mem_singleton_iff] at ht
obtain ⟨j, s, s_open, ts⟩ :
∃ j s, IsOpen s ∧ t = (localTrivAsPartialEquiv Z j).source ∩ localTrivAsPartialEquiv Z j ⁻¹' s := ht
rw [ts]
simp only [preimage_inter]
let e := Z.localTrivAsPartialEquiv i
let e' := Z.localTrivAsPartialEquiv j
let f := e.symm.trans e'
have : IsOpen (f.source ∩ f ⁻¹' s) :=
by
rw [PartialEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsPartialEquiv_trans i j)]
exact (continuousOn_open_iff (Z.trivChange i j).open_source).1 (Z.trivChange i j).continuousOn _ s_open
convert this using 1
dsimp [f, PartialEquiv.trans_source]
rw [← preimage_comp, inter_assoc]
toPartialEquiv := Z.localTrivAsPartialEquiv i
