ExceptionalPolynomial.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A scalar double block in an integral return matrix

The centralizer of the root SL₂ has a scalar two-dimensional block. The remaining block in a sufficiently separated return has simple real spectrum. Such a return matrix cannot be conjugate to an integral special-linear matrix unless the scalar eigenvalue is ±1.

lemma OAI.DukePrimeDegree.double_factor_unique_repeated_root line 21

theorem OAI.DukePrimeDegree.integer_unit_polynomial_double_factor line 41

Source documentation

The arithmetic obstruction only needs a scalar double factor and a separable residual polynomial, not a complete eigenbasis.

theorem integer_unit_polynomial_double_factor
    (p : ℤ[X]) (hp : p.Monic) (hc : IsUnit (p.coeff 0))
    (c : ℝ) (q : ℝ[X]) (hq : q.Monic) (hsep : q.Separable)
    (hfactor : p.map (algebraMap ℤ ℝ) = (X - C c) ^ 2 * q) :
    c = 1 ∨ c = -1 := by
…

theorem OAI.DukePrimeDegree.integer_sl_double_factor line 65

Source documentation

No integral special-linear return can have a nonunit scalar double block and a separable complementary characteristic factor.

theorem integer_sl_double_factor {ι : Type*} [Fintype ι] [DecidableEq ι]
    (g : Matrix.SpecialLinearGroup ι ℤ)
    (c : ℝ) (q : ℝ[X]) (hq : q.Monic) (hsep : q.Separable)
    (hfactor : g.val.charpoly.map (algebraMap ℤ ℝ) = (X - C c) ^ 2 * q) :
    c = 1 ∨ c = -1 := by
…

theorem OAI.DukePrimeDegree.integer_sl_scalar_double_block line 79

Source documentation

The matrix form of the double-factor obstruction, invariant under a real change of basis.

theorem integer_sl_scalar_double_block {ι : Type*} [Fintype ι] [DecidableEq ι]
    (g : Matrix.SpecialLinearGroup (Fin 2 ⊕ ι) ℤ)
    (P : Matrix.SpecialLinearGroup (Fin 2 ⊕ ι) ℝ)
    (c : ℝ) (B : Matrix ι ι ℝ) (hsep : B.charpoly.Separable)
    (hblock : P.val * g.val.map (algebraMap ℤ ℝ) * (P⁻¹).val =
      Matrix.fromBlocks (Matrix.diagonal (fun _ : Fin 2 => c)) 0 0 B) :
    c = 1 ∨ c = -1 := by
…

theorem OAI.DukePrimeDegree.no_integral_scalar_double_return line 101

Source documentation

A sufficiently small return with separated complementary weights cannot be integral up to conjugacy when its scalar double block is not a unit.

theorem no_integral_scalar_double_return {ι : Type*} [Fintype ι] [DecidableEq ι]
    (g : Matrix.SpecialLinearGroup (Fin 2 ⊕ ι) ℤ)
    (P : Matrix.SpecialLinearGroup (Fin 2 ⊕ ι) ℝ)
    (c : ℝ) (hc : c ≠ 1 ∧ c ≠ -1)
    (ell : ι → ℝ) (hgap : ∀ i j, i ≠ j → 1 < |ell i - ell j|)
    (H : Matrix ι ι ℝ)
    (hH : ∀ i, ∑ j, ‖(H - 1) i j‖ < spectralRelativeRadius)
    (hblock : P.val * g.val.map (algebraMap ℤ ℝ) * (P⁻¹).val =
      Matrix.fromBlocks (Matrix.diagonal (fun _ : Fin 2 => c)) 0 0
        (H * Matrix.diagonal (fun j => Real.exp (ell j)))) : False := by
…

Mentions: OAI.DukePrimeDegree.spectralRelativeRadius