feat(linear_algebra/free_module/strong_rank_condition): add `comm_rin…

…g_strong_rank_condition` (#9486)

We add `comm_ring_strong_rank_condition`: any commutative ring satisfies the strong rank condition.

Because of a circular import, this can't be in `linear_algebra.invariant_basis_number`.

src/linear_algebra/charpoly/basic.lean

@@ -71,7 +71,7 @@ minpoly.dvd _ _ (aeval_self_charpoly f)
 
 variable {f}
 
-lemma charpoly_coeff_zero_of_injective (hf : function.injective f) : (minpoly R f).coeff 0 ≠ 0 :=
+lemma minpoly_coeff_zero_of_injective (hf : function.injective f) : (minpoly R f).coeff 0 ≠ 0 :=
 begin
   intro h,
   obtain ⟨P, hP⟩ := X_dvd_iff.2 h,

src/linear_algebra/free_module/strong_rank_condition.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2021 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca
+-/
+
+import linear_algebra.charpoly.basic
+import linear_algebra.invariant_basis_number
+
+/-!
+
+# Strong rank condition for commutative rings
+
+We prove that any nontrivial commutative ring satisfies `strong_rank_condition`, meaning that
+if there is an injective linear map `(fin n → R) →ₗ[R] fin m → R`, then `n ≤ m`. This implies that
+any commutative ring satisfies `invariant_basis_number`: the rank of a finitely generated free
+module is well defined.
+
+## Main result
+
+* `comm_ring_strong_rank_condition R` : `R` has the `strong_rank_condition`.
+
+## References
+
+We follow the proof given in https://mathoverflow.net/a/47846/7845.
+The argument is the following: it is enough to prove that for all `n`, there is no injective linear
+map `(fin (n + 1) → R) →ₗ[R] fin n → R`. Given such an `f`, we get by extension an injective
+linear map `g : (fin n → R) →ₗ[R] fin n → R`. Injectivity implies that `P`, the minimal polynomial
+of `g`, has non-zero constant term `a₀ ≠ 0`. But evaluating `0 = P(g)` at the vector `(0,...,0,1)`
+gives `a₀`, contradiction.
+
+-/
+
+variables (R : Type*) [comm_ring R] [nontrivial R]
+
+open polynomial function fin linear_map
+
+/-- Any commutative ring satisfies the `strong_rank_condition`. -/
+@[priority 100]
+instance comm_ring_strong_rank_condition : strong_rank_condition R :=
+begin
+  suffices : ∀ n, ∀ f : (fin (n + 1) → R) →ₗ[R] fin n → R, ¬injective f,
+  { rwa strong_rank_condition_iff_succ R },
+  intros n f, by_contradiction hf,
+
+  letI := module.finite.of_basis (pi.basis_fun R (fin (n + 1))),
+
+  let g : (fin (n + 1) → R) →ₗ[R] fin (n + 1) → R :=
+    (extend_by_zero.linear_map R cast_succ).comp f,
+  have hg : injective g := (extend_injective (rel_embedding.injective cast_succ) 0).comp hf,
+
+  have hnex : ¬∃ i : fin n, cast_succ i = last n := λ ⟨i, hi⟩, ne_of_lt (cast_succ_lt_last i) hi,
+
+  let a₀ := (minpoly R g).coeff 0,
+  have : a₀ ≠ 0 := minpoly_coeff_zero_of_injective hg,
+  have : a₀ = 0,
+  { -- evaluate the `(minpoly R g) g` at the vector `(0,...,0,1)`
+    have heval := linear_map.congr_fun (minpoly.aeval R g) (pi.single (fin.last n) 1),
+    obtain ⟨P, hP⟩ := X_dvd_iff.2 (erase_same (minpoly R g) 0),
+    rw [← monomial_add_erase (minpoly R g) 0, hP] at heval,
+    replace heval := congr_fun heval (fin.last n),
+    simpa [hnex] using heval },
+  contradiction,
+end

src/linear_algebra/invariant_basis_number.lean

@@ -34,9 +34,11 @@ We show that every nontrivial left-noetherian ring satisfies the strong rank con
 (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
+More generally, every commutative ring satisfies the strong rank condition. This is proved in
+`linear_algebra/free_module/strong_rank_condition`. We keep
+`invariant_basis_number_of_nontrivial_of_comm_ring` here since it imports fewer files.
 
-We can improve these results: in fact every commutative ring satisfies the strong rank condition.
+## Future work
 
 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