Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 5be98b9

Browse files
hrmacbethfpvandoorn
hrmacbeth
and
fpvandoorn
committed
feat(geometry/manifold/vector_bundle): smooth_fiberwise_linear groupoid (#17302)
Let `B` be a smooth manifold and `F` a normed space. We build the groupoid of local homeomorphisms of `B × F` which are "smooth and fibrewise linear": that is, they are of the form `λ x, (x.1, φ x.1 x.2)` for some function `φ` from `B` to the automorphisms of `F`, which is smooth and has smooth inverse on the proposed domain. Membership in this groupoid is the natural property characterizing the transition functions of a smooth vector bundle over `B` modelled on `F`. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
1 parent a8e7ac8 commit 5be98b9

File tree

2 files changed

+292
-5
lines changed

2 files changed

+292
-5
lines changed

‎src/geometry/manifold/cont_mdiff.lean

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1624,14 +1624,24 @@ lemma continuous_linear_map.cont_mdiff (L : E →L[𝕜] F) :
16241624
L.cont_diff.cont_mdiff
16251625

16261626
-- the following proof takes very long to elaborate in pure term mode
1627+
lemma cont_mdiff_within_at.clm_comp {g : M → F →L[𝕜] F''} {f : M → F' →L[𝕜] F} {s : set M} {x : M}
1628+
(hg : cont_mdiff_within_at I 𝓘(𝕜, F →L[𝕜] F'') n g s x)
1629+
(hf : cont_mdiff_within_at I 𝓘(𝕜, F' →L[𝕜] F) n f s x) :
1630+
cont_mdiff_within_at I 𝓘(𝕜, F' →L[𝕜] F'') n (λ x, (g x).comp (f x)) s x :=
1631+
@cont_diff_within_at.comp_cont_mdiff_within_at _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
1632+
(λ x : (F →L[𝕜] F'') × (F' →L[𝕜] F), x.1.comp x.2) (λ x, (g x, f x)) s _ x
1633+
(by { apply cont_diff.cont_diff_at, exact cont_diff_fst.clm_comp cont_diff_snd })
1634+
(hg.prod_mk_space hf) (by simp_rw [preimage_univ, subset_univ])
1635+
16271636
lemma cont_mdiff_at.clm_comp {g : M → F →L[𝕜] F''} {f : M → F' →L[𝕜] F} {x : M}
16281637
(hg : cont_mdiff_at I 𝓘(𝕜, F →L[𝕜] F'') n g x) (hf : cont_mdiff_at I 𝓘(𝕜, F' →L[𝕜] F) n f x) :
16291638
cont_mdiff_at I 𝓘(𝕜, F' →L[𝕜] F'') n (λ x, (g x).comp (f x)) x :=
1630-
@cont_diff_at.comp_cont_mdiff_at _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
1631-
(λ x : (F →L[𝕜] F'') × (F' →L[𝕜] F), x.1.comp x.2) (λ x, (g x, f x)) x
1632-
(by { apply cont_diff.cont_diff_at, apply is_bounded_bilinear_map.cont_diff,
1633-
exact is_bounded_bilinear_map_comp }) -- todo: simplify after #16946
1634-
(hg.prod_mk_space hf)
1639+
(hg.cont_mdiff_within_at.clm_comp hf.cont_mdiff_within_at).cont_mdiff_at univ_mem
1640+
1641+
lemma cont_mdiff_on.clm_comp {g : M → F →L[𝕜] F''} {f : M → F' →L[𝕜] F} {s : set M}
1642+
(hg : cont_mdiff_on I 𝓘(𝕜, F →L[𝕜] F'') n g s) (hf : cont_mdiff_on I 𝓘(𝕜, F' →L[𝕜] F) n f s) :
1643+
cont_mdiff_on I 𝓘(𝕜, F' →L[𝕜] F'') n (λ x, (g x).comp (f x)) s :=
1644+
λ x hx, (hg x hx).clm_comp (hf x hx)
16351645

16361646
lemma cont_mdiff.clm_comp {g : M → F →L[𝕜] F''} {f : M → F' →L[𝕜] F}
16371647
(hg : cont_mdiff I 𝓘(𝕜, F →L[𝕜] F'') n g) (hf : cont_mdiff I 𝓘(𝕜, F' →L[𝕜] F) n f) :

‎src/geometry/manifold/vector_bundle.lean

Lines changed: 277 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,277 @@
1+
/-
2+
Copyright (c) 2022 Floris van Doorn, Heather Macbeth. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Floris van Doorn, Heather Macbeth
5+
-/
6+
import geometry.manifold.cont_mdiff
7+
8+
/-! # Smooth vector bundles
9+
10+
This file will eventually contain the definition of a smooth vector bundle. For now, it contains
11+
preliminaries regarding an associated `structure_groupoid`, the groupoid of
12+
`smooth_fibrewise_linear` functions. When a (topological) vector bundle is smooth, then the
13+
composition of charts associated to the vector bundle belong to this groupoid.
14+
-/
15+
16+
noncomputable theory
17+
18+
open set topological_space
19+
open_locale manifold topology
20+
21+
/-! ### The groupoid of smooth, fibrewise-linear maps -/
22+
23+
variables {𝕜 B F : Type*} [topological_space B]
24+
variables [nontrivially_normed_field 𝕜] [normed_add_comm_group F] [normed_space 𝕜 F]
25+
26+
namespace fiberwise_linear
27+
28+
variables {φ φ' : B → F ≃L[𝕜] F} {U U' : set B}
29+
30+
/-- For `B` a topological space and `F` a `𝕜`-normed space, a map from `U : set B` to `F ≃L[𝕜] F`
31+
determines a local homeomorphism from `B × F` to itself by its action fibrewise. -/
32+
def local_homeomorph (φ : B → F ≃L[𝕜] F) (hU : is_open U)
33+
(hφ : continuous_on (λ x, φ x : B → F →L[𝕜] F) U)
34+
(h2φ : continuous_on (λ x, (φ x).symm : B → F →L[𝕜] F) U) :
35+
local_homeomorph (B × F) (B × F) :=
36+
{ to_fun := λ x, (x.1, φ x.1 x.2),
37+
inv_fun := λ x, (x.1, (φ x.1).symm x.2),
38+
source := U ×ˢ univ,
39+
target := U ×ˢ univ,
40+
map_source' := λ x hx, mk_mem_prod hx.1 (mem_univ _),
41+
map_target' := λ x hx, mk_mem_prod hx.1 (mem_univ _),
42+
left_inv' := λ x _, prod.ext rfl (continuous_linear_equiv.symm_apply_apply _ _),
43+
right_inv' := λ x _, prod.ext rfl (continuous_linear_equiv.apply_symm_apply _ _),
44+
open_source := hU.prod is_open_univ,
45+
open_target := hU.prod is_open_univ,
46+
continuous_to_fun := begin
47+
have : continuous_on (λ p : B × F, ((φ p.1 : F →L[𝕜] F), p.2)) (U ×ˢ univ),
48+
{ exact hφ.prod_map continuous_on_id },
49+
exact continuous_on_fst.prod (is_bounded_bilinear_map_apply.continuous.comp_continuous_on this),
50+
end,
51+
continuous_inv_fun := begin
52+
have : continuous_on (λ p : B × F, (((φ p.1).symm : F →L[𝕜] F), p.2)) (U ×ˢ univ),
53+
{ exact h2φ.prod_map continuous_on_id },
54+
exact continuous_on_fst.prod (is_bounded_bilinear_map_apply.continuous.comp_continuous_on this),
55+
end, }
56+
57+
/-- Compute the composition of two local homeomorphisms induced by fiberwise linear
58+
equivalences. -/
59+
lemma trans_local_homeomorph_apply
60+
(hU : is_open U)
61+
(hφ : continuous_on (λ x, φ x : B → F →L[𝕜] F) U)
62+
(h2φ : continuous_on (λ x, (φ x).symm : B → F →L[𝕜] F) U)
63+
(hU' : is_open U')
64+
(hφ' : continuous_on (λ x, φ' x : B → F →L[𝕜] F) U')
65+
(h2φ' : continuous_on (λ x, (φ' x).symm : B → F →L[𝕜] F) U')
66+
(b : B) (v : F) :
67+
(fiberwise_linear.local_homeomorph φ hU hφ h2φ ≫ₕ
68+
fiberwise_linear.local_homeomorph φ' hU' hφ' h2φ') ⟨b, v⟩ = ⟨b, φ' b (φ b v)⟩ :=
69+
rfl
70+
71+
/-- Compute the source of the composition of two local homeomorphisms induced by fiberwise linear
72+
equivalences. -/
73+
lemma source_trans_local_homeomorph
74+
(hU : is_open U)
75+
(hφ : continuous_on (λ x, φ x : B → F →L[𝕜] F) U)
76+
(h2φ : continuous_on (λ x, (φ x).symm : B → F →L[𝕜] F) U)
77+
(hU' : is_open U')
78+
(hφ' : continuous_on (λ x, φ' x : B → F →L[𝕜] F) U')
79+
(h2φ' : continuous_on (λ x, (φ' x).symm : B → F →L[𝕜] F) U') :
80+
(fiberwise_linear.local_homeomorph φ hU hφ h2φ ≫ₕ
81+
fiberwise_linear.local_homeomorph φ' hU' hφ' h2φ').source = (U ∩ U') ×ˢ univ :=
82+
by { dsimp [fiberwise_linear.local_homeomorph], mfld_set_tac }
83+
84+
/-- Compute the target of the composition of two local homeomorphisms induced by fiberwise linear
85+
equivalences. -/
86+
lemma target_trans_local_homeomorph
87+
(hU : is_open U)
88+
(hφ : continuous_on (λ x, φ x : B → F →L[𝕜] F) U)
89+
(h2φ : continuous_on (λ x, (φ x).symm : B → F →L[𝕜] F) U)
90+
(hU' : is_open U')
91+
(hφ' : continuous_on (λ x, φ' x : B → F →L[𝕜] F) U')
92+
(h2φ' : continuous_on (λ x, (φ' x).symm : B → F →L[𝕜] F) U') :
93+
(fiberwise_linear.local_homeomorph φ hU hφ h2φ ≫ₕ
94+
fiberwise_linear.local_homeomorph φ' hU' hφ' h2φ').target = (U ∩ U') ×ˢ univ :=
95+
by { dsimp [fiberwise_linear.local_homeomorph], mfld_set_tac }
96+
97+
end fiberwise_linear
98+
99+
variables {EB : Type*} [normed_add_comm_group EB] [normed_space 𝕜 EB]
100+
{HB : Type*} [topological_space HB] [charted_space HB B] {IB : model_with_corners 𝕜 EB HB}
101+
102+
/-- Let `e` be a local homeomorphism of `B × F`. Suppose that at every point `p` in the source of
103+
`e`, there is some neighbourhood `s` of `p` on which `e` is equal to a bi-smooth fibrewise linear
104+
local homeomorphism.
105+
106+
Then the source of `e` is of the form `U ×ˢ univ`, for some set `U` in `B`, and, at any point `x` in
107+
`U`, admits a neighbourhood `u` of `x` such that `e` is equal on `u ×ˢ univ` to some bi-smooth
108+
fibrewise linear local homeomorphism. -/
109+
lemma smooth_fibrewise_linear.locality_aux₁ (e : local_homeomorph (B × F) (B × F))
110+
(h : ∀ p ∈ e.source, ∃ s : set (B × F), is_open s ∧ p ∈ s ∧
111+
∃ (φ : B → (F ≃L[𝕜] F)) (u : set B) (hu : is_open u)
112+
(hφ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, (φ x : F →L[𝕜] F)) u)
113+
(h2φ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, ((φ x).symm : F →L[𝕜] F)) u),
114+
(e.restr s).eq_on_source
115+
(fiberwise_linear.local_homeomorph φ hu hφ.continuous_on h2φ.continuous_on)) :
116+
∃ (U : set B) (hU : e.source = U ×ˢ univ),
117+
∀ x ∈ U, ∃ (φ : B → (F ≃L[𝕜] F)) (u : set B) (hu : is_open u) (huU : u ⊆ U) (hux : x ∈ u)
118+
(hφ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, (φ x : F →L[𝕜] F)) u)
119+
(h2φ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, ((φ x).symm : F →L[𝕜] F)) u),
120+
(e.restr (u ×ˢ univ)).eq_on_source
121+
(fiberwise_linear.local_homeomorph φ hu hφ.continuous_on h2φ.continuous_on) :=
122+
begin
123+
rw set_coe.forall' at h,
124+
choose s hs hsp φ u hu hφ h2φ heφ using h,
125+
have hesu : ∀ p : e.source, e.source ∩ s p = u p ×ˢ univ,
126+
{ intros p,
127+
rw ← e.restr_source' (s _) (hs _),
128+
exact (heφ p).1 },
129+
have hu' : ∀ p : e.source, (p : B × F).fst ∈ u p,
130+
{ intros p,
131+
have : (p : B × F) ∈ e.source ∩ s p := ⟨p.prop, hsp p⟩,
132+
simpa only [hesu, mem_prod, mem_univ, and_true] using this },
133+
have heu : ∀ p : e.source, ∀ q : B × F, q.fst ∈ u p → q ∈ e.source,
134+
{ intros p q hq,
135+
have : q ∈ u p ×ˢ (univ : set F) := ⟨hq, trivial⟩,
136+
rw ← hesu p at this,
137+
exact this.1 },
138+
have he : e.source = (prod.fst '' e.source) ×ˢ (univ : set F),
139+
{ apply has_subset.subset.antisymm,
140+
{ intros p hp,
141+
exact ⟨⟨p, hp, rfl⟩, trivial⟩ },
142+
{ rintros ⟨x, v⟩ ⟨⟨p, hp, rfl : p.fst = x⟩, -⟩,
143+
exact heu ⟨p, hp⟩ (p.fst, v) (hu' ⟨p, hp⟩) } },
144+
refine ⟨prod.fst '' e.source, he, _⟩,
145+
rintros x ⟨p, hp, rfl⟩,
146+
refine ⟨φ ⟨p, hp⟩, u ⟨p, hp⟩, hu ⟨p, hp⟩, _, hu' _, hφ ⟨p, hp⟩, h2φ ⟨p, hp⟩, _⟩,
147+
{ intros y hy, refine ⟨(y, 0), heu ⟨p, hp⟩ ⟨_, _⟩ hy, rfl⟩ },
148+
{ rw [← hesu, e.restr_source_inter], exact heφ ⟨p, hp⟩ },
149+
end
150+
151+
/-- Let `e` be a local homeomorphism of `B × F` whose source is `U ×ˢ univ`, for some set `U` in
152+
`B`, and which, at any point `x` in `U`, admits a neighbourhood `u` of `x` such that `e` is equal on
153+
`u ×ˢ univ` to some bi-smooth fibrewise linear local homeomorphism. Then `e` itself is equal to
154+
some bi-smooth fibrewise linear local homeomorphism.
155+
156+
This is the key mathematical point of the `locality` condition in the construction of the
157+
`structure_groupoid` of bi-smooth fibrewise linear local homeomorphisms. The proof is by gluing
158+
together the various bi-smooth fibrewise linear local homeomorphism which exist locally.
159+
160+
The `U` in the conclusion is the same `U` as in the hypothesis. We state it like this, because this
161+
is exactly what we need for `smooth_fiberwise_linear`. -/
162+
lemma smooth_fibrewise_linear.locality_aux₂ (e : local_homeomorph (B × F) (B × F))
163+
(U : set B) (hU : e.source = U ×ˢ univ)
164+
(h : ∀ x ∈ U, ∃ (φ : B → (F ≃L[𝕜] F)) (u : set B) (hu : is_open u) (hUu : u ⊆ U) (hux : x ∈ u)
165+
(hφ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, (φ x : F →L[𝕜] F)) u)
166+
(h2φ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, ((φ x).symm : F →L[𝕜] F)) u),
167+
(e.restr (u ×ˢ univ)).eq_on_source
168+
(fiberwise_linear.local_homeomorph φ hu hφ.continuous_on h2φ.continuous_on)) :
169+
∃ (Φ : B → (F ≃L[𝕜] F)) (U : set B) (hU₀ : is_open U)
170+
(hΦ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, (Φ x : F →L[𝕜] F)) U)
171+
(h2Φ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, ((Φ x).symm : F →L[𝕜] F)) U),
172+
e.eq_on_source (fiberwise_linear.local_homeomorph Φ hU₀ hΦ.continuous_on h2Φ.continuous_on) :=
173+
begin
174+
classical,
175+
rw set_coe.forall' at h,
176+
choose! φ u hu hUu hux hφ h2φ heφ using h,
177+
have heuφ : ∀ x : U, eq_on e (λ q, (q.1, φ x q.1 q.2)) (u x ×ˢ univ),
178+
{ intros x p hp,
179+
refine (heφ x).2 _,
180+
rw (heφ x).1,
181+
exact hp },
182+
have huφ : ∀ (x x' : U) (y : B) (hyx : y ∈ u x) (hyx' : y ∈ u x'), φ x y = φ x' y,
183+
{ intros p p' y hyp hyp',
184+
ext v,
185+
have h1 : e (y, v) = (y, φ p y v) := heuφ _ ⟨(id hyp : (y, v).fst ∈ u p), trivial⟩,
186+
have h2 : e (y, v) = (y, φ p' y v) := heuφ _ ⟨(id hyp' : (y, v).fst ∈ u p'), trivial⟩,
187+
exact congr_arg prod.snd (h1.symm.trans h2) },
188+
have hUu' : U = ⋃ i, u i,
189+
{ ext x,
190+
rw mem_Union,
191+
refine ⟨λ h, ⟨⟨x, h⟩, hux _⟩, _⟩,
192+
rintros ⟨x, hx⟩,
193+
exact hUu x hx },
194+
have hU' : is_open U,
195+
{ rw hUu',
196+
apply is_open_Union hu },
197+
let Φ₀ : U → F ≃L[𝕜] F := Union_lift u (λ x, (φ x) ∘ coe) huφ U hUu'.le,
198+
let Φ : B → F ≃L[𝕜] F := λ y, if hy : y ∈ U then Φ₀ ⟨y, hy⟩ else continuous_linear_equiv.refl 𝕜 F,
199+
have hΦ : ∀ (y) (hy : y ∈ U), Φ y = Φ₀ ⟨y, hy⟩ := λ y hy, dif_pos hy,
200+
have hΦφ : ∀ x : U, ∀ y ∈ u x, Φ y = φ x y,
201+
{ intros x y hyu,
202+
refine (hΦ y (hUu x hyu)).trans _,
203+
exact Union_lift_mk ⟨y, hyu⟩ _ },
204+
have hΦ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ y, (Φ y : F →L[𝕜] F)) U,
205+
{ apply cont_mdiff_on_of_locally_cont_mdiff_on,
206+
intros x hx,
207+
refine ⟨u ⟨x, hx⟩, hu ⟨x, hx⟩, hux _, _⟩,
208+
refine (cont_mdiff_on.congr (hφ ⟨x, hx⟩) _).mono (inter_subset_right _ _),
209+
intros y hy,
210+
rw hΦφ ⟨x, hx⟩ y hy },
211+
have h2Φ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ y, ((Φ y).symm : F →L[𝕜] F)) U,
212+
{ apply cont_mdiff_on_of_locally_cont_mdiff_on,
213+
intros x hx,
214+
refine ⟨u ⟨x, hx⟩, hu ⟨x, hx⟩, hux _, _⟩,
215+
refine (cont_mdiff_on.congr (h2φ ⟨x, hx⟩) _).mono (inter_subset_right _ _),
216+
intros y hy,
217+
rw hΦφ ⟨x, hx⟩ y hy },
218+
refine ⟨Φ, U, hU', hΦ, h2Φ, hU, λ p hp, _⟩,
219+
rw [hU] at hp,
220+
-- using rw on the next line seems to cause a timeout in kernel type-checking
221+
refine (heuφ ⟨p.fst, hp.1⟩ ⟨hux _, hp.2⟩).trans _,
222+
congrm (_, _),
223+
rw hΦφ,
224+
apply hux
225+
end
226+
227+
variables (F B IB)
228+
/-- For `B` a manifold and `F` a normed space, the groupoid on `B × F` consisting of local
229+
homeomorphisms which are bi-smooth and fibrewise linear, and induce the identity on `B`.
230+
When a (topological) vector bundle is smooth, then the composition of charts associated
231+
to the vector bundle belong to this groupoid. -/
232+
def smooth_fiberwise_linear : structure_groupoid (B × F) :=
233+
{ members := ⋃ (φ : B → F ≃L[𝕜] F) (U : set B) (hU : is_open U)
234+
(hφ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, φ x : B → F →L[𝕜] F) U)
235+
(h2φ : smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ x, (φ x).symm : B → F →L[𝕜] F) U),
236+
{e | e.eq_on_source (fiberwise_linear.local_homeomorph φ hU hφ.continuous_on h2φ.continuous_on)},
237+
trans' := begin
238+
simp_rw [mem_Union],
239+
rintros e e' ⟨φ, U, hU, hφ, h2φ, heφ⟩ ⟨φ', U', hU', hφ', h2φ', heφ'⟩,
240+
refine ⟨λ b, (φ b).trans (φ' b), _, hU.inter hU', _, _, setoid.trans (heφ.trans' heφ') ⟨_, _⟩⟩,
241+
{ show smooth_on IB 𝓘(𝕜, F →L[𝕜] F)
242+
(λ (x : B), (φ' x).to_continuous_linear_map ∘L (φ x).to_continuous_linear_map) (U ∩ U'),
243+
exact (hφ'.mono $ inter_subset_right _ _).clm_comp (hφ.mono $ inter_subset_left _ _) },
244+
{ show smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ (x : B),
245+
(φ x).symm.to_continuous_linear_map ∘L (φ' x).symm.to_continuous_linear_map) (U ∩ U'),
246+
exact (h2φ.mono $ inter_subset_left _ _).clm_comp (h2φ'.mono $ inter_subset_right _ _) },
247+
{ apply fiberwise_linear.source_trans_local_homeomorph },
248+
{ rintros ⟨b, v⟩ hb, apply fiberwise_linear.trans_local_homeomorph_apply }
249+
end,
250+
symm' := begin
251+
simp_rw [mem_Union],
252+
rintros e ⟨φ, U, hU, hφ, h2φ, heφ⟩,
253+
refine ⟨λ b, (φ b).symm, U, hU, h2φ, _, heφ.symm'⟩,
254+
simp_rw continuous_linear_equiv.symm_symm,
255+
exact hφ
256+
end,
257+
id_mem' := begin
258+
simp_rw [mem_Union],
259+
refine ⟨λ b, continuous_linear_equiv.refl 𝕜 F, univ, is_open_univ, _, _, ⟨_, λ b hb, _⟩⟩,
260+
{ apply cont_mdiff_on_const },
261+
{ apply cont_mdiff_on_const },
262+
{ simp only [fiberwise_linear.local_homeomorph, local_homeomorph.refl_local_equiv,
263+
local_equiv.refl_source, univ_prod_univ] },
264+
{ simp only [fiberwise_linear.local_homeomorph, local_homeomorph.refl_apply, prod.mk.eta,
265+
id.def, continuous_linear_equiv.coe_refl', local_homeomorph.mk_coe, local_equiv.coe_mk] },
266+
end,
267+
locality' := begin -- the hard work has been extracted to `locality_aux₁` and `locality_aux₂`
268+
simp_rw [mem_Union],
269+
intros e he,
270+
obtain ⟨U, hU, h⟩ := smooth_fibrewise_linear.locality_aux₁ e he,
271+
exact smooth_fibrewise_linear.locality_aux₂ e U hU h,
272+
end,
273+
eq_on_source' := begin
274+
simp_rw [mem_Union],
275+
rintros e e' ⟨φ, U, hU, hφ, h2φ, heφ⟩ hee',
276+
exact ⟨φ, U, hU, hφ, h2φ, setoid.trans hee' heφ⟩,
277+
end }

0 commit comments

Comments
 (0)