English
There is a local homeomorphism (trivialization change) between two indexed trivializations i and j on their common baseSet, given by the coordinate change.
Русский
Существует локальная гомеоморфия между тривиализациями с индексами i и j на их общей базе, задаваемая координатной перестановкой.
LaTeX
$$trivChange(i,j) : OpenPartialHomeomorph((B×F),(B×F))$$
Lean4
/-- Local homeomorphism version of the trivialization change. -/
def trivChange (i j : ι) : OpenPartialHomeomorph (B × F) (B × F)
where
source := (Z.baseSet i ∩ Z.baseSet j) ×ˢ univ
target := (Z.baseSet i ∩ Z.baseSet j) ×ˢ univ
toFun p := ⟨p.1, Z.coordChange i j p.1 p.2⟩
invFun p := ⟨p.1, Z.coordChange j i p.1 p.2⟩
map_source' p hp := by simpa using hp
map_target' p hp := by simpa using hp
left_inv' := by
rintro ⟨x, v⟩ hx
simp only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ] at hx
dsimp only
rw [coordChange_comp, Z.coordChange_self]
exacts [hx.1, ⟨⟨hx.1, hx.2⟩, hx.1⟩]
right_inv' := by
rintro ⟨x, v⟩ hx
simp only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ] at hx
dsimp only
rw [Z.coordChange_comp, Z.coordChange_self]
· exact hx.2
· simp [hx]
open_source := ((Z.isOpen_baseSet i).inter (Z.isOpen_baseSet j)).prod isOpen_univ
open_target := ((Z.isOpen_baseSet i).inter (Z.isOpen_baseSet j)).prod isOpen_univ
continuousOn_toFun := continuous_fst.continuousOn.prodMk (Z.continuousOn_coordChange i j)
continuousOn_invFun := by simpa [inter_comm] using continuous_fst.continuousOn.prodMk (Z.continuousOn_coordChange j i)
