feat(ring_theory): every left-noetherian ring has invariant basis number (#7678)

This is a lovely case where we get more for less.

By directly proving that every left-noetherian ring has invariant basis number, we don't need to import `linear_algebra.finite_dimensional` in order to do the `field` case. This means that in a future PR we can instead import `ring_theory.invariant_basis_number` in `linear_algebra.finite_dimensional`, and set up the theory of bases in greater generality.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Author: kim-em

src/algebra/module/linear_map.lean

@@ -133,6 +133,9 @@ variables (f g)
 @[simp] lemma map_zero : f 0 = 0 :=
 f.to_distrib_mul_action_hom.map_zero
 
+@[simp] lemma map_eq_zero_iff (h : function.injective f) {x : M} : f x = 0 ↔ x = 0 :=
+⟨λ w, by { apply h, simp [w], }, λ w, by { subst w, simp, }⟩
+
 variables (M M₂)
 /--
 A typeclass for `has_scalar` structures which can be moved through a `linear_map`.

src/linear_algebra/basic.lean

@@ -2635,6 +2635,30 @@ theorem fun_left_comp (f₁ : n → p) (f₂ : m → n) :
   fun_left R M (f₁ ∘ f₂) = (fun_left R M f₂).comp (fun_left R M f₁) :=
 rfl
 
+theorem fun_left_surjective_of_injective (f : m → n) (hf : injective f) :
+  surjective (fun_left R M f) :=
+begin
+  classical,
+  intro g,
+  refine ⟨λ x, if h : ∃ y, f y = x then g h.some else 0, _⟩,
+  { ext,
+    dsimp only [fun_left_apply],
+    split_ifs with w,
+    { congr,
+      exact hf w.some_spec, },
+    { simpa only [not_true, exists_apply_eq_apply] using w } },
+end
+
+theorem fun_left_injective_of_surjective (f : m → n) (hf : surjective f) :
+  injective (fun_left R M f) :=
+begin
+  obtain ⟨g, hg⟩ := hf.has_right_inverse,
+  suffices : left_inverse (fun_left R M g) (fun_left R M f),
+  { exact this.injective },
+  intro x,
+  simp only [← linear_map.comp_apply, ← fun_left_comp, hg.id, fun_left_id]
+end
+
 /-- Given an `R`-module `M` and an equivalence `m ≃ n` between arbitrary types,
 construct a linear equivalence `(n → M) ≃ₗ[R] (m → M)` -/
 def fun_congr_left (e : m ≃ n) : (n → M) ≃ₗ[R] (m → M) :=

src/linear_algebra/invariant_basis_number.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import linear_algebra.finite_dimensional
+import ring_theory.principal_ideal_domain
 import ring_theory.ideal.basic
 
 /-!
@@ -14,19 +14,34 @@ notion of the rank of a finitely generated free (left) `R`-module. Since a finit
 module with a basis consisting of `n` elements is linearly equivalent to `fin n → R`, it is
 sufficient that `(fin n → R) ≃ₗ[R] (fin m → R)` implies `n = m`.
 
+It is also useful to consider two stronger conditions, namely the rank condition,
+that a surjective linear map `(fin n → R) →ₗ[R] (fin m → R)` implies `m ≤ n` and
+the strong rank condition, that an injective linear map `(fin n → R) →ₗ[R] (fin m → R)`
+implies `n ≤ m`.
+
+The strong rank condition implies the rank condition, and the rank condition implies
+the invariant basis number property.
+
 ## Main definitions
 
+`strong_rank_condition R` is a type class stating that `R` satisfies the strong rank condition.
+`rank_condition R` is a type class stating that `R` satisfies the rank condition.
 `invariant_basis_number R` is a type class stating that `R` has the invariant basis number property.
 
 ## Main results
 
-We show that every nontrivial commutative ring has the invariant basis number property.
+We show that every nontrivial left-noetherian ring satifies the rank condition,
+(and so in particular every division ring or field),
+and then use this to show every nontrivial commutative ring has the invariant basis number property.
 
 ## Future work
 
+We can improve these results: in fact every nontrivial left-noetherian ring,
+and every commutative rings, satisfies the strong rank condition.
+
 So far, there is no API at all for the `invariant_basis_number` class. There are several natural
 ways to formulate that a module `M` is finitely generated and free, for example
-`M ≃ₗ[R] (fin n → R)`, `M ≃ₗ[R] (ι → R)`, where `ι` is a fintype, or prividing a basis indexed by
+`M ≃ₗ[R] (fin n → R)`, `M ≃ₗ[R] (ι → R)`, where `ι` is a fintype, or providing a basis indexed by
 a finite type. There should be lemmas applying the invariant basis number property to each
 situation.
 
@@ -37,6 +52,7 @@ variants) should be formalized.
 ## References
 
 * https://en.wikipedia.org/wiki/Invariant_basis_number
+* https://mathoverflow.net/a/2574/
 
 ## Tags
 
@@ -47,18 +63,45 @@ free module, rank, invariant basis number, IBN
 noncomputable theory
 
 open_locale classical big_operators
+open function
 
 universes u v w
 
 section
 variables (R : Type u) [ring R]
 
+/-- We say that `R` satisfies the strong rank condition if `(fin n → R) →ₗ[R] (fin m → R)` injective
+    implies `n ≤ m`. -/
+class strong_rank_condition : Prop :=
+(le_of_fin_injective : ∀ {n m : ℕ} (f : (fin n → R) →ₗ[R] (fin m → R)), injective f → n ≤ m)
+
+lemma le_of_fin_injective [strong_rank_condition R] {n m : ℕ} (f : (fin n → R) →ₗ[R] (fin m → R)) :
+  injective f → n ≤ m :=
+strong_rank_condition.le_of_fin_injective f
+
+/-- We say that `R` satisfies the rank condition if `(fin n → R) →ₗ[R] (fin m → R)` surjective
+    implies `m ≤ n`. -/
+class rank_condition : Prop :=
+(le_of_fin_surjective : ∀ {n m : ℕ} (f : (fin n → R) →ₗ[R] (fin m → R)), surjective f → m ≤ n)
+
+lemma le_of_fin_surjective [rank_condition R] {n m : ℕ} (f : (fin n → R) →ₗ[R] (fin m → R)) :
+  surjective f → m ≤ n :=
+rank_condition.le_of_fin_surjective f
+
+-- TODO the strong rank condition implies the rank condition
+
 /-- We say that `R` has the invariant basis number property if `(fin n → R) ≃ₗ[R] (fin m → R)`
     implies `n = m`. This gives rise to a well-defined notion of rank of a finitely generated free
     module. -/
 class invariant_basis_number : Prop :=
 (eq_of_fin_equiv : ∀ {n m : ℕ}, ((fin n → R) ≃ₗ[R] (fin m → R)) → n = m)
 
+@[priority 100]
+instance invariant_basis_number_of_rank_condition [rank_condition R] : invariant_basis_number R :=
+{ eq_of_fin_equiv := λ n m e, le_antisymm
+    (le_of_fin_surjective R e.symm.to_linear_map e.symm.surjective)
+    (le_of_fin_surjective R e.to_linear_map e.surjective) }
+
 end
 
 section
@@ -79,17 +122,44 @@ end
 end
 
 section
-open finite_dimensional
-
-/-- A field has invariant basis number. This will be superseded below by the fact that any nonzero
-    commutative ring has invariant basis number. -/
-lemma invariant_basis_number_field {K : Type u} [field K] : invariant_basis_number K :=
-⟨λ n m e,
-  calc n = fintype.card (fin n) : eq.symm $ fintype.card_fin n
-     ... = finrank K (fin n → K) : eq.symm $ finrank_eq_card_basis (pi.basis_fun K (fin n))
-     ... = finrank K (fin m → K) : linear_equiv.finrank_eq e
-     ... = fintype.card (fin m) : finrank_eq_card_basis (pi.basis_fun K (fin m))
-     ... = m                    : fintype.card_fin m⟩
+variables (R : Type u) [ring R] [nontrivial R] [is_noetherian_ring R]
+
+-- TODO: in fact, any nontrivial noetherian ring satisfies the strong rank condition.
+
+/-- Any nontrivial noetherian ring satisfies the rank condition. -/
+-- Note this includes fields,
+-- and we use this below to show any commutative ring has invariant basis number.
+@[priority 100]
+instance noetherian_ring_rank_condition : rank_condition R :=
+⟨begin
+  intros n m f fs,
+  by_contradiction h,
+  rw [not_le, ←nat.add_one_le_iff, le_iff_exists_add] at h,
+  obtain ⟨m, rfl⟩ := h,
+  -- Let `g` be the projection map discarding the last `n` coordinates.
+  let g : (fin ((n + 1) + m) → R) →ₗ[R] (fin n → R) :=
+    linear_map.fun_left R R ((fin.cast_add 1).trans (fin.cast_add m)),
+  have gs : function.surjective g :=
+    linear_map.fun_left_surjective_of_injective _ _ _
+      ((fin.cast_add m).injective.comp (fin.cast_add 1).injective),
+  -- Since `g` composed with the `f` is a surjective endomorphism of
+  -- a noetherian module, it is injective, and so `f` itself is injective.
+  have gi : function.injective g :=
+    (is_noetherian.injective_of_surjective_endomorphism (f.comp g)
+      (function.surjective.comp fs gs)).of_comp,
+  -- But this gives an easy contradiction.
+  let i : fin (n + 1 + m) := fin.cast_add m (fin.nat_add n 0),
+  let x : fin (n + 1 + m) → R := finsupp.single i 1,
+  have z : g x = 0 := begin
+    ext j,
+    simp only [g, x, i, linear_map.fun_left_apply, pi.zero_apply],
+    rw finsupp.single_eq_of_ne,
+    refine fin.ne_of_vne _,
+    simp only [add_zero, fin.coe_zero, fin.val_eq_coe, fin.coe_nat_add, ne.def, fin.coe_cast_add],
+    exact j.2.ne.symm,
+  end,
+  simpa [x] using congr_fun ((g.map_eq_zero_iff gi).mp z) i,
+end⟩
 
 end
 
@@ -134,8 +204,9 @@ end
 end
 
 section
-local attribute [instance] invariant_basis_number_field
-local attribute [instance, priority 1] ideal.quotient.field
+local attribute [instance] ideal.quotient.field
+
+-- TODO: in fact, any nontrivial commutative ring satisfies the strong rank condition.
 
 /-- Nontrivial commutative rings have the invariant basis number property. -/
 @[priority 100]