-
Notifications
You must be signed in to change notification settings - Fork 297
/
circle.lean
112 lines (90 loc) · 4.92 KB
/
circle.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
/-
Copyright (c) 2021 Heather Macbeth. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Heather Macbeth
-/
import geometry.manifold.instances.sphere
/-!
# The circle
This file defines `circle` to be the metric sphere (`metric.sphere`) in `ℂ` centred at `0` of
radius `1`. We equip it with the following structure:
* a submonoid of `ℂ`
* a group
* a topological group
* a charted space with model space `euclidean_space ℝ (fin 1)` (inherited from `metric.sphere`)
* a Lie group with model with corners `𝓡 1`
We furthermore define `exp_map_circle` to be the natural map `λ t, exp (t * I)` from `ℝ` to
`circle`, and show that this map is a group homomorphism and is smooth.
## Implementation notes
To borrow the smooth manifold structure cleanly, the circle needs to be defined using
`metric.sphere`, and therefore the underlying set is `{z : ℂ | abs (z - 0) = 1}`. This prevents
certain algebraic facts from working definitionally -- for example, the circle is not defeq to
`{z : ℂ | abs z = 1}`, which is the kernel of `complex.abs` considered as a homomorphism from `ℂ`
to `ℝ`, nor is it defeq to `{z : ℂ | norm_sq z = 1}`, which is the kernel of the homomorphism
`complex.norm_sq` from `ℂ` to `ℝ`.
-/
noncomputable theory
open complex finite_dimensional metric
open_locale manifold
local attribute [instance] findim_real_complex_fact
/-- The unit circle in `ℂ`, here given the structure of a submonoid of `ℂ`. -/
def circle : submonoid ℂ :=
{ carrier := sphere (0:ℂ) 1,
one_mem' := by simp,
mul_mem' := λ a b, begin
simp only [norm_eq_abs, mem_sphere_zero_iff_norm],
intros ha hb,
simp [ha, hb],
end }
@[simp] lemma mem_circle_iff_abs (z : ℂ) : z ∈ circle ↔ abs z = 1 := mem_sphere_zero_iff_norm
lemma circle_def : ↑circle = {z : ℂ | abs z = 1} := by { ext, simp }
@[simp] lemma abs_eq_of_mem_circle (z : circle) : abs z = 1 := by { convert z.2, simp }
instance : group circle :=
{ inv := λ z, ⟨conj z, by simp⟩,
mul_left_inv := λ z, subtype.ext $ by { simp [has_inv.inv, ← norm_sq_eq_conj_mul_self,
← mul_self_abs] },
.. circle.to_monoid }
@[simp] lemma coe_inv_circle (z : circle) : ↑(z⁻¹) = conj z := rfl
@[simp] lemma coe_div_circle (z w : circle) : ↑(z / w) = ↑z * conj w := rfl
-- the following result could instead be deduced from the Lie group structure on the circle using
-- `topological_group_of_lie_group`, but that seems a little awkward since one has to first provide
-- and then forget the model space
instance : topological_group circle :=
{ continuous_mul := let h : continuous (λ x : circle, (x : ℂ)) := continuous_subtype_coe in
continuous_induced_rng (continuous_mul.comp (h.prod_map h)),
continuous_inv := continuous_induced_rng $
complex.conj_clm.continuous.comp continuous_subtype_coe }
/-- The unit circle in `ℂ` is a charted space modelled on `euclidean_space ℝ (fin 1)`. This
follows by definition from the corresponding result for `metric.sphere`. -/
instance : charted_space (euclidean_space ℝ (fin 1)) circle := metric.sphere.charted_space
/-- The unit circle in `ℂ` is a Lie group. -/
instance : lie_group (𝓡 1) circle :=
{ smooth_mul := begin
let c : circle → ℂ := coe,
have h₁ : times_cont_mdiff _ _ _ (prod.map c c) :=
times_cont_mdiff_coe_sphere.prod_map times_cont_mdiff_coe_sphere,
have h₂ : times_cont_mdiff (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ)) 𝓘(ℝ, ℂ) ∞ (λ (z : ℂ × ℂ), z.fst * z.snd),
{ rw times_cont_mdiff_iff,
exact ⟨continuous_mul, λ x y, (times_cont_diff_mul.restrict_scalars ℝ).times_cont_diff_on⟩ },
convert (h₂.comp h₁).cod_restrict_sphere _,
convert smooth_manifold_with_corners.prod circle circle,
{ exact metric.sphere.smooth_manifold_with_corners },
{ exact metric.sphere.smooth_manifold_with_corners }
end,
smooth_inv := (complex.conj_clm.times_cont_diff.times_cont_mdiff.comp
times_cont_mdiff_coe_sphere).cod_restrict_sphere _,
.. metric.sphere.smooth_manifold_with_corners }
/-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ`. -/
def exp_map_circle (t : ℝ) : circle :=
⟨exp (t * I), by simp [exp_mul_I, abs_cos_add_sin_mul_I]⟩
/-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ`, considered as a homomorphism of
groups. -/
def exp_map_circle_hom : ℝ →+ (additive circle) :=
{ to_fun := exp_map_circle,
map_zero' := by { rw exp_map_circle, convert of_mul_one, simp },
map_add' := λ x y, show exp_map_circle (x + y) = (exp_map_circle x) * (exp_map_circle y),
from subtype.ext $ by simp [exp_map_circle, exp_add, add_mul] }
/-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ` is smooth. -/
lemma times_cont_mdiff_exp_map_circle : times_cont_mdiff 𝓘(ℝ, ℝ) (𝓡 1) ∞ exp_map_circle :=
(((times_cont_diff_exp.restrict_scalars ℝ).comp
(times_cont_diff_id.smul times_cont_diff_const)).times_cont_mdiff).cod_restrict_sphere _