SmithAction.lean

1 import Mathlib.Basic.Complex.Basic
2 import Mathlib.Tactic
3 
4 /-!
5 Author: Komorebi P.
6 Normalized homogeneous Smith action. Pair coordinates represent [u:v], so the
7 half-turn swaps zero and infinity. Chart formulas carry explicit denominators.
8 -/
9 
10 namespace KomorebiPaperV.SmithAction
11 
12 noncomputable def action (a : ℂ) (p : ℂ × ℂ) : ℂ × ℂ :=
13   (((1 + a) * p.1 + (1 - a) * p.2) / 2,
14    ((1 - a) * p.1 + (1 + a) * p.2) / 2)
15 
16 theorem action_mul (a b : ℂ) (p : ℂ × ℂ) :
17     action a (action b p) = action (a * b) p := by
18   apply Prod.ext <;> dsimp [action] <;> ring
19 
20 theorem action_one (p : ℂ × ℂ) : action 1 p = p := by
21   apply Prod.ext <;> dsimp [action] <;> ring
22 
23 theorem action_scale (a c : ℂ) (p : ℂ × ℂ) :
24     action a (c * p.1, c * p.2) =
25       (c * (action a p).1, c * (action a p).2) := by
26   apply Prod.ext <;> dsimp [action] <;> ring
27 
28 theorem action_nonzero (a : ℂ) (ha : a ≠ 0) (p : ℂ × ℂ) (hp : p ≠ 0) :
29     action a p ≠ 0 := by
30   intro h
31   have hi := action_mul a⁻¹ a p
32   rw [inv_mul_cancel₀ ha, action_one, h] at hi
33   have hz : action a⁻¹ (0 : ℂ × ℂ) = 0 := by simp [action]
34   exact hp (hi.symm.trans hz)
35 
36 theorem half_turn (p : ℂ × ℂ) : action (-1) p = (p.2, p.1) := by
37   apply Prod.ext <;> dsimp [action] <;> ring
38 
39 theorem half_turn_zero : action (-1) ((0 : ℂ), 1) = (1, 0) := by
40   exact half_turn _
41 
42 theorem half_turn_infinity : action (-1) ((1 : ℂ), 0) = (0, 1) := by
43   exact half_turn _
44 
45 def denominator (a z : ℂ) : ℂ := (1 - a) * z + (1 + a)
46 
47 noncomputable def mobius (a z : ℂ) : ℂ := ((1 + a) * z + (1 - a)) / denominator a z
48 
49 theorem homogeneous_chart (a z : ℂ) :
50     (action a (z, 1)).1 / (action a (z, 1)).2 = mobius a z := by
51   dsimp [action, mobius, denominator]
52   simp only [mul_one]
53   exact div_div_div_cancel_right₀ (by norm_num : (2 : ℂ) ≠ 0) _ _
54 
55 theorem chart_composition (a b z : ℂ)
56     (hb : denominator b z ≠ 0)
57     (hab : denominator (a * b) z ≠ 0)
58     (ha : denominator a (mobius b z) ≠ 0) :
59     mobius a (mobius b z) = mobius (a * b) z := by
60   have hrel : mobius b z * denominator b z = (1 + b) * z + (1 - b) :=
61     div_mul_cancel₀ _ hb
62   apply (div_eq_div_iff ha hab).mpr
63   dsimp only [denominator] at hrel ⊢
64   linear_combination 2 * a * hrel
65 
66 theorem finite_half_turn (z : ℂ) (hz : z ≠ 0) :
67     denominator (-1) z ≠ 0 ∧ mobius (-1) z = z⁻¹ := by
68   constructor
69   · simpa [denominator] using hz
70   · dsimp [mobius, denominator]
71     field_simp [hz]
72     ring
73 
74 end KomorebiPaperV.SmithAction

Back to source controls