From f8d5c649eae0f7cd7693c6a1d3f2f4f98fa058e1 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 25 May 2022 09:48:16 +0000 Subject: [PATCH] feat(topology/vector_bundle): use trivialization.symm to simplify the product of vector bundles (#14361) --- src/topology/vector_bundle.lean | 111 +++++++++----------------------- 1 file changed, 30 insertions(+), 81 deletions(-) diff --git a/src/topology/vector_bundle.lean b/src/topology/vector_bundle.lean index 50781a530bec3..7e6af956784d7 100644 --- a/src/topology/vector_bundle.lean +++ b/src/topology/vector_bundle.lean @@ -169,9 +169,9 @@ by rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)] /-- A pretrivialization for a topological vector bundle defines linear equivalences between the fibers and the model space. -/ -def linear_equiv_at (e : pretrivialization R F E) (b : B) - (hb : b ∈ e.base_set) : E b ≃ₗ[R] F := -{ to_fun := λ y, (e ⟨b, y⟩).2, +@[simps] def linear_equiv_at (e : pretrivialization R F E) (b : B) (hb : b ∈ e.base_set) : + E b ≃ₗ[R] F := +{ to_fun := λ y, (e (total_space_mk E b y)).2, inv_fun := e.symm b, left_inv := e.symm_apply_apply_mk hb, right_inv := λ v, by simp_rw [e.apply_mk_symm hb v], @@ -393,9 +393,9 @@ namespace trivialization /-- In a topological vector bundle, a trivialization in the fiber (which is a priori only linear) is in fact a continuous linear equiv between the fibers and the model fiber. -/ -def continuous_linear_equiv_at (e : trivialization R F E) (b : B) +@[simps apply symm_apply] def continuous_linear_equiv_at (e : trivialization R F E) (b : B) (hb : b ∈ e.base_set) : E b ≃L[R] F := -{ to_fun := λ y, (e ⟨b, y⟩).2, +{ to_fun := λ y, (e (total_space_mk E b y)).2, inv_fun := e.symm b, continuous_to_fun := continuous_snd.comp (e.to_local_homeomorph.continuous_on.comp_continuous (total_space_mk_inducing R F E b).continuous (λ x, e.mem_source.mpr hb)), @@ -406,9 +406,6 @@ def continuous_linear_equiv_at (e : trivialization R F E) (b : B) end, .. e.to_pretrivialization.linear_equiv_at b hb } -@[simp] lemma continuous_linear_equiv_at_apply (e : trivialization R F E) (b : B) - (hb : b ∈ e.base_set) (y : E b) : e.continuous_linear_equiv_at b hb y = (e ⟨b, y⟩).2 := rfl - @[simp] lemma continuous_linear_equiv_at_apply' (e : trivialization R F E) (x : total_space E) (hx : x ∈ e.source) : e.continuous_linear_equiv_at (proj E x) (e.mem_source.1 hx) x.2 = (e x).2 := by { cases x, refl } @@ -902,18 +899,18 @@ variables (E₁ : B → Type*) (E₂ : B → Type*) variables [topological_space (total_space E₁)] [topological_space (total_space E₂)] /-- Equip the total space of the fibrewise product of two topological vector bundles `E₁`, `E₂` with -the induced topology from the diagonal embedding into `(total_space E₁) × (total_space E₂)`. -/ +the induced topology from the diagonal embedding into `total_space E₁ × total_space E₂`. -/ instance prod.topological_space : topological_space (total_space (E₁ ×ᵇ E₂)) := topological_space.induced (λ p, ((⟨p.1, p.2.1⟩ : total_space E₁), (⟨p.1, p.2.2⟩ : total_space E₂))) - (by apply_instance : topological_space ((total_space E₁) × (total_space E₂))) + (by apply_instance : topological_space (total_space E₁ × total_space E₂)) /-- The diagonal map from the total space of the fibrewise product of two topological vector bundles -`E₁`, `E₂` into `(total_space E₁) × (total_space E₂)` is `inducing`. -/ +`E₁`, `E₂` into `total_space E₁ × total_space E₂` is `inducing`. -/ lemma prod.inducing_diag : inducing (λ p, (⟨p.1, p.2.1⟩, ⟨p.1, p.2.2⟩) : - total_space (E₁ ×ᵇ E₂) → (total_space E₁) × (total_space E₂)) := + total_space (E₁ ×ᵇ E₂) → total_space E₁ × total_space E₂) := ⟨rfl⟩ end defs @@ -965,48 +962,21 @@ end variables (e₁ e₂) -variables [Π x : B, topological_space (E₁ x)] [Π x : B, topological_space (E₂ x)] - [topological_vector_bundle R F₁ E₁] [topological_vector_bundle R F₂ E₂] - /-- Given trivializations `e₁`, `e₂` for vector bundles `E₁`, `E₂` over a base `B`, the inverse function for the construction `topological_vector_bundle.trivialization.prod`, the induced trivialization for the direct sum of `E₁` and `E₂`. -/ def prod.inv_fun' (p : B × (F₁ × F₂)) : total_space (E₁ ×ᵇ E₂) := -begin - obtain ⟨x, w₁, w₂⟩ := p, - refine ⟨x, _, _⟩, - { by_cases h : x ∈ e₁.base_set, - { exact (e₁.continuous_linear_equiv_at x h).symm w₁ }, - { exact 0 } }, - { by_cases h : x ∈ e₂.base_set, - { exact (e₂.continuous_linear_equiv_at x h).symm w₂ }, - { exact 0 } }, -end +⟨p.1, e₁.symm p.1 p.2.1, e₂.symm p.1 p.2.2⟩ variables {e₁ e₂} -lemma prod.inv_fun'_apply {x : B} (hx₁ : x ∈ e₁.base_set) (hx₂ : x ∈ e₂.base_set) - (w₁ : F₁) (w₂ : F₂) : - prod.inv_fun' e₁ e₂ ⟨x, w₁, w₂⟩ - = ⟨x, ((e₁.continuous_linear_equiv_at x hx₁).symm w₁, - (e₂.continuous_linear_equiv_at x hx₂).symm w₂)⟩ := -begin - dsimp [prod.inv_fun'], - rw [dif_pos, dif_pos], -end - lemma prod.left_inv {x : total_space (E₁ ×ᵇ E₂)} (h : x ∈ proj (E₁ ×ᵇ E₂) ⁻¹' (e₁.base_set ∩ e₂.base_set)) : prod.inv_fun' e₁ e₂ (prod.to_fun' e₁ e₂ x) = x := begin obtain ⟨x, v₁, v₂⟩ := x, - simp only [prod.to_fun', prod.inv_fun', sigma.mk.inj_iff, true_and, eq_self_iff_true, - prod.mk.inj_iff, heq_iff_eq], - split, - { rw [dif_pos, ← e₁.continuous_linear_equiv_at_apply x h.1, - continuous_linear_equiv.symm_apply_apply] }, - { rw [dif_pos, ← e₂.continuous_linear_equiv_at_apply x h.2, - continuous_linear_equiv.symm_apply_apply] }, + obtain ⟨h₁ : x ∈ e₁.base_set, h₂ : x ∈ e₂.base_set⟩ := h, + simp only [prod.to_fun', prod.inv_fun', symm_apply_apply_mk, h₁, h₂] end lemma prod.right_inv {x : B × F₁ × F₂} @@ -1014,46 +984,28 @@ lemma prod.right_inv {x : B × F₁ × F₂} prod.to_fun' e₁ e₂ (prod.inv_fun' e₁ e₂ x) = x := begin obtain ⟨x, w₁, w₂⟩ := x, - obtain ⟨h, -⟩ := h, - dsimp only [prod.to_fun', prod.inv_fun'], - simp only [prod.mk.inj_iff, eq_self_iff_true, true_and], - split, - { rw [dif_pos, ← e₁.continuous_linear_equiv_at_apply x h.1, - continuous_linear_equiv.apply_symm_apply] }, - { rw [dif_pos, ← e₂.continuous_linear_equiv_at_apply x h.2, - continuous_linear_equiv.apply_symm_apply] }, + obtain ⟨⟨h₁ : x ∈ e₁.base_set, h₂ : x ∈ e₂.base_set⟩, -⟩ := h, + simp only [prod.to_fun', prod.inv_fun', apply_mk_symm, h₁, h₂] end lemma prod.continuous_inv_fun : continuous_on (prod.inv_fun' e₁ e₂) ((e₁.base_set ∩ e₂.base_set) ×ˢ (univ : set (F₁ × F₂))) := begin rw (prod.inducing_diag E₁ E₂).continuous_on_iff, - suffices : continuous_on (λ p : B × F₁ × F₂, - (e₁.to_local_homeomorph.symm ⟨p.1, p.2.1⟩, e₂.to_local_homeomorph.symm ⟨p.1, p.2.2⟩)) - ((e₁.base_set ∩ e₂.base_set) ×ˢ (univ : set (F₁ × F₂))), - { refine this.congr _, - rintros ⟨b, v₁, v₂⟩ ⟨⟨h₁, h₂⟩, _⟩, - dsimp at ⊢ h₁ h₂, - rw [prod.inv_fun'_apply h₁ h₂, e₁.symm_apply_eq_mk_continuous_linear_equiv_at_symm b h₁, - e₂.symm_apply_eq_mk_continuous_linear_equiv_at_symm b h₂] }, have H₁ : continuous (λ p : B × F₁ × F₂, ((p.1, p.2.1), (p.1, p.2.2))) := (continuous_id.prod_map continuous_fst).prod_mk (continuous_id.prod_map continuous_snd), - have H₂ := e₁.to_local_homeomorph.symm.continuous_on.prod_map - e₂.to_local_homeomorph.symm.continuous_on, - refine H₂.comp H₁.continuous_on (λ x h, ⟨_, _⟩), - { dsimp, - rw e₁.target_eq, - exact ⟨h.1.1, mem_univ _⟩ }, - { dsimp, - rw e₂.target_eq, - exact ⟨h.1.2, mem_univ _⟩ } + refine (e₁.continuous_on_symm.prod_map e₂.continuous_on_symm).comp H₁.continuous_on _, + exact λ x h, ⟨⟨h.1.1, mem_univ _⟩, ⟨h.1.2, mem_univ _⟩⟩ end variables (e₁ e₂) +variables [Π x : B, topological_space (E₁ x)] [Π x : B, topological_space (E₂ x)] + [topological_vector_bundle R F₁ E₁] [topological_vector_bundle R F₂ E₂] /-- Given trivializations `e₁`, `e₂` for vector bundles `E₁`, `E₂` over a base `B`, the induced trivialization for the direct sum of `E₁` and `E₂`, whose base set is `e₁.base_set ∩ e₂.base_set`. -/ +@[nolint unused_arguments] def prod : trivialization R (F₁ × F₂) (E₁ ×ᵇ E₂) := { to_fun := prod.to_fun' e₁ e₂, inv_fun := prod.inv_fun' e₁ e₂, @@ -1066,7 +1018,7 @@ def prod : trivialization R (F₁ × F₂) (E₁ ×ᵇ E₂) := open_source := begin refine (e₁.open_base_set.inter e₂.open_base_set).preimage _, have : continuous (proj E₁) := continuous_proj R B F₁, - exact this.comp (continuous_fst.comp (prod.inducing_diag E₁ E₂).continuous), + exact this.comp (prod.inducing_diag E₁ E₂).continuous.fst, end, open_target := (e₁.open_base_set.inter e₂.open_base_set).prod is_open_univ, continuous_to_fun := prod.continuous_to_fun, @@ -1093,11 +1045,9 @@ lemma prod_apply {x : B} (hx₁ : x ∈ e₁.base_set) (hx₂ : x ∈ e₂.base_ = ⟨x, e₁.continuous_linear_equiv_at x hx₁ v₁, e₂.continuous_linear_equiv_at x hx₂ v₂⟩ := rfl -lemma prod_symm_apply {x : B} (hx₁ : x ∈ e₁.base_set) (hx₂ : x ∈ e₂.base_set) (w₁ : F₁) (w₂ : F₂) : - (prod e₁ e₂).to_local_equiv.symm (x, (w₁, w₂)) - = ⟨x, ((e₁.continuous_linear_equiv_at x hx₁).symm w₁, - (e₂.continuous_linear_equiv_at x hx₂).symm w₂)⟩ := -prod.inv_fun'_apply hx₁ hx₂ w₁ w₂ +lemma prod_symm_apply (x : B) (w₁ : F₁) (w₂ : F₂) : (prod e₁ e₂).to_local_equiv.symm (x, w₁, w₂) + = ⟨x, e₁.symm x w₁, e₂.symm x w₂⟩ := +rfl end trivialization @@ -1128,7 +1078,7 @@ instance _root_.bundle.prod.topological_vector_bundle : let ε := coord_change he₁ he'₁, let η := coord_change he₂ he'₂, have fact : (s ∩ t) ×ˢ (univ : set $ F₁ × F₂) = - (e₁.base_set ∩ e₂.base_set ∩ (e'₁.base_set ∩ e'₂.base_set)) ×ˢ (univ : set $ F₁ × F₂), + (e₁.base_set ∩ e₂.base_set ∩ (e'₁.base_set ∩ e'₂.base_set)) ×ˢ (univ : set $ F₁ × F₂), by mfld_set_tac, refine ⟨s ∩ t, _, _, λ b, (ε b).prod (η b), _, _⟩, { rw fact, @@ -1139,14 +1089,13 @@ instance _root_.bundle.prod.topological_vector_bundle : have hη := (continuous_on_coord_change he₂ he'₂).mono (inter_subset_right s t), exact hε.prod_map_equivL R hη }, { rintros b ⟨hbs, hbt⟩ ⟨u, v⟩, - have h : (e₁.prod e₂).to_local_homeomorph.symm _ = _ := prod_symm_apply hbs.1 hbt.1 u v, - simp only [ε, η, h, prod_apply hbs.2 hbt.2, - ← comp_continuous_linear_equiv_at_eq_coord_change he₁ he'₁ hbs, + have h : (e₁.prod e₂).to_local_homeomorph.symm _ = _ := prod_symm_apply b u v, + simp_rw [ε, local_equiv.coe_trans, local_homeomorph.coe_coe_symm, local_homeomorph.coe_coe, + function.comp_app, h, η, topological_vector_bundle.trivialization.coe_coe, + prod_apply hbs.2 hbt.2, ← comp_continuous_linear_equiv_at_eq_coord_change he₁ he'₁ hbs, ← comp_continuous_linear_equiv_at_eq_coord_change he₂ he'₂ hbt, - eq_self_iff_true, function.comp_app, local_equiv.coe_trans, local_homeomorph.coe_coe, - local_homeomorph.coe_coe_symm, prod.mk.inj_iff, - topological_vector_bundle.trivialization.coe_coe, true_and, - continuous_linear_equiv.prod_apply, continuous_linear_equiv.trans_apply] }, + continuous_linear_equiv.prod_apply, continuous_linear_equiv.trans_apply, + continuous_linear_equiv_at_symm_apply] }, end } variables {R F₁ E₁ F₂ E₂}