feat: Rank-nullity theorem for commutative domains (#9412)

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

Mathlib.lean

@@ -334,6 +334,7 @@ import Mathlib.Algebra.Module.Submodule.Basic
 import Mathlib.Algebra.Module.Submodule.Bilinear
 import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.Algebra.Module.Submodule.LinearMap
+import Mathlib.Algebra.Module.Submodule.Localization
 import Mathlib.Algebra.Module.Submodule.Map
 import Mathlib.Algebra.Module.Submodule.Pointwise
 import Mathlib.Algebra.Module.Torsion
@@ -2394,6 +2395,7 @@ import Mathlib.LinearAlgebra.Dimension.Finite
 import Mathlib.LinearAlgebra.Dimension.Finrank
 import Mathlib.LinearAlgebra.Dimension.Free
 import Mathlib.LinearAlgebra.Dimension.LinearMap
+import Mathlib.LinearAlgebra.Dimension.Localization
 import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 import Mathlib.LinearAlgebra.DirectSum.Finsupp
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct

Mathlib/Algebra/Module/LocalizedModule.lean

@@ -551,7 +551,11 @@ variable {R : Type*} [CommSemiring R] (S : Submonoid R)
 
 variable {M M' M'' : Type*} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M'']
 
-variable [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'')
+variable {A : Type*} [CommSemiring A] [Algebra R A] [Module A M'] [IsLocalization S A]
+
+variable [Module R M] [Module R M'] [Module R M''] [IsScalarTower R A M']
+
+variable (f : M →ₗ[R] M') (g : M →ₗ[R] M'')
 
 /-- The characteristic predicate for localized module.
 `IsLocalizedModule S f` describes that `f : M ⟶ M'` is the localization map identifying `M'` as
@@ -1045,6 +1049,14 @@ theorem mk_eq_mk' (s : S) (m : M) :
     LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_apply]
 #align is_localized_module.mk_eq_mk' IsLocalizedModule.mk_eq_mk'
 
+variable (A) in
+lemma mk'_smul_mk' (x : R) (m : M) (s t : S) :
+    IsLocalization.mk' A x s • mk' f m t = mk' f (x • m) (s * t) := by
+  apply smul_injective f (s * t)
+  conv_lhs => simp only [smul_assoc, mul_smul, smul_comm t]
+  simp only [mk'_cancel', map_smul, Submonoid.smul_def s]
+  rw [← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul]
+
 variable (S)
 
 theorem eq_zero_iff {m : M} : f m = 0 ↔ ∃ s' : S, s' • m = 0 :=
@@ -1089,10 +1101,6 @@ theorem mkOfAlgebra {R S S' : Type*} [CommRing R] [CommRing S] [CommRing S'] [Al
 
 end Algebra
 
-variable {A : Type*}
-  [CommSemiring A] [Algebra R A] [Module A M'] [IsScalarTower R A M'] [IsLocalization S A]
-
-
 /-- If `(f : M →ₗ[R] M')` is a localization of modules, then the map
 `(localization S) × M → N, (s, m) ↦ s • f m` is the tensor product (insomuch as it is the universal
 bilinear map).

Mathlib/Algebra/Module/Submodule/Localization.lean

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.Algebra.Module.LocalizedModule
+
+/-!
+# Localization of Submodules
+
+Results about localizations of submodules and quotient modules are provided in this file.
+
+## Main result
+- `Submodule.localized`:
+  The localization of an `R`-submodule of `M` at `p` viewed as an `Rₚ`-submodule of `Mₚ`.
+- `Submodule.toLocalized`:
+  The localization map of a submodule `M' →ₗ[R] M'.localized p`.
+- `Submodule.toLocalizedQuotient`:
+  The localization map of a quotient module `M ⧸ M' →ₗ[R] LocalizedModule p M ⧸ M'.localized p`.
+
+## TODO
+- Statements regarding the exactness of localization.
+- Connection with flatness.
+
+-/
+
+open nonZeroDivisors
+
+universe u u' v v'
+
+variable {R : Type u} (S : Type u') {M : Type v} {N : Type v'}
+variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M]
+variable [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N]
+variable (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f]
+variable (hp : p ≤ R⁰)
+
+variable (M' : Submodule R M)
+
+/-- Let `S` be the localization of `R` at `p` and `N` be the localization of `M` at `p`.
+This is the localization of an `R`-submodule of `M` viewed as an `S`-submodule of `N`. -/
+def Submodule.localized' : Submodule S N where
+  carrier := { x | ∃ m ∈ M', ∃ s : p, IsLocalizedModule.mk' f m s = x }
+  add_mem' := fun {x} {y} ⟨m, hm, s, hx⟩ ⟨n, hn, t, hy⟩ ↦ ⟨t • m + s • n, add_mem (M'.smul_mem t hm)
+    (M'.smul_mem s hn), s * t, by rw [← hx, ← hy, IsLocalizedModule.mk'_add_mk']⟩
+  zero_mem' := ⟨0, zero_mem _, 1, by simp⟩
+  smul_mem' := fun r x h ↦ by
+    have ⟨m, hm, s, hx⟩ := h
+    have ⟨y, t, hyt⟩ := IsLocalization.mk'_surjective p r
+    exact ⟨y • m, M'.smul_mem y hm, t * s, by simp [← hyt, ← hx, IsLocalizedModule.mk'_smul_mk']⟩
+
+/-- The localization of an `R`-submodule of `M` at `p` viewed as an `Rₚ`-submodule of `Mₚ`. -/
+abbrev Submodule.localized : Submodule (Localization p) (LocalizedModule p M) :=
+  M'.localized' (Localization p) p (LocalizedModule.mkLinearMap p M)
+
+/-- The localization map of a submodule. -/
+@[simps!]
+def Submodule.toLocalized' : M' →ₗ[R] M'.localized' S p f :=
+  f.restrict (q := (M'.localized' S p f).restrictScalars R) (fun x hx ↦ ⟨x, hx, 1, by simp⟩)
+
+/-- The localization map of a submodule. -/
+abbrev Submodule.toLocalized : M' →ₗ[R] M'.localized p :=
+  M'.toLocalized' (Localization p) p (LocalizedModule.mkLinearMap p M)
+
+instance Submodule.isLocalizedModule : IsLocalizedModule p (M'.toLocalized' S p f) where
+  map_units x := by
+    simp_rw [Module.End_isUnit_iff]
+    constructor
+    · exact fun _ _ e ↦ Subtype.ext
+        (IsLocalizedModule.smul_injective f x (congr_arg Subtype.val e))
+    · rintro m
+      use (IsLocalization.mk' S 1 x) • m
+      rw [Module.algebraMap_end_apply, ← smul_assoc, IsLocalization.smul_mk'_one,
+        IsLocalization.mk'_self', one_smul]
+  surj' := by
+    rintro ⟨y, x, hx, s, rfl⟩
+    exact ⟨⟨⟨x, hx⟩, s⟩, by ext; simp⟩
+  exists_of_eq e := by simpa [Subtype.ext_iff] using
+      IsLocalizedModule.exists_of_eq (S := p) (f := f) (congr_arg Subtype.val e)
+
+/-- The localization map of a quotient module. -/
+def Submodule.toLocalizedQuotient' : M ⧸ M' →ₗ[R] N ⧸ M'.localized' S p f :=
+  Submodule.mapQ M' ((M'.localized' S p f).restrictScalars R) f (fun x hx ↦ ⟨x, hx, 1, by simp⟩)
+
+/-- The localization map of a quotient module. -/
+abbrev Submodule.toLocalizedQuotient : M ⧸ M' →ₗ[R] LocalizedModule p M ⧸ M'.localized p :=
+  M'.toLocalizedQuotient' (Localization p) p (LocalizedModule.mkLinearMap p M)
+
+@[simp]
+lemma Submodule.toLocalizedQuotient'_mk (x : M) :
+    M'.toLocalizedQuotient' S p f (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x) := rfl
+
+open Submodule Submodule.Quotient IsLocalization in
+instance IsLocalizedModule.toLocalizedQuotient' (M' : Submodule R M) :
+    IsLocalizedModule p (M'.toLocalizedQuotient' S p f) where
+  map_units x := by
+    refine (Module.End_isUnit_iff _).mpr ⟨fun m n e ↦ ?_, fun m ↦ ⟨(IsLocalization.mk' S 1 x) • m,
+        by rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]⟩⟩
+    obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)
+    simp only [Module.algebraMap_end_apply, ← mk_smul, Submodule.Quotient.eq, ← smul_sub] at e
+    replace e := Submodule.smul_mem _ (IsLocalization.mk' S 1 x) e
+    rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e
+  surj' y := by
+    obtain ⟨y, rfl⟩ := mk_surjective _ y
+    obtain ⟨⟨y, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f y
+    exact ⟨⟨Submodule.Quotient.mk y, s⟩,
+      by simp only [Function.uncurry_apply_pair, toLocalizedQuotient'_mk, ← mk_smul, mk'_cancel']⟩
+  exists_of_eq {m n} e := by
+    obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)
+    obtain ⟨x, hx, s, hs⟩ : f (m - n) ∈ _ := by simpa [Submodule.Quotient.eq] using e
+    obtain ⟨c, hc⟩ := exists_of_eq (S := p) (show f (s • (m - n)) = f x by simp [-map_sub, ← hs])
+    exact ⟨c * s, by simpa only [← Quotient.mk_smul, Submodule.Quotient.eq,
+      ← smul_sub, mul_smul, hc] using M'.smul_mem c hx⟩
+
+instance (M' : Submodule R M) : IsLocalizedModule p (M'.toLocalizedQuotient p) :=
+  IsLocalizedModule.toLocalizedQuotient' _ _ _ _

Mathlib/Algebra/Module/Zlattice.lean

@@ -464,7 +464,7 @@ theorem Zlattice.rank : finrank ℤ L = finrank K E := by
         Finset.sdiff_eq_empty_iff_subset] at h
       replace h := Finset.card_le_card h
       rwa [not_lt, h_card, ← topEquiv.finrank_eq, ← h_spanE, ← ht_span,
-        finrank_span_set_eq_card _ ht_lin]
+        finrank_span_set_eq_card ht_lin]
     -- Assume that `e ∪ {v}` is not `ℤ`-linear independent then we get the contradiction
     suffices ¬ LinearIndependent ℤ (fun x : ↥(insert v (Set.range e)) => (x : E)) by
       contrapose! this
@@ -500,6 +500,6 @@ theorem Zlattice.rank : finrank ℤ L = finrank K E := by
   · -- To prove that `finrank K E ≤ finrank ℤ L`, we use the fact `b` generates `E` over `K`
     -- and thus `finrank K E ≤ card b = finrank ℤ L`
     rw [← topEquiv.finrank_eq, ← h_spanE]
-    convert finrank_span_le_card (K := K) (Set.range b)
+    convert finrank_span_le_card (R := K) (Set.range b)
 
 end Zlattice

Mathlib/LinearAlgebra/Dimension/Constructions.lean

@@ -374,27 +374,6 @@ theorem FiniteDimensional.finrank_tensorProduct :
 
 end TensorProduct
 
-section Span
-
-variable [StrongRankCondition R]
-
-theorem rank_span_le_of_finite {s : Set M} (hs : s.Finite) : Module.rank R (span R s) ≤ #s := by
-  rw [Module.rank_def]
-  apply ciSup_le'
-  rintro ⟨t, ht⟩
-  letI := hs.fintype
-  simpa [Cardinal.mk_image_eq Subtype.val_injective] using linearIndependent_le_span' _
-    (ht.map (f := Submodule.subtype _) (by simp)).image s (fun x ↦ by aesop)
-
-theorem rank_span_finset_le (s : Finset M) : Module.rank R (span R (s : Set M)) ≤ s.card := by
-  simpa using rank_span_le_of_finite s.finite_toSet
-
-theorem rank_span_of_finset (s : Finset M) : Module.rank R (span R (s : Set M)) < ℵ₀ :=
-  (rank_span_finset_le s).trans_lt (Cardinal.nat_lt_aleph0 _)
-#align rank_span_of_finset rank_span_of_finset
-
-end Span
-
 section SubmoduleRank
 
 section
@@ -449,9 +428,93 @@ theorem Submodule.finrank_le_finrank_of_le {s t : Submodule R M} [Module.Finite
 
 end
 
-
 end SubmoduleRank
 
+section Span
+
+variable [StrongRankCondition R]
+
+theorem rank_span_le (s : Set M) : Module.rank R (span R s) ≤ #s := by
+  rw [Finsupp.span_eq_range_total, ← lift_strictMono.le_iff_le]
+  refine (lift_rank_range_le _).trans ?_
+  rw [rank_finsupp_self]
+  simp only [lift_lift, ge_iff_le, le_refl]
+#align rank_span_le rank_span_le
+
+theorem rank_span_finset_le (s : Finset M) : Module.rank R (span R (s : Set M)) ≤ s.card := by
+  simpa using rank_span_le s.toSet
+
+theorem rank_span_of_finset (s : Finset M) : Module.rank R (span R (s : Set M)) < ℵ₀ :=
+  (rank_span_finset_le s).trans_lt (Cardinal.nat_lt_aleph0 _)
+#align rank_span_of_finset rank_span_of_finset
+
+open Submodule FiniteDimensional
+
+variable (R)
+
+/-- The rank of a set of vectors as a natural number. -/
+protected noncomputable def Set.finrank (s : Set M) : ℕ :=
+  finrank R (span R s)
+#align set.finrank Set.finrank
+
+variable {R}
+
+theorem finrank_span_le_card (s : Set M) [Fintype s] : finrank R (span R s) ≤ s.toFinset.card :=
+  finrank_le_of_rank_le (by simpa using rank_span_le (R := R) s)
+#align finrank_span_le_card finrank_span_le_card
+
+theorem finrank_span_finset_le_card (s : Finset M) : (s : Set M).finrank R ≤ s.card :=
+  calc
+    (s : Set M).finrank R ≤ (s : Set M).toFinset.card := finrank_span_le_card (M := M) s
+    _ = s.card := by simp
+#align finrank_span_finset_le_card finrank_span_finset_le_card
+
+theorem finrank_range_le_card {ι : Type*} [Fintype ι] (b : ι → M) :
+    (Set.range b).finrank R ≤ Fintype.card ι := by
+  classical
+  refine (finrank_span_le_card _).trans ?_
+  rw [Set.toFinset_range]
+  exact Finset.card_image_le
+#align finrank_range_le_card finrank_range_le_card
+
+theorem finrank_span_eq_card [Nontrivial R] {ι : Type*} [Fintype ι] {b : ι → M}
+    (hb : LinearIndependent R b) :
+    finrank R (span R (Set.range b)) = Fintype.card ι :=
+  finrank_eq_of_rank_eq
+    (by
+      have : Module.rank R (span R (Set.range b)) = #(Set.range b) := rank_span hb
+      rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
+        lift_eq_nat_iff] at this)
+#align finrank_span_eq_card finrank_span_eq_card
+
+theorem finrank_span_set_eq_card {s : Set M} [Fintype s] (hs : LinearIndependent R ((↑) : s → M)) :
+    finrank R (span R s) = s.toFinset.card :=
+  finrank_eq_of_rank_eq
+    (by
+      have : Module.rank R (span R s) = #s := rank_span_set hs
+      rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this)
+#align finrank_span_set_eq_card finrank_span_set_eq_card
+
+theorem finrank_span_finset_eq_card {s : Finset M} (hs : LinearIndependent R ((↑) : s → M)) :
+    finrank R (span R (s : Set M)) = s.card := by
+  convert finrank_span_set_eq_card (s := (s : Set M)) hs
+  ext
+  simp
+#align finrank_span_finset_eq_card finrank_span_finset_eq_card
+
+theorem span_lt_of_subset_of_card_lt_finrank {s : Set M} [Fintype s] {t : Submodule R M}
+    (subset : s ⊆ t) (card_lt : s.toFinset.card < finrank R t) : span R s < t :=
+  lt_of_le_of_finrank_lt_finrank (span_le.mpr subset)
+    (lt_of_le_of_lt (finrank_span_le_card _) card_lt)
+#align span_lt_of_subset_of_card_lt_finrank span_lt_of_subset_of_card_lt_finrank
+
+theorem span_lt_top_of_card_lt_finrank {s : Set M} [Fintype s]
+    (card_lt : s.toFinset.card < finrank R M) : span R s < ⊤ :=
+  lt_top_of_finrank_lt_finrank (lt_of_le_of_lt (finrank_span_le_card _) card_lt)
+#align span_lt_top_of_card_lt_finrank span_lt_top_of_card_lt_finrank
+
+end Span
+
 section SubalgebraRank
 
 open Module