feat: Generalize corollaries of rank-nullity theorem. (#9626)

Added a class `HasRankNullity` consisting of the rings that satisfy the rank-nullity theorem.
Generalized the corollaries of the rank-nullity theorem from division rings to rings satisfying the class,
and moved them into a new file `LinearAlgebra.Dimension.RankNullity`.



Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib.lean

@@ -2577,6 +2577,7 @@ import Mathlib.LinearAlgebra.Dimension.Finrank
 import Mathlib.LinearAlgebra.Dimension.Free
 import Mathlib.LinearAlgebra.Dimension.LinearMap
 import Mathlib.LinearAlgebra.Dimension.Localization
+import Mathlib.LinearAlgebra.Dimension.RankNullity
 import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 import Mathlib.LinearAlgebra.DirectSum.Finsupp
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct

Mathlib/LinearAlgebra/Dimension/Constructions.lean

@@ -44,25 +44,35 @@ variable [Module R M] [Module R M'] [Module R M₁]
 
 section Quotient
 
+theorem LinearIndependent.sum_elim_of_quotient
+    {M' : Submodule R M} {ι₁ ι₂} {f : ι₁ → M'} (hf : LinearIndependent R f) (g : ι₂ → M)
+    (hg : LinearIndependent R (Submodule.Quotient.mk (p := M') ∘ g)) :
+      LinearIndependent R (Sum.elim (f · : ι₁ → M) g) := by
+  refine .sum_type (hf.map' M'.subtype M'.ker_subtype) (.of_comp M'.mkQ hg) ?_
+  refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_
+  have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ (f i).prop) h₁
+  obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₂
+  simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsupp_sum, map_smul, mkQ_apply] at this
+  rw [linearIndependent_iff.mp hg _ this, Finsupp.sum_zero_index]
+
+theorem LinearIndependent.union_of_quotient
+    {M' : Submodule R M} {s : Set M} (hs : s ⊆ M') (hs' : LinearIndependent (ι := s) R Subtype.val)
+  {t : Set M} (ht : LinearIndependent (ι := t) R (Submodule.Quotient.mk (p := M') ∘ Subtype.val)) :
+    LinearIndependent (ι := (s ∪ t : _)) R Subtype.val := by
+  refine (LinearIndependent.sum_elim_of_quotient (f := Set.embeddingOfSubset s M' hs)
+    (of_comp M'.subtype (by simpa using hs')) Subtype.val ht).to_subtype_range' ?_
+  simp only [embeddingOfSubset_apply_coe, Sum.elim_range, Subtype.range_val]
+
 theorem rank_quotient_add_rank_le [Nontrivial R] (M' : Submodule R M) :
     Module.rank R (M ⧸ M') + Module.rank R M' ≤ Module.rank R M := by
-  simp_rw [Module.rank_def]
+  conv_lhs => simp only [Module.rank_def]
   have := nonempty_linearIndependent_set R (M ⧸ M')
   have := nonempty_linearIndependent_set R M'
   rw [Cardinal.ciSup_add_ciSup _ (bddAbove_range.{v, v} _) _ (bddAbove_range.{v, v} _)]
   refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_
   choose f hf using Quotient.mk_surjective M'
-  let g : s ⊕ t → M := Sum.elim (f ·) (·)
-  suffices LinearIndependent R g by
-    refine le_trans ?_ (le_ciSup (bddAbove_range.{v, v} _) ⟨_, this.to_subtype_range⟩)
-    rw [mk_range_eq _ this.injective, mk_sum, lift_id, lift_id]
-  refine .sum_type (.of_comp M'.mkQ ?_) (ht.map' M'.subtype M'.ker_subtype) ?_
-  · convert hs; ext x; exact hf x
-  refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_
-  have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ i.1.2) h₂
-  obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₁
-  simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsupp_sum, map_smul, mkQ_apply, hf] at this
-  rw [linearIndependent_iff.mp hs _ this, Finsupp.sum_zero_index]
+  simpa [add_comm] using (LinearIndependent.sum_elim_of_quotient ht (fun (i : s) ↦ f i)
+    (by simpa [Function.comp, hf] using hs)).cardinal_le_rank
 
 theorem rank_quotient_le (p : Submodule R M) : Module.rank R (M ⧸ p) ≤ Module.rank R M :=
   (mkQ p).rank_le_of_surjective (surjective_quot_mk _)

Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

@@ -7,7 +7,7 @@ Scott Morrison, Chris Hughes, Anne Baanen, Junyan Xu
 import Mathlib.LinearAlgebra.Basis.VectorSpace
 import Mathlib.LinearAlgebra.Dimension.Finite
 import Mathlib.SetTheory.Cardinal.Subfield
-import Mathlib.LinearAlgebra.Dimension.Constructions
+import Mathlib.LinearAlgebra.Dimension.RankNullity
 
 #align_import linear_algebra.dimension from "leanprover-community/mathlib"@"47a5f8186becdbc826190ced4312f8199f9db6a5"
 
@@ -21,7 +21,7 @@ over division rings.
 
 For vector spaces (i.e. modules over a field), we have
 
-* `rank_quotient_add_rank`: if `V₁` is a submodule of `V`, then
+* `rank_quotient_add_rank_of_divisionRing`: if `V₁` is a submodule of `V`, then
   `Module.rank (V/V₁) + Module.rank V₁ = Module.rank V`.
 * `rank_range_add_rank_ker`: the rank-nullity theorem.
 * `rank_dual_eq_card_dual_of_aleph0_le_rank`: The **Erdős-Kaplansky Theorem** which says that
@@ -33,7 +33,7 @@ For vector spaces (i.e. modules over a field), we have
 
 noncomputable section
 
-universe u v v' v'' u₁' w w'
+universe u₀ u v v' v'' u₁' w w'
 
 variable {K R : Type u} {V V₁ V₂ V₃ : Type v} {V' V'₁ : Type v'} {V'' : Type v''}
 variable {ι : Type w} {ι' : Type w'} {η : Type u₁'} {φ : η → Type*}
@@ -55,60 +55,20 @@ theorem Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0 (h : Module.rank K V <
   finite_def.2 <| (Basis.ofVectorSpace K V).nonempty_fintype_index_of_rank_lt_aleph0 h
 #align basis.finite_of_vector_space_index_of_rank_lt_aleph_0 Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0
 
-theorem rank_quotient_add_rank (p : Submodule K V) :
+/-- Also see `rank_quotient_add_rank`. -/
+theorem rank_quotient_add_rank_of_divisionRing (p : Submodule K V) :
     Module.rank K (V ⧸ p) + Module.rank K p = Module.rank K V := by
   classical
     let ⟨f⟩ := quotient_prod_linearEquiv p
     exact rank_prod'.symm.trans f.rank_eq
-#align rank_quotient_add_rank rank_quotient_add_rank
-
-/-- The **rank-nullity theorem** -/
-theorem rank_range_add_rank_ker (f : V →ₗ[K] V₁) :
-    Module.rank K (LinearMap.range f) + Module.rank K (LinearMap.ker f) = Module.rank K V := by
-  haveI := fun p : Submodule K V => Classical.decEq (V ⧸ p)
-  rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank]
-#align rank_range_add_rank_ker rank_range_add_rank_ker
-
-theorem rank_eq_of_surjective (f : V →ₗ[K] V₁) (h : Surjective f) :
-    Module.rank K V = Module.rank K V₁ + Module.rank K (LinearMap.ker f) := by
-  rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h]
-#align rank_eq_of_surjective rank_eq_of_surjective
-
-/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend
-the family by another vector while retaining linear independence. -/
-theorem exists_linearIndependent_cons_of_lt_rank {n : ℕ} {v : Fin n → V}
-    (hv : LinearIndependent K v) (h : n < Module.rank K V) :
-    ∃ (x : V), LinearIndependent K (Fin.cons x v) := by
-  have A : Submodule.span K (range v) ≠ ⊤ := by
-    intro H
-    rw [← rank_top, ← H] at h
-    have : Module.rank K (Submodule.span K (range v)) ≤ n := by
-      have := Cardinal.mk_range_le_lift (f := v)
-      simp only [Cardinal.lift_id'] at this
-      exact (rank_span_le _).trans (this.trans (by simp))
-    exact lt_irrefl _ (h.trans_le this)
-  obtain ⟨x, hx⟩ : ∃ x, x ∉ Submodule.span K (range v) := by
-    contrapose! A
-    exact Iff.mpr Submodule.eq_top_iff' A
-  exact ⟨x, linearIndependent_fin_cons.2 ⟨hv, hx⟩⟩
-
-/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend
-the family by another vector while retaining linear independence. -/
-theorem exists_linearIndependent_snoc_of_lt_rank {n : ℕ} {v : Fin n → V}
-    (hv : LinearIndependent K v) (h : n < Module.rank K V) :
-    ∃ (x : V), LinearIndependent K (Fin.snoc v x) := by
-  simpa [linearIndependent_fin_cons, ← linearIndependent_fin_snoc]
-    using exists_linearIndependent_cons_of_lt_rank hv h
-
-/-- Given a nonzero vector in a space of dimension `> 1`, one may find another vector linearly
-independent of the first one. -/
-theorem exists_linearIndependent_pair_of_one_lt_rank
-    (h : 1 < Module.rank K V) {x : V} (hx : x ≠ 0) :
-    ∃ y, LinearIndependent K ![x, y] := by
-  obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (linearIndependent_unique ![x] hx) h
-  have : Fin.snoc ![x] y = ![x, y] := Iff.mp List.ofFn_inj rfl
-  rw [this] at hy
-  exact ⟨y, hy⟩
+
+instance DivisionRing.hasRankNullity : HasRankNullity.{u₀} K where
+  rank_quotient_add_rank := rank_quotient_add_rank_of_divisionRing
+  exists_set_linearIndependent V _ _ := by
+    let b := Module.Free.chooseBasis K V
+    refine ⟨range b, ?_, b.linearIndependent.to_subtype_range⟩
+    rw [← lift_injective.eq_iff, mk_range_eq_of_injective b.injective,
+      Module.Free.rank_eq_card_chooseBasisIndex]
 
 section
 
@@ -125,7 +85,7 @@ theorem rank_add_rank_split (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd
   have hf : Surjective (coprod db eb) := by rwa [← range_eq_top, range_coprod, eq_top_iff]
   conv =>
     rhs
-    rw [← rank_prod', rank_eq_of_surjective _ hf]
+    rw [← rank_prod', rank_eq_of_surjective hf]
   congr 1
   apply LinearEquiv.rank_eq
   let L : V₁ →ₗ[K] ker (coprod db eb) := by -- Porting note: this is needed to avoid a timeout
@@ -148,29 +108,6 @@ theorem rank_add_rank_split (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd
     rw [h₂, _root_.neg_neg]
 #align rank_add_rank_split rank_add_rank_split
 
-theorem Submodule.rank_sup_add_rank_inf_eq (s t : Submodule K V) :
-    Module.rank K (s ⊔ t : Submodule K V) + Module.rank K (s ⊓ t : Submodule K V) =
-    Module.rank K s + Module.rank K t :=
-  rank_add_rank_split
-    (inclusion le_sup_left) (inclusion le_sup_right)
-    (inclusion inf_le_left) (inclusion inf_le_right)
-    (by
-      rw [← map_le_map_iff' (ker_subtype <| s ⊔ t), Submodule.map_sup, Submodule.map_top, ←
-        LinearMap.range_comp, ← LinearMap.range_comp, subtype_comp_inclusion,
-        subtype_comp_inclusion, range_subtype, range_subtype, range_subtype])
-    (ker_inclusion _ _ _) (by ext ⟨x, hx⟩; rfl)
-    (by
-      rintro ⟨b₁, hb₁⟩ ⟨b₂, hb₂⟩ eq
-      obtain rfl : b₁ = b₂ := congr_arg Subtype.val eq
-      exact ⟨⟨b₁, hb₁, hb₂⟩, rfl, rfl⟩)
-#align submodule.rank_sup_add_rank_inf_eq Submodule.rank_sup_add_rank_inf_eq
-
-theorem Submodule.rank_add_le_rank_add_rank (s t : Submodule K V) :
-    Module.rank K (s ⊔ t : Submodule K V) ≤ Module.rank K s + Module.rank K t := by
-  rw [← Submodule.rank_sup_add_rank_inf_eq]
-  exact self_le_add_right _ _
-#align submodule.rank_add_le_rank_add_rank Submodule.rank_add_le_rank_add_rank
-
 end
 
 end DivisionRing
@@ -307,35 +244,6 @@ theorem Module.rank_le_one_iff_top_isPrincipal :
 
 end Module
 
-section Span
-
-open Submodule FiniteDimensional
-
-variable [DivisionRing K] [AddCommGroup V] [Module K V]
-
-/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
-dimension `> n`, one may extend the family by another vector while retaining linear independence. -/
-theorem exists_linearIndependent_snoc_of_lt_finrank {n : ℕ} {v : Fin n → V}
-    (hv : LinearIndependent K v) (h : n < finrank K V) :
-    ∃ (x : V), LinearIndependent K (Fin.snoc v x) :=
-  exists_linearIndependent_snoc_of_lt_rank hv (lt_rank_of_lt_finrank h)
-
-/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
-dimension `> n`, one may extend the family by another vector while retaining linear independence. -/
-theorem exists_linearIndependent_cons_of_lt_finrank {n : ℕ} {v : Fin n → V}
-    (hv : LinearIndependent K v) (h : n < finrank K V) :
-    ∃ (x : V), LinearIndependent K (Fin.cons x v) :=
-  exists_linearIndependent_cons_of_lt_rank hv (lt_rank_of_lt_finrank h)
-
-/-- Given a nonzero vector in a finite-dimensional space of dimension `> 1`, one may find another
-vector linearly independent of the first one. -/
-theorem exists_linearIndependent_pair_of_one_lt_finrank
-    (h : 1 < finrank K V) {x : V} (hx : x ≠ 0) :
-    ∃ y, LinearIndependent K ![x, y] :=
-  exists_linearIndependent_pair_of_one_lt_rank (one_lt_rank_of_one_lt_finrank h) hx
-
-end Span
-
 section Basis
 
 open FiniteDimensional

Mathlib/LinearAlgebra/Dimension/Finite.lean

@@ -211,6 +211,54 @@ alias finset_card_le_finrank_of_linearIndependent := LinearIndependent.finset_ca
 @[deprecated]
 alias Module.Finite.lt_aleph0_of_linearIndependent := LinearIndependent.lt_aleph0_of_finite
 
+lemma exists_set_linearIndependent_of_lt_rank {n : Cardinal} (hn : n < Module.rank R M) :
+    ∃ s : Set M, #s = n ∧ LinearIndependent R ((↑) : s → M) := by
+  obtain ⟨⟨s, hs⟩, hs'⟩ := exists_lt_of_lt_ciSup' (hn.trans_eq (Module.rank_def R M))
+  obtain ⟨t, ht, ht'⟩ := le_mk_iff_exists_subset.mp hs'.le
+  exact ⟨t, ht', .mono ht hs⟩
+
+lemma exists_finset_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.rank R M) :
+    ∃ s : Finset M, s.card = n ∧ LinearIndependent R ((↑) : s → M) := by
+  have := nonempty_linearIndependent_set
+  cases' hn.eq_or_lt with h h
+  · obtain ⟨⟨s, hs⟩, hs'⟩ := Cardinal.exists_eq_natCast_of_iSup_eq _
+      (Cardinal.bddAbove_range.{v, v} _) _ (h.trans (Module.rank_def R M)).symm
+    have : Finite s := lt_aleph0_iff_finite.mp (hs' ▸ nat_lt_aleph0 n)
+    cases nonempty_fintype s
+    exact ⟨s.toFinset, by simpa using hs', by convert hs <;> exact Set.mem_toFinset⟩
+  · obtain ⟨s, hs, hs'⟩ := exists_set_linearIndependent_of_lt_rank h
+    have : Finite s := lt_aleph0_iff_finite.mp (hs ▸ nat_lt_aleph0 n)
+    cases nonempty_fintype s
+    exact ⟨s.toFinset, by simpa using hs, by convert hs' <;> exact Set.mem_toFinset⟩
+
+lemma exists_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.rank R M) :
+    ∃ f : Fin n → M, LinearIndependent R f :=
+  have ⟨_, hs, hs'⟩ := exists_finset_linearIndependent_of_le_rank hn
+  ⟨_, (linearIndependent_equiv (Finset.equivFinOfCardEq hs).symm).mpr hs'⟩
+
+lemma natCast_le_rank_iff {n : ℕ} :
+    n ≤ Module.rank R M ↔ ∃ f : Fin n → M, LinearIndependent R f :=
+  ⟨exists_linearIndependent_of_le_rank,
+    fun H ↦ by simpa using H.choose_spec.cardinal_lift_le_rank⟩
+
+lemma natCast_le_rank_iff_finset {n : ℕ} :
+    n ≤ Module.rank R M ↔ ∃ s : Finset M, s.card = n ∧ LinearIndependent R ((↑) : s → M) :=
+  ⟨exists_finset_linearIndependent_of_le_rank,
+    fun ⟨s, h₁, h₂⟩ ↦ by simpa [h₁] using h₂.cardinal_le_rank⟩
+
+lemma exists_finset_linearIndependent_of_le_finrank {n : ℕ} (hn : n ≤ finrank R M) :
+    ∃ s : Finset M, s.card = n ∧ LinearIndependent R ((↑) : s → M) := by
+  by_cases h : finrank R M = 0
+  · rw [le_zero_iff.mp (hn.trans_eq h)]
+    exact ⟨∅, rfl, by convert linearIndependent_empty R M using 2 <;> aesop⟩
+  exact exists_finset_linearIndependent_of_le_rank
+    ((natCast_le.mpr hn).trans_eq (cast_toNat_of_lt_aleph0 (toNat_ne_zero.mp h).2))
+
+lemma exists_linearIndependent_of_le_finrank {n : ℕ} (hn : n ≤ finrank R M) :
+    ∃ f : Fin n → M, LinearIndependent R f :=
+  have ⟨_, hs, hs'⟩ := exists_finset_linearIndependent_of_le_finrank hn
+  ⟨_, (linearIndependent_equiv (Finset.equivFinOfCardEq hs).symm).mpr hs'⟩
+
 variable [Module.Finite R M]
 
 theorem Module.Finite.not_linearIndependent_of_infinite {ι : Type*} [Infinite ι]