English
If two trivializations e and e' have disjoint base sets, then there is a trivialization on the union base set that agrees with e on e.baseSet and with e' on e'.baseSet.
Русский
Если две тривиализации e и e' имеют непересекающиеся базовые множества, существует тривиализация на объединённом базовом множестве, которая совпадает с e на e.baseSet и с e' на e'.baseSet.
LaTeX
$$$\exists\,\tilde{e} = e\sqcup_H e'\;:\;\text{Trivialization } F\ proj,\quad \operatorname{baseSet}(\tilde{e})=e.baseSet\cup e'.baseSet,\quad \tilde{e}|_{e.baseSet}=e,\quad \tilde{e}|_{e'.baseSet}=e'.$$
Lean4
/-- Given two bundle trivializations `e`, `e'` over disjoint sets, `e.disjoint_union e' H` is the
bundle trivialization over the union of the base sets that agrees with `e` and `e'` over their
base sets. -/
noncomputable def disjointUnion (e e' : Trivialization F proj) (H : Disjoint e.baseSet e'.baseSet) :
Trivialization F proj
where
toOpenPartialHomeomorph :=
e.toOpenPartialHomeomorph.disjointUnion e'.toOpenPartialHomeomorph
(by
rw [e.source_eq, e'.source_eq]
exact H.preimage _)
(by
rw [e.target_eq, e'.target_eq, disjoint_iff_inf_le]
intro x hx
exact H.le_bot ⟨hx.1.1, hx.2.1⟩)
baseSet := e.baseSet ∪ e'.baseSet
open_baseSet := IsOpen.union e.open_baseSet e'.open_baseSet
source_eq := congr_arg₂ (· ∪ ·) e.source_eq e'.source_eq
target_eq := (congr_arg₂ (· ∪ ·) e.target_eq e'.target_eq).trans union_prod.symm
proj_toFun := by
rintro p (hp | hp')
· change (e.source.piecewise e e' p).1 = proj p
rw [piecewise_eq_of_mem, e.coe_fst] <;> exact hp
· change (e.source.piecewise e e' p).1 = proj p
rw [piecewise_eq_of_notMem, e'.coe_fst hp']
simp only [source_eq] at hp' ⊢
exact fun h => H.le_bot ⟨h, hp'⟩
