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

Commit be2c24f

Browse files
hrmacbethfpvandoorn
hrmacbeth
and
fpvandoorn
committed
feat(geometry/manifold/vector_bundle/basic): smooth vector bundles (#17611)
Definition of smooth vector bundle, and basic constructions (direct sum, pullback, core construction). Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
1 parent 7826122 commit be2c24f

13 files changed

Lines changed: 425 additions & 49 deletions

‎src/geometry/manifold/cont_mdiff.lean‎

Lines changed: 69 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -68,8 +68,11 @@ variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
6868
{F' : Type*} [normed_add_comm_group F'] [normed_space 𝕜 F']
6969
{G' : Type*} [topological_space G'] {J' : model_with_corners 𝕜 F' G'}
7070
{N' : Type*} [topological_space N'] [charted_space G' N'] [J's : smooth_manifold_with_corners J' N']
71-
-- F'' is a normed space
72-
{F'' : Type*} [normed_add_comm_group F''] [normed_space 𝕜 F'']
71+
-- F₁, F₂, F₃, F₄ are normed spaces
72+
{F₁ : Type*} [normed_add_comm_group F₁] [normed_space 𝕜 F₁]
73+
{F₂ : Type*} [normed_add_comm_group F₂] [normed_space 𝕜 F₂]
74+
{F₃ : Type*} [normed_add_comm_group F₃] [normed_space 𝕜 F₃]
75+
{F₄ : Type*} [normed_add_comm_group F₄] [normed_space 𝕜 F₄]
7376
-- declare functions, sets, points and smoothness indices
7477
{e : local_homeomorph M H} {e' : local_homeomorph M' H'}
7578
{f f₁ : M → M'} {s s₁ t : set M} {x : M} {m n : ℕ∞}
@@ -1623,31 +1626,80 @@ lemma continuous_linear_map.cont_mdiff (L : E →L[𝕜] F) :
16231626
cont_mdiff 𝓘(𝕜, E) 𝓘(𝕜, F) n L :=
16241627
L.cont_diff.cont_mdiff
16251628

1626-
-- 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 :=
1629+
lemma cont_mdiff_within_at.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : set M} {x : M}
1630+
(hg : cont_mdiff_within_at I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s x)
1631+
(hf : cont_mdiff_within_at I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s x) :
1632+
cont_mdiff_within_at I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (λ x, (g x).comp (f x)) s x :=
16311633
@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
1634+
(λ x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₁), x.1.comp x.2) (λ x, (g x, f x)) s _ x
16331635
(by { apply cont_diff.cont_diff_at, exact cont_diff_fst.clm_comp cont_diff_snd })
16341636
(hg.prod_mk_space hf) (by simp_rw [preimage_univ, subset_univ])
16351637

1636-
lemma cont_mdiff_at.clm_comp {g : M → F →L[𝕜] F''} {f : M → F' →L[𝕜] F} {x : M}
1637-
(hg : cont_mdiff_at I 𝓘(𝕜, F →L[𝕜] F'') n g x) (hf : cont_mdiff_at I 𝓘(𝕜, F' →L[𝕜] F) n f x) :
1638-
cont_mdiff_at I 𝓘(𝕜, F' →L[𝕜] F'') n (λ x, (g x).comp (f x)) x :=
1638+
lemma cont_mdiff_at.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {x : M}
1639+
(hg : cont_mdiff_at I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x) (hf : cont_mdiff_at I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f x) :
1640+
cont_mdiff_at I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (λ x, (g x).comp (f x)) x :=
16391641
(hg.cont_mdiff_within_at.clm_comp hf.cont_mdiff_within_at).cont_mdiff_at univ_mem
16401642

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 :=
1643+
lemma cont_mdiff_on.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : set M}
1644+
(hg : cont_mdiff_on I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s) (hf : cont_mdiff_on I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s) :
1645+
cont_mdiff_on I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (λ x, (g x).comp (f x)) s :=
16441646
λ x hx, (hg x hx).clm_comp (hf x hx)
16451647

1646-
lemma cont_mdiff.clm_comp {g : M → F →L[𝕜] F''} {f : M → F' →L[𝕜] F}
1647-
(hg : cont_mdiff I 𝓘(𝕜, F →L[𝕜] F'') n g) (hf : cont_mdiff I 𝓘(𝕜, F' →L[𝕜] F) n f) :
1648-
cont_mdiff I 𝓘(𝕜, F' →L[𝕜] F'') n (λ x, (g x).comp (f x)) :=
1648+
lemma cont_mdiff.clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁}
1649+
(hg : cont_mdiff I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g) (hf : cont_mdiff I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f) :
1650+
cont_mdiff I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (λ x, (g x).comp (f x)) :=
16491651
λ x, (hg x).clm_comp (hf x)
16501652

1653+
lemma cont_mdiff_within_at.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : set M} {x : M}
1654+
(hg : cont_mdiff_within_at I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x)
1655+
(hf : cont_mdiff_within_at I 𝓘(𝕜, F₁) n f s x) :
1656+
cont_mdiff_within_at I 𝓘(𝕜, F₂) n (λ x, g x (f x)) s x :=
1657+
@cont_diff_within_at.comp_cont_mdiff_within_at _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
1658+
(λ x : (F₁ →L[𝕜] F₂) × F₁, x.1 x.2) (λ x, (g x, f x)) s _ x
1659+
(by { apply cont_diff.cont_diff_at, exact cont_diff_fst.clm_apply cont_diff_snd })
1660+
(hg.prod_mk_space hf) (by simp_rw [preimage_univ, subset_univ])
1661+
1662+
lemma cont_mdiff_at.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M}
1663+
(hg : cont_mdiff_at I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g x) (hf : cont_mdiff_at I 𝓘(𝕜, F₁) n f x) :
1664+
cont_mdiff_at I 𝓘(𝕜, F₂) n (λ x, g x (f x)) x :=
1665+
(hg.cont_mdiff_within_at.clm_apply hf.cont_mdiff_within_at).cont_mdiff_at univ_mem
1666+
1667+
lemma cont_mdiff_on.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : set M}
1668+
(hg : cont_mdiff_on I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s) (hf : cont_mdiff_on I 𝓘(𝕜, F₁) n f s) :
1669+
cont_mdiff_on I 𝓘(𝕜, F₂) n (λ x, g x (f x)) s :=
1670+
λ x hx, (hg x hx).clm_apply (hf x hx)
1671+
1672+
lemma cont_mdiff.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁}
1673+
(hg : cont_mdiff I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g) (hf : cont_mdiff I 𝓘(𝕜, F₁) n f) :
1674+
cont_mdiff I 𝓘(𝕜, F₂) n (λ x, g x (f x)) :=
1675+
λ x, (hg x).clm_apply (hf x)
1676+
1677+
lemma cont_mdiff_within_at.clm_prod_map
1678+
{g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {s : set M} {x : M}
1679+
(hg : cont_mdiff_within_at I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s x)
1680+
(hf : cont_mdiff_within_at I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f s x) :
1681+
cont_mdiff_within_at I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n (λ x, (g x).prod_map (f x)) s x :=
1682+
@cont_diff_within_at.comp_cont_mdiff_within_at _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
1683+
(λ x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₄), x.1.prod_map x.2) (λ x, (g x, f x)) s _ x
1684+
(by { apply cont_diff.cont_diff_at,
1685+
exact (continuous_linear_map.prod_mapL 𝕜 F₁ F₃ F₂ F₄).cont_diff })
1686+
(hg.prod_mk_space hf) (by simp_rw [preimage_univ, subset_univ])
1687+
1688+
lemma cont_mdiff_at.clm_prod_map {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {x : M}
1689+
(hg : cont_mdiff_at I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x) (hf : cont_mdiff_at I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f x) :
1690+
cont_mdiff_at I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n (λ x, (g x).prod_map (f x)) x :=
1691+
(hg.cont_mdiff_within_at.clm_prod_map hf.cont_mdiff_within_at).cont_mdiff_at univ_mem
1692+
1693+
lemma cont_mdiff_on.clm_prod_map {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄} {s : set M}
1694+
(hg : cont_mdiff_on I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s) (hf : cont_mdiff_on I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f s) :
1695+
cont_mdiff_on I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n (λ x, (g x).prod_map (f x)) s :=
1696+
λ x hx, (hg x hx).clm_prod_map (hf x hx)
1697+
1698+
lemma cont_mdiff.clm_prod_map {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄}
1699+
(hg : cont_mdiff I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g) (hf : cont_mdiff I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f) :
1700+
cont_mdiff I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n (λ x, (g x).prod_map (f x)) :=
1701+
λ x, (hg x).clm_prod_map (hf x)
1702+
16511703
/-! ### Smoothness of standard operations -/
16521704

16531705
variables {V : Type*} [normed_add_comm_group V] [normed_space 𝕜 V]

‎src/geometry/manifold/cont_mdiff_map.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,11 @@ by cases f; cases g; cases h; refl
8484
@[ext] theorem ext (h : ∀ x, f x = g x) : f = g :=
8585
by cases f; cases g; congr'; exact funext h
8686

87+
instance : continuous_map_class C^n⟮I, M; I', M'⟯ M M' :=
88+
{ coe := (λ f, ⇑f),
89+
coe_injective' := coe_inj,
90+
map_continuous := λ f, f.cont_mdiff.continuous }
91+
8792
/-- The identity as a smooth map. -/
8893
def id : C^n⟮I, M; I, M⟯ := ⟨id, cont_mdiff_id⟩
8994

‎src/geometry/manifold/local_invariant_properties.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -678,6 +678,7 @@ variables {H₁ : Type*} [topological_space H₁] {H₂ : Type*} [topological_sp
678678
{G₁ : structure_groupoid H₁} [has_groupoid H₂ G₁] [closed_under_restriction G₁]
679679
(G₂ : structure_groupoid H₂) [has_groupoid H₃ G₂]
680680

681+
variables (G₂)
681682
lemma has_groupoid.comp
682683
(H : ∀ e ∈ G₂, lift_prop_on (is_local_structomorph_within_at G₁) (e : H₂ → H₂) e.source) :
683684
@has_groupoid H₁ _ H₃ _ (charted_space.comp H₁ H₂ H₃) G₁ :=

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

Lines changed: 230 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,230 @@
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.vector_bundle.fiberwise_linear
7+
import topology.vector_bundle.constructions
8+
9+
/-! # Smooth vector bundles
10+
11+
This file defines smooth vector bundles over a smooth manifold.
12+
13+
Let `E` be a topological vector bundle, with model fiber `F` and base space `B`. We consider `E` as
14+
carrying a charted space structure given by its trivializations -- these are charts to `B × F`.
15+
Then, by "composition", if `B` is itself a charted space over `H` (e.g. a smooth manifold), then `E`
16+
is also a charted space over `H × F`
17+
18+
Now, we define `smooth_vector_bundle` as the `Prop` of having smooth transition functions.
19+
Recall the structure groupoid `smooth_fiberwise_linear` on `B × F` consisting of smooth, fiberwise
20+
linear local homeomorphisms. We show that our definition of "smooth vector bundle" implies
21+
`has_groupoid` for this groupoid, and show (by a "composition" of `has_groupoid` instances) that
22+
this means that a smooth vector bundle is a smooth manifold.
23+
24+
Since `smooth_vector_bundle` is a mixin, it should be easy to make variants and for many such
25+
variants to coexist -- vector bundles can be smooth vector bundles over several different base
26+
fields, they can also be C^k vector bundles, etc.
27+
28+
## Main definitions and constructions
29+
30+
* `fiber_bundle.charted_space`: A fiber bundle `E` over a base `B` with model fiber `F` is naturally
31+
a charted space modelled on `B × F`.
32+
33+
* `fiber_bundle.charted_space'`: Let `B` be a charted space modelled on `HB`. Then a fiber bundle
34+
`E` over a base `B` with model fiber `F` is naturally a charted space modelled on `HB.prod F`.
35+
36+
* `smooth_vector_bundle`: Mixin class stating that a (topological) `vector_bundle` is smooth, in the
37+
sense of having smooth transition functions.
38+
39+
* `smooth_fiberwise_linear.has_groupoid`: For a smooth vector bundle `E` over `B` with fiber
40+
modelled on `F`, the change-of-co-ordinates between two trivializations `e`, `e'` for `E`,
41+
considered as charts to `B × F`, is smooth and fiberwise linear, in the sense of belonging to the
42+
structure groupoid `smooth_fiberwise_linear`.
43+
44+
* `bundle.total_space.smooth_manifold_with_corners`: A smooth vector bundle is naturally a smooth
45+
manifold.
46+
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.
50+
51+
* `bundle.prod.smooth_vector_bundle`: The direct sum of two smooth vector bundles is a smooth vector
52+
bundle.
53+
-/
54+
55+
assert_not_exists mfderiv
56+
57+
open bundle set local_homeomorph
58+
open_locale manifold bundle
59+
60+
variables {𝕜 B B' F M : Type*} {E : B → Type*}
61+
62+
/-! ### Charted space structure on a fiber bundle -/
63+
64+
section
65+
variables [topological_space F] [topological_space (total_space E)] [∀ x, topological_space (E x)]
66+
{HB : Type*} [topological_space HB]
67+
[topological_space B] [charted_space HB B]
68+
69+
/-- A fiber bundle `E` over a base `B` with model fiber `F` is naturally a charted space modelled on
70+
`B × F`. -/
71+
instance fiber_bundle.charted_space [fiber_bundle F E] :
72+
charted_space (B × F) (total_space E) :=
73+
{ atlas := (λ e : trivialization F (π E), e.to_local_homeomorph) '' trivialization_atlas F E,
74+
chart_at := λ x, (trivialization_at F E x.proj).to_local_homeomorph,
75+
mem_chart_source := λ x, (trivialization_at F E x.proj).mem_source.mpr
76+
(mem_base_set_trivialization_at F E x.proj),
77+
chart_mem_atlas := λ x, mem_image_of_mem _ (trivialization_mem_atlas F E _) }
78+
79+
local attribute [reducible] model_prod
80+
81+
/-- Let `B` be a charted space modelled on `HB`. Then a fiber bundle `E` over a base `B` with model
82+
fiber `F` is naturally a charted space modelled on `HB.prod F`. -/
83+
instance fiber_bundle.charted_space' [fiber_bundle F E] :
84+
charted_space (model_prod HB F) (total_space E) :=
85+
charted_space.comp _ (model_prod B F) _
86+
87+
end
88+
89+
/-! ### Smooth vector bundles -/
90+
91+
variables [nontrivially_normed_field 𝕜] [∀ x, add_comm_monoid (E x)] [∀ x, module 𝕜 (E x)]
92+
[normed_add_comm_group F] [normed_space 𝕜 F]
93+
[topological_space (total_space E)] [∀ x, topological_space (E x)]
94+
95+
{EB : Type*} [normed_add_comm_group EB] [normed_space 𝕜 EB]
96+
{HB : Type*} [topological_space HB] (IB : model_with_corners 𝕜 EB HB)
97+
[topological_space B] [charted_space HB B] [smooth_manifold_with_corners IB B]
98+
99+
variables (F E) [fiber_bundle F E] [vector_bundle 𝕜 F E]
100+
101+
/-- When `B` is a smooth manifold with corners with respect to a model `IB` and `E` is a
102+
topological vector bundle over `B` with fibers isomorphic to `F`, then `smooth_vector_bundle F E IB`
103+
registers that the bundle is smooth, in the sense of having smooth transition functions.
104+
This is a mixin, not carrying any new data`. -/
105+
class smooth_vector_bundle : Prop :=
106+
(smooth_on_coord_change : ∀ (e e' : trivialization F (π E))
107+
[mem_trivialization_atlas e] [mem_trivialization_atlas e'],
108+
smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (λ b : B, (e.coord_changeL 𝕜 e' b : F →L[𝕜] F))
109+
(e.base_set ∩ e'.base_set))
110+
111+
export smooth_vector_bundle (smooth_on_coord_change)
112+
113+
variables [smooth_vector_bundle F E IB]
114+
115+
116+
/-- For a smooth vector bundle `E` over `B` with fiber modelled on `F`, the change-of-co-ordinates
117+
between two trivializations `e`, `e'` for `E`, considered as charts to `B × F`, is smooth and
118+
fiberwise linear. -/
119+
instance : has_groupoid (total_space E) (smooth_fiberwise_linear B F IB) :=
120+
{ compatible := begin
121+
rintros _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩,
122+
haveI : mem_trivialization_atlas e := ⟨he⟩,
123+
haveI : mem_trivialization_atlas e' := ⟨he'⟩,
124+
resetI,
125+
rw mem_smooth_fiberwise_linear_iff,
126+
refine ⟨_, _, e.open_base_set.inter e'.open_base_set, smooth_on_coord_change e e', _, _, _⟩,
127+
{ rw inter_comm,
128+
apply cont_mdiff_on.congr (smooth_on_coord_change e' e),
129+
{ intros b hb,
130+
rw e.symm_coord_changeL e' hb },
131+
{ apply_instance },
132+
{ apply_instance }, },
133+
{ simp only [e.symm_trans_source_eq e', fiberwise_linear.local_homeomorph,
134+
trans_to_local_equiv, symm_to_local_equiv]},
135+
{ rintros ⟨b, v⟩ hb,
136+
have hb' : b ∈ e.base_set ∩ e'.base_set,
137+
{ simpa only [trans_to_local_equiv, symm_to_local_equiv, e.symm_trans_source_eq e',
138+
coe_coe_symm, prod_mk_mem_set_prod_eq, mem_univ, and_true] using hb },
139+
exact e.apply_symm_apply_eq_coord_changeL e' hb' v, }
140+
end }
141+
142+
/-- A smooth vector bundle `E` is naturally a smooth manifold. -/
143+
instance : smooth_manifold_with_corners (IB.prod 𝓘(𝕜, F)) (total_space E) :=
144+
begin
145+
refine { .. structure_groupoid.has_groupoid.comp (smooth_fiberwise_linear B F IB) _ },
146+
intros e he,
147+
rw mem_smooth_fiberwise_linear_iff at he,
148+
obtain ⟨φ, U, hU, hφ, h2φ, heφ⟩ := he,
149+
rw [is_local_structomorph_on_cont_diff_groupoid_iff],
150+
refine ⟨cont_mdiff_on.congr _ heφ.eq_on, cont_mdiff_on.congr _ heφ.symm'.eq_on⟩,
151+
{ rw heφ.source_eq,
152+
apply smooth_on_fst.prod_mk,
153+
exact (hφ.comp cont_mdiff_on_fst $ prod_subset_preimage_fst _ _).clm_apply cont_mdiff_on_snd },
154+
{ rw heφ.target_eq,
155+
apply smooth_on_fst.prod_mk,
156+
exact (h2φ.comp cont_mdiff_on_fst $ prod_subset_preimage_fst _ _).clm_apply cont_mdiff_on_snd },
157+
end
158+
159+
/-! ### Core construction for smooth vector bundles -/
160+
161+
namespace vector_bundle_core
162+
variables {ι : Type*} {F} (Z : vector_bundle_core 𝕜 B F ι)
163+
164+
/-- Mixin for a `vector_bundle_core` stating smoothness (of transition functions). -/
165+
class is_smooth (IB : model_with_corners 𝕜 EB HB) : Prop :=
166+
(smooth_on_coord_change [] :
167+
∀ i j, smooth_on IB 𝓘(𝕜, F →L[𝕜] F) (Z.coord_change i j) (Z.base_set i ∩ Z.base_set j))
168+
169+
export is_smooth (renaming smooth_on_coord_change → vector_bundle_core.smooth_on_coord_change)
170+
171+
variables [Z.is_smooth IB]
172+
173+
/-- If a `vector_bundle_core` has the `is_smooth` mixin, then the vector bundle constructed from it
174+
is a smooth vector bundle. -/
175+
instance smooth_vector_bundle : smooth_vector_bundle F Z.fiber IB :=
176+
{ smooth_on_coord_change := begin
177+
rintros - - ⟨i, rfl⟩ ⟨i', rfl⟩,
178+
refine (Z.smooth_on_coord_change IB i i').congr (λ b hb, _),
179+
ext v,
180+
exact Z.local_triv_coord_change_eq i i' hb v,
181+
end }
182+
183+
end vector_bundle_core
184+
185+
/-! ### The trivial smooth vector bundle -/
186+
187+
/-- A trivial vector bundle over a smooth manifold is a smooth vector bundle. -/
188+
instance bundle.trivial.smooth_vector_bundle : smooth_vector_bundle F (bundle.trivial B F) IB :=
189+
{ smooth_on_coord_change := begin
190+
introsI e e' he he',
191+
unfreezingI { obtain rfl := bundle.trivial.eq_trivialization B F e },
192+
unfreezingI { obtain rfl := bundle.trivial.eq_trivialization B F e' },
193+
simp_rw bundle.trivial.trivialization.coord_changeL,
194+
exact smooth_const.smooth_on
195+
end }
196+
197+
/-! ### Direct sums of smooth vector bundles -/
198+
199+
section prod
200+
variables (F₁ : Type*) [normed_add_comm_group F₁] [normed_space 𝕜 F₁]
201+
(E₁ : B → Type*) [topological_space (total_space E₁)]
202+
[Π x, add_comm_monoid (E₁ x)] [Π x, module 𝕜 (E₁ x)]
203+
204+
variables (F₂ : Type*) [normed_add_comm_group F₂] [normed_space 𝕜 F₂]
205+
(E₂ : B → Type*) [topological_space (total_space E₂)]
206+
[Π x, add_comm_monoid (E₂ x)] [Π x, module 𝕜 (E₂ x)]
207+
208+
variables [Π x : B, topological_space (E₁ x)] [Π x : B, topological_space (E₂ x)]
209+
[fiber_bundle F₁ E₁] [fiber_bundle F₂ E₂]
210+
[vector_bundle 𝕜 F₁ E₁] [vector_bundle 𝕜 F₂ E₂]
211+
[smooth_vector_bundle F₁ E₁ IB] [smooth_vector_bundle F₂ E₂ IB]
212+
213+
/-- The direct sum of two smooth vector bundles over the same base is a smooth vector bundle. -/
214+
instance bundle.prod.smooth_vector_bundle :
215+
smooth_vector_bundle (F₁ × F₂) (E₁ ×ᵇ E₂) IB :=
216+
{ smooth_on_coord_change := begin
217+
rintros _ _ ⟨e₁, e₂, i₁, i₂, rfl⟩ ⟨e₁', e₂', i₁', i₂', rfl⟩,
218+
resetI,
219+
rw [smooth_on],
220+
refine cont_mdiff_on.congr _ (e₁.coord_changeL_prod 𝕜 e₁' e₂ e₂'),
221+
refine cont_mdiff_on.clm_prod_map _ _,
222+
{ refine (smooth_on_coord_change e₁ e₁').mono _,
223+
simp only [trivialization.base_set_prod] with mfld_simps,
224+
mfld_set_tac },
225+
{ refine (smooth_on_coord_change e₂ e₂').mono _,
226+
simp only [trivialization.base_set_prod] with mfld_simps,
227+
mfld_set_tac },
228+
end }
229+
230+
end prod

0 commit comments

Comments
 (0)