fixpointPolynomial_aeval_eq_zero_iff

English

Same as above for GL(2,K): g • (Some k) is ∞ if denominator zero, else the Möbius expression.

Русский

То же самое для GL(2,K): g • (Some k) равно ∞ если знаменатель ноль, иначе выражение Мёбиуса.

LaTeX

$$$g\\cdot (\\mathrm{OnePoint.some}\\ k) = \\begin{cases} \\infty, & g_{10}k+g_{11}=0 \\\\ \\mathrm{OnePoint.some}\\left(\\dfrac{g_{00}k+g_{01}}{g_{10}k+g_{11}}\\right), & \\text{иначе} \\end{cases}$$$

Lean4

/-- The roots of `g.fixpointPolynomial` are the fixed points of `g ∈ GL(2, K)` acting on the finite
part of `OnePoint K`. -/
theorem fixpointPolynomial_aeval_eq_zero_iff {c : K} {g : GL (Fin 2) K} :
    g.fixpointPolynomial.aeval c = 0 ↔ g • (c : OnePoint K) = c :=
  by
  simp only [fixpointPolynomial, map_sub, map_mul, map_add, aeval_X_pow, aeval_C, aeval_X,
    Algebra.algebraMap_self_apply, OnePoint.smul_some_eq_ite]
  split_ifs with h
  · refine ⟨fun hg ↦ (g.det_ne_zero ?_).elim, fun hg ↦ (infty_ne_coe _ hg).elim⟩
    rw [det_fin_two]
    grind
  · rw [coe_eq_coe, div_eq_iff h]
    grind

Похожие утверждения