feat(linear_algebra): strong rank condition implies rank condition (#…

…7683)




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

src/data/finsupp/basic.lean

@@ -141,6 +141,9 @@ lemma ext_iff' {f g : α →₀ M} : f = g ↔ f.support = g.support ∧ ∀ x 
     have hg : g a = 0, by rwa [h₁, not_mem_support_iff] at h,
     by rw [hf, hg]⟩
 
+lemma congr_fun {f g : α →₀ M} (h : f = g) (a : α) : f a = g a :=
+congr_fun (congr_arg finsupp.to_fun h) a
+
 @[simp] lemma support_eq_empty {f : α →₀ M} : f.support = ∅ ↔ f = 0 :=
 by exact_mod_cast @function.support_eq_empty_iff _ _ _ f
 
@@ -338,6 +341,14 @@ by simp only [card_eq_one, support_eq_singleton]
 lemma card_support_eq_one' {f : α →₀ M} : card f.support = 1 ↔ ∃ a (b ≠ 0), f = single a b :=
 by simp only [card_eq_one, support_eq_singleton']
 
+@[simp] lemma equiv_fun_on_fintype_single [fintype α] (x : α) (m : M) :
+  (@finsupp.equiv_fun_on_fintype α M _ _) (finsupp.single x m) = pi.single x m :=
+by { ext, simp [finsupp.single_eq_pi_single, finsupp.equiv_fun_on_fintype], }
+
+@[simp] lemma equiv_fun_on_fintype_symm_single [fintype α] (x : α) (m : M) :
+  (@finsupp.equiv_fun_on_fintype α M _ _).symm (pi.single x m) = finsupp.single x m :=
+by { ext, simp [finsupp.single_eq_pi_single, finsupp.equiv_fun_on_fintype], }
+
 end single
 
 /-! ### Declarations about `on_finset` -/

src/linear_algebra/basic.lean

@@ -98,6 +98,24 @@ variable (R)
   map_smul' := λ c f, by { ext, refl },
   .. equiv_fun_on_fintype }
 
+@[simp] lemma linear_equiv_fun_on_fintype_single {α} [decidable_eq α] [fintype α]
+  [add_comm_monoid M] [semiring R] [module R M] (x : α) (m : M) :
+  (@linear_equiv_fun_on_fintype R M α _ _ _ _) (single x m) = pi.single x m :=
+begin
+  ext a,
+  change (equiv_fun_on_fintype (single x m)) a = _,
+  convert _root_.congr_fun (equiv_fun_on_fintype_single x m) a,
+end
+
+@[simp] lemma linear_equiv_fun_on_fintype_symm_single {α} [decidable_eq α] [fintype α]
+  [add_comm_monoid M] [semiring R] [module R M] (x : α) (m : M) :
+  (@linear_equiv_fun_on_fintype R M α _ _ _ _).symm (pi.single x m) = single x m :=
+begin
+  ext a,
+  change (equiv_fun_on_fintype.symm (pi.single x m)) a = _,
+  convert congr_fun (equiv_fun_on_fintype_symm_single x m) a,
+end
+
 end finsupp
 
 section

src/linear_algebra/basis.lean

@@ -635,7 +635,8 @@ basis.of_repr $ e.trans $ linear_equiv.symm $ finsupp.linear_equiv_fun_on_fintyp
 
 @[simp] lemma basis.coe_of_equiv_fun (e : M ≃ₗ[R] (ι → R)) :
   (basis.of_equiv_fun e : ι → M) = λ i, e.symm (function.update 0 i 1) :=
-funext $ λ i, e.injective $ funext $ λ j, by simp [basis.of_equiv_fun, finsupp.single_eq_update]
+funext $ λ i, e.injective $ funext $ λ j,
+  by simp [basis.of_equiv_fun, ←finsupp.single_eq_pi_single, finsupp.single_eq_update]
 
 variables (S : Type*) [semiring S] [module S M']
 variables [smul_comm_class R S M']

src/linear_algebra/finsupp.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 import data.finsupp.basic
 import linear_algebra.basic
+import linear_algebra.pi
 
 /-!
 # Properties of the module `α →₀ M`
@@ -821,3 +822,63 @@ def module.subsingleton_equiv (R M ι: Type*) [semiring R] [subsingleton R] [add
   right_inv := λ f, by simp only [eq_iff_true_of_subsingleton],
   map_add' := λ m n, (add_zero 0).symm,
   map_smul' := λ r m, (smul_zero r).symm }
+
+namespace linear_map
+
+variables {R M} {α : Type*}
+open finsupp function
+
+/-- A surjective linear map to finitely supported functions has a splitting. -/
+-- See also `linear_map.splitting_of_fun_on_fintype_surjective`
+def splitting_of_finsupp_surjective (f : M →ₗ[R] (α →₀ R)) (s : surjective f) : (α →₀ R) →ₗ[R] M :=
+finsupp.lift _ _ _ (λ x : α, (s (finsupp.single x 1)).some)
+
+lemma splitting_of_finsupp_surjective_splits (f : M →ₗ[R] (α →₀ R)) (s : surjective f) :
+  f.comp (splitting_of_finsupp_surjective f s) = linear_map.id :=
+begin
+  ext x y,
+  dsimp [splitting_of_finsupp_surjective],
+  congr,
+  rw [sum_single_index, one_smul],
+  { exact (s (finsupp.single x 1)).some_spec, },
+  { rw zero_smul, },
+end
+
+lemma left_inverse_splitting_of_finsupp_surjective (f : M →ₗ[R] (α →₀ R)) (s : surjective f) :
+  left_inverse f (splitting_of_finsupp_surjective f s) :=
+λ g, linear_map.congr_fun (splitting_of_finsupp_surjective_splits f s) g
+
+lemma splitting_of_finsupp_surjective_injective (f : M →ₗ[R] (α →₀ R)) (s : surjective f) :
+  injective (splitting_of_finsupp_surjective f s) :=
+(left_inverse_splitting_of_finsupp_surjective f s).injective
+
+/-- A surjective linear map to functions on a finite type has a splitting. -/
+-- See also `linear_map.splitting_of_finsupp_surjective`
+def splitting_of_fun_on_fintype_surjective [fintype α] (f : M →ₗ[R] (α → R)) (s : surjective f) :
+  (α → R) →ₗ[R] M :=
+(finsupp.lift _ _ _ (λ x : α, (s (finsupp.single x 1)).some)).comp
+  (@linear_equiv_fun_on_fintype R R α _ _ _ _).symm.to_linear_map
+
+lemma splitting_of_fun_on_fintype_surjective_splits
+  [fintype α] (f : M →ₗ[R] (α → R)) (s : surjective f) :
+  f.comp (splitting_of_fun_on_fintype_surjective f s) = linear_map.id :=
+begin
+  ext x y,
+  dsimp [splitting_of_fun_on_fintype_surjective],
+  rw [linear_equiv_fun_on_fintype_symm_single, finsupp.sum_single_index, one_smul,
+    linear_map.id_coe, id_def,
+    (s (finsupp.single x 1)).some_spec, finsupp.single_eq_pi_single],
+  rw [zero_smul],
+end
+
+lemma left_inverse_splitting_of_fun_on_fintype_surjective
+  [fintype α] (f : M →ₗ[R] (α → R)) (s : surjective f) :
+  left_inverse f (splitting_of_fun_on_fintype_surjective f s) :=
+λ g, linear_map.congr_fun (splitting_of_fun_on_fintype_surjective_splits f s) g
+
+lemma splitting_of_fun_on_fintype_surjective_injective
+  [fintype α] (f : M →ₗ[R] (α → R)) (s : surjective f) :
+  injective (splitting_of_fun_on_fintype_surjective f s) :=
+(left_inverse_splitting_of_fun_on_fintype_surjective f s).injective
+
+end linear_map

src/linear_algebra/invariant_basis_number.lean

@@ -30,7 +30,7 @@ the invariant basis number property.
 
 ## Main results
 
-We show that every nontrivial left-noetherian ring satifies the rank condition,
+We show that every nontrivial left-noetherian ring satisfies 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.
 
@@ -88,7 +88,15 @@ lemma le_of_fin_surjective [rank_condition R] {n m : ℕ} (f : (fin n → R) →
   surjective f → m ≤ n :=
 rank_condition.le_of_fin_surjective f
 
--- TODO the strong rank condition implies the rank condition
+/--
+By the universal property for free modules, any surjective map `(fin n → R) →ₗ[R] (fin m → R)`
+has an injective splitting `(fin m → R) →ₗ[R] (fin n → R)`
+from which the strong rank condition gives the necessary inequality for the rank condition.
+-/
+@[priority 100]
+instance rank_condition_of_strong_rank_condition [strong_rank_condition R] : rank_condition R :=
+{ le_of_fin_surjective := λ n m f s,
+    le_of_fin_injective R _ (f.splitting_of_fun_on_fintype_surjective_injective s), }
 
 /-- 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