feat: miscellaneous results about finrank (#18064)

From `flt-regular`.

Mathlib/LinearAlgebra/Dimension/RankNullity.lean

@@ -24,7 +24,7 @@ See `nonempty_oreSet_of_strongRankCondition` for a start.
 -/
 universe u v
 
-open Function Set Cardinal
+open Function Set Cardinal Submodule LinearMap
 
 variable {R} {M M₁ M₂ M₃ : Type u} {M' : Type v} [Ring R]
 variable [AddCommGroup M] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M']
@@ -49,7 +49,7 @@ class HasRankNullity (R : Type v) [inst : Ring R] : Prop where
 
 variable [HasRankNullity.{u} R]
 
-lemma rank_quotient_add_rank (N : Submodule R M) :
+lemma Submodule.rank_quotient_add_rank (N : Submodule R M) :
     Module.rank R (M ⧸ N) + Module.rank R N = Module.rank R M :=
   HasRankNullity.rank_quotient_add_rank N
 
@@ -66,24 +66,24 @@ theorem nontrivial_of_hasRankNullity : Nontrivial R := by
 
 attribute [local instance] nontrivial_of_hasRankNullity
 
-theorem lift_rank_range_add_rank_ker (f : M →ₗ[R] M') :
+theorem LinearMap.lift_rank_range_add_rank_ker (f : M →ₗ[R] M') :
     lift.{u} (Module.rank R (LinearMap.range f)) + lift.{v} (Module.rank R (LinearMap.ker f)) =
       lift.{v} (Module.rank R M) := by
   haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p)
   rw [← f.quotKerEquivRange.lift_rank_eq, ← lift_add, rank_quotient_add_rank]
 
 /-- The **rank-nullity theorem** -/
-theorem rank_range_add_rank_ker (f : M →ₗ[R] M₁) :
+theorem LinearMap.rank_range_add_rank_ker (f : M →ₗ[R] M₁) :
     Module.rank R (LinearMap.range f) + Module.rank R (LinearMap.ker f) = Module.rank R M := by
   haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p)
   rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank]
 
-theorem lift_rank_eq_of_surjective {f : M →ₗ[R] M'} (h : Surjective f) :
+theorem LinearMap.lift_rank_eq_of_surjective {f : M →ₗ[R] M'} (h : Surjective f) :
     lift.{v} (Module.rank R M) =
       lift.{u} (Module.rank R M') + lift.{v} (Module.rank R (LinearMap.ker f)) := by
   rw [← lift_rank_range_add_rank_ker f, ← rank_range_of_surjective f h]
 
-theorem rank_eq_of_surjective {f : M →ₗ[R] M₁} (h : Surjective f) :
+theorem LinearMap.rank_eq_of_surjective {f : M →ₗ[R] M₁} (h : Surjective f) :
     Module.rank R M = Module.rank R M₁ + Module.rank R (LinearMap.ker f) := by
   rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h]
 
@@ -92,7 +92,7 @@ theorem exists_linearIndependent_of_lt_rank [StrongRankCondition R]
     ∃ t, s ⊆ t ∧ #t = Module.rank R M ∧ LinearIndependent (ι := t) R Subtype.val := by
   obtain ⟨t, ht, ht'⟩ := exists_set_linearIndependent R (M ⧸ Submodule.span R s)
   choose sec hsec using Submodule.Quotient.mk_surjective (Submodule.span R s)
-  have hsec' : Submodule.Quotient.mk ∘ sec = id := funext hsec
+  have hsec' : Submodule.Quotient.mk ∘ sec = _root_.id := funext hsec
   have hst : Disjoint s (sec '' t) := by
     rw [Set.disjoint_iff]
     rintro _ ⟨hxs, ⟨x, hxt, rfl⟩⟩
@@ -140,8 +140,8 @@ theorem exists_linearIndependent_pair_of_one_lt_rank [StrongRankCondition R]
   rw [this] at hy
   exact ⟨y, hy⟩
 
-theorem exists_smul_not_mem_of_rank_lt {N : Submodule R M} (h : Module.rank R N < Module.rank R M) :
-    ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N := by
+theorem Submodule.exists_smul_not_mem_of_rank_lt {N : Submodule R M}
+    (h : Module.rank R N < Module.rank R M) : ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N := by
   have : Module.rank R (M ⧸ N) ≠ 0 := by
     intro e
     rw [← rank_quotient_add_rank N, e, zero_add] at h
@@ -196,4 +196,38 @@ theorem exists_linearIndependent_pair_of_one_lt_finrank [NoZeroSMulDivisors R M]
     ∃ y, LinearIndependent R ![x, y] :=
   exists_linearIndependent_pair_of_one_lt_rank (one_lt_rank_of_one_lt_finrank h) hx
 
+/-- Rank-nullity theorem using `finrank`. -/
+lemma Submodule.finrank_quotient_add_finrank [Module.Finite R M] (N : Submodule R M) :
+    finrank R (M ⧸ N) + finrank R N = finrank R M := by
+  rw [← Nat.cast_inj (R := Cardinal), Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
+    Submodule.finrank_eq_rank]
+  exact HasRankNullity.rank_quotient_add_rank _
+
+
+/-- Rank-nullity theorem using `finrank` and subtraction. -/
+lemma Submodule.finrank_quotient [Module.Finite R M] {S : Type*} [Ring S] [SMul R S] [Module S M]
+    [IsScalarTower R S M] (N : Submodule S M) : finrank R (M ⧸ N) = finrank R M - finrank R N := by
+  rw [← (N.restrictScalars R).finrank_quotient_add_finrank]
+  exact Nat.eq_sub_of_add_eq rfl
+
 end Finrank
+
+section
+
+open Submodule Module
+
+variable [StrongRankCondition R] [Module.Finite R M]
+
+lemma Submodule.exists_of_finrank_lt (N : Submodule R M) (h : finrank R N < finrank R M) :
+    ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N := by
+  obtain ⟨s, hs, hs'⟩ :=
+    exists_finset_linearIndependent_of_le_finrank (R := R) (M := M ⧸ N) le_rfl
+  obtain ⟨v, hv⟩ : s.Nonempty := by rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
+    hs, finrank_quotient, tsub_eq_zero_iff_le, not_le]
+  obtain ⟨v, rfl⟩ := N.mkQ_surjective v
+  refine ⟨v, fun r hr ↦ mt ?_ hr⟩
+  have := linearIndependent_iff.mp hs' (Finsupp.single ⟨_, hv⟩ r)
+  rwa [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← LinearMap.map_smul,
+    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this
+
+end

Mathlib/LinearAlgebra/FiniteDimensional.lean

@@ -33,14 +33,6 @@ section DivisionRing
 
 variable [DivisionRing K] [AddCommGroup V] [Module K V]
 
-/-- In a finite-dimensional vector space, the dimensions of a submodule and of the corresponding
-quotient add up to the dimension of the space. -/
-theorem finrank_quotient_add_finrank [FiniteDimensional K V] (s : Submodule K V) :
-    finrank K (V ⧸ s) + finrank K s = finrank K V := by
-  have := rank_quotient_add_rank s
-  rw [← finrank_eq_rank, ← finrank_eq_rank, ← finrank_eq_rank] at this
-  exact mod_cast this
-
 /-- The dimension of a strict submodule is strictly bounded by the dimension of the ambient
 space. -/
 theorem finrank_lt [FiniteDimensional K V] {s : Submodule K V} (h : s < ⊤) :

Mathlib/NumberTheory/RamificationInertia.lean

@@ -588,7 +588,7 @@ theorem rank_pow_quot_aux [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 :
   letI : Field (R ⧸ p) := Ideal.Quotient.field _
   rw [← rank_range_of_injective _ (powQuotSuccInclusion_injective f p P i),
     (quotientRangePowQuotSuccInclusionEquiv f p P hP0 hi).symm.rank_eq]
-  exact (rank_quotient_add_rank (LinearMap.range (powQuotSuccInclusion f p P i))).symm
+  exact (Submodule.rank_quotient_add_rank (LinearMap.range (powQuotSuccInclusion f p P i))).symm
 
 theorem rank_pow_quot [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥)
     (i : ℕ) (hi : i ≤ e) :