From 97ccfcfb1e48d7a203ee61543e882baa3f71895f Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 24 Sep 2020 16:56:04 +0200
Subject: Injectivity for additive functions and mulmxr.

---
 CHANGELOG_UNRELEASED.md      |  7 +++++++
 mathcomp/algebra/mxalgebra.v | 12 ++++++++++++
 mathcomp/algebra/ssralg.v    |  9 +++++----
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 0a59193..b08875c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -137,6 +137,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   dual lattices.
 
 - in `matrix.v` new lemma `det_mx11`.
+- in `ssralg.v`, new lemma `raddf_inj`, characterizing injectivity for
+  additive maps.
+- in `mxalgebra.v`, new lemma `row_free_injr` which duplicates
+  `row_free_inj` but exposing `mulmxr` for compositionality purposes
+  (e.g. with `raddf_eq0`), and lemma `inj_row_free` characterizing
+  `row_free` matrices `A`  through `v *m A = 0 -> v = 0` for all `v`.
+
 
 ### Changed
 
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 686da21..f1cc062 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -686,6 +686,11 @@ case/row_freeP=> A' AK; apply: can_inj (mulmx^~ A') _ => B.
 by rewrite -mulmxA AK mulmx1.
 Qed.
 
+(* A variant of row_free_inj that exposes mulmxr, an alias for mulmx^~ *)
+(* but which is canonically additive *)
+Definition row_free_injr m n p A : row_free A -> injective (@mulmxr A) :=
+  @row_free_inj m n p A.
+
 Lemma row_free_unit n (A : 'M_n) : row_free A = (A \in unitmx).
 Proof.
 apply/row_fullP/idP=> [[A'] | uA]; first by case/mulmx1_unit.
@@ -1222,6 +1227,13 @@ Lemma mulmx_free_eq0 m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
   row_free B -> (A *m B == 0) = (A == 0).
 Proof. by rewrite -sub_kermx -kermx_eq0 => /eqP->; rewrite submx0. Qed.
 
+Lemma inj_row_free m n (A : 'M_(m, n)) :
+  (forall v : 'rV_m, v *m A = 0 -> v = 0) -> row_free A.
+Proof.
+move=> Ainj; rewrite -kermx_eq0; apply/eqP/row_matrixP => i.
+by rewrite row0; apply/Ainj; rewrite -row_mul mulmx_ker row0.
+Qed.
+
 Lemma mulmx0_rank_max m n p (A : 'M_(m, n)) (B : 'M_(n, p)) :
   A *m B = 0 -> \rank A + \rank B <= n.
 Proof.
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 9a3c7d7..6128fa0 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -1878,6 +1878,9 @@ Proof. by rewrite -[0]subr0 raddfB subrr. Qed.
 Lemma raddf_eq0 x : injective f -> (f x == 0) = (x == 0).
 Proof. by move=> /inj_eq <-; rewrite raddf0. Qed.
 
+Lemma raddf_inj : (forall x, f x = 0 -> x = 0) -> injective f.
+Proof. by move=> fI x y eqxy; apply/subr0_eq/fI; rewrite raddfB eqxy subrr. Qed.
+
 Lemma raddfN : {morph f : x / - x}.
 Proof. by move=> x /=; rewrite -sub0r raddfB raddf0 sub0r. Qed.
 
@@ -4933,10 +4936,7 @@ by rewrite -rmorphM mulVf // mulr0 rmorph1 ?oner_eq0.
 Qed.
 
 Lemma fmorph_inj : injective f.
-Proof.
-move=> x y eqfxy; apply/eqP; rewrite -subr_eq0 -fmorph_eq0 rmorphB //.
-by rewrite eqfxy subrr.
-Qed.
+Proof. by apply/raddf_inj => x /eqP; rewrite fmorph_eq0 => /eqP. Qed.
 
 Lemma fmorph_eq1 x : (f x == 1) = (x == 1).
 Proof. by rewrite -(inj_eq fmorph_inj) rmorph1. Qed.
@@ -5899,6 +5899,7 @@ Definition size_sol := size_sol.
 Definition solve_monicpoly := solve_monicpoly.
 Definition raddf0 := raddf0.
 Definition raddf_eq0 := raddf_eq0.
+Definition raddf_inj := raddf_inj.
 Definition raddfN := raddfN.
 Definition raddfD := raddfD.
 Definition raddfB := raddfB.
-- 
cgit v1.2.3