English
Given a linear map φ with free finite modules and L, if finrank R M ≤ #R, there exists x ∈ L with IsNilRegular φ x.
Русский
При условии finrank R M ≤ #R существует x ∈ L такое, что IsNilRegular φ x.
LaTeX
$$∃ x : L, IsNilRegular φ x$$
Lean4
theorem exists_isNilRegular_of_finrank_le_card (h : finrank R M ≤ #R) : ∃ x : L, IsNilRegular φ x :=
by
let b := chooseBasis R L
let bₘ := chooseBasis R M
let n := Fintype.card (ChooseBasisIndex R M)
have aux : ((polyCharpoly φ b).coeff (nilRank φ)).IsHomogeneous (n - nilRank φ) :=
polyCharpoly_coeff_isHomogeneous _ b (nilRank φ) (n - nilRank φ)
(by simp [n, nilRank_le_card φ bₘ, finrank_eq_card_chooseBasisIndex])
obtain ⟨x, hx⟩ : ∃ r, eval r ((polyCharpoly _ b).coeff (nilRank φ)) ≠ 0 :=
by
by_contra! h₀
apply polyCharpoly_coeff_nilRank_ne_zero φ b
apply aux.eq_zero_of_forall_eval_eq_zero_of_le_card h₀ (le_trans _ h)
simp only [n, finrank_eq_card_chooseBasisIndex, Nat.cast_le, Nat.sub_le]
let c := Finsupp.equivFunOnFinite.symm x
use b.repr.symm c
rwa [isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero _ b, LinearEquiv.apply_symm_apply]
