From 6f0170b1eb06d968a7d17a02971484defce081cb Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 2 Apr 2026 14:12:19 +0200 Subject: [PATCH 1/2] feat: continuousLinearMapAt_apply_of_mem Also mark (Pre)Trivialization.coe_linearMapAt_of_mem simp, and use this to golf two proofs. From #36036, i.e. the path towards Ehresmann connections. Co-authored by: Patrick Massot --- .../Geometry/Manifold/Riemannian/Basic.lean | 3 +-- .../Manifold/VectorBundle/Riemannian.lean | 2 +- Mathlib/Topology/VectorBundle/Basic.lean | 20 ++++++++++--------- Mathlib/Topology/VectorBundle/Riemannian.lean | 2 +- 4 files changed, 14 insertions(+), 13 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Riemannian/Basic.lean b/Mathlib/Geometry/Manifold/Riemannian/Basic.lean index e0a72953c32d35..f3b1a21af91a0e 100644 --- a/Mathlib/Geometry/Manifold/Riemannian/Basic.lean +++ b/Mathlib/Geometry/Manifold/Riemannian/Basic.lean @@ -121,8 +121,7 @@ noncomputable def riemannianMetricVectorSpace : rw [contMDiffAt_section] convert contMDiffAt_const (c := innerSL ℝ) ext v w - simp [hom_trivializationAt_apply, ContinuousLinearMap.inCoordinates, - Trivialization.linearMapAt_apply, TangentSpace] + simp [hom_trivializationAt_apply, ContinuousLinearMap.inCoordinates, TangentSpace] noncomputable instance : RiemannianBundle (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x) := ⟨(riemannianMetricVectorSpace F).toRiemannianMetric⟩ diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean b/Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean index fa5942782a2311..331d404adddd21 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean @@ -103,7 +103,7 @@ instance : IsContMDiffRiemannianBundle IB n F₁ (Bundle.Trivial B F₁) := by simp only [contMDiffAt_section] convert contMDiffAt_const (c := innerSL ℝ) ext v w - simp [hom_trivializationAt_apply, inCoordinates, Trivialization.linearMapAt_apply] + simp [hom_trivializationAt_apply, inCoordinates] end Trivial diff --git a/Mathlib/Topology/VectorBundle/Basic.lean b/Mathlib/Topology/VectorBundle/Basic.lean index 4b3a8b884580f1..8d192ed686c855 100644 --- a/Mathlib/Topology/VectorBundle/Basic.lean +++ b/Mathlib/Topology/VectorBundle/Basic.lean @@ -121,6 +121,7 @@ theorem coe_linearMapAt (e : Pretrivialization F (π F E)) [e.IsLinear R] (b : B rw [Pretrivialization.linearMapAt] split_ifs <;> rfl +@[simp] theorem coe_linearMapAt_of_mem (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) : ⇑(e.linearMapAt R b) = fun y => (e ⟨b, y⟩).2 := by simp_rw [coe_linearMapAt, if_pos hb] @@ -143,14 +144,10 @@ theorem linearMapAt_eq_zero (e : Pretrivialization F (π F E)) [e.IsLinear R] {b dif_neg hb theorem symmₗ_linearMapAt (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B} - (hb : b ∈ e.baseSet) (y : E b) : e.symmₗ R b (e.linearMapAt R b y) = y := by - rw [e.linearMapAt_def_of_mem hb] - exact (e.linearEquivAt R b hb).left_inv y + (hb : b ∈ e.baseSet) (y : E b) : e.symmₗ R b (e.linearMapAt R b y) = y := by simp [hb] theorem linearMapAt_symmₗ (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B} - (hb : b ∈ e.baseSet) (y : F) : e.linearMapAt R b (e.symmₗ R b y) = y := by - rw [e.linearMapAt_def_of_mem hb] - exact (e.linearEquivAt R b hb).right_inv y + (hb : b ∈ e.baseSet) (y : F) : e.linearMapAt R b (e.symmₗ R b y) = y := by simp [hb] end Pretrivialization @@ -214,6 +211,7 @@ theorem coe_linearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) : ⇑(e.linearMapAt R b) = fun y => if b ∈ e.baseSet then (e ⟨b, y⟩).2 else 0 := e.toPretrivialization.coe_linearMapAt b +@[simp] theorem coe_linearMapAt_of_mem (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) : ⇑(e.linearMapAt R b) = fun y => (e ⟨b, y⟩).2 := by simp_rw [coe_linearMapAt, if_pos hb] @@ -231,7 +229,6 @@ theorem linearMapAt_def_of_notMem (e : Trivialization F (π F E)) [e.IsLinear R] (hb : b ∉ e.baseSet) : e.linearMapAt R b = 0 := dif_neg hb -@[simp] theorem symm_linearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) (y : E b) : e.symm b (e.linearMapAt R b y) = y := e.toPretrivialization.symmₗ_linearMapAt hb y @@ -392,6 +389,11 @@ def continuousLinearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) exact (e.continuousOn.comp_continuous (FiberBundle.totalSpaceMk_isInducing F E b).continuous fun x => e.mem_source.mpr hb).snd } +lemma continuousLinearMapAt_apply_of_mem (e : Trivialization F TotalSpace.proj) + [Trivialization.IsLinear R e] {b : B} (hb : b ∈ e.baseSet) (y : E b) : + (continuousLinearMapAt R e b) y = (e ⟨b, y⟩).2 := by + simp [coe_linearMapAt_of_mem e hb] + /-- Backwards map of `Bundle.Trivialization.continuousLinearEquivAt`, defined everywhere. -/ @[simps -fullyApplied apply] def symmL (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) : F →L[R] E b := @@ -708,8 +710,8 @@ variable {i j} theorem localTriv_continuousLinearMapAt {b : B} (hb : b ∈ (Z.localTriv i).baseSet) : (Z.localTriv i).continuousLinearMapAt R b = Z.coordChange (Z.indexAt b) i b := by ext1 v - rw [(Z.localTriv i).continuousLinearMapAt_apply R, (Z.localTriv i).coe_linearMapAt_of_mem] - exacts [rfl, hb] + simp_all + rfl @[simp, mfld_simps] theorem trivializationAt_continuousLinearMapAt {b₀ b : B} diff --git a/Mathlib/Topology/VectorBundle/Riemannian.lean b/Mathlib/Topology/VectorBundle/Riemannian.lean index 8b008e8df7fb85..d34d3540c09a8c 100644 --- a/Mathlib/Topology/VectorBundle/Riemannian.lean +++ b/Mathlib/Topology/VectorBundle/Riemannian.lean @@ -80,7 +80,7 @@ instance : IsContinuousRiemannianBundle F₁ (Bundle.Trivial B F₁) := by refine ⟨continuousAt_id, ?_⟩ convert continuousAt_const (y := innerSL ℝ) ext v w - simp [hom_trivializationAt_apply, inCoordinates, Trivialization.linearMapAt_apply] + simp [hom_trivializationAt_apply, inCoordinates] end Trivial From 9170bd1e654db7ea5db9fa7ae5cba6b71b2b53bf Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 2 Apr 2026 15:14:17 +0200 Subject: [PATCH 2/2] chore: golf rw [...]; rfl proofs to simp [...] Each of these involves the newly added simp lemma. --- Mathlib/Topology/VectorBundle/Riemannian.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/Mathlib/Topology/VectorBundle/Riemannian.lean b/Mathlib/Topology/VectorBundle/Riemannian.lean index d34d3540c09a8c..ce32b6145ac055 100644 --- a/Mathlib/Topology/VectorBundle/Riemannian.lean +++ b/Mathlib/Topology/VectorBundle/Riemannian.lean @@ -189,8 +189,7 @@ lemma eventually_norm_symmL_trivializationAt_self_comp_lt (x : B) {r : ℝ} (hr have A : ((trivializationAt F E x).symm y) ((trivializationAt F E x).linearMapAt ℝ y v) = v := by convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'y).symm_apply_apply v - rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'y] - rfl + simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'y] simp [A, w] have hgx : g x ((trivializationAt F E x).symm x w) ((trivializationAt F E x).symm x w) = g' x w w := by @@ -232,8 +231,7 @@ lemma eventually_norm_trivializationAt_lt (x : B) : simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply, Function.comp_apply, coe_id', id_eq] convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v - rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'x] - rfl + simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x] have : (trivializationAt F E x).continuousLinearMapAt ℝ y = (ContinuousLinearMap.id _ _) ∘L ((trivializationAt F E x).continuousLinearMapAt ℝ y) := by simp grw [this, ← A, comp_assoc, opNorm_comp_le] @@ -294,8 +292,7 @@ lemma eventually_norm_symmL_trivializationAt_comp_self_lt (x : B) {r : ℝ} (hr have A : ((trivializationAt F E x).symm x) ((trivializationAt F E x).linearMapAt ℝ x v) = v := by convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).symm_apply_apply v - rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'x] - rfl + simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x] simp [A, w] have hgy : g y ((trivializationAt F E x).symm y w) ((trivializationAt F E x).symm y w) = g' y w w := by @@ -339,8 +336,7 @@ lemma eventually_norm_symmL_trivializationAt_lt (x : B) : simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply, Function.comp_apply, coe_id', id_eq] convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v - rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'x] - rfl + simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x] have : (trivializationAt F E x).symmL ℝ y = ((trivializationAt F E x).symmL ℝ y) ∘L (ContinuousLinearMap.id _ _) := by simp grw [this, ← A, ← comp_assoc, opNorm_comp_le]