Preferred trivializations and disjoint unions of trivializations

Near a point v₀ of the total space of a fibre bundle, every point lies over the base set of the preferred trivialization at the base point v₀.proj, so it can be read in that trivialization. A compact subset of the total space lies over finitely many preferred trivializing base sets. An arbitrary family of trivializations over pairwise disjoint open base sets glues to one trivialization over their union, with the same forward and inverse maps on each constituent. The coordinate change between two trivializations is jointly continuous in the base point and the fibre coordinate over the overlap of their base sets, which makes the transition functions of a fibre bundle continuous. Finally, the inverse of a trivialization undoes a coordinate change into it, and over a point of its base set a trivialization is an equivalence between the fibre and the model fibre.

Main results

• Bundle.TotalSpace.eventually_proj_mem_baseSet_trivializationAt: near v₀, points lie over the base set of the trivialization at v₀.proj.
• IsCompact.exists_finset_subset_preimage_biUnion_baseSet: a compact subset of the total space lies over a finite union of preferred trivializing base sets.
• Bundle.Trivialization.continuousOn_coordChange: coordinate changes are jointly continuous over the overlap of the base sets.
• Bundle.Trivialization.symm_mk_coordChange: the inverse of e₂ undoes the coordinate change from e₁ to e₂, landing on the point with the original fibre coordinate in e₁.
• Bundle.Trivialization.equivAt: a trivialization as an equivalence between the fibre over a point of its base set and the model fibre.
• Bundle.Trivialization.isOpen_sheet: for a trivialization with discrete fibre of a map, the sheet of a given index over an open subset of the base set is open.
• Bundle.Trivialization.map_mem_sheet_iff, Bundle.Trivialization.map_symm_eq_of_mem_sheet: a continuous map g over the base, between two trivialized maps with discrete target fibre, carries the sheets of p over a preconnected set onto sheets of q.

theorem Bundle.TotalSpace.eventually_proj_mem_baseSet_trivializationAt {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [(x : B) → TopologicalSpace (E x)] [FiberBundle F E] (v₀ : TotalSpace F E) : ∀ᶠ (v : TotalSpace F E) in nhds v₀, v.proj ∈ (trivializationAt F E v₀.proj).baseSet

Near a point v₀ of the total space, every point lies over the base set of the trivialization at v₀.proj.

theorem Bundle.Trivialization.continuousOn_coordChange {B : Type u_1} {F : Type u_2} {Z : Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace Z] {proj : Z → B} (e₁ e₂ : Trivialization F proj) : ContinuousOn (fun (p : B × F) => e₁.coordChange e₂ p.1 p.2) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ)

The coordinate change (b, v) ↦ e₁.coordChange e₂ b v between two trivializations is jointly continuous over the overlap of their base sets.

theorem IsCompact.exists_finset_subset_preimage_biUnion_baseSet {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [TopologicalSpace F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] {K : Set (Bundle.TotalSpace F E)} (hK : IsCompact K) : ∃ (s : Finset B), K ⊆ Bundle.TotalSpace.proj ⁻¹' ⋃ b ∈ s, (trivializationAt F E b).baseSet

A compact subset of a fibre bundle's total space lies over a finite union of the chosen trivializing base sets.

noncomputable def Bundle.Trivialization.iUnion {ι : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [Nonempty F] [∀ (b : B), Nonempty (E b)] (e : ι → Trivialization F TotalSpace.proj) (hd : Pairwise fun (i j : ι) => Disjoint (e i).baseSet (e j).baseSet) : Trivialization F TotalSpace.proj

Glue an arbitrary family of trivializations with pairwise disjoint base sets. The base set is their union. No local finiteness is required: every base set is open. The nonempty fibers supply arbitrary values outside the source and target, where a trivialization has no meaning.

@[simp]

theorem Bundle.Trivialization.iUnion_baseSet {ι : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [Nonempty F] [∀ (b : B), Nonempty (E b)] (e : ι → Trivialization F TotalSpace.proj) (hd : Pairwise fun (i j : ι) => Disjoint (e i).baseSet (e j).baseSet) : (iUnion e hd).baseSet = ⋃ (i : ι), (e i).baseSet

theorem Bundle.Trivialization.iUnion_apply {ι : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [Nonempty F] [∀ (b : B), Nonempty (E b)] (e : ι → Trivialization F TotalSpace.proj) (hd : Pairwise fun (i j : ι) => Disjoint (e i).baseSet (e j).baseSet) {i : ι} {p : TotalSpace F E} (hp : p.proj ∈ (e i).baseSet) : ↑(iUnion e hd) p = ↑(e i) p

The glued trivialization agrees with a constituent over its base set.

theorem Bundle.Trivialization.iUnion_symm_apply {ι : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [Nonempty F] [∀ (b : B), Nonempty (E b)] (e : ι → Trivialization F TotalSpace.proj) (hd : Pairwise fun (i j : ι) => Disjoint (e i).baseSet (e j).baseSet) {i : ι} {p : B × F} (hp : p.1 ∈ (e i).baseSet) : ↑(iUnion e hd).symm p = ↑(e i).symm p

The inverse of the glued trivialization agrees with the corresponding local inverse.

theorem Bundle.Trivialization.symm_mk_coordChange {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [∀ (x : B), Nonempty (E x)] (e₁ e₂ : Trivialization F TotalSpace.proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) (v : F) : ↑e₂.symm (b, e₁.coordChange e₂ b v) = { proj := b, snd := e₁.symm b v }

Reading a coordinate change from e₁ to e₂ back through e₂ gives the point of the fibre that e₁ sends to the original fibre coordinate.

noncomputable def Bundle.Trivialization.equivAt {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [∀ (x : B), Nonempty (E x)] (e : Trivialization F TotalSpace.proj) (b : B) (hb : b ∈ e.baseSet) : E b ≃ F

The equivalence between the fibre over a point of the base set of a trivialization and the model fibre, given by the trivialization. Compare Bundle.Trivialization.linearEquivAt.

@[simp]

theorem Bundle.Trivialization.equivAt_apply {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [∀ (x : B), Nonempty (E x)] (e : Trivialization F TotalSpace.proj) (b : B) (hb : b ∈ e.baseSet) (p : E b) : (e.equivAt b hb) p = (↑e { proj := b, snd := p }).2

@[simp]

theorem Bundle.Trivialization.equivAt_symm_apply {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (TotalSpace F E)] [∀ (x : B), Nonempty (E x)] (e : Trivialization F TotalSpace.proj) (b : B) (hb : b ∈ e.baseSet) (v : F) : (e.equivAt b hb).symm v = e.symm b v

theorem Bundle.Trivialization.isOpen_sheet {Z : Type u_1} {B : Type u_2} {J : Type u_3} [TopologicalSpace Z] [TopologicalSpace B] [TopologicalSpace J] [DiscreteTopology J] {q : Z → B} (tq : Trivialization J q) {V : Set B} (hVopen : IsOpen V) (hVsub : V ⊆ tq.baseSet) (j : J) : IsOpen {f : Z | q f ∈ V ∧ (↑tq f).2 = j}

For a trivialization tq of a map q with discrete fibre, the sheet of index j over an open set V inside the base set, the set of points lying over V with fibre coordinate j, is open.

theorem Bundle.Trivialization.map_symm_mem_source {E : Type u_1} {F : Type u_2} {X : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} {g : E → F} (hqg : ∀ (e : E), q (g e) = p e) {I : Type u_4} {J : Type u_5} [TopologicalSpace I] [TopologicalSpace J] (tp : Trivialization I p) (tq : Trivialization J q) {V : Set X} (hVsub : V ⊆ tp.baseSet ∩ tq.baseSet) (i : I) {v : X} (hv : v ∈ V) : g (↑tp.symm (v, i)) ∈ tq.source

A point of a sheet of p over a set V inside both base sets is sent by g into the source of tq, so its sheet index for q is defined.

theorem Bundle.Trivialization.snd_map_symm_eq {E : Type u_1} {F : Type u_2} {X : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} {g : E → F} (hg : Continuous g) (hqg : ∀ (e : E), q (g e) = p e) {I : Type u_4} {J : Type u_5} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] (tp : Trivialization I p) (tq : Trivialization J q) {V : Set X} (hVconn : IsPreconnected V) (hVsub : V ⊆ tp.baseSet ∩ tq.baseSet) (i : I) {v x₀ : X} (hv : v ∈ V) (hx₀ : x₀ ∈ V) : (↑tq (g (↑tp.symm (v, i)))).2 = (↑tq (g (↑tp.symm (x₀, i)))).2

The q-sheet index of the image under g of a point of a p-sheet over a preconnected set V is constant along the sheet, because the index is continuous and J is discrete.

theorem Bundle.Trivialization.map_mem_sheet_iff {E : Type u_1} {F : Type u_2} {X : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} {g : E → F} (hg : Continuous g) (hqg : ∀ (e : E), q (g e) = p e) {I : Type u_4} {J : Type u_5} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] (tp : Trivialization I p) (tq : Trivialization J q) {V : Set X} (hVconn : IsPreconnected V) (hVsub : V ⊆ tp.baseSet ∩ tq.baseSet) {x₀ : X} (hx₀ : x₀ ∈ V) (j : J) (e : E) : q (g e) ∈ V ∧ (↑tq (g e)).2 = j ↔ p e ∈ V ∧ (↑tq (g (↑tp.symm (x₀, (↑tp e).2)))).2 = j

Whether g e lies in the q-sheet of index j over V is read off the sheet index of p at e.

theorem Bundle.Trivialization.map_symm_eq_of_mem_sheet {E : Type u_1} {F : Type u_2} {X : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace X] {p : E → X} {q : F → X} {g : E → F} (hg : Continuous g) (hqg : ∀ (e : E), q (g e) = p e) {I : Type u_4} {J : Type u_5} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] (tp : Trivialization I p) (tq : Trivialization J q) {V : Set X} (hVconn : IsPreconnected V) (hVsub : V ⊆ tp.baseSet ∩ tq.baseSet) {x₀ : X} (hx₀ : x₀ ∈ V) {j : J} {w : F} {i : I} (hw : q w ∈ V ∧ (↑tq w).2 = j) (hi : (↑tq (g (↑tp.symm (x₀, i)))).2 = j) : g (↑tp.symm (q w, i)) = w

The point tp.symm (q w, i) of the p-sheet of index i lying over q w is mapped by g to w, provided q w lies in a preconnected set V contained in both base sets and w is in the q-sheet of index j, and the image under g of the point of that p-sheet over the reference base point x₀ ∈ V lies in the same q-sheet of index j.