English
A rational parameterization of the unit circle: the map hk ↦ circleEquivGen hk is a bijection between the field K and points on the unit circle with second coordinate not equal to -1.
Русский
Рациональная параметризация единичной окружности: отображение circleEquivGen hk задаёт биекцию между K и точками на окружности с координатой y не равной -1.
LaTeX
$$\exists hk : ∀ x, 1 + x^2 ≠ 0, circleEquivGen hk : K ≃ { p : K × K // p.1^2 + p.2^2 = 1 ∧ p.2 ≠ -1 }$$
Lean4
/-- A parameterization of the unit circle that is useful for classifying Pythagorean triples.
(To be applied in the case where `K = ℚ`.) -/
def circleEquivGen (hk : ∀ x : K, 1 + x ^ 2 ≠ 0) : K ≃ { p : K × K // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
where
toFun
x :=
⟨⟨2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)⟩, by field_simp [hk x]; ring,
by
simp only [Ne, div_eq_iff (hk x), neg_mul, one_mul, neg_add, sub_eq_add_neg, add_left_inj]
simpa only [eq_neg_iff_add_eq_zero, one_pow] using hk 1⟩
invFun p := (p : K × K).1 / ((p : K × K).2 + 1)
left_inv
x := by
have h2 : (1 + 1 : K) = 2 := by norm_num
have h3 : (2 : K) ≠ 0 := by
convert hk 1
rw [one_pow 2, h2]
simp [field, hk x, h2, add_assoc, add_comm, add_sub_cancel, mul_comm]
right_inv := fun ⟨⟨x, y⟩, hxy, hy⟩ => by
change x ^ 2 + y ^ 2 = 1 at hxy
have h2 : y + 1 ≠ 0 := mt eq_neg_of_add_eq_zero_left hy
have h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1) :=
by
rw [(add_neg_eq_iff_eq_add.mpr hxy.symm).symm]
ring
have h4 : (2 : K) ≠ 0 := by
convert hk 1
rw [one_pow 2]
ring
simp only [Prod.mk_inj, Subtype.mk_eq_mk]
constructor
· simp [field, h3]
· simp [field, h3]
rw [← add_neg_eq_iff_eq_add.mpr hxy.symm]
ring
