Skip to content

Commit 2363852

Browse files
urkudurkud
committed
feat: port Geometry.Manifold.Algebra.LieGroup (#5439)
1 parent 21fb5ac commit 2363852

File tree

2 files changed

+232
-0
lines changed

2 files changed

+232
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1813,6 +1813,7 @@ import Mathlib.Geometry.Euclidean.Sphere.Power
18131813
import Mathlib.Geometry.Euclidean.Sphere.Ptolemy
18141814
import Mathlib.Geometry.Euclidean.Sphere.SecondInter
18151815
import Mathlib.Geometry.Euclidean.Triangle
1816+
import Mathlib.Geometry.Manifold.Algebra.LieGroup
18161817
import Mathlib.Geometry.Manifold.Algebra.Monoid
18171818
import Mathlib.Geometry.Manifold.BumpFunction
18181819
import Mathlib.Geometry.Manifold.ChartedSpace

‎Mathlib/Geometry/Manifold/Algebra/LieGroup.lean‎

Lines changed: 231 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,231 @@
1+
/-
2+
Copyright © 2020 Nicolò Cavalleri. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Nicolò Cavalleri
5+
6+
! This file was ported from Lean 3 source module geometry.manifold.algebra.lie_group
7+
! leanprover-community/mathlib commit f9ec187127cc5b381dfcf5f4a22dacca4c20b63d
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Geometry.Manifold.Algebra.Monoid
12+
13+
/-!
14+
# Lie groups
15+
16+
A Lie group is a group that is also a smooth manifold, in which the group operations of
17+
multiplication and inversion are smooth maps. Smoothness of the group multiplication means that
18+
multiplication is a smooth mapping of the product manifold `G` × `G` into `G`.
19+
20+
Note that, since a manifold here is not second-countable and Hausdorff a Lie group here is not
21+
guaranteed to be second-countable (even though it can be proved it is Hausdorff). Note also that Lie
22+
groups here are not necessarily finite dimensional.
23+
24+
## Main definitions and statements
25+
26+
* `LieAddGroup I G` : a Lie additive group where `G` is a manifold on the model with corners `I`.
27+
* `LieGroup I G` : a Lie multiplicative group where `G` is a manifold on the model with
28+
corners `I`.
29+
* `normedSpaceLieAddGroup` : a normed vector space over a nontrivially normed field
30+
is an additive Lie group.
31+
32+
## Implementation notes
33+
34+
A priori, a Lie group here is a manifold with corners.
35+
36+
The definition of Lie group cannot require `I : ModelWithCorners 𝕜 E E` with the same space as the
37+
model space and as the model vector space, as one might hope, beause in the product situation,
38+
the model space is `ModelProd E E'` and the model vector space is `E × E'`, which are not the same,
39+
so the definition does not apply. Hence the definition should be more general, allowing
40+
`I : ModelWithCorners 𝕜 E H`.
41+
-/
42+
43+
44+
noncomputable section
45+
46+
open scoped Manifold
47+
48+
-- See note [Design choices about smooth algebraic structures]
49+
/-- A Lie (additive) group is a group and a smooth manifold at the same time in which
50+
the addition and negation operations are smooth. -/
51+
class LieAddGroup {𝕜 : Type _} [NontriviallyNormedField 𝕜] {H : Type _} [TopologicalSpace H]
52+
{E : Type _} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type _)
53+
[AddGroup G] [TopologicalSpace G] [ChartedSpace H G] extends HasSmoothAdd I G : Prop where
54+
smooth_neg : Smooth I I fun a : G => -a
55+
#align lie_add_group LieAddGroup
56+
57+
-- See note [Design choices about smooth algebraic structures]
58+
/-- A Lie group is a group and a smooth manifold at the same time in which
59+
the multiplication and inverse operations are smooth. -/
60+
@[to_additive]
61+
class LieGroup {𝕜 : Type _} [NontriviallyNormedField 𝕜] {H : Type _} [TopologicalSpace H]
62+
{E : Type _} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (G : Type _)
63+
[Group G] [TopologicalSpace G] [ChartedSpace H G] extends HasSmoothMul I G : Prop where
64+
smooth_inv : Smooth I I fun a : G => a⁻¹
65+
#align lie_group LieGroup
66+
67+
section LieGroup
68+
69+
variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {H : Type _} [TopologicalSpace H] {E : Type _}
70+
[NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {F : Type _}
71+
[NormedAddCommGroup F] [NormedSpace 𝕜 F] {J : ModelWithCorners 𝕜 F F} {G : Type _}
72+
[TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type _}
73+
[NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type _} [TopologicalSpace H']
74+
{I' : ModelWithCorners 𝕜 E' H'} {M : Type _} [TopologicalSpace M] [ChartedSpace H' M]
75+
{E'' : Type _} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type _} [TopologicalSpace H'']
76+
{I'' : ModelWithCorners 𝕜 E'' H''} {M' : Type _} [TopologicalSpace M'] [ChartedSpace H'' M']
77+
{n : ℕ∞}
78+
79+
section
80+
81+
variable (I)
82+
83+
@[to_additive]
84+
theorem smooth_inv : Smooth I I fun x : G => x⁻¹ :=
85+
LieGroup.smooth_inv
86+
#align smooth_inv smooth_inv
87+
#align smooth_neg smooth_neg
88+
89+
/-- A Lie group is a topological group. This is not an instance for technical reasons,
90+
see note [Design choices about smooth algebraic structures]. -/
91+
@[to_additive "An additive Lie group is an additive topological group. This is not an instance for
92+
technical reasons, see note [Design choices about smooth algebraic structures]."]
93+
theorem topologicalGroup_of_lieGroup : TopologicalGroup G :=
94+
{ continuousMul_of_smooth I with continuous_inv := (smooth_inv I).continuous }
95+
#align topological_group_of_lie_group topologicalGroup_of_lieGroup
96+
#align topological_add_group_of_lie_add_group topologicalAddGroup_of_lieAddGroup
97+
98+
end
99+
100+
@[to_additive]
101+
theorem ContMDiffWithinAt.inv {f : M → G} {s : Set M} {x₀ : M}
102+
(hf : ContMDiffWithinAt I' I n f s x₀) : ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s x₀ :=
103+
((smooth_inv I).of_le le_top).contMDiffAt.contMDiffWithinAt.comp x₀ hf <| Set.mapsTo_univ _ _
104+
#align cont_mdiff_within_at.inv ContMDiffWithinAt.inv
105+
#align cont_mdiff_within_at.neg ContMDiffWithinAt.neg
106+
107+
@[to_additive]
108+
theorem ContMDiffAt.inv {f : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) :
109+
ContMDiffAt I' I n (fun x => (f x)⁻¹) x₀ :=
110+
((smooth_inv I).of_le le_top).contMDiffAt.comp x₀ hf
111+
#align cont_mdiff_at.inv ContMDiffAt.inv
112+
#align cont_mdiff_at.neg ContMDiffAt.neg
113+
114+
@[to_additive]
115+
theorem ContMDiffOn.inv {f : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s) :
116+
ContMDiffOn I' I n (fun x => (f x)⁻¹) s := fun x hx => (hf x hx).inv
117+
#align cont_mdiff_on.inv ContMDiffOn.inv
118+
#align cont_mdiff_on.neg ContMDiffOn.neg
119+
120+
@[to_additive]
121+
theorem ContMDiff.inv {f : M → G} (hf : ContMDiff I' I n f) : ContMDiff I' I n fun x => (f x)⁻¹ :=
122+
fun x => (hf x).inv
123+
#align cont_mdiff.inv ContMDiff.inv
124+
#align cont_mdiff.neg ContMDiff.neg
125+
126+
@[to_additive]
127+
nonrec theorem SmoothWithinAt.inv {f : M → G} {s : Set M} {x₀ : M}
128+
(hf : SmoothWithinAt I' I f s x₀) : SmoothWithinAt I' I (fun x => (f x)⁻¹) s x₀ :=
129+
hf.inv
130+
#align smooth_within_at.inv SmoothWithinAt.inv
131+
#align smooth_within_at.neg SmoothWithinAt.neg
132+
133+
@[to_additive]
134+
nonrec theorem SmoothAt.inv {f : M → G} {x₀ : M} (hf : SmoothAt I' I f x₀) :
135+
SmoothAt I' I (fun x => (f x)⁻¹) x₀ :=
136+
hf.inv
137+
#align smooth_at.inv SmoothAt.inv
138+
#align smooth_at.neg SmoothAt.neg
139+
140+
@[to_additive]
141+
nonrec theorem SmoothOn.inv {f : M → G} {s : Set M} (hf : SmoothOn I' I f s) :
142+
SmoothOn I' I (fun x => (f x)⁻¹) s :=
143+
hf.inv
144+
#align smooth_on.inv SmoothOn.inv
145+
#align smooth_on.neg SmoothOn.neg
146+
147+
@[to_additive]
148+
nonrec theorem Smooth.inv {f : M → G} (hf : Smooth I' I f) : Smooth I' I fun x => (f x)⁻¹ :=
149+
hf.inv
150+
#align smooth.inv Smooth.inv
151+
#align smooth.neg Smooth.neg
152+
153+
@[to_additive]
154+
theorem ContMDiffWithinAt.div {f g : M → G} {s : Set M} {x₀ : M}
155+
(hf : ContMDiffWithinAt I' I n f s x₀) (hg : ContMDiffWithinAt I' I n g s x₀) :
156+
ContMDiffWithinAt I' I n (fun x => f x / g x) s x₀ := by
157+
simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv
158+
#align cont_mdiff_within_at.div ContMDiffWithinAt.div
159+
#align cont_mdiff_within_at.sub ContMDiffWithinAt.sub
160+
161+
@[to_additive]
162+
theorem ContMDiffAt.div {f g : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀)
163+
(hg : ContMDiffAt I' I n g x₀) : ContMDiffAt I' I n (fun x => f x / g x) x₀ := by
164+
simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv
165+
#align cont_mdiff_at.div ContMDiffAt.div
166+
#align cont_mdiff_at.sub ContMDiffAt.sub
167+
168+
@[to_additive]
169+
theorem ContMDiffOn.div {f g : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s)
170+
(hg : ContMDiffOn I' I n g s) : ContMDiffOn I' I n (fun x => f x / g x) s := by
171+
simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv
172+
#align cont_mdiff_on.div ContMDiffOn.div
173+
#align cont_mdiff_on.sub ContMDiffOn.sub
174+
175+
@[to_additive]
176+
theorem ContMDiff.div {f g : M → G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
177+
ContMDiff I' I n fun x => f x / g x := by simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv
178+
#align cont_mdiff.div ContMDiff.div
179+
#align cont_mdiff.sub ContMDiff.sub
180+
181+
@[to_additive]
182+
nonrec theorem SmoothWithinAt.div {f g : M → G} {s : Set M} {x₀ : M}
183+
(hf : SmoothWithinAt I' I f s x₀) (hg : SmoothWithinAt I' I g s x₀) :
184+
SmoothWithinAt I' I (fun x => f x / g x) s x₀ :=
185+
hf.div hg
186+
#align smooth_within_at.div SmoothWithinAt.div
187+
#align smooth_within_at.sub SmoothWithinAt.sub
188+
189+
@[to_additive]
190+
nonrec theorem SmoothAt.div {f g : M → G} {x₀ : M} (hf : SmoothAt I' I f x₀)
191+
(hg : SmoothAt I' I g x₀) : SmoothAt I' I (fun x => f x / g x) x₀ :=
192+
hf.div hg
193+
#align smooth_at.div SmoothAt.div
194+
#align smooth_at.sub SmoothAt.sub
195+
196+
@[to_additive]
197+
nonrec theorem SmoothOn.div {f g : M → G} {s : Set M} (hf : SmoothOn I' I f s)
198+
(hg : SmoothOn I' I g s) : SmoothOn I' I (f / g) s :=
199+
hf.div hg
200+
#align smooth_on.div SmoothOn.div
201+
#align smooth_on.sub SmoothOn.sub
202+
203+
@[to_additive]
204+
nonrec theorem Smooth.div {f g : M → G} (hf : Smooth I' I f) (hg : Smooth I' I g) :
205+
Smooth I' I (f / g) :=
206+
hf.div hg
207+
#align smooth.div Smooth.div
208+
#align smooth.sub Smooth.sub
209+
210+
end LieGroup
211+
212+
section ProdLieGroup
213+
214+
-- Instance of product group
215+
@[to_additive]
216+
instance {𝕜 : Type _} [NontriviallyNormedField 𝕜] {H : Type _} [TopologicalSpace H] {E : Type _}
217+
[NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type _}
218+
[TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I G] {E' : Type _}
219+
[NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type _} [TopologicalSpace H']
220+
{I' : ModelWithCorners 𝕜 E' H'} {G' : Type _} [TopologicalSpace G'] [ChartedSpace H' G']
221+
[Group G'] [LieGroup I' G'] : LieGroup (I.prod I') (G × G') :=
222+
{ HasSmoothMul.prod _ _ _ _ with smooth_inv := smooth_fst.inv.prod_mk smooth_snd.inv }
223+
224+
end ProdLieGroup
225+
226+
/-! ### Normed spaces are Lie groups -/
227+
228+
instance normedSpaceLieAddGroup {𝕜 : Type _} [NontriviallyNormedField 𝕜] {E : Type _}
229+
[NormedAddCommGroup E] [NormedSpace 𝕜 E] : LieAddGroup 𝓘(𝕜, E) E where
230+
smooth_neg := contDiff_neg.contMDiff
231+
#align normed_space_lie_add_group normedSpaceLieAddGroup

0 commit comments

Comments
 (0)