feat(geometry/manifold/vector_bundle/tangent): some equations about t…

…rivializations (#18825)

* From the sphere eversion project

src/geometry/manifold/vector_bundle/tangent.lean

@@ -141,11 +141,10 @@ does not pick wrong instances. In this section, we record the right instances fo
 them, noting in particular that the tangent bundle is a smooth manifold. -/
 
 section
-local attribute [reducible] tangent_space
 
 variables {M} (x : M)
 
-instance : module 𝕜 (tangent_space I x) := by apply_instance
+instance : module 𝕜 (tangent_space I x) := by delta_instance tangent_space
 instance : inhabited (tangent_space I x) := ⟨0⟩
 
 end
@@ -219,6 +218,41 @@ by simp only [fiber_bundle.charted_space_chart_at, and_iff_left_iff_imp] with mf
 @[simp, mfld_simps] lemma coe_chart_at_symm_fst (p : H × E) (q : TM) :
   ((chart_at (model_prod H E) q).symm p).1 = ((chart_at H q.1).symm : H → M) p.1 := rfl
 
+@[simp, mfld_simps] lemma trivialization_at_continuous_linear_map_at {b₀ b : M}
+  (hb : b ∈ (trivialization_at E (tangent_space I) b₀).base_set) :
+  (trivialization_at E (tangent_space I) b₀).continuous_linear_map_at 𝕜 b =
+  (tangent_bundle_core I M).coord_change (achart H b) (achart H b₀) b :=
+(tangent_bundle_core I M).local_triv_continuous_linear_map_at hb
+
+@[simp, mfld_simps] lemma trivialization_at_symmL {b₀ b : M}
+  (hb : b ∈ (trivialization_at E (tangent_space I) b₀).base_set) :
+  (trivialization_at E (tangent_space I) b₀).symmL 𝕜 b =
+    (tangent_bundle_core I M).coord_change (achart H b₀) (achart H b) b :=
+(tangent_bundle_core I M).local_triv_symmL hb
+
+@[simp, mfld_simps]
+lemma coord_change_model_space (b b' x : F) :
+  (tangent_bundle_core 𝓘(𝕜, F) F).coord_change (achart F b) (achart F b') x = 1 :=
+by simpa only [tangent_bundle_core_coord_change] with mfld_simps using
+    fderiv_within_id unique_diff_within_at_univ
+
+@[simp, mfld_simps]
+lemma symmL_model_space (b b' : F) :
+  (trivialization_at F (tangent_space 𝓘(𝕜, F)) b).symmL 𝕜 b' = (1 : F →L[𝕜] F) :=
+begin
+  rw [tangent_bundle.trivialization_at_symmL, coord_change_model_space],
+  apply mem_univ
+end
+
+@[simp, mfld_simps]
+lemma continuous_linear_map_at_model_space (b b' : F) :
+  (trivialization_at F (tangent_space 𝓘(𝕜, F)) b).continuous_linear_map_at 𝕜 b' =
+  (1 : F →L[𝕜] F) :=
+begin
+  rw [tangent_bundle.trivialization_at_continuous_linear_map_at, coord_change_model_space],
+  apply mem_univ
+end
+
 end tangent_bundle
 
 instance tangent_bundle_core.is_smooth : (tangent_bundle_core I M).is_smooth I :=
@@ -270,6 +304,11 @@ by { unfold_coes, simp_rw [tangent_bundle_model_space_chart_at], refl }
 by { unfold_coes,
   simp_rw [local_homeomorph.symm_to_local_equiv, tangent_bundle_model_space_chart_at], refl }
 
+lemma tangent_bundle_core_coord_change_model_space (x x' z : H) :
+  (tangent_bundle_core I H).coord_change (achart H x) (achart H x') z =
+  continuous_linear_map.id 𝕜 E :=
+by { ext v, exact (tangent_bundle_core I H).coord_change_self (achart _ z) z (mem_univ _) v }
+
 variable (H)
 /-- The canonical identification between the tangent bundle to the model space and the product,
 as a homeomorphism -/

src/topology/vector_bundle/basic.lean

@@ -43,7 +43,7 @@ noncomputable theory
 open bundle set
 open_locale classical bundle
 
-variables (R 𝕜 : Type*) {B : Type*} (F : Type*) (E : B → Type*)
+variables (R : Type*) {B : Type*} (F : Type*) (E : B → Type*)
 
 section topological_vector_space
 variables {B F E} [semiring R]
@@ -560,13 +560,13 @@ instance add_comm_group_fiber [add_comm_group F] : ∀ (x : B), add_comm_group (
 by dsimp [vector_bundle_core.fiber];  delta_instance fiber_bundle_core.fiber
 
 /-- The projection from the total space of a fiber bundle core, on its base. -/
-@[reducible, simp, mfld_simps] def proj : total_space Z.fiber → B := total_space.proj
+@[reducible, simp, mfld_simps] protected def proj : total_space Z.fiber → B := total_space.proj
 
 /-- The total space of the vector bundle, as a convenience function for dot notation.
 It is by definition equal to `bundle.total_space Z.fiber`, a.k.a. `Σ x, Z.fiber x` but with a
 different name for typeclass inference. -/
 @[nolint unused_arguments, reducible]
-def total_space := bundle.total_space Z.fiber
+protected def total_space := bundle.total_space Z.fiber
 
 /-- Local homeomorphism version of the trivialization change. -/
 def triv_change (i j : ι) : local_homeomorph (B × F) (B × F) :=
@@ -675,6 +675,38 @@ fiber_bundle_core.continuous_proj Z
 lemma is_open_map_proj : is_open_map Z.proj :=
 fiber_bundle_core.is_open_map_proj Z
 
+variables {i j}
+
+@[simp, mfld_simps] lemma local_triv_continuous_linear_map_at {b : B} (hb : b ∈ Z.base_set i) :
+  (Z.local_triv i).continuous_linear_map_at R b = Z.coord_change (Z.index_at b) i b :=
+begin
+  ext1 v,
+  rw [(Z.local_triv i).continuous_linear_map_at_apply R, (Z.local_triv i).coe_linear_map_at_of_mem],
+  exacts [rfl, hb]
+end
+
+@[simp, mfld_simps] lemma trivialization_at_continuous_linear_map_at {b₀ b : B}
+  (hb : b ∈ (trivialization_at F Z.fiber b₀).base_set) :
+  (trivialization_at F Z.fiber b₀).continuous_linear_map_at R b =
+  Z.coord_change (Z.index_at b) (Z.index_at b₀) b :=
+Z.local_triv_continuous_linear_map_at hb
+
+@[simp, mfld_simps] lemma local_triv_symmL {b : B} (hb : b ∈ Z.base_set i) :
+  (Z.local_triv i).symmL R b = Z.coord_change i (Z.index_at b) b :=
+by { ext1 v, rw [(Z.local_triv i).symmL_apply R, (Z.local_triv i).symm_apply], exacts [rfl, hb] }
+
+@[simp, mfld_simps] lemma trivialization_at_symmL {b₀ b : B}
+  (hb : b ∈ (trivialization_at F Z.fiber b₀).base_set) :
+  (trivialization_at F Z.fiber b₀).symmL R b = Z.coord_change (Z.index_at b₀) (Z.index_at b) b :=
+Z.local_triv_symmL hb
+
+@[simp, mfld_simps] lemma trivialization_at_coord_change_eq {b₀ b₁ b : B}
+  (hb : b ∈ (trivialization_at F Z.fiber b₀).base_set ∩ (trivialization_at F Z.fiber b₁).base_set)
+  (v : F) :
+  (trivialization_at F Z.fiber b₀).coord_changeL R (trivialization_at F Z.fiber b₁) b v =
+  Z.coord_change (Z.index_at b₀) (Z.index_at b₁) b v :=
+Z.local_triv_coord_change_eq _ _ hb v
+
 end vector_bundle_core
 
 end