Skip to content

Commit

Permalink
feat(topology/topological_fiber_bundle): topological fiber bundle ove…
Browse files Browse the repository at this point in the history 
…r `[a, b]` is trivial (#6555)
  • Loading branch information
@urkud
urkud committed Apr 14, 2021
1 parent b3eabc1 commit f12575e
Showing 1 changed file with 271 additions and 3 deletions.
274 changes: 271 additions & 3 deletions src/topology/topological_fiber_bundle.lean
View file
Expand Up @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel
-/
import topology.local_homeomorph
import topology.algebra.ordered

/-!
# Fiber bundles
Expand Down Expand Up @@ -139,7 +140,7 @@ Fiber bundle, topological bundle, vector bundle, local trivialization, structure
variables {ι : Type*} {B : Type*} {F : Type*}

open topological_space filter set
open_locale topological_space
open_locale topological_space classical

/-! ### General definition of topological fiber bundles -/

Expand Down Expand Up @@ -204,6 +205,18 @@ lemma bundle_trivialization.coe_fst' (e : bundle_trivialization F proj) {x : Z}
(ex : proj x ∈ e.base_set) : (e x).1 = proj x :=
e.coe_fst (e.mem_source.2 ex)

lemma bundle_trivialization.mk_proj_snd (e : bundle_trivialization F proj) {x : Z}
(ex : x ∈ e.source) : (proj x, (e x).2) = e x :=
prod.ext (e.coe_fst ex).symm rfl

lemma bundle_trivialization.mk_proj_snd' (e : bundle_trivialization F proj) {x : Z}
(ex : proj x ∈ e.base_set) : (proj x, (e x).2) = e x :=
prod.ext (e.coe_fst' ex).symm rfl

protected lemma bundle_trivialization.eq_on (e : bundle_trivialization F proj) :
eq_on (prod.fst ∘ e) proj e.source :=
λ x hx, e.coe_fst hx

lemma bundle_trivialization.proj_symm_apply (e : bundle_trivialization F proj) {x : B × F}
(hx : x ∈ e.target) : proj (e.to_local_homeomorph.symm x) = x.1 :=
begin
Expand Down Expand Up @@ -310,7 +323,100 @@ lemma is_topological_fiber_bundle.comp_homeomorph {Z' : Type*} [topological_spac
λ x, let ⟨e, he⟩ := e x in
⟨e.comp_homeomorph h, by simpa [bundle_trivialization.comp_homeomorph] using he⟩

section induced
namespace bundle_trivialization

/-- If `e` is a `bundle_trivialization` of `proj : Z → B` with fiber `F` and `h` is a homeomorphism
`F ≃ₜ F'`, then `e.trans_fiber_homeomorph h` is the trivialization of `proj` with the fiber `F'`
that sends `p : Z` to `((e p).1, h (e p).2)`. -/
def trans_fiber_homeomorph {F' : Type*} [topological_space F']
(e : bundle_trivialization F proj) (h : F ≃ₜ F') : bundle_trivialization F' proj :=
{ to_local_homeomorph := e.to_local_homeomorph.trans
((homeomorph.refl _).prod_congr h).to_local_homeomorph,
base_set := e.base_set,
open_base_set := e.open_base_set,
source_eq := by simp [e.source_eq],
target_eq := by { ext, simp [e.target_eq] },
proj_to_fun := λ p hp, have p ∈ e.source, by simpa using hp, by simp [this] }

@[simp] lemma trans_fiber_homeomorph_apply {F' : Type*} [topological_space F']
(e : bundle_trivialization F proj) (h : F ≃ₜ F') (x : Z) :
e.trans_fiber_homeomorph h x = ((e x).1, h (e x).2) :=
rfl

/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations. See also
`bundle_trivialization.coord_change_homeomorph` for a version bundled as `F ≃ₜ F`. -/
def coord_change (e₁ e₂ : bundle_trivialization F proj) (b : B) (x : F) : F :=
(e₂ $ e₁.to_local_homeomorph.symm (b, x)).2

lemma mk_coord_change
(e₁ e₂ : bundle_trivialization F proj) {b : B}
(h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) (x : F) :
(b, e₁.coord_change e₂ b x) = e₂ (e₁.to_local_homeomorph.symm (b, x)) :=
begin
refine prod.ext _ rfl,
rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_symm_apply' h₁],
{ rwa [e₁.proj_symm_apply' h₁] },
{ rwa [e₁.proj_symm_apply' h₁] }
end

lemma coord_change_apply_snd
(e₁ e₂ : bundle_trivialization F proj) {p : Z}
(h : proj p ∈ e₁.base_set) :
e₁.coord_change e₂ (proj p) (e₁ p).snd = (e₂ p).snd :=
by rw [coord_change, e₁.symm_apply_mk_proj (e₁.mem_source.2 h)]

lemma coord_change_same_apply
(e : bundle_trivialization F proj) {b : B} (h : b ∈ e.base_set) (x : F) :
e.coord_change e b x = x :=
by rw [bundle_trivialization.coord_change, e.apply_symm_apply' h]

lemma coord_change_same
(e : bundle_trivialization F proj) {b : B} (h : b ∈ e.base_set) :
e.coord_change e b = id :=
funext $ e.coord_change_same_apply h

lemma coord_change_coord_change
(e₁ e₂ e₃ : bundle_trivialization F proj) {b : B}
(h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) (x : F) :
e₂.coord_change e₃ b (e₁.coord_change e₂ b x) = e₁.coord_change e₃ b x :=
begin
rw [bundle_trivialization.coord_change, e₁.mk_coord_change _ h₁ h₂, ← e₂.coe_coe,
e₂.to_local_homeomorph.left_inv, bundle_trivialization.coord_change],
rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]
end

lemma continuous_coord_change (e₁ e₂ : bundle_trivialization F proj) {b : B}
(h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) :
continuous (e₁.coord_change e₂ b) :=
begin
refine continuous_snd.comp (e₂.to_local_homeomorph.continuous_on.comp_continuous
(e₁.to_local_homeomorph.continuous_on_symm.comp_continuous _ _) _),
{ exact continuous_const.prod_mk continuous_id },
{ exact λ x, e₁.mem_target.2 h₁ },
{ intro x,
rwa [e₂.mem_source, e₁.proj_symm_apply' h₁] }
end

/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations,
as a homeomorphism. -/
def coord_change_homeomorph
(e₁ e₂ : bundle_trivialization F proj) {b : B} (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) :
F ≃ₜ F :=
{ to_fun := e₁.coord_change e₂ b,
inv_fun := e₂.coord_change e₁ b,
left_inv := λ x, by simp only [*, coord_change_coord_change, coord_change_same_apply],
right_inv := λ x, by simp only [*, coord_change_coord_change, coord_change_same_apply],
continuous_to_fun := e₁.continuous_coord_change e₂ h₁ h₂,
continuous_inv_fun := e₂.continuous_coord_change e₁ h₂ h₁ }

@[simp] lemma coord_change_homeomorph_coe
(e₁ e₂ : bundle_trivialization F proj) {b : B} (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) :
⇑(e₁.coord_change_homeomorph e₂ h₁ h₂) = e₁.coord_change e₂ b :=
rfl

end bundle_trivialization

section comap

open_locale classical

Expand Down Expand Up @@ -372,7 +478,169 @@ lemma is_topological_fiber_bundle.comap (h : is_topological_fiber_bundle F proj)
is_topological_fiber_bundle F (λ x : {p : B' × Z | f p.1 = proj p.2}, (x : B' × Z).1) :=
λ x, let ⟨e, he⟩ := h (f x) in ⟨e.comap f hf x he, he⟩

end induced
end comap

lemma bundle_trivialization.is_image_preimage_prod (e : bundle_trivialization F proj) (s : set B) :
e.to_local_homeomorph.is_image (proj ⁻¹' s) (s.prod univ) :=
λ x hx, by simp [e.coe_fst', hx]

/-- Restrict a `bundle_trivialization` to an open set in the base. `-/
def bundle_trivialization.restr_open (e : bundle_trivialization F proj) (s : set B)
(hs : is_open s) :
bundle_trivialization F proj :=
{ to_local_homeomorph := ((e.is_image_preimage_prod s).symm.restr
(is_open_inter e.open_target (hs.prod is_open_univ))).symm,
base_set := e.base_set ∩ s,
open_base_set := is_open_inter e.open_base_set hs,
source_eq := by simp [e.source_eq],
target_eq := by simp [e.target_eq, prod_univ],
proj_to_fun := λ p hp, e.proj_to_fun p hp.1 }

section piecewise

lemma bundle_trivialization.frontier_preimage (e : bundle_trivialization F proj) (s : set B) :
e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.base_set ∩ frontier s) :=
by rw [← (e.is_image_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
(e.is_image_preimage_prod _).preimage_eq, e.source_eq, preimage_inter]

/-- Given two bundle trivializations `e`, `e'` of `proj : Z → B` and a set `s : set B` such that
the base sets of `e` and `e'` intersect `frontier s` on the same set and `e p = e' p` whenever
`proj p ∈ e.base_set ∩ frontier s`, `e.piecewise e' s Hs Heq` is the bundle trivialization over
`set.ite s e.base_set e'.base_set` that is equal to `e` on `proj ⁻¹ s` and is equal to `e'`
otherwise. -/
noncomputable def bundle_trivialization.piecewise (e e' : bundle_trivialization F proj) (s : set B)
(Hs : e.base_set ∩ frontier s = e'.base_set ∩ frontier s)
(Heq : eq_on e e' $ proj ⁻¹' (e.base_set ∩ frontier s)) :
bundle_trivialization F proj :=
{ to_local_homeomorph := e.to_local_homeomorph.piecewise e'.to_local_homeomorph
(proj ⁻¹' s) (s.prod univ) (e.is_image_preimage_prod s) (e'.is_image_preimage_prod s)
(by rw [e.frontier_preimage, e'.frontier_preimage, Hs])
(by rwa e.frontier_preimage),
base_set := s.ite e.base_set e'.base_set,
open_base_set := e.open_base_set.ite e'.open_base_set Hs,
source_eq := by simp [e.source_eq, e'.source_eq],
target_eq := by simp [e.target_eq, e'.target_eq, prod_univ],
proj_to_fun := by rintro p (⟨he, hs⟩|⟨he, hs⟩); simp * }

/-- Given two bundle trivializations `e`, `e'` of a topological fiber bundle `proj : Z → B`
over a linearly ordered base `B` and a point `a ∈ e.base_set ∩ e'.base_set` such that
`e` equals `e'` on `proj ⁻¹' {a}`, `e.piecewise_le_of_eq e' a He He' Heq` is the bundle
trivialization over `set.ite (Iic a) e.base_set e'.base_set` that is equal to `e` on points `p`
such that `proj p ≤ a` and is equal to `e'` otherwise. -/
noncomputable def bundle_trivialization.piecewise_le_of_eq [linear_order B] [order_topology B]
(e e' : bundle_trivialization F proj) (a : B) (He : a ∈ e.base_set) (He' : a ∈ e'.base_set)
(Heq : ∀ p, proj p = a → e p = e' p) :
bundle_trivialization F proj :=
e.piecewise e' (Iic a)
(set.ext $ λ x, and.congr_left_iff.2 $ λ hx,
by simp [He, He', mem_singleton_iff.1 (frontier_Iic_subset _ hx)])
(λ p hp, Heq p $ frontier_Iic_subset _ hp.2)

/-- Given two bundle trivializations `e`, `e'` of a topological fiber bundle `proj : Z → B` over a
linearly ordered base `B` and a point `a ∈ e.base_set ∩ e'.base_set`, `e.piecewise_le e' a He He'`
is the bundle trivialization over `set.ite (Iic a) e.base_set e'.base_set` that is equal to `e` on
points `p` such that `proj p ≤ a` and is equal to `((e' p).1, h (e' p).2)` otherwise, where
`h = `e'.coord_change_homeomorph e _ _` is the homeomorphism of the fiber such that
`h (e' p).2 = (e p).2` whenever `e p = a`. -/
noncomputable def bundle_trivialization.piecewise_le [linear_order B] [order_topology B]
(e e' : bundle_trivialization F proj) (a : B) (He : a ∈ e.base_set) (He' : a ∈ e'.base_set) :
bundle_trivialization F proj :=
e.piecewise_le_of_eq (e'.trans_fiber_homeomorph (e'.coord_change_homeomorph e He' He))
a He He' $ by { unfreezingI {rintro p rfl },
ext1,
{ simp [e.coe_fst', e'.coe_fst', *] },
{ simp [e'.coord_change_apply_snd, *] } }

/-- 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 bundle_trivialization.disjoint_union (e e' : bundle_trivialization F proj)
(H : disjoint e.base_set e'.base_set) :
bundle_trivialization F proj :=
{ to_local_homeomorph := e.to_local_homeomorph.disjoint_union e'.to_local_homeomorph
(λ x hx, by { rw [e.source_eq, e'.source_eq] at hx, exact H hx })
(λ x hx, by { rw [e.target_eq, e'.target_eq] at hx, exact H ⟨hx.1.1, hx.2.1⟩ }),
base_set := e.base_set ∪ e'.base_set,
open_base_set := is_open_union e.open_base_set e'.open_base_set,
source_eq := congr_arg2 (∪) e.source_eq e'.source_eq,
target_eq := (congr_arg2 (∪) e.target_eq e'.target_eq).trans union_prod.symm,
proj_to_fun :=
begin
rintro p (hp|hp'),
{ show (e.source.piecewise e e' p).1 = proj p,
rw [piecewise_eq_of_mem, e.coe_fst]; exact hp },
{ show (e.source.piecewise e e' p).1 = proj p,
rw [piecewise_eq_of_not_mem, e'.coe_fst hp'],
simp only [e.source_eq, e'.source_eq] at hp' ⊢,
exact λ h, H ⟨h, hp'⟩ }
end }

/-- If `h` is a topological fiber bundle over a conditionally complete linear order,
then it is trivial over any closed interval. -/
lemma is_topological_fiber_bundle.exists_trivialization_Icc_subset
[conditionally_complete_linear_order B] [order_topology B]
(h : is_topological_fiber_bundle F proj) (a b : B) :
∃ e : bundle_trivialization F proj, Icc a b ⊆ e.base_set :=
begin
classical,
obtain ⟨ea, hea⟩ : ∃ ea : bundle_trivialization F proj, a ∈ ea.base_set := h a,
-- If `a < b`, then `[a, b] = ∅`, and the statement is trivial
cases le_or_lt a b with hab hab; [skip, exact ⟨ea, by simp *⟩],
/- Let `s` be the set of points `x ∈ [a, b]` such that `proj` is trivializable over `[a, x]`.
We need to show that `b ∈ s`. Let `c = Sup s`. We will show that `c ∈ s` and `c = b`. -/
set s : set B := {x ∈ Icc a b | ∃ e : bundle_trivialization F proj, Icc a x ⊆ e.base_set},
have ha : a ∈ s, from ⟨left_mem_Icc.2 hab, ea, by simp [hea]⟩,
have sne : s.nonempty := ⟨a, ha⟩,
have hsb : b ∈ upper_bounds s, from λ x hx, hx.1.2,
have sbd : bdd_above s := ⟨b, hsb⟩,
set c := Sup s,
have hsc : is_lub s c, from is_lub_cSup sne sbd,
have hc : c ∈ Icc a b, from ⟨hsc.1 ha, hsc.2 hsb⟩,
obtain ⟨-, ec : bundle_trivialization F proj, hec : Icc a c ⊆ ec.base_set⟩ : c ∈ s,
{ cases hc.1.eq_or_lt with heq hlt, { rwa ← heq },
refine ⟨hc, _⟩,
/- In order to show that `c ∈ s`, consider a trivialization `ec` of `proj` over a neighborhood
of `c`. Its base set includes `(c', c]` for some `c' ∈ [a, c)`. -/
rcases h c with ⟨ec, hc⟩,
obtain ⟨c', hc', hc'e⟩ : ∃ c' ∈ Ico a c, Ioc c' c ⊆ ec.base_set :=
(mem_nhds_within_Iic_iff_exists_mem_Ico_Ioc_subset hlt).1
(mem_nhds_within_of_mem_nhds $ mem_nhds_sets ec.open_base_set hc),
/- Since `c' < c = Sup s`, there exists `d ∈ s ∩ (c', c]`. Let `ead` be a trivialization of
`proj` over `[a, d]`. Then we can glue `ead` and `ec` into a trivialization over `[a, c]`. -/
obtain ⟨d, ⟨hdab, ead, had⟩, hd⟩ : ∃ d ∈ s, d ∈ Ioc c' c := hsc.exists_between hc'.2,
refine ⟨ead.piecewise_le ec d (had ⟨hdab.1, le_rfl⟩) (hc'e hd), subset_ite.2 _⟩,
refine ⟨λ x hx, had ⟨hx.1.1, hx.2⟩, λ x hx, hc'e ⟨hd.1.trans (not_le.1 hx.2), hx.1.2⟩⟩ },
/- So, `c ∈ s`. Let `ec` be a trivialization of `proj` over `[a, c]`. If `c = b`, then we are
done. Otherwise we show that `proj` can be trivialized over a larger interval `[a, d]`,
`d ∈ (c, b]`, hence `c` is not an upper bound of `s`. -/
cases hc.2.eq_or_lt with heq hlt, { exact ⟨ec, heq ▸ hec⟩ },
suffices : ∃ (d ∈ Ioc c b) (e : bundle_trivialization F proj), Icc a d ⊆ e.base_set,
{ rcases this with ⟨d, hdcb, hd⟩,
exact ((hsc.1 ⟨⟨hc.1.trans hdcb.1.le, hdcb.2⟩, hd⟩).not_lt hdcb.1).elim },
/- Since the base set of `ec` is open, it includes `[c, d)` (hence, `[a, d)`) for some
`d ∈ (c, b]`. -/
obtain ⟨d, hdcb, hd⟩ : ∃ d ∈ Ioc c b, Ico c d ⊆ ec.base_set :=
(mem_nhds_within_Ici_iff_exists_mem_Ioc_Ico_subset hlt).1
(mem_nhds_within_of_mem_nhds $ mem_nhds_sets ec.open_base_set (hec ⟨hc.1, le_rfl⟩)),
have had : Ico a d ⊆ ec.base_set,
from subset.trans Ico_subset_Icc_union_Ico (union_subset hec hd),
by_cases he : disjoint (Iio d) (Ioi c),
{ /- If `(c, d) = ∅`, then let `ed` be a trivialization of `proj` over a neighborhood of `d`.
Then the disjoint union of `ec` restricted to `(-∞, d)` and `ed` restricted to `(c, ∞)` is
a trivialization over `[a, d]`. -/
rcases h d with ⟨ed, hed⟩,
refine ⟨d, hdcb, (ec.restr_open (Iio d) is_open_Iio).disjoint_union
(ed.restr_open (Ioi c) is_open_Ioi) (he.mono (inter_subset_right _ _)
(inter_subset_right _ _)), λ x hx, _⟩,
rcases hx.2.eq_or_lt with rfl|hxd,
exacts [or.inr ⟨hed, hdcb.1⟩, or.inl ⟨had ⟨hx.1, hxd⟩, hxd⟩] },
{ /- If `(c, d)` is nonempty, then take `d' ∈ (c, d)`. Since the base set of `ec` includes
`[a, d)`, it includes `[a, d'] ⊆ [a, d)` as well. -/
rw [disjoint_left] at he, push_neg at he, rcases he with ⟨d', hdd' : d' < d, hd'c⟩,
exact ⟨d', ⟨hd'c, hdd'.le.trans hdcb.2⟩, ec, subset.trans (Icc_subset_Ico_right hdd') had⟩ }
end

end piecewise

end topological_fiber_bundle

Expand Down

0 comments on commit f12575e

Please sign in to comment.