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

Commit c89fe2d

Browse files
fpvandoornfpvandoorn
committed
feat(geometry/manifold/vector_bundle/hom): the hom bundle is smooth (#18828)
* From the sphere eversion project
1 parent 17fe363 commit c89fe2d

2 files changed

Lines changed: 199 additions & 7 deletions

File tree

‎src/geometry/manifold/vector_bundle/basic.lean‎

Lines changed: 77 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -44,9 +44,13 @@ fields, they can also be C^k vector bundles, etc.
4444
* `bundle.total_space.smooth_manifold_with_corners`: A smooth vector bundle is naturally a smooth
4545
manifold.
4646
47-
* `vector_bundle_core.smooth_vector_bundle`: If a (topological) `vector_bundle_core` is smooth, in
48-
the sense of having smooth transition functions, then the vector bundle constructed from it is a
49-
smooth vector bundle.
47+
* `vector_bundle_core.smooth_vector_bundle`: If a (topological) `vector_bundle_core` is smooth,
48+
in the sense of having smooth transition functions (cf. `vector_bundle_core.is_smooth`),
49+
then the vector bundle constructed from it is a smooth vector bundle.
50+
51+
* `vector_prebundle.smooth_vector_bundle`: If a `vector_prebundle` is smooth,
52+
in the sense of having smooth transition functions (cf. `vector_prebundle.is_smooth`),
53+
then the vector bundle constructed from it is a smooth vector bundle.
5054
5155
* `bundle.prod.smooth_vector_bundle`: The direct sum of two smooth vector bundles is a smooth vector
5256
bundle.
@@ -237,17 +241,20 @@ end
237241

238242
/-! ### Smooth vector bundles -/
239243

240-
variables [nontrivially_normed_field 𝕜] [∀ x, add_comm_monoid (E x)] [∀ x, module 𝕜 (E x)]
241-
[normed_add_comm_group F] [normed_space 𝕜 F]
242-
[topological_space (total_space E)] [∀ x, topological_space (E x)]
243-
244+
variables [nontrivially_normed_field 𝕜]
244245
{EB : Type*} [normed_add_comm_group EB] [normed_space 𝕜 EB]
245246
{HB : Type*} [topological_space HB] (IB : model_with_corners 𝕜 EB HB)
246247
[topological_space B] [charted_space HB B] [smooth_manifold_with_corners IB B]
247248
{EM : Type*} [normed_add_comm_group EM] [normed_space 𝕜 EM]
248249
{HM : Type*} [topological_space HM] {IM : model_with_corners 𝕜 EM HM}
249250
[topological_space M] [charted_space HM M] [Is : smooth_manifold_with_corners IM M]
250251
{n : ℕ∞}
252+
[∀ x, add_comm_monoid (E x)] [∀ x, module 𝕜 (E x)]
253+
[normed_add_comm_group F] [normed_space 𝕜 F]
254+
255+
section with_topology
256+
257+
variables [topological_space (total_space E)] [∀ x, topological_space (E x)]
251258

252259
variables (F E) [fiber_bundle F E] [vector_bundle 𝕜 F E]
253260

@@ -380,3 +387,66 @@ instance bundle.prod.smooth_vector_bundle :
380387
end }
381388

382389
end prod
390+
391+
end with_topology
392+
393+
/-! ### Prebundle construction for smooth vector bundles -/
394+
395+
namespace vector_prebundle
396+
397+
variables {F E}
398+
399+
/-- Mixin for a `vector_prebundle` stating smoothness of coordinate changes. -/
400+
class is_smooth (a : vector_prebundle 𝕜 F E) : Prop :=
401+
(exists_smooth_coord_change : ∀ (e e' ∈ a.pretrivialization_atlas), ∃ f : B → F →L[𝕜] F,
402+
smooth_on IB 𝓘(𝕜, F →L[𝕜] F) f (e.base_set ∩ e'.base_set) ∧
403+
∀ (b : B) (hb : b ∈ e.base_set ∩ e'.base_set) (v : F),
404+
f b v = (e' (total_space_mk b (e.symm b v))).2)
405+
406+
variables (a : vector_prebundle 𝕜 F E) [ha : a.is_smooth IB] {e e' : pretrivialization F (π E)}
407+
include ha
408+
409+
/-- A randomly chosen coordinate change on a `smooth_vector_prebundle`, given by
410+
the field `exists_coord_change`. Note that `a.smooth_coord_change` need not be the same as
411+
`a.coord_change`. -/
412+
noncomputable def smooth_coord_change (he : e ∈ a.pretrivialization_atlas)
413+
(he' : e' ∈ a.pretrivialization_atlas) (b : B) : F →L[𝕜] F :=
414+
classical.some (ha.exists_smooth_coord_change e he e' he') b
415+
416+
variables {IB}
417+
lemma smooth_on_smooth_coord_change (he : e ∈ a.pretrivialization_atlas)
418+
(he' : e' ∈ a.pretrivialization_atlas) :
419+
smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (a.smooth_coord_change IB he he') (e.base_set ∩ e'.base_set) :=
420+
(classical.some_spec (ha.exists_smooth_coord_change e he e' he')).1
421+
422+
lemma smooth_coord_change_apply (he : e ∈ a.pretrivialization_atlas)
423+
(he' : e' ∈ a.pretrivialization_atlas) {b : B} (hb : b ∈ e.base_set ∩ e'.base_set) (v : F) :
424+
a.smooth_coord_change IB he he' b v = (e' (total_space_mk b (e.symm b v))).2 :=
425+
(classical.some_spec (ha.exists_smooth_coord_change e he e' he')).2 b hb v
426+
427+
lemma mk_smooth_coord_change (he : e ∈ a.pretrivialization_atlas)
428+
(he' : e' ∈ a.pretrivialization_atlas) {b : B} (hb : b ∈ e.base_set ∩ e'.base_set) (v : F) :
429+
(b, (a.smooth_coord_change IB he he' b v)) = e' (total_space_mk b (e.symm b v)) :=
430+
begin
431+
ext,
432+
{ rw [e.mk_symm hb.1 v, e'.coe_fst', e.proj_symm_apply' hb.1],
433+
rw [e.proj_symm_apply' hb.1], exact hb.2 },
434+
{ exact a.smooth_coord_change_apply he he' hb v }
435+
end
436+
437+
variables (IB)
438+
/-- Make a `smooth_vector_bundle` from a `smooth_vector_prebundle`. -/
439+
lemma smooth_vector_bundle :
440+
@smooth_vector_bundle _ _ F E _ _ _ _ _ _ IB _ _ _ _ _ _ _
441+
a.total_space_topology a.fiber_topology a.to_fiber_bundle a.to_vector_bundle :=
442+
{ smooth_on_coord_change := begin
443+
rintros _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩,
444+
refine (a.smooth_on_smooth_coord_change he he').congr _,
445+
intros b hb,
446+
ext v,
447+
rw [a.smooth_coord_change_apply he he' hb v, continuous_linear_equiv.coe_coe,
448+
trivialization.coord_changeL_apply],
449+
exacts [rfl, hb]
450+
end }
451+
452+
end vector_prebundle

‎src/geometry/manifold/vector_bundle/hom.lean‎

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
/-
2+
Copyright (c) 2022 Floris van Doorn. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Floris van Doorn
5+
-/
6+
import geometry.manifold.vector_bundle.basic
7+
import topology.vector_bundle.hom
8+
9+
/-! # Homs of smooth vector bundles over the same base space
10+
11+
Here we show that `bundle.continuous_linear_map` is a smooth vector bundle.
12+
13+
Note that we only do this for bundles of linear maps, not for bundles of arbitrary semilinear maps.
14+
To do it for semilinear maps, we would need to generalize `continuous_linear_map.cont_mdiff`
15+
(and `continuous_linear_map.cont_diff`) to semilinear maps.
16+
-/
17+
18+
noncomputable theory
19+
20+
open bundle set local_homeomorph continuous_linear_map pretrivialization
21+
open_locale manifold bundle
22+
23+
variables {𝕜 B F F₁ F₂ M M₁ M₂ : Type*}
24+
{E : B → Type*} {E₁ : B → Type*} {E₂ : B → Type*}
25+
[nontrivially_normed_field 𝕜]
26+
[∀ x, add_comm_monoid (E x)] [∀ x, module 𝕜 (E x)]
27+
[normed_add_comm_group F] [normed_space 𝕜 F]
28+
[topological_space (total_space E)] [∀ x, topological_space (E x)]
29+
[∀ x, add_comm_monoid (E₁ x)] [∀ x, module 𝕜 (E₁ x)]
30+
[normed_add_comm_group F₁] [normed_space 𝕜 F₁]
31+
[topological_space (total_space E₁)] [∀ x, topological_space (E₁ x)]
32+
[∀ x, add_comm_monoid (E₂ x)] [∀ x, module 𝕜 (E₂ x)]
33+
[normed_add_comm_group F₂] [normed_space 𝕜 F₂]
34+
[topological_space (total_space E₂)] [∀ x, topological_space (E₂ x)]
35+
36+
{EB : Type*} [normed_add_comm_group EB] [normed_space 𝕜 EB]
37+
{HB : Type*} [topological_space HB] (IB : model_with_corners 𝕜 EB HB)
38+
[topological_space B] [charted_space HB B]
39+
{EM : Type*} [normed_add_comm_group EM] [normed_space 𝕜 EM]
40+
{HM : Type*} [topological_space HM] {IM : model_with_corners 𝕜 EM HM}
41+
[topological_space M] [charted_space HM M] [Is : smooth_manifold_with_corners IM M]
42+
{n : ℕ∞}
43+
[fiber_bundle F₁ E₁] [vector_bundle 𝕜 F₁ E₁]
44+
[fiber_bundle F₂ E₂] [vector_bundle 𝕜 F₂ E₂]
45+
{e₁ e₁' : trivialization F₁ (π E₁)} {e₂ e₂' : trivialization F₂ (π E₂)}
46+
47+
local notation `LE₁E₂` := total_space (bundle.continuous_linear_map (ring_hom.id 𝕜) F₁ E₁ F₂ E₂)
48+
49+
/- This proof is slow, especially the `simp only` and the elaboration of `h₂`. -/
50+
lemma smooth_on_continuous_linear_map_coord_change
51+
[smooth_manifold_with_corners IB B]
52+
[smooth_vector_bundle F₁ E₁ IB] [smooth_vector_bundle F₂ E₂ IB]
53+
[mem_trivialization_atlas e₁] [mem_trivialization_atlas e₁']
54+
[mem_trivialization_atlas e₂] [mem_trivialization_atlas e₂'] :
55+
smooth_on IB 𝓘(𝕜, ((F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₂)))
56+
(continuous_linear_map_coord_change (ring_hom.id 𝕜) e₁ e₁' e₂ e₂')
57+
((e₁.base_set ∩ e₂.base_set) ∩ (e₁'.base_set ∩ e₂'.base_set)) :=
58+
begin
59+
let L₁ := compL 𝕜 F₁ F₂ F₂,
60+
have h₁ : smooth _ _ _ := L₁.cont_mdiff,
61+
have h₂ : smooth _ _ _ := (continuous_linear_map.flip (compL 𝕜 F₁ F₁ F₂)).cont_mdiff,
62+
have h₃ : smooth_on IB _ _ _ := smooth_on_coord_change e₁' e₁,
63+
have h₄ : smooth_on IB _ _ _ := smooth_on_coord_change e₂ e₂',
64+
refine ((h₁.comp_smooth_on (h₄.mono _)).clm_comp (h₂.comp_smooth_on (h₃.mono _))).congr _,
65+
{ mfld_set_tac },
66+
{ mfld_set_tac },
67+
{ intros b hb, ext L v,
68+
simp only [continuous_linear_map_coord_change, continuous_linear_equiv.coe_coe,
69+
continuous_linear_equiv.arrow_congrSL_apply, comp_apply, function.comp, compL_apply,
70+
flip_apply, continuous_linear_equiv.symm_symm] },
71+
end
72+
73+
variables [∀ x, has_continuous_add (E₂ x)] [∀ x, has_continuous_smul 𝕜 (E₂ x)]
74+
75+
lemma hom_chart (y₀ y : LE₁E₂) :
76+
chart_at (model_prod HB (F₁ →L[𝕜] F₂)) y₀ y =
77+
(chart_at HB y₀.1 y.1, in_coordinates F₁ E₁ F₂ E₂ y₀.1 y.1 y₀.1 y.1 y.2) :=
78+
by simp_rw [fiber_bundle.charted_space_chart_at, trans_apply, local_homeomorph.prod_apply,
79+
trivialization.coe_coe, local_homeomorph.refl_apply, function.id_def, hom_trivialization_at_apply]
80+
81+
variables {IB}
82+
83+
lemma cont_mdiff_at_hom_bundle (f : M → LE₁E₂) {x₀ : M} {n : ℕ∞} :
84+
cont_mdiff_at IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) n f x₀ ↔
85+
cont_mdiff_at IM IB n (λ x, (f x).1) x₀ ∧
86+
cont_mdiff_at IM 𝓘(𝕜, F₁ →L[𝕜] F₂) n
87+
(λ x, in_coordinates F₁ E₁ F₂ E₂ (f x₀).1 (f x).1 (f x₀).1 (f x).1 (f x).2) x₀ :=
88+
by apply cont_mdiff_at_total_space
89+
90+
lemma smooth_at_hom_bundle (f : M → LE₁E₂) {x₀ : M} :
91+
smooth_at IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) f x₀ ↔
92+
smooth_at IM IB (λ x, (f x).1) x₀ ∧
93+
smooth_at IM 𝓘(𝕜, F₁ →L[𝕜] F₂)
94+
(λ x, in_coordinates F₁ E₁ F₂ E₂ (f x₀).1 (f x).1 (f x₀).1 (f x).1 (f x).2) x₀ :=
95+
cont_mdiff_at_hom_bundle f
96+
97+
variables [smooth_manifold_with_corners IB B]
98+
[smooth_vector_bundle F₁ E₁ IB] [smooth_vector_bundle F₂ E₂ IB]
99+
100+
instance bundle.continuous_linear_map.vector_prebundle.is_smooth :
101+
(bundle.continuous_linear_map.vector_prebundle (ring_hom.id 𝕜) F₁ E₁ F₂ E₂).is_smooth IB :=
102+
{ exists_smooth_coord_change := begin
103+
rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩ _ ⟨e₁', e₂', he₁', he₂', rfl⟩,
104+
resetI,
105+
refine ⟨continuous_linear_map_coord_change (ring_hom.id 𝕜) e₁ e₁' e₂ e₂',
106+
smooth_on_continuous_linear_map_coord_change IB,
107+
continuous_linear_map_coord_change_apply (ring_hom.id 𝕜) e₁ e₁' e₂ e₂'⟩
108+
end }
109+
110+
/-- Todo: remove this definition. It is probably needed because of the type-class pi bug
111+
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/vector.20bundles.20--.20typeclass.20inference.20issue
112+
-/
113+
@[reducible]
114+
def smooth_vector_bundle.continuous_linear_map.aux (x) :
115+
topological_space (bundle.continuous_linear_map (ring_hom.id 𝕜) F₁ E₁ F₂ E₂ x) :=
116+
by apply_instance
117+
local attribute [instance, priority 1] smooth_vector_bundle.continuous_linear_map.aux
118+
119+
instance smooth_vector_bundle.continuous_linear_map :
120+
smooth_vector_bundle (F₁ →L[𝕜] F₂) (bundle.continuous_linear_map (ring_hom.id 𝕜) F₁ E₁ F₂ E₂)
121+
IB :=
122+
(bundle.continuous_linear_map.vector_prebundle (ring_hom.id 𝕜) F₁ E₁ F₂ E₂).smooth_vector_bundle IB

0 commit comments

Comments
 (0)