English
If g ∈ GL(2,K) is parabolic and CharZero K, then for any n > 0, the parabolic fixed point is preserved under taking powers: (g^n).parabolicFixedPoint = g.parabolicFixedPoint.
Русский
Если g ∈ GL(2,K) параболический и CharZero K, то для любого n > 0 параболическая фиксированная точка сохраняется при возведении в степень: (g^n).parabolicFixedPoint = g.parabolicFixedPoint.
LaTeX
$$$\\text{If } g\\text{ is parabolic and }\\mathrm{CharZero}(K)\\text{ then }(g^n).parabolicFixedPoint = g.parabolicFixedPoint\\text{ for } n\\neq 0.$$$
Lean4
theorem smul_eq_self_iff {g : GL (Fin 2) K} (hg : g.IsParabolic) [NeZero (2 : K)] {c : OnePoint K} :
g • c = c ↔ c = parabolicFixedPoint g := by
rcases hg with ⟨hg, hdisc⟩
rw [disc_fin_two, trace_fin_two, det_fin_two] at hdisc
cases c with
| infty => by_cases h : g 1 0 = 0 <;> simp [parabolicFixedPoint, smul_infty_eq_ite, h]
| coe
c =>
suffices g 1 0 * c ^ 2 + (g 1 1 - g 0 0) * c - g 0 1 = 0 ↔ c = g.parabolicFixedPoint by
simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial]
by_cases hc : g 1 0 = 0
· have hd : g 1 1 = g 0 0 := by grind
suffices g 0 1 ≠ 0 by
simpa [parabolicFixedPoint, hc, hd]
-- can't have `g 0 1 ≠ 0` since that would force `g` to be scalar
refine fun hb ↦ fixpointPolynomial_eq_zero_iff.not.mpr hg ?_
simp [fixpointPolynomial, hb, hc, hd]
· have : discrim (g 1 0) (g 1 1 - g 0 0) (-g 0 1) = 0 := by rw [discrim]; grind
simpa [parabolicFixedPoint, if_neg hc, sq, sub_eq_add_neg] using
quadratic_eq_zero_iff_of_discrim_eq_zero hc this c
