English
For any matrices A, and index maps r,c, the rank of the submatrix A.submatrix r c does not exceed the rank of A (up to a universe lift).
Русский
Для любой матрицы A и вложенных отображений r, c ранг подматрицы A.submatrix r c не превосходит ранг самой матрицы A (с учётом переноса вселенных).
LaTeX
$$$\operatorname{lift}(A_{r,c}).\operatorname{cRank} \le \operatorname{lift}(A).\operatorname{cRank}.$$$
Lean4
theorem lift_cRank_submatrix_le (A : Matrix m n R) (r : m₀ → m) (c : n₀ → n) :
lift.{um} (A.submatrix r c).cRank ≤ lift.{um₀} A.cRank :=
by
have h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank :=
Submodule.rank_mono <| span_mono <| by rintro _ ⟨x, rfl⟩; exact ⟨c x, rfl⟩
refine (Cardinal.lift_monotone h).trans ?_
let f : (m → R) →ₗ[R] (m₀ → R) := LinearMap.funLeft R R r
have h_eq : Submodule.map f (span R (range Aᵀ)) = span R (range (A.submatrix r id)ᵀ) :=
by
rw [LinearMap.map_span, ← image_univ, image_image, transpose_submatrix]
aesop
rw [cRank, ← h_eq]
have hwin := lift_rank_map_le f (span R (range Aᵀ))
simp_rw [← lift_umax] at hwin ⊢
exact hwin
