English
In a finite-dimensional representation, the eigenvalue μ of a primitive vector is a natural number. More precisely, under suitable Noetherian and domain assumptions with CharZero, there exists n ∈ ℕ such that μ = n.
Русский
В конечномерном представлении вес примитивного вектора μ является натуральным числом. Точнее: при приближённых условиях Noetherian, без нулевых делителей и CharZero существует n ∈ ℕ такое, что μ = n.
LaTeX
$$$\exists n \in \mathbb{N},\ \mu = n$$$
Lean4
/-- The eigenvalue of a primitive vector must be a natural number if the representation is
finite-dimensional. -/
theorem exists_nat [IsNoetherian R M] [NoZeroSMulDivisors R M] [IsDomain R] [CharZero R] : ∃ n : ℕ, μ = n :=
by
suffices ∃ n : ℕ, (ψ n) = 0
by
obtain ⟨n, hn₁, hn₂⟩ := Nat.exists_not_and_succ_of_not_zero_of_exists P.ne_zero this
refine ⟨n, ?_⟩
have := lie_e_pow_succ_toEnd_f P n
rw [hn₂, lie_zero, eq_comm, smul_eq_zero_iff_left hn₁, mul_eq_zero, sub_eq_zero] at this
exact this.resolve_left <| Nat.cast_add_one_ne_zero n
have hs : (range <| fun (n : ℕ) ↦ μ - 2 * n).Infinite := by rw [infinite_range_iff (fun n m ↦ by simp)];
infer_instance
by_contra! contra
exact
hs
((toEnd R L M h).eigenvectors_linearIndependent {μ - 2 * n | n : ℕ} (fun ⟨s, hs⟩ ↦ ψ Classical.choose hs)
(fun ⟨r, hr⟩ ↦ by
simp [lie_h_pow_toEnd_f P, Classical.choose_spec hr, contra, Module.End.hasEigenvector_iff])).finite
