From 1f958eab61d9a9946ffca250a8932a046d9966b8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Tue, 20 Feb 2024 15:26:45 +0100
Subject: [PATCH] Add and prove val_zero_equiv, mk_sub_zero,              
 sub_m_f_sum_compat, gmS_injS_sub_equiv,               sub_{Ker,Rg}_equiv,
 {KerS,RgS}_sub_equiv,               fct_sub_m_f_sum_compat,
 gmS_injS_fct_sub_equiv,               sub_ms_f_comb_lin_compat,
 lmS_injS_sub_equiv,               fct_sub_ms_f_comb_lin_compat,
 lmS_injS_fct_sub_equiv.

---
 FEM/Algebra/Sub_struct.v | 83 ++++++++++++++++++++++++++++++++++++++--
 1 file changed, 80 insertions(+), 3 deletions(-)

diff --git a/FEM/Algebra/Sub_struct.v b/FEM/Algebra/Sub_struct.v
index f051d9b8..b1956bbd 100644
--- a/FEM/Algebra/Sub_struct.v
+++ b/FEM/Algebra/Sub_struct.v
@@ -735,6 +735,11 @@ Canonical Structure sub_AbelianMonoid :=
 Lemma val_zero : val (0 : sub_struct HPG) = (0 : G).
 Proof. easy. Qed.
 
+Lemma val_zero_equiv : forall (x : sub_struct HPG), val x = 0 <-> x = 0.
+Proof.
+intros; split; [rewrite -val_zero; apply val_inj | intros; subst; easy].
+Qed.
+
 Lemma val_plus : forall (x y : sub_struct HPG), val (x + y) = val x + val y.
 Proof. easy. Qed.
 
@@ -746,6 +751,9 @@ intros; rewrite 2!sum_nil; easy.
 intros; rewrite 2!sum_ind_l; simpl; f_equal; apply Hn.
 Qed.
 
+Lemma mk_sub_zero : sub_zero = (0 : sub_struct HPG).
+Proof. easy. Qed.
+
 Lemma mk_sub_zero_equiv : forall {x} (Hx : PG x), mk_sub Hx = 0 <-> x = 0.
 Proof. intros; split; [move=> /val_eq | intros; apply val_inj]; easy. Qed.
 
@@ -825,12 +833,42 @@ Proof. intros Hf x1 y1; apply val_inj; rewrite HfS Hf -!HfS; easy. Qed.
 Lemma sub_m_f_zero_compat : f_zero_compat f -> f_zero_compat fS.
 Proof. intros Hf; apply val_inj; rewrite HfS Hf; easy. Qed.
 
+Lemma sub_m_f_sum_compat : f_sum_compat f -> f_sum_compat fS.
+Proof.
+intros Hf n u1; apply val_inj; rewrite HfS !val_sum Hf; f_equal.
+apply extF; intros i; rewrite !mapF_correct; easy.
+Qed.
+
 Lemma sub_m_morphism : morphism_m f -> morphism_m fS.
 Proof.
 intros [Hf1 Hf2]; split;
     [apply (sub_m_f_plus_compat Hf1) | apply (sub_m_f_zero_compat Hf2)].
 Qed.
 
+Lemma sub_Ker_equiv :
+  forall (x1 : sub_struct HPG1), Ker fS x1 <-> KerS PG1 f (val x1).
+Proof.
+intros; rewrite Ker_equiv KerS_equiv -HfS; split; intros Hx1.
+split; [apply in_sub | apply val_zero_equiv; easy].
+apply val_inj; easy.
+Qed.
+
+Lemma KerS_sub_equiv :
+  forall {x1} (Hx1 : PG1 x1), KerS PG1 f x1 <-> Ker fS (mk_sub Hx1).
+Proof. intros; rewrite sub_Ker_equiv; easy. Qed.
+
+Lemma sub_Rg_equiv :
+  forall (x2 : sub_struct HPG2), Rg fS x2 <-> RgS PG1 f (val x2).
+Proof.
+intros x2; split; [intros [x1 Hx1]; rewrite HfS; apply Im, in_sub |].
+intros Hx2; inversion Hx2 as [x1 Hx1a Hx1b].
+apply Rg_ex; exists (mk_sub Hx1a); apply val_inj; rewrite HfS; easy.
+Qed.
+
+Lemma RgS_sub_equiv :
+  forall {x2} (Hx2 : PG2 x2), RgS PG1 f x2 <-> Rg fS (mk_sub Hx2).
+Proof. intros; rewrite sub_Rg_equiv; easy. Qed.
+
 End Sub_Monoid_Morphism_Facts2a.
 
 
@@ -882,6 +920,9 @@ Proof. apply sub_m_f_plus_compat, fct_sub_correct. Qed.
 Lemma fct_sub_m_f_zero_compat : f_zero_compat f -> f_zero_compat fct_sub_m.
 Proof. apply sub_m_f_zero_compat, fct_sub_correct. Qed.
 
+Lemma fct_sub_m_f_sum_compat : f_sum_compat f -> f_sum_compat fct_sub_m.
+Proof. apply sub_m_f_sum_compat, fct_sub_correct. Qed.
+
 Lemma fct_sub_m_morphism : morphism_m f -> morphism_m fct_sub_m.
 Proof. apply sub_m_morphism, fct_sub_correct. Qed.
 
@@ -1136,9 +1177,8 @@ Qed.
 
 Lemma gmS_injS : incl (KerS PG1 f) zero_sub_struct -> injS PG1 f.
 Proof.
-intros Hf1 x1 y1 Hx1 Hy1 H1.
-apply minus_zero_reg, Hf1, KerS_correct; [apply HPG1; easy |].
-rewrite morphism_g_minus// minus_zero_compat; easy.
+intros Hf1 x1 y1 Hx1 Hy1; rewrite -2!minus_zero_equiv -(morphism_g_minus _ Hf).
+intros H1; apply Hf1, KerS_equiv; split; [apply HPG1 |]; easy.
 Qed.
 
 Lemma gmS_injS_rev : injS PG1 f -> KerS PG1 f = zero_sub_struct.
@@ -1438,6 +1478,18 @@ Proof. intros Hf x1 y1; apply val_inj; rewrite HfS Hf -!HfS; easy. Qed.
 Lemma sub_g_morphism : morphism_g f -> morphism_g fS.
 Proof. apply sub_m_f_plus_compat, HfS. Qed.
 
+Lemma gmS_injS_sub_equiv :
+  morphism_g f -> injS PG1 f <-> Ker fS = zero_sub_struct.
+Proof.
+intros Hf; rewrite gmS_injS_equiv//; split;
+    intros Hf1; apply subset_ext; intros x1.
+rewrite (sub_Ker_equiv _ _ HfS) Hf1; apply val_zero_equiv.
+destruct (classic_dec (PG1 x1)) as [Hx1 | Hx1a].
+rewrite (KerS_sub_equiv _ _ HfS Hx1) Hf1; apply mk_sub_zero_equiv.
+split; intros Hx1b; contradict Hx1a;
+    [apply Hx1b | rewrite Hx1b; apply compatible_g_zero, HPG1].
+Qed.
+
 End Sub_Group_Morphism_Facts2a.
 
 
@@ -1492,6 +1544,10 @@ Proof. apply sub_g_f_minus_compat, fct_sub_correct. Qed.
 Lemma fct_sub_g_morphism : morphism_g f -> morphism_g fct_sub_g.
 Proof. apply sub_g_morphism, fct_sub_correct. Qed.
 
+Lemma gmS_injS_fct_sub_equiv :
+  morphism_g f -> injS PG1 f <-> Ker fct_sub_g = zero_sub_struct.
+Proof. apply gmS_injS_sub_equiv, fct_sub_correct. Qed.
+
 End Sub_Group_Morphism_Facts2b.
 
 
@@ -2538,12 +2594,25 @@ Proof. apply sub_g_bij_equiv, HfS. Qed.
 Lemma sub_ms_f_scal_compat : f_scal_compat f -> f_scal_compat fS.
 Proof. intros Hf a x1; apply val_inj; rewrite HfS Hf -!HfS; easy. Qed.
 
+Lemma sub_ms_f_comb_lin_compat : f_comb_lin_compat f -> f_comb_lin_compat fS.
+Proof.
+intros Hf n L B; apply val_inj; rewrite HfS !val_comb_lin Hf; f_equal.
+apply extF; intros i; rewrite !mapF_correct; easy.
+Qed.
+
 Lemma sub_ms_linear_mapping : is_linear_mapping f -> is_linear_mapping fS.
 Proof.
 intros [Hf1 Hf2]; split; [apply (sub_g_morphism _ _ HfS Hf1) |
     move=>>; apply sub_ms_f_scal_compat; move=>>; easy].
 Qed.
 
+Lemma lmS_injS_sub_equiv :
+  is_linear_mapping f -> injS PE1 f <-> Ker fS = zero_sub_struct.
+Proof.
+intros; apply gmS_injS_sub_equiv;
+    [apply HfS | apply is_linear_mapping_morphism_g, H].
+Qed.
+
 End Sub_Linear_Mapping_Facts2a.
 
 
@@ -2593,10 +2662,18 @@ Proof. apply fct_sub_g_bij_equiv. Qed.
 Lemma fct_sub_ms_f_scal_compat : f_scal_compat f -> f_scal_compat fct_sub_ms.
 Proof. apply sub_ms_f_scal_compat, fct_sub_correct. Qed.
 
+Lemma fct_sub_ms_f_comb_lin_compat :
+  f_comb_lin_compat f -> f_comb_lin_compat fct_sub_ms.
+Proof. apply sub_ms_f_comb_lin_compat, fct_sub_correct. Qed.
+
 Lemma fct_sub_ms_linear_mapping :
   is_linear_mapping f -> is_linear_mapping fct_sub_ms.
 Proof. apply sub_ms_linear_mapping, fct_sub_correct. Qed.
 
+Lemma lmS_injS_fct_sub_equiv :
+  is_linear_mapping f -> injS PE1 f <-> Ker fct_sub_ms = zero_sub_struct.
+Proof. apply lmS_injS_sub_equiv, fct_sub_correct. Qed.
+
 End Sub_Linear_Mapping_Facts2b.
 
 
-- 
GitLab