/
smooth_section.lean
213 lines (170 loc) · 7.2 KB
/
smooth_section.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
/-
Copyright © 2023 Heather Macbeth. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Heather Macbeth, Floris van Doorn
-/
import geometry.manifold.cont_mdiff_mfderiv
import topology.continuous_function.basic
import geometry.manifold.algebra.lie_group
/-!
# Smooth sections
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
In this file we define the type `cont_mdiff_section` of `n` times continuously differentiable
sections of a smooth vector bundle over a manifold `M` and prove that it's a module.
-/
open bundle filter function
open_locale bundle manifold
variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
{E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E]
{E' : Type*} [normed_add_comm_group E'] [normed_space 𝕜 E']
{H : Type*} [topological_space H]
{H' : Type*} [topological_space H']
(I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H')
{M : Type*} [topological_space M] [charted_space H M]
{M' : Type*} [topological_space M'] [charted_space H' M']
{E'' : Type*} [normed_add_comm_group E''] [normed_space 𝕜 E'']
{H'' : Type*} [topological_space H'']
{I'' : model_with_corners 𝕜 E'' H''}
{M'' : Type*} [topological_space M''] [charted_space H'' M'']
[smooth_manifold_with_corners I M]
variables (F : Type*) [normed_add_comm_group F] [normed_space 𝕜 F] -- `F` model fiber
(n : ℕ∞)
(V : M → Type*) [topological_space (total_space F V)] -- `V` vector bundle
[Π x, add_comm_group (V x)] [Π x, module 𝕜 (V x)]
variables [Π x : M, topological_space (V x)]
[fiber_bundle F V]
[vector_bundle 𝕜 F V]
[smooth_vector_bundle F V I]
/-- Bundled `n` times continuously differentiable sections of a vector bundle. -/
@[protect_proj]
structure cont_mdiff_section :=
(to_fun : Π x, V x)
(cont_mdiff_to_fun : cont_mdiff I (I.prod 𝓘(𝕜, F)) n (λ x, total_space.mk' F x (to_fun x)))
/-- Bundled smooth sections of a vector bundle. -/
@[reducible] def smooth_section := cont_mdiff_section I F ⊤ V
localized "notation (name := cont_mdiff_section) `Cₛ^` n `⟮` I `; ` F `, ` V `⟯` :=
cont_mdiff_section I F n V" in manifold
namespace cont_mdiff_section
variables {I} {I'} {n} {F} {V}
instance : has_coe_to_fun Cₛ^n⟮I; F, V⟯ (λ s, Π x, V x) := ⟨cont_mdiff_section.to_fun⟩
variables {s t : Cₛ^n⟮I; F, V⟯}
@[simp] lemma coe_fn_mk (s : Π x, V x)
(hs : cont_mdiff I (I.prod 𝓘(𝕜, F)) n (λ x, total_space.mk x (s x))) :
(mk s hs : Π x, V x) = s :=
rfl
protected lemma cont_mdiff (s : Cₛ^n⟮I; F, V⟯) :
cont_mdiff I (I.prod 𝓘(𝕜, F)) n (λ x, total_space.mk' F x (s x : V x)) := s.cont_mdiff_to_fun
protected lemma smooth (s : Cₛ^∞⟮I; F, V⟯) :
smooth I (I.prod 𝓘(𝕜, F)) (λ x, total_space.mk' F x (s x : V x)) := s.cont_mdiff_to_fun
protected lemma mdifferentiable' (s : Cₛ^n⟮I; F, V⟯) (hn : 1 ≤ n) :
mdifferentiable I (I.prod 𝓘(𝕜, F)) (λ x, total_space.mk' F x (s x : V x)) :=
s.cont_mdiff.mdifferentiable hn
protected lemma mdifferentiable (s : Cₛ^∞⟮I; F, V⟯) :
mdifferentiable I (I.prod 𝓘(𝕜, F)) (λ x, total_space.mk' F x (s x : V x)) :=
s.cont_mdiff.mdifferentiable le_top
protected lemma mdifferentiable_at (s : Cₛ^∞⟮I; F, V⟯) {x} :
mdifferentiable_at I (I.prod 𝓘(𝕜, F)) (λ x, total_space.mk' F x (s x : V x)) x :=
s.mdifferentiable x
lemma coe_inj ⦃s t : Cₛ^n⟮I; F, V⟯⦄ (h : (s : Π x, V x) = t) : s = t :=
by cases s; cases t; cases h; refl
lemma coe_injective : injective (coe_fn : Cₛ^n⟮I; F, V⟯ → Π x, V x) :=
coe_inj
@[ext] theorem ext (h : ∀ x, s x = t x) : s = t :=
by cases s; cases t; congr'; exact funext h
instance has_add : has_add Cₛ^n⟮I; F, V⟯ :=
begin
refine ⟨λ s t, ⟨s + t, _⟩⟩,
intro x₀,
have hs := s.cont_mdiff x₀,
have ht := t.cont_mdiff x₀,
rw [cont_mdiff_at_section] at hs ht ⊢,
set e := trivialization_at F V x₀,
refine (hs.add ht).congr_of_eventually_eq _,
refine eventually_of_mem (e.open_base_set.mem_nhds $ mem_base_set_trivialization_at F V x₀) _,
intros x hx,
apply (e.linear 𝕜 hx).1,
end
@[simp]
lemma coe_add (s t : Cₛ^n⟮I; F, V⟯) : ⇑(s + t) = s + t := rfl
instance has_sub : has_sub Cₛ^n⟮I; F, V⟯ :=
begin
refine ⟨λ s t, ⟨s - t, _⟩⟩,
intro x₀,
have hs := s.cont_mdiff x₀,
have ht := t.cont_mdiff x₀,
rw [cont_mdiff_at_section] at hs ht ⊢,
set e := trivialization_at F V x₀,
refine (hs.sub ht).congr_of_eventually_eq _,
refine eventually_of_mem (e.open_base_set.mem_nhds $ mem_base_set_trivialization_at F V x₀) _,
intros x hx,
apply (e.linear 𝕜 hx).map_sub,
end
@[simp]
lemma coe_sub (s t : Cₛ^n⟮I; F, V⟯) : ⇑(s - t) = s - t := rfl
instance has_zero : has_zero Cₛ^n⟮I; F, V⟯ :=
⟨⟨λ x, 0, (smooth_zero_section 𝕜 V).of_le le_top⟩⟩
instance inhabited : inhabited Cₛ^n⟮I; F, V⟯ := ⟨0⟩
@[simp]
lemma coe_zero : ⇑(0 : Cₛ^n⟮I; F, V⟯) = 0 := rfl
instance has_smul : has_smul 𝕜 Cₛ^n⟮I; F, V⟯ :=
begin
refine ⟨λ c s, ⟨c • s, _⟩⟩,
intro x₀,
have hs := s.cont_mdiff x₀,
rw [cont_mdiff_at_section] at hs ⊢,
set e := trivialization_at F V x₀,
refine (cont_mdiff_at_const.smul hs).congr_of_eventually_eq _,
{ exact c },
refine eventually_of_mem (e.open_base_set.mem_nhds $ mem_base_set_trivialization_at F V x₀) _,
intros x hx,
apply (e.linear 𝕜 hx).2,
end
@[simp]
lemma coe_smul (r : 𝕜) (s : Cₛ^n⟮I; F, V⟯) : ⇑(r • s : Cₛ^n⟮I; F, V⟯) = r • s := rfl
instance has_neg : has_neg Cₛ^n⟮I; F, V⟯ :=
begin
refine ⟨λ s, ⟨- s, _⟩⟩,
intro x₀,
have hs := s.cont_mdiff x₀,
rw [cont_mdiff_at_section] at hs ⊢,
set e := trivialization_at F V x₀,
refine hs.neg.congr_of_eventually_eq _,
refine eventually_of_mem (e.open_base_set.mem_nhds $ mem_base_set_trivialization_at F V x₀) _,
intros x hx,
apply (e.linear 𝕜 hx).map_neg
end
@[simp]
lemma coe_neg (s : Cₛ^n⟮I; F, V⟯) : ⇑(- s : Cₛ^n⟮I; F, V⟯) = - s := rfl
instance has_nsmul : has_smul ℕ Cₛ^n⟮I; F, V⟯ :=
⟨nsmul_rec⟩
@[simp]
lemma coe_nsmul (s : Cₛ^n⟮I; F, V⟯) (k : ℕ) : ⇑(k • s : Cₛ^n⟮I; F, V⟯) = k • s :=
begin
induction k with k ih,
{ simp_rw [zero_smul], refl },
simp_rw [succ_nsmul, ← ih], refl,
end
instance has_zsmul : has_smul ℤ Cₛ^n⟮I; F, V⟯ :=
⟨zsmul_rec⟩
@[simp]
lemma coe_zsmul (s : Cₛ^n⟮I; F, V⟯) (z : ℤ) : ⇑(z • s : Cₛ^n⟮I; F, V⟯) = z • s :=
begin
cases z with n n,
refine (coe_nsmul s n).trans _,
simp only [int.of_nat_eq_coe, coe_nat_zsmul],
refine (congr_arg has_neg.neg (coe_nsmul s (n+1))).trans _,
simp only [zsmul_neg_succ_of_nat, neg_inj]
end
instance add_comm_group : add_comm_group Cₛ^n⟮I; F, V⟯ :=
coe_injective.add_comm_group _ coe_zero coe_add coe_neg coe_sub coe_nsmul coe_zsmul
variables (I F V n)
/-- The additive morphism from smooth sections to dependent maps. -/
def coe_add_hom : Cₛ^n⟮I; F, V⟯ →+ Π x, V x :=
{ to_fun := coe_fn,
map_zero' := coe_zero,
map_add' := coe_add }
variables {I F V n}
instance module : module 𝕜 Cₛ^n⟮I; F, V⟯ :=
coe_injective.module 𝕜 (coe_add_hom I F n V) coe_smul
end cont_mdiff_section