English
For each index i, there is a partial bijection between the portion of the total space lying over baseSet i and baseSet i × F, given by projecting to the base and applying the coordinate-change on the fiber. The inverse uses the opposite coordinate-change. This exhibits the fiber bundle as locally a product near baseSet i.
Русский
Для каждого индекса i существует частичное биекционирование между частью общего пространства, лежащей над baseSet i, и baseSet i × F, задаваемое проекцией на основание и координатной перестройкой на волокне. Обратное отображение использует обратную координатную перестройку. Это демонстрирует, что биндель-фибра локально удовлетворяет структуру произведения над baseSet i.
LaTeX
$$$\\text{For each index } i, \\text{ there is a partial equivalence } \\mathcal{L}_i: \\mathrm{TotalSpace} \\dashrightarrow B \\times F, \\\\ \\text{with } \\operatorname{source}(\\mathcal{L}_i)=\\mathrm{proj}^{-1}(\\mathrm{baseSet}\\,i),\\ \\operatorname{target}(\\mathcal{L}_i)=\\mathrm{baseSet}\\,i \\times \\mathbb{F}, \\\\ \\mathcal{L}_i(p)=(p.1, \\mathrm{coordChange}(\\mathrm{indexAt}(p.1), i, p.1, p.2)).$$$
Lean4
/-- Associate to a trivialization index `i : ι` the corresponding trivialization, i.e., a bijection
between `proj ⁻¹ (baseSet i)` and `baseSet i × F`. As the fiber above `x` is `F` but read in the
chart with index `index_at x`, the trivialization in the fiber above x is by definition the
coordinate change from i to `index_at x`, so it depends on `x`.
The local trivialization will ultimately be an open partial homeomorphism. For now, we only
introduce the partial equivalence version, denoted with a prime.
In further developments, avoid this auxiliary version, and use `Z.local_triv` instead. -/
def localTrivAsPartialEquiv (i : ι) : PartialEquiv Z.TotalSpace (B × F)
where
source := Z.proj ⁻¹' Z.baseSet i
target := Z.baseSet i ×ˢ univ
invFun p := ⟨p.1, Z.coordChange i (Z.indexAt p.1) p.1 p.2⟩
toFun p := ⟨p.1, Z.coordChange (Z.indexAt p.1) i p.1 p.2⟩
map_source' p hp := by simpa only [Set.mem_preimage, and_true, Set.mem_univ, Set.prodMk_mem_set_prod_eq] using hp
map_target' p hp := by simpa only [Set.mem_preimage, and_true, Set.mem_univ, Set.mem_prod] using hp
left_inv' := by
rintro ⟨x, v⟩ hx
replace hx : x ∈ Z.baseSet i := hx
dsimp only
rw [Z.coordChange_comp, Z.coordChange_self] <;> apply_rules [mem_baseSet_at, mem_inter]
right_inv' := by
rintro ⟨x, v⟩ hx
simp only [prodMk_mem_set_prod_eq, and_true, mem_univ] at hx
dsimp only
rw [Z.coordChange_comp, Z.coordChange_self]
exacts [hx, ⟨⟨hx, Z.mem_baseSet_at _⟩, hx⟩]
