English
Let w be a function from the index set to the field, and consider the diagonal matrix diag(w). Then the rank of diag(w) equals the cardinal lifted value of the set of indices where w is nonzero.
Русский
Пусть w : m → R и возьмём диагональную матрицу diag(w). Тогда ранг diag(w) равен поднятому к лейблу кардиналу множества индексов i таких, что w(i) ≠ 0.
LaTeX
$$$ (\mathrm{diag}(w)).\mathrm{cRank} = \operatorname{lift} \{ i \mid w(i) \neq 0\}. $$$
Lean4
theorem cRank_diagonal [DecidableEq m] (w : m → R) : (diagonal w).cRank = lift.{uR} #{ i // (w i) ≠ 0 } := by
classical
set w' : { i // (w i) ≠ 0 } → _ := fun i ↦ (diagonal w) i
have h : LinearIndependent R w' :=
by
have hli' :=
Pi.linearIndependent_single_of_ne_zero (R := R) (v := fun i : m ↦ if w i = 0 then (1 : R) else w i)
(by simp [ite_eq_iff'])
convert hli'.comp Subtype.val Subtype.val_injective
ext ⟨j, hj⟩ k
simp [w', diagonal, hj, Pi.single_apply, eq_comm]
have hrw : insert 0 (range (diagonal w)ᵀ) = insert 0 (range w') :=
by
suffices ∀ a, diagonal w a = 0 ∨ ∃ b, w b ≠ 0 ∧ diagonal w b = diagonal w a by
simpa [subset_antisymm_iff, subset_def, w']
simp_rw [or_iff_not_imp_right, not_exists, not_and, not_imp_not]
simp +contextual [funext_iff, diagonal]
rw [cRank, ← span_insert_zero, hrw, span_insert_zero, rank_span h, ← lift_umax, ←
Cardinal.mk_range_eq_of_injective h.injective, lift_id']
