Prove using rational root theorem

Stream: new members

[Nick_adfor]

Now I want to prove: For an integer matrix A, if q/p (p ≠ 1 and q, p coprime) is a rational eigenvalue of A, then the corresponding eigenvector X must be zero.

I leave some sorry that I don't know how to fill in.

import Mathlib

open Matrix Polynomial
/-
Rational eigenvector problem for integer matrices

We prove: For an integer matrix A, if q/p (p ≠ 1 and q, p coprime) is a rational eigenvalue of A, then the corresponding eigenvector X must be zero.
The main tools are the characteristic polynomial and the rational root theorem.
-/

/-- Map an integer matrix A to a rational matrix -/
def Aq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : Matrix (Fin n) (Fin n) ℚ :=
  A.map (Int.castRingHom ℚ) -- Use the ring homomorphism to map each element from ℤ to ℚ

/--
Key lemma: eigenvalue condition translated into a polynomial root
-/
lemma matrix_root_iff_charpoly_root
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (r : ℚ)
  (X : Fin n → ℚ) (hX : X ≠ 0) :
  (Aq A).mulVec X = r • X → aeval r (charpoly (Aq A)) = 0 := by
  intro h
  -- Step 1: Show (r•I - A)X = 0
  have hker : (r • (1 : Matrix _ _ ℚ) - Aq A).mulVec X = 0 := by
    rw [Matrix.sub_mulVec, Matrix.smul_mulVec_assoc, one_mulVec, h, sub_self]
  -- Step 2: Non-zero solution implies determinant is 0
  have hdet : (r • (1 : Matrix _ _ ℚ) - Aq A).det = 0 := by
    refine (Matrix.exists_mulVec_eq_zero_iff_aux).mp ⟨X, hX, hker⟩
  -- Step 3: Show det(r•I - A) = charpoly(A)(r)
  have : (charpoly (Aq A)).eval r = (r • (1 : Matrix (Fin n) (Fin n) ℚ) - Aq A).det := by
    rw [charpoly, charmatrix, eval_det, scalar_apply, RingHom.mapMatrix_apply, map_sub]
    simp only [scalar_apply, matPolyEquiv_diagonal_X, matPolyEquiv_map_C, eval_sub, eval_X, eval_C, smul_one_eq_diagonal]
  -- Final conclusion
  rw [← this] at hdet
  exact hdet

/-!
Main theorem: only trivial solution exists
-/
theorem only_trivial_solution
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (q p : ℤ)
  (hp : p.natAbs ≠ 1) (hcoprime : IsCoprime q p) :
  ∀ (X : Fin n → ℚ), (Aq A).mulVec X = (q / p : ℚ) • X → X = 0 := by
  -- Proof by contradiction: assume there exists a non-zero solution X ≠ 0
  intro X h
  by_contra hX
  push_neg at hX

  -- Define key objects
  let Aℚ := Aq A                    -- Rational matrix
  let r : ℚ := q / p                -- Eigenvalue q/p
  let f : Polynomial ℚ := charpoly Aℚ -- Characteristic polynomial

  -- Step 1: Show r is a root of f
  have h_root : aeval r f = 0 :=
    matrix_root_iff_charpoly_root A r X hX h

  -- Step 2: Relate integer coefficients to rational characteristic polynomial
  have charpoly_map : f = Polynomial.map (Int.castRingHom ℚ) (charpoly A) := by
    simp only [← charpoly_map, Int.coe_castRingHom]
    exact rfl

  -- Step 3: Show leading coefficient is 1
  have leading_one : f.leadingCoeff = 1 := by
    rw [MonCat.one_of, ← Monic.def]
    exact charpoly_monic Aℚ

  -- Step 4: Extract numerator and denominator
  let d := r.den  -- Denominator (since r = q/p is reduced, d = p.natAbs)

  -- Step 5: Apply the rational root theorem
  have den_dvd_1 : d = 1 := by
    have A_leading_one : A.charpoly.leadingCoeff = 1 := by
      have := charpoly_monic A
      exact this
    have leading_one' : f.leadingCoeff = 1 := leading_one
    rw [charpoly_map] at leading_one
    have leading_coeff_map : f.leadingCoeff = Int.castRingHom ℚ A.charpoly.leadingCoeff := by
      rw [charpoly_map, leading_one]
      exact Rat.ext (id (Eq.symm A_leading_one)) rfl
    have leading_coeff_map' : 1 = Int.castRingHom ℚ A.charpoly.leadingCoeff := by
      rw [← leading_coeff_map, ← leading_one, charpoly_map]
    have h_root_int : aeval r (charpoly A) = 0 := by
      sorry
    have dvd1 : ((IsFractionRing.den ℤ r) : ℤ) ∣ (charpoly A).leadingCoeff := by
      exact den_dvd_of_is_root h_root_int
    rw [A_leading_one] at dvd1
    have abs1 : ((IsFractionRing.den ℤ r : ℤ)).natAbs = 1 := by
      have hu : IsUnit (IsFractionRing.den ℤ r : ℤ) :=
        isUnit_of_dvd_one dvd1
      exact Int.natAbs_of_isUnit hu
    sorry
  have r_int : r.den = 1 := den_dvd_1
  have r_eq_int : r = r.num := by
    rw [Rat.coe_int_num_of_den_eq_one den_dvd_1]
  -- Step 7: r = q / p, but r ∈ ℤ, so q / p ∈ ℤ
  have q_div_p_int : (q / p : ℚ) = r.num := by
    rw [← r_eq_int]

  -- Step 8: Contradiction
  have : p.natAbs = 1 := by
    have r_den_eq_p : r.den = p.natAbs := by
      by_cases h_pos : 0 < p
      · have p_eq_natAbs : p = p.natAbs := by
          rw [Int.natCast_natAbs, abs_of_pos h_pos]
        have h_den_nat : r.den = p.natAbs := by
          unfold r
          have h_coprime : q.natAbs.Coprime p.natAbs := by
            exact Int.isCoprime_iff_nat_coprime.mp hcoprime
          have h_temp := Rat.den_div_eq_of_coprime h_pos h_coprime
          sorry
        exact h_den_nat
      · have h_nonzero : p ≠ 0 := by
          sorry
        have h_neg : p < 0 := lt_of_le_of_ne (not_lt.mp h_pos) h_nonzero
        have eq : q / p = (-q) / p.natAbs := by
          sorry
        sorry
    have p_natAbs_eq_1 : p.natAbs = 1 := by
      rw [← r_den_eq_p, ← den_dvd_1]
    exact p_natAbs_eq_1


  -- Contradiction obtained, finish proof
  contradiction

[Ruben Van de Velde]

Can you prove that p = (q/p).den? Then it's (r.num : Rat).den and there should be a theorem that that's 1

[Nick_adfor]

What's that theorem?

[Ruben Van de Velde]

Apparently both docs#Rat.intCast_den and docs#Rat.den_intCast

[Nick_adfor]

Ruben Van de Velde said:

Apparently both docs#Rat.intCast_den and docs#Rat.den_intCast

I cannot fix the sorry because of too much more from N to Z. I have no way to do with the last sorry.

[Ruben Van de Velde]

Does this help?

import Mathlib

open Matrix Polynomial
/-
Rational eigenvector problem for integer matrices

We prove: For an integer matrix A, if q/p (p ≠ 1 and q, p coprime) is a rational eigenvalue of A, then the corresponding eigenvector X must be zero.
The main tools are the characteristic polynomial and the rational root theorem.
-/

/-- Map an integer matrix A to a rational matrix -/
def Aq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : Matrix (Fin n) (Fin n) ℚ :=
  A.map (Int.castRingHom ℚ) -- Use the ring homomorphism to map each element from ℤ to ℚ

/--
Key lemma: eigenvalue condition translated into a polynomial root
-/
lemma matrix_root_iff_charpoly_root
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (r : ℚ)
  (X : Fin n → ℚ) (hX : X ≠ 0) :
  (Aq A).mulVec X = r • X → aeval r (charpoly (Aq A)) = 0 := by
  intro h
  -- Step 1: Show (r•I - A)X = 0
  have hker : (r • (1 : Matrix _ _ ℚ) - Aq A).mulVec X = 0 := by
    rw [Matrix.sub_mulVec, Matrix.smul_mulVec_assoc, one_mulVec, h, sub_self]
  -- Step 2: Non-zero solution implies determinant is 0
  have hdet : (r • (1 : Matrix _ _ ℚ) - Aq A).det = 0 := by
    refine (Matrix.exists_mulVec_eq_zero_iff_aux).mp ⟨X, hX, hker⟩
  -- Step 3: Show det(r•I - A) = charpoly(A)(r)
  have : (charpoly (Aq A)).eval r = (r • (1 : Matrix (Fin n) (Fin n) ℚ) - Aq A).det := by
    rw [charpoly, charmatrix, eval_det, scalar_apply, RingHom.mapMatrix_apply, map_sub]
    simp only [scalar_apply, matPolyEquiv_diagonal_X, matPolyEquiv_map_C, eval_sub, eval_X, eval_C, smul_one_eq_diagonal]
  -- Final conclusion
  rw [← this] at hdet
  exact hdet

/-!
Main theorem: only trivial solution exists
-/
theorem only_trivial_solution
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (q p : ℤ)
  (hp : p.natAbs ≠ 1) (hcoprime : IsCoprime q p) :
  ∀ (X : Fin n → ℚ), (Aq A).mulVec X = (q / p : ℚ) • X → X = 0 := by
  -- Proof by contradiction: assume there exists a non-zero solution X ≠ 0
  intro X h
  by_contra hX
  push_neg at hX

  -- Define key objects
  let Aℚ := Aq A                    -- Rational matrix
  let r : ℚ := q / p                -- Eigenvalue q/p
  let f : Polynomial ℚ := charpoly Aℚ -- Characteristic polynomial

  -- Step 1: Show r is a root of f
  have h_root : aeval r f = 0 :=
    matrix_root_iff_charpoly_root A r X hX h

  -- Step 2: Relate integer coefficients to rational characteristic polynomial
  have charpoly_map : f = Polynomial.map (Int.castRingHom ℚ) (charpoly A) := by
    simp only [← charpoly_map, Int.coe_castRingHom]
    exact rfl

  -- Step 3: Show leading coefficient is 1
  have leading_one : f.leadingCoeff = 1 := by
    rw [MonCat.one_of, ← Monic.def]
    exact charpoly_monic Aℚ

  -- Step 4: Extract numerator and denominator
  let d := r.den  -- Denominator (since r = q/p is reduced, d = p.natAbs)

  -- Step 5: Apply the rational root theorem
  have den_dvd_1 : d = 1 := by
    have A_leading_one : A.charpoly.leadingCoeff = 1 := by
      have := charpoly_monic A
      exact this
    have leading_one' : f.leadingCoeff = 1 := leading_one
    rw [charpoly_map] at leading_one
    have leading_coeff_map : f.leadingCoeff = Int.castRingHom ℚ A.charpoly.leadingCoeff := by
      rw [charpoly_map, leading_one]
      exact Rat.ext (id (Eq.symm A_leading_one)) rfl
    have leading_coeff_map' : 1 = Int.castRingHom ℚ A.charpoly.leadingCoeff := by
      rw [← leading_coeff_map, ← leading_one, charpoly_map]
    have h_root_int : aeval r (charpoly A) = 0 := by
      sorry
    have dvd1 : ((IsFractionRing.den ℤ r) : ℤ) ∣ (charpoly A).leadingCoeff := by
      exact den_dvd_of_is_root h_root_int
    rw [A_leading_one] at dvd1
    have abs1 : ((IsFractionRing.den ℤ r : ℤ)).natAbs = 1 := by
      have hu : IsUnit (IsFractionRing.den ℤ r : ℤ) :=
        isUnit_of_dvd_one dvd1
      exact Int.natAbs_of_isUnit hu
    sorry
  have r_int : r.den = 1 := den_dvd_1
  have r_eq_int : r = r.num := by
    rw [Rat.coe_int_num_of_den_eq_one den_dvd_1]
  -- Step 7: r = q / p, but r ∈ ℤ, so q / p ∈ ℤ
  have q_div_p_int : (q / p : ℚ) = r.num := by
    rw [← r_eq_int]

  -- Step 8: Contradiction
  have h_coprime : q.natAbs.Coprime p.natAbs := by
    exact Int.isCoprime_iff_nat_coprime.mp hcoprime
  have r_den_eq_p : r.den = p.natAbs := by
    by_cases h_pos : 0 < p
    · have p_eq_natAbs : p = p.natAbs := by
        rw [Int.natCast_natAbs, abs_of_pos h_pos]
      unfold r
      have h_temp := Rat.den_div_eq_of_coprime h_pos h_coprime
      have := h_temp.trans p_eq_natAbs
      simp only [Nat.cast_inj] at this
      exact this
    · have h_nonzero : p ≠ 0 := by
        rintro rfl
        simp [r, d, isCoprime_zero_right, Int.isUnit_iff_natAbs_eq] at *
        -- Not sure this is true
        sorry
      have h_neg : p < 0 := lt_of_le_of_ne (not_lt.mp h_pos) h_nonzero
      have h_pos : 0 < -p := by linarith
      have h_temp := Rat.den_div_eq_of_coprime h_pos (by simpa using h_coprime)
      unfold r
      simp only [Int.cast_neg, div_neg, Rat.neg_den] at h_temp
      apply Nat.cast_injective (R := ℤ)
      rw [h_temp, Int.ofNat_natAbs_of_nonpos h_neg.le]
  have : p.natAbs = 1 := by
    rw [← r_den_eq_p, ← den_dvd_1]


  -- Contradiction obtained, finish proof
  contradiction

[Nick_adfor]

That's very kind of you. As p is not 0 can be write in

theorem only_trivial_solution
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (q p : ℤ)
  (hp : p.natAbs ≠ 1) (h_nonzero : p ≠ 0) (hcoprime : IsCoprime q p) :
  ∀ (X : Fin n → ℚ), (Aq A).mulVec X = (q / p : ℚ) • X → X = 0 := by

All is fine.

[Nick_adfor]

Now with sorry in step 5. I'm quite confused from Z to Q.

import Mathlib

open Matrix Polynomial
/-
Rational eigenvector problem for integer matrices

We prove: For an integer matrix A, if q/p (p ≠ 1 and q, p coprime) is a rational eigenvalue of A, then the corresponding eigenvector X must be zero.
The main tools are the characteristic polynomial and the rational root theorem.
-/

/-- Map an integer matrix A to a rational matrix -/
def Aq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : Matrix (Fin n) (Fin n) ℚ :=
  A.map (Int.castRingHom ℚ) -- Use the ring homomorphism to map each element from ℤ to ℚ

/--
Key lemma: eigenvalue condition translated into a polynomial root
-/
lemma matrix_root_iff_charpoly_root
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (r : ℚ)
  (X : Fin n → ℚ) (hX : X ≠ 0) :
  (Aq A).mulVec X = r • X → aeval r (charpoly (Aq A)) = 0 := by
  intro h
  -- Step 1: Show (r•I - A)X = 0
  have hker : (r • (1 : Matrix _ _ ℚ) - Aq A).mulVec X = 0 := by
    rw [Matrix.sub_mulVec, Matrix.smul_mulVec_assoc, one_mulVec, h, sub_self]
  -- Step 2: Non-zero solution implies determinant is 0
  have hdet : (r • (1 : Matrix _ _ ℚ) - Aq A).det = 0 := by
    refine (Matrix.exists_mulVec_eq_zero_iff_aux).mp ⟨X, hX, hker⟩
  -- Step 3: Show det(r•I - A) = charpoly(A)(r)
  have : (charpoly (Aq A)).eval r = (r • (1 : Matrix (Fin n) (Fin n) ℚ) - Aq A).det := by
    rw [charpoly, charmatrix, eval_det, scalar_apply, RingHom.mapMatrix_apply, map_sub]
    simp only [scalar_apply, matPolyEquiv_diagonal_X, matPolyEquiv_map_C, eval_sub, eval_X, eval_C, smul_one_eq_diagonal]
  -- Final conclusion
  rw [← this] at hdet
  exact hdet

/--
Main theorem: only trivial solution exists
-/
theorem only_trivial_solution
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (q p : ℤ)
  (hp : p.natAbs ≠ 1) (h_nonzero : p ≠ 0) (hcoprime : IsCoprime q p) :
  ∀ (X : Fin n → ℚ), (Aq A).mulVec X = (q / p : ℚ) • X → X = 0 := by
  -- Proof by contradiction: assume there exists a non-zero solution X ≠ 0
  intro X h
  by_contra hX
  push_neg at hX

  -- Define key objects
  let Aℚ := Aq A                    -- Rational matrix
  let r : ℚ := q / p                -- Eigenvalue q/p
  let f : Polynomial ℚ := charpoly Aℚ -- Characteristic polynomial

  -- Step 1: Show r is a root of f
  have h_root : aeval r f = 0 :=
    matrix_root_iff_charpoly_root A r X hX h

  -- Step 2: Relate integer coefficients to rational characteristic polynomial
  have charpoly_map : f = Polynomial.map (Int.castRingHom ℚ) (charpoly A) := by
    simp only [← charpoly_map, Int.coe_castRingHom]
    exact rfl

  -- Step 3: Show leading coefficient is 1
  have leading_one : f.leadingCoeff = 1 := by
    rw [MonCat.one_of, ← Monic.def]
    exact charpoly_monic Aℚ

  -- Step 4: Extract numerator and denominator
  let d := r.den

  -- Step 5: Apply the rational root theorem
  have den_dvd_1 : d = 1 := by
    have A_leading_one : A.charpoly.leadingCoeff = 1 := by
      have := charpoly_monic A
      exact this
    have leading_one' : f.leadingCoeff = 1 := leading_one
    rw [charpoly_map] at leading_one
    have leading_coeff_map : f.leadingCoeff = Int.castRingHom ℚ A.charpoly.leadingCoeff := by
      rw [charpoly_map, leading_one]
      exact Rat.ext (id (Eq.symm A_leading_one)) rfl
    have leading_coeff_map' : 1 = Int.castRingHom ℚ A.charpoly.leadingCoeff := by
      rw [← leading_coeff_map, ← leading_one, charpoly_map]
    have h_root_int : aeval r (charpoly A) = 0 := by
      rw [aeval_def] at h_root ⊢
      have : eval₂ (algebraMap ℤ ℚ) r (A.charpoly) = eval₂ (algebraMap ℚ ℚ) r f := by
        rw [charpoly_map, Polynomial.eval₂_map]
        have : (algebraMap ℚ ℚ).comp (Int.castRingHom ℚ) = algebraMap ℤ ℚ := by
          ext x
          simp [algebraMap_int_eq]
        rw [this]
      rw [this, h_root]
    have dvd1 : ((IsFractionRing.den ℤ r) : ℤ) ∣ (charpoly A).leadingCoeff := by
      exact den_dvd_of_is_root h_root_int
    rw [A_leading_one] at dvd1
    have abs1 : ((IsFractionRing.den ℤ r : ℤ)).natAbs = 1 := by
      have hu : IsUnit (IsFractionRing.den ℤ r : ℤ) :=
        isUnit_of_dvd_one dvd1
      exact Int.natAbs_of_isUnit hu
    have den_eq : d = ((IsFractionRing.den ℤ r : ℤ)).natAbs := by
      rw [← Rat.num_div_den r]
      have : ∃ (q' : ℤ) (p' : ℤ),
        IsFractionRing.den ℤ r = p' ∧
        r = algebraMap ℤ ℚ q' / algebraMap ℤ ℚ p' := by
        sorry
      obtain ⟨q', p', h_den, h_frac⟩ := this
      have cross_mul : q * p' = p * q' := by
        have h1 : r = q / p := by rw [div_eq_div_iff_comm]
        have h2 : r = q' / p' := by sorry
        have h_eq' : q / p = q' / p' := by sorry
        apply_fun (fun x => x * (p * p')) at h_eq'
        have h_eq : q / p * (p * p') = q' / p' * (p * p') := by
          rw [h_eq']
        have : q / p * (p * p') = q * p' := by sorry
        sorry
      simp [mul_assoc, mul_comm, algebraMap_int_eq] at cross_mul
      have p'_div_p : p' ∣ p := by
        sorry
      have h_coprime : q.natAbs.Coprime p.natAbs := by
        exact Int.isCoprime_iff_nat_coprime.mp hcoprime
      sorry
    rw [← abs1, den_eq]
  have r_int : r.den = 1 := den_dvd_1
  --step 6: r is an integer
  have r_eq_int : r = r.num := by
    rw [Rat.coe_int_num_of_den_eq_one den_dvd_1]
  -- Step 7: r = q / p, but r ∈ ℤ, so q / p ∈ ℤ
  have q_div_p_int : (q / p : ℚ) = r.num := by
    rw [← r_eq_int]

  -- Step 8: Contradiction
  have h_coprime : q.natAbs.Coprime p.natAbs := by
    exact Int.isCoprime_iff_nat_coprime.mp hcoprime
  have : p.natAbs = 1 := by
    have r_den_eq_p : r.den = p.natAbs := by
      by_cases h_pos : 0 < p
      · have p_eq_natAbs : p = p.natAbs := by
          rw [Int.natCast_natAbs, abs_of_pos h_pos]
        unfold r
        have h_temp := Rat.den_div_eq_of_coprime h_pos h_coprime
        have := h_temp.trans p_eq_natAbs
        simp only [Nat.cast_inj] at this
        exact this
      · have h_neg : p < 0 := lt_of_le_of_ne (not_lt.mp h_pos) h_nonzero
        have h_pos : 0 < -p := by linarith
        have h_temp := Rat.den_div_eq_of_coprime h_pos (by simpa using h_coprime)
        unfold r
        simp only [Int.cast_neg, div_neg, Rat.neg_den] at h_temp
        apply Nat.cast_injective (R := ℤ)
        rw [h_temp, Int.ofNat_natAbs_of_nonpos h_neg.le]
    have p_natAbs_eq_1 : p.natAbs = 1 := by
      rw [← r_den_eq_p, ← den_dvd_1]
    exact p_natAbs_eq_1


  -- Contradiction obtained, finish proof
  contradiction

[Ruben Van de Velde]

Ugh, that was more annoying than expected:

import Mathlib

open Matrix Polynomial
/-
Rational eigenvector problem for integer matrices

We prove: For an integer matrix A, if q/p (p ≠ 1 and q, p coprime) is a rational eigenvalue of A, then the corresponding eigenvector X must be zero.
The main tools are the characteristic polynomial and the rational root theorem.
-/

/-- Map an integer matrix A to a rational matrix -/
def Aq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : Matrix (Fin n) (Fin n) ℚ :=
  A.map (Int.castRingHom ℚ) -- Use the ring homomorphism to map each element from ℤ to ℚ

/--
Key lemma: eigenvalue condition translated into a polynomial root
-/
lemma matrix_root_iff_charpoly_root
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (r : ℚ)
  (X : Fin n → ℚ) (hX : X ≠ 0) :
  (Aq A).mulVec X = r • X → aeval r (charpoly (Aq A)) = 0 := by
  intro h
  -- Step 1: Show (r•I - A)X = 0
  have hker : (r • (1 : Matrix _ _ ℚ) - Aq A).mulVec X = 0 := by
    rw [Matrix.sub_mulVec, Matrix.smul_mulVec_assoc, one_mulVec, h, sub_self]
  -- Step 2: Non-zero solution implies determinant is 0
  have hdet : (r • (1 : Matrix _ _ ℚ) - Aq A).det = 0 := by
    refine (Matrix.exists_mulVec_eq_zero_iff_aux).mp ⟨X, hX, hker⟩
  -- Step 3: Show det(r•I - A) = charpoly(A)(r)
  have : (charpoly (Aq A)).eval r = (r • (1 : Matrix (Fin n) (Fin n) ℚ) - Aq A).det := by
    rw [charpoly, charmatrix, eval_det, scalar_apply, RingHom.mapMatrix_apply, map_sub]
    simp only [scalar_apply, matPolyEquiv_diagonal_X, matPolyEquiv_map_C, eval_sub, eval_X, eval_C, smul_one_eq_diagonal]
  -- Final conclusion
  rw [← this] at hdet
  exact hdet

/-!
Main theorem: only trivial solution exists
-/
theorem only_trivial_solution
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (q p : ℤ)
  (hp : p.natAbs ≠ 1) (h_nonzero : p ≠ 0) (hcoprime : IsCoprime q p) :
  ∀ (X : Fin n → ℚ), (Aq A).mulVec X = (q / p : ℚ) • X → X = 0 := by
  -- Proof by contradiction: assume there exists a non-zero solution X ≠ 0
  intro X h
  by_contra hX
  push_neg at hX

  -- Define key objects
  let Aℚ := Aq A                    -- Rational matrix
  let r : ℚ := q / p                -- Eigenvalue q/p
  let f : Polynomial ℚ := charpoly Aℚ -- Characteristic polynomial

  -- Step 1: Show r is a root of f
  have h_root : aeval r f = 0 :=
    matrix_root_iff_charpoly_root A r X hX h

  -- Step 2: Relate integer coefficients to rational characteristic polynomial
  have charpoly_map : f = Polynomial.map (Int.castRingHom ℚ) (charpoly A) := by
    simp only [← charpoly_map, Int.coe_castRingHom]
    exact rfl

  -- Step 3: Show leading coefficient is 1
  have leading_one : f.leadingCoeff = 1 := by
    rw [MonCat.one_of, ← Monic.def]
    exact charpoly_monic Aℚ

  -- Step 4: Extract numerator and denominator
  let d := r.den  -- Denominator (since r = q/p is reduced, d = p.natAbs)

  -- Step 5: Apply the rational root theorem
  have den_dvd_1 : d = 1 := by
    have A_leading_one : A.charpoly.leadingCoeff = 1 := by
      have := charpoly_monic A
      exact this
    have leading_one' : f.leadingCoeff = 1 := leading_one
    rw [charpoly_map] at leading_one
    have leading_coeff_map : f.leadingCoeff = Int.castRingHom ℚ A.charpoly.leadingCoeff := by
      rw [charpoly_map, leading_one]
      exact Rat.ext (id (Eq.symm A_leading_one)) rfl
    have leading_coeff_map' : 1 = Int.castRingHom ℚ A.charpoly.leadingCoeff := by
      rw [← leading_coeff_map, ← leading_one, charpoly_map]
    have h_root_int : aeval r (charpoly A) = 0 := by
      rw [aeval_def] at h_root ⊢
      have : eval₂ (algebraMap ℤ ℚ) r (A.charpoly) = eval₂ (algebraMap ℚ ℚ) r f := by
        rw [charpoly_map, Polynomial.eval₂_map]
        have : (algebraMap ℚ ℚ).comp (Int.castRingHom ℚ) = algebraMap ℤ ℚ := by
          ext x
          simp [algebraMap_int_eq]
        rw [this]
      rw [this, h_root]
    have dvd1 : ((IsFractionRing.den ℤ r) : ℤ) ∣ (charpoly A).leadingCoeff := by
      exact den_dvd_of_is_root h_root_int
    rw [A_leading_one] at dvd1
    have hu : IsUnit (IsFractionRing.den ℤ r : ℤ) :=
      isUnit_of_dvd_one dvd1
    have abs1 : ((IsFractionRing.den ℤ r : ℤ)).natAbs = 1 := by
      exact Int.natAbs_of_isUnit hu
    rw [IsFractionRing.isUnit_den_iff, IsLocalization.IsInteger] at hu
    simp at hu
    obtain ⟨r', hr⟩ := hu
    unfold d
    rw [← hr]
    simp
  have r_int : r.den = 1 := den_dvd_1
  --step 6: r is an integer
  have r_eq_int : r = r.num := by
    rw [Rat.coe_int_num_of_den_eq_one den_dvd_1]
  -- Step 7: r = q / p, but r ∈ ℤ, so q / p ∈ ℤ
  have q_div_p_int : (q / p : ℚ) = r.num := by
    rw [← r_eq_int]

  -- Step 8: Contradiction
  have h_coprime : q.natAbs.Coprime p.natAbs := by
    exact Int.isCoprime_iff_nat_coprime.mp hcoprime
  have : p.natAbs = 1 := by
    have r_den_eq_p : r.den = p.natAbs := by
      by_cases h_pos : 0 < p
      · have p_eq_natAbs : p = p.natAbs := by
          rw [Int.natCast_natAbs, abs_of_pos h_pos]
        unfold r
        have h_temp := Rat.den_div_eq_of_coprime h_pos h_coprime
        have := h_temp.trans p_eq_natAbs
        simp only [Nat.cast_inj] at this
        exact this
      · have h_neg : p < 0 := lt_of_le_of_ne (not_lt.mp h_pos) h_nonzero
        have h_pos : 0 < -p := by linarith
        have h_temp := Rat.den_div_eq_of_coprime h_pos (by simpa using h_coprime)
        unfold r
        simp only [Int.cast_neg, div_neg, Rat.neg_den] at h_temp
        apply Nat.cast_injective (R := ℤ)
        rw [h_temp, Int.ofNat_natAbs_of_nonpos h_neg.le]
    have p_natAbs_eq_1 : p.natAbs = 1 := by
      rw [← r_den_eq_p, ← den_dvd_1]
    exact p_natAbs_eq_1


  -- Contradiction obtained, finish proof
  contradiction

[Nick_adfor]

It is unbelivable that you fix it in a short time!

[Nick_adfor]

IsFractionRing.isUnit_den_iff and IsLocalization.IsInteger are something I have never thought of.

[Nick_adfor]

(deleted)

[Ruben Van de Velde]

You had the result about IsFractionRing.den, which I didn't really know anything about, so I searched loogle, which only had 14 results, only one of which seemed relevant

[Ruben Van de Velde]

In the sense that IsLocalization.IsInteger sounded exactly like what you needed - but not quite in the right form. So I searched for IsLocalization.IsInteger on loogle and didn't really find anything relevant to the concrete Int/Rat case, so I tried simplifying the definition and was lucky that that basically solved it

[Ruben Van de Velde]

This was the lemma I was looking for but we don't have yet:

lemma Rat.isLocalizationIsInteger_iff (q : ℚ) :
    IsLocalization.IsInteger ℤ q ↔ q ∈ Set.range Int.cast := by
  simp [IsLocalization.IsInteger]

[Nick_adfor]

I cut some unused have and write more notes in. I think the way to find the two needed theorem IsFractionRing.isUnit_den_iff and IsLocalization.IsInteger is totally amazing.

[Nick_adfor]

import Mathlib

open Matrix Polynomial

/-
Rational eigenvector problem for integer matrices

We prove: For an integer matrix A, if q/p (p ≠ 1 and q, p coprime) is a rational eigenvalue of A, then the corresponding eigenvector X must be zero.
The main tools are the characteristic polynomial and the rational root theorem.
-/

/-- Map an integer matrix A to a rational matrix -/
def Aq {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : Matrix (Fin n) (Fin n) ℚ :=
  A.map (Int.castRingHom ℚ)

/--
Key lemma: eigenvalue condition translated into a polynomial root
-/
lemma matrix_root_iff_charpoly_root
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (r : ℚ)
  (X : Fin n → ℚ) (hX : X ≠ 0) :
  (Aq A).mulVec X = r • X → aeval r (charpoly (Aq A)) = 0 := by
  intro h
  -- (r•I - A)X = 0
  have hker : (r • (1 : Matrix _ _ ℚ) - Aq A).mulVec X = 0 := by
    rw [Matrix.sub_mulVec, Matrix.smul_mulVec_assoc, one_mulVec, h, sub_self]
  -- Non-zero solution implies determinant is 0
  have hdet : (r • (1 : Matrix _ _ ℚ) - Aq A).det = 0 := by
    refine (Matrix.exists_mulVec_eq_zero_iff_aux).mp ⟨X, hX, hker⟩
  -- det(r•I - A) = charpoly(A)(r)
  have : (charpoly (Aq A)).eval r = (r • (1 : Matrix (Fin n) (Fin n) ℚ) - Aq A).det := by
    rw [charpoly, charmatrix, eval_det, scalar_apply, RingHom.mapMatrix_apply, map_sub]
    simp only [scalar_apply, matPolyEquiv_diagonal_X, matPolyEquiv_map_C, eval_sub, eval_X, eval_C, smul_one_eq_diagonal]
  rw [← this] at hdet
  exact hdet

/--
Main theorem: only trivial solution exists
-/
theorem only_trivial_solution
  {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (q p : ℤ)
  (hp : p.natAbs ≠ 1) (h_nonzero : p ≠ 0) (hcoprime : IsCoprime q p) :
  ∀ (X : Fin n → ℚ), (Aq A).mulVec X = (q / p : ℚ) • X → X = 0 := by
  intro X h
  by_contra hX
  push_neg at hX

  let Aℚ := Aq A
  let r : ℚ := q / p
  let f : Polynomial ℚ := charpoly Aℚ

  -- r is a root of the characteristic polynomial
  have h_root : aeval r f = 0 :=
    matrix_root_iff_charpoly_root A r X hX h

  -- Characteristic polynomial relation between ℤ and ℚ
  have charpoly_map : f = Polynomial.map (Int.castRingHom ℚ) (charpoly A) := by
    simp only [← charpoly_map, Int.coe_castRingHom]
    exact rfl

  let d := r.den

-- Denominator must be 1 (rational root theorem)
  have den_dvd_1 : d = 1 := by
    -- The characteristic polynomial of an integer matrix is monic (leading coefficient 1)
    have A_leading_one : A.charpoly.leadingCoeff = 1 := by
      have := charpoly_monic A  -- From Mathlib: charpoly of any matrix over a commutative ring is monic
      exact this

    -- Show r is a root of the integer version of the characteristic polynomial
    have h_root_int : aeval r (charpoly A) = 0 := by
      rw [aeval_def] at h_root ⊢
      -- Relate evaluation of mapped polynomial to original polynomial
      have : eval₂ (algebraMap ℤ ℚ) r (A.charpoly) = eval₂ (algebraMap ℚ ℚ) r f := by
        rw [charpoly_map, Polynomial.eval₂_map]
        -- Show the composition of maps equals the direct integer to rational map
        have : (algebraMap ℚ ℚ).comp (Int.castRingHom ℚ) = algebraMap ℤ ℚ := by
          ext x
          simp [algebraMap_int_eq]
        rw [this]
      rw [this, h_root]

    -- By rational root theorem, denominator must divide leading coefficient
    have dvd1 : ((IsFractionRing.den ℤ r) : ℤ) ∣ (charpoly A).leadingCoeff := by
      exact den_dvd_of_is_root h_root_int

    -- Since leading coefficient is 1, denominator must divide 1
    rw [A_leading_one] at dvd1
    have hu : IsUnit (IsFractionRing.den ℤ r : ℤ) :=
      isUnit_of_dvd_one dvd1

    -- An integer is a unit iff it's ±1, which means denominator is in the range of algebraMap
    rw [IsFractionRing.isUnit_den_iff, IsLocalization.IsInteger] at hu
    simp only [algebraMap_int_eq, RingHom.mem_rangeS, eq_intCast] at hu
    obtain ⟨r', hr⟩ := hu

    -- Unfold definition of d and show it equals 1
    unfold d
    rw [← hr]
    simp only [Rat.intCast_den]

  -- Convert coprimality from integers to natural numbers
  have h_coprime : q.natAbs.Coprime p.natAbs := by
    exact Int.isCoprime_iff_nat_coprime.mp hcoprime

  -- Show p.natAbs must equal denominator of r (which we've shown equals 1)
  have : p.natAbs = 1 := by
    -- First show denominator of r equals |p|
    have r_den_eq_p : r.den = p.natAbs := by
      by_cases h_pos : 0 < p
      · -- Case when p is positive
        have p_eq_natAbs : p = p.natAbs := by
          rw [Int.natCast_natAbs, abs_of_pos h_pos]
        unfold r
        -- Rat.den_div_eq_of_coprime gives denominator for reduced fraction
        have h_temp := Rat.den_div_eq_of_coprime h_pos h_coprime
        have := h_temp.trans p_eq_natAbs
        simp only [Nat.cast_inj] at this
        exact this
      · -- Case when p is negative
        have h_neg : p < 0 := lt_of_le_of_ne (not_lt.mp h_pos) h_nonzero
        have h_pos : 0 < -p := by linarith
        -- Similar reasoning for negative p
        have h_temp := Rat.den_div_eq_of_coprime h_pos (by simpa using h_coprime)
        unfold r
        simp only [Int.cast_neg, div_neg, Rat.neg_den] at h_temp
        apply Nat.cast_injective (R := ℤ)
        rw [h_temp, Int.ofNat_natAbs_of_nonpos h_neg.le]

    -- Combine with previous result that denominator equals 1
    have p_natAbs_eq_1 : p.natAbs = 1 := by
      rw [← r_den_eq_p, ← den_dvd_1]
    exact p_natAbs_eq_1

  contradiction

[Ruben Van de Velde]

The more you try, the easier it becomes :)

[Ruben Van de Velde]

#28399

[Nick_adfor]

Ruben Van de Velde said:

The more you try, the easier it becomes :)

As my hu is in abs1, I can never use hu in the later proof : (

And all I've tried is to rw?, but it can never generate obtain. Also, I'm not familiar with IsFractionRing and IsLocalization, so I will even avoid using them.

[Nick_adfor]

Int.castRingHom, IsFractionRing.den, algebraMap, Rat.intcast,
Int.isCoprime in the former code are all generated automatically. But I do not try to read the related name space and package, which is important.

[Nick_adfor]

As for IsLocalization.IsInteger, I've never heard of that.