feat: port Topology.VectorBundle.Constructions (#4207)

Mathlib.lean

@@ -2360,6 +2360,7 @@ import Mathlib.Topology.UnitInterval
 import Mathlib.Topology.UrysohnsBounded
 import Mathlib.Topology.UrysohnsLemma
 import Mathlib.Topology.VectorBundle.Basic
+import Mathlib.Topology.VectorBundle.Constructions
 import Mathlib.Util.AddRelatedDecl
 import Mathlib.Util.AssertNoSorry
 import Mathlib.Util.AtomM

Mathlib/Topology/VectorBundle/Constructions.lean

@@ -0,0 +1,202 @@
+/-
+Copyright © 2022 Nicolò Cavalleri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nicolò Cavalleri, Sébastien Gouëzel, Heather Macbeth, Floris van Doorn
+
+! This file was ported from Lean 3 source module topology.vector_bundle.constructions
+! leanprover-community/mathlib commit be2c24f56783935652cefffb4bfca7e4b25d167e
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.FiberBundle.Constructions
+import Mathlib.Topology.VectorBundle.Basic
+
+/-!
+# Standard constructions on vector bundles
+
+This file contains several standard constructions on vector bundles:
+
+* `Bundle.Trivial.vectorBundle 𝕜 B F`: the trivial vector bundle with scalar field `𝕜` and model
+  fiber `F` over the base `B`
+
+* `VectorBundle.prod`: for vector bundles `E₁` and `E₂` with scalar field `𝕜` over a common base,
+  a vector bundle structure on their direct sum `E₁ ×ᵇ E₂` (the notation stands for
+  `λ x, E₁ x × E₂ x`).
+
+* `VectorBundle.pullback`: for a vector bundle `E` over `B`, a vector bundle structure on its
+  pullback `f *ᵖ E` by a map `f : B' → B` (the notation is a type synonym for `E ∘ f`).
+
+## Tags
+Vector bundle, direct sum, pullback
+-/
+
+
+noncomputable section
+
+open Bundle Set FiberBundle Classical
+
+/-! ### The trivial vector bundle -/
+
+namespace Bundle.Trivial
+
+variable (𝕜 : Type _) (B : Type _) (F : Type _) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F]
+  [NormedSpace 𝕜 F] [TopologicalSpace B]
+
+instance trivialization.isLinear : (trivialization B F).IsLinear 𝕜 where
+  linear _ _ := ⟨fun _ _ => rfl, fun _ _ => rfl⟩
+#align bundle.trivial.trivialization.is_linear Bundle.Trivial.trivialization.isLinear
+
+variable {𝕜}
+
+theorem trivialization.coordChangeL (b : B) :
+    (trivialization B F).coordChangeL 𝕜 (trivialization B F) b =
+      ContinuousLinearEquiv.refl 𝕜 F := by
+  ext v
+  rw [Trivialization.coordChangeL_apply']
+  exacts [rfl, ⟨mem_univ _, mem_univ _⟩]
+set_option linter.uppercaseLean3 false in
+#align bundle.trivial.trivialization.coord_changeL Bundle.Trivial.trivialization.coordChangeL
+
+variable (𝕜)
+
+instance vectorBundle : VectorBundle 𝕜 F (Bundle.Trivial B F) where
+  trivialization_linear' e he := by
+    rw [eq_trivialization B F e]
+    infer_instance
+  continuousOn_coordChange' e e' he he' := by
+    obtain rfl := eq_trivialization B F e
+    obtain rfl := eq_trivialization B F e'
+    simp only [trivialization.coordChangeL]
+    exact continuous_const.continuousOn
+#align bundle.trivial.vector_bundle Bundle.Trivial.vectorBundle
+
+end Bundle.Trivial
+
+/-! ### Direct sum of two vector bundles -/
+
+section
+
+variable (𝕜 : Type _) {B : Type _} [NontriviallyNormedField 𝕜] [TopologicalSpace B] (F₁ : Type _)
+  [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] (E₁ : B → Type _) [TopologicalSpace (TotalSpace E₁)]
+  (F₂ : Type _) [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] (E₂ : B → Type _)
+  [TopologicalSpace (TotalSpace E₂)]
+
+namespace Trivialization
+
+variable {F₁ E₁ F₂ E₂}
+variable [∀ x, AddCommMonoid (E₁ x)] [∀ x, Module 𝕜 (E₁ x)]
+  [∀ x, AddCommMonoid (E₂ x)] [∀ x, Module 𝕜 (E₂ x)] (e₁ e₁' : Trivialization F₁ (π E₁))
+  (e₂ e₂' : Trivialization F₂ (π E₂))
+
+instance prod.isLinear [e₁.IsLinear 𝕜] [e₂.IsLinear 𝕜] : (e₁.prod e₂).IsLinear 𝕜 where
+  linear := fun _ ⟨h₁, h₂⟩ =>
+    (((e₁.linear 𝕜 h₁).mk' _).prodMap ((e₂.linear 𝕜 h₂).mk' _)).isLinear
+#align trivialization.prod.is_linear Trivialization.prod.isLinear
+
+@[simp]
+theorem coordChangeL_prod [e₁.IsLinear 𝕜] [e₁'.IsLinear 𝕜] [e₂.IsLinear 𝕜] [e₂'.IsLinear 𝕜] ⦃b⦄
+    (hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet) :
+    ((e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b : F₁ × F₂ →L[𝕜] F₁ × F₂) =
+      (e₁.coordChangeL 𝕜 e₁' b : F₁ →L[𝕜] F₁).prodMap (e₂.coordChangeL 𝕜 e₂' b) := by
+  rw [ContinuousLinearMap.ext_iff, ContinuousLinearMap.coe_prodMap']
+  rintro ⟨v₁, v₂⟩
+  show
+    (e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) =
+      (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)
+  rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
+  exacts [rfl, hb, ⟨hb.1.2, hb.2.2⟩, ⟨hb.1.1, hb.2.1⟩]
+set_option linter.uppercaseLean3 false in
+#align trivialization.coord_changeL_prod Trivialization.coordChangeL_prod
+
+variable {e₁ e₂} [∀ x : B, TopologicalSpace (E₁ x)] [∀ x : B, TopologicalSpace (E₂ x)]
+  [FiberBundle F₁ E₁] [FiberBundle F₂ E₂]
+
+theorem prod_apply [e₁.IsLinear 𝕜] [e₂.IsLinear 𝕜] {x : B} (hx₁ : x ∈ e₁.baseSet)
+    (hx₂ : x ∈ e₂.baseSet) (v₁ : E₁ x) (v₂ : E₂ x) :
+    prod e₁ e₂ ⟨x, (v₁, v₂)⟩ =
+      ⟨x, e₁.continuousLinearEquivAt 𝕜 x hx₁ v₁, e₂.continuousLinearEquivAt 𝕜 x hx₂ v₂⟩ :=
+  rfl
+#align trivialization.prod_apply Trivialization.prod_apply
+
+end Trivialization
+
+open Trivialization
+
+variable [∀ x, AddCommMonoid (E₁ x)] [∀ x, Module 𝕜 (E₁ x)] [∀ x, AddCommMonoid (E₂ x)]
+  [∀ x, Module 𝕜 (E₂ x)] [∀ x : B, TopologicalSpace (E₁ x)] [∀ x : B, TopologicalSpace (E₂ x)]
+  [FiberBundle F₁ E₁] [FiberBundle F₂ E₂]
+
+/-- The product of two vector bundles is a vector bundle. -/
+instance VectorBundle.prod [VectorBundle 𝕜 F₁ E₁] [VectorBundle 𝕜 F₂ E₂] :
+    VectorBundle 𝕜 (F₁ × F₂) (E₁ ×ᵇ E₂) where
+  trivialization_linear' := by
+    rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩; skip
+    infer_instance
+  continuousOn_coordChange' := by
+    rintro _ _ ⟨e₁, e₂, he₁, he₂, rfl⟩ ⟨e₁', e₂', he₁', he₂', rfl⟩; skip
+    refine' (((continuousOn_coordChange 𝕜 e₁ e₁').mono _).prod_mapL 𝕜
+      ((continuousOn_coordChange 𝕜 e₂ e₂').mono _)).congr _ <;>
+      dsimp only [baseSet_prod, mfld_simps]
+    · mfld_set_tac
+    · mfld_set_tac
+    · rintro b hb
+      rw [ContinuousLinearMap.ext_iff]
+      rintro ⟨v₁, v₂⟩
+      show (e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) =
+        (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)
+      rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
+      exacts[rfl, hb, ⟨hb.1.2, hb.2.2⟩, ⟨hb.1.1, hb.2.1⟩]
+#align vector_bundle.prod VectorBundle.prod
+
+variable {𝕜 F₁ E₁ F₂ E₂}
+
+@[simp] -- porting note: changed arguments to make `simpNF` happy: merged `hx₁` and `hx₂` into `hx`
+theorem Trivialization.continuousLinearEquivAt_prod {e₁ : Trivialization F₁ (π E₁)}
+    {e₂ : Trivialization F₂ (π E₂)} [e₁.IsLinear 𝕜] [e₂.IsLinear 𝕜] {x : B}
+    (hx : x ∈ (e₁.prod e₂).baseSet) :
+    (e₁.prod e₂).continuousLinearEquivAt 𝕜 x hx =
+      (e₁.continuousLinearEquivAt 𝕜 x hx.1).prod (e₂.continuousLinearEquivAt 𝕜 x hx.2) := by
+  ext v : 2
+  obtain ⟨v₁, v₂⟩ := v
+  rw [(e₁.prod e₂).continuousLinearEquivAt_apply 𝕜, Trivialization.prod]
+  exact (congr_arg Prod.snd (prod_apply 𝕜 hx.1 hx.2 v₁ v₂) : _)
+#align trivialization.continuous_linear_equiv_at_prod Trivialization.continuousLinearEquivAt_prodₓ
+
+end
+
+/-! ### Pullbacks of vector bundles -/
+
+section
+
+variable (R 𝕜 : Type _) {B : Type _} (F : Type _) (E : B → Type _) {B' : Type _} (f : B' → B)
+
+instance [i : ∀ x : B, AddCommMonoid (E x)] (x : B') : AddCommMonoid ((f *ᵖ E) x) := i _
+
+instance [Semiring R] [∀ x : B, AddCommMonoid (E x)] [i : ∀ x, Module R (E x)] (x : B') :
+    Module R ((f *ᵖ E) x) := i _
+
+variable {E F} [TopologicalSpace B'] [TopologicalSpace (TotalSpace E)] [NontriviallyNormedField 𝕜]
+  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace B] [∀ x, AddCommMonoid (E x)]
+  [∀ x, Module 𝕜 (E x)] {K : Type _} [ContinuousMapClass K B' B]
+
+instance Trivialization.pullback_linear (e : Trivialization F (π E)) [e.IsLinear 𝕜] (f : K) :
+    (@Trivialization.pullback _ _ _ B' _ _ _ _ _ _ _ e f).IsLinear 𝕜 where
+  linear _ h := e.linear 𝕜 h
+#align trivialization.pullback_linear Trivialization.pullback_linear
+
+instance VectorBundle.pullback [∀ x, TopologicalSpace (E x)] [FiberBundle F E] [VectorBundle 𝕜 F E]
+    (f : K) : VectorBundle 𝕜 F ((f : B' → B) *ᵖ E) where
+  trivialization_linear' := by
+    rintro _ ⟨e, he, rfl⟩
+    infer_instance
+  continuousOn_coordChange' := by
+    rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩
+    refine' ((continuousOn_coordChange 𝕜 e e').comp
+      (map_continuous f).continuousOn fun b hb => hb).congr _
+    rintro b (hb : f b ∈ e.baseSet ∩ e'.baseSet); ext v
+    show ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v
+    rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]
+    exacts [rfl, hb]
+#align vector_bundle.pullback VectorBundle.pullback
+
+end