SmithCyclic.lean

1 import KomorebiPaperV.SmithAction
2 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
3 
4 /-! Author: Komorebi P. The cyclic Smith action on the full projective line. -/
5 namespace KomorebiPaperV.SmithCyclic
6 open KomorebiPaperV.SmithAction
7 
8 noncomputable def omega (N : ℕ) : ℂ := Complex.exp (2 * Real.pi * Complex.I / N)
9 
10 theorem omega_ne_zero (N : ℕ) : omega N ≠ 0 := Complex.exp_ne_zero _
11 
12 theorem omega_pow (N : ℕ) (hN : 0 < N) : omega N ^ N = 1 := by
13   rw [omega, ← Complex.exp_nat_mul]
14   have hNc : (N : ℂ) ≠ 0 := by exact_mod_cast hN.ne'
15   have he : (N : ℂ) * (2 * Real.pi * Complex.I / N) = 2 * Real.pi * Complex.I := by
16     field_simp
17   rw [he, Complex.exp_two_pi_mul_I]
18 
19 theorem omega_two : omega 2 = -1 := by
20   unfold omega
21   convert Complex.exp_pi_mul_I using 1; congr 1; ring
22 
23 abbrev Point := {p : ℂ × ℂ // p ≠ 0}
24 
25 def same (p q : Point) : Prop := ∃ c : ℂ, c ≠ 0 ∧ q.val = (c * p.val.1, c * p.val.2)
26 
27 noncomputable def pointSetoid : Setoid Point where
28   r := same
29   iseqv := {
30     refl := by intro p; exact ⟨1, one_ne_zero, by simp⟩
31     symm := by
32       rintro p q ⟨c, hc, hq⟩
33       refine ⟨c⁻¹, inv_ne_zero hc, ?_⟩
34       rw [hq]
35       simp [hc]
36     trans := by
37       rintro p q r ⟨c, hc, hq⟩ ⟨d, hd, hr⟩
38       exact ⟨d*c, mul_ne_zero hd hc, by rw [hr, hq]; simp [mul_assoc]⟩ }
39 
40 abbrev Projective := Quotient pointSetoid
41 
42 noncomputable def pointAction (a : ℂ) (ha : a ≠ 0) (p : Point) : Point :=
43   ⟨action a p.val, action_nonzero a ha p.val p.property⟩
44 
45 theorem action_respects_scaling (a : ℂ) (ha : a ≠ 0) (p q : Point) (h : same p q) :
46     same (pointAction a ha p) (pointAction a ha q) := by
47   obtain ⟨c, hc, hq⟩ := h
48   refine ⟨c, hc, ?_⟩
49   change action a q.val = _
50   rw [hq, action_scale]
51   rfl
52 
53 noncomputable def projectiveAction (a : ℂ) (ha : a ≠ 0) : Projective → Projective :=
54   Quotient.map (pointAction a ha) (action_respects_scaling a ha)
55 
56 theorem projective_mul (a b : ℂ) (ha : a ≠ 0) (hb : b ≠ 0) (p : Projective) :
57     projectiveAction a ha (projectiveAction b hb p) =
58       projectiveAction (a*b) (mul_ne_zero ha hb) p := by
59   induction p using Quotient.inductionOn with
60   | h p =>
61     apply congrArg Quotient.mk''
62     apply Subtype.ext
63     exact action_mul a b p.val
64 
65 theorem projective_one (p : Projective) : projectiveAction 1 one_ne_zero p = p := by
66   induction p using Quotient.inductionOn with
67   | h p =>
68     apply congrArg Quotient.mk''
69     apply Subtype.ext
70     exact action_one p.val
71 
72 noncomputable def cyclicAction (N k : ℕ) : Projective → Projective :=
73   projectiveAction (omega N ^ k) (pow_ne_zero _ (omega_ne_zero N))
74 
75 theorem cyclic_zero (N : ℕ) (p : Projective) : cyclicAction N 0 p = p := by
76   exact projective_one p
77 
78 theorem cyclic_composition (N : ℕ) (hN : 0 < N) (k l : ℕ) (p : Projective) :
79     cyclicAction N k (cyclicAction N l p) = cyclicAction N ((k+l)%N) p := by
80   unfold cyclicAction
81   rw [projective_mul]
82   have he : omega N ^ k * omega N ^ l = omega N ^ ((k+l)%N) := by
83     rw [← pow_add, pow_eq_pow_mod (k+l) (omega_pow N hN)]
84   congr 1
85 
86 /-- Conjugacy with reflection-coordinate rotation, before taking the quotient. -/
87 theorem cayley_conjugacy (a : ℂ) (p : ℂ × ℂ) :
88     ((action a p).1 - (action a p).2, (action a p).1 + (action a p).2) =
89       (a * (p.1-p.2), p.1+p.2) := by
90   apply Prod.ext <;> dsimp [action] <;> ring
91 
92 theorem cyclic_chart (N k : ℕ) (z : ℂ) :
93     (action (omega N ^ k) (z,1)).1 / (action (omega N ^ k) (z,1)).2 =
94       ((1+omega N ^ k)*z+(1-omega N ^ k)) /
95       ((1-omega N ^ k)*z+(1+omega N ^ k)) := homogeneous_chart _ _
96 
97 theorem two_phase_swap (p : ℂ × ℂ) : action (omega 2 ^ 1) p = (p.2,p.1) := by
98   rw [pow_one, omega_two, half_turn]
99 
100 theorem two_phase_impedance_admittance (z : ℂ) (hz : z ≠ 0) :
101     denominator (omega 2 ^ 1) z ≠ 0 ∧ mobius (omega 2 ^ 1) z = z⁻¹ := by
102   rw [pow_one, omega_two]
103   exact finite_half_turn z hz
104 
105 end KomorebiPaperV.SmithCyclic

Back to source controls