From 3474ced5a35e6e9fabf2e6e48ff757d4537849fa 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 18:37:33 +0100
Subject: [PATCH] Make some arguments implicit. Rename sub_Ker_equiv ->
Ker_sub_KerS_equiv, KerS_sub_equiv -> KerS_Ker_sub_equiv,
sub_Rg_equiv -> Rg_sub_RgS_equiv, RgS_sub_equiv, RgS_Rg_sub_equiv. Add
and prove Ker_sub_zero_equiv, mk_sub_g_zero{,_equiv},
mk_sub_g_inj, Ker_sub_g_KerS_zero_equiv,
KerS_g_zero_equiv_alt, Ker_sub_g_zero_equiv,
gmS_injS_sub_equiv_alt, gmS_bijS_sub_equiv{,_alt},
Ker_fct_sub_g_KerS_zero_equiv, Ker_fct_sub_g_zero_equiv,
gmS_bijS_fct_sub_equiv, mk_sub_r_inj, mk_sub_ms_inj,
Ker_sub_ms_KerS_zero_equiv, KerS_ms_zero_equiv_alt,
Ker_sub_ms_zero_equiv, lmS_injS_sub_equiv_alt,
lmS_bijS_sub_equiv{,_alt}, Ker_fct_sub_ms_KerS_zero_equiv,
Ker_fct_sub_ms_zero_equiv, lmS_bijS_fct_sub_equiv.
---
FEM/Algebra/Sub_struct.v | 188 +++++++++++++++++++++++++++++++++++----
1 file changed, 171 insertions(+), 17 deletions(-)
diff --git a/FEM/Algebra/Sub_struct.v b/FEM/Algebra/Sub_struct.v
index b1956bbd..e6dfe6cf 100644
--- a/FEM/Algebra/Sub_struct.v
+++ b/FEM/Algebra/Sub_struct.v
@@ -55,7 +55,7 @@ Definition in_sub (x : sub_struct HPT) : PT x := in_sub_ HPT x.
Lemma val_eq : forall {x y : sub_struct HPT}, x = y -> val x = val y.
Proof. apply f_equal. Qed.
-Lemma val_inj : forall {x y : sub_struct HPT}, val x = val y -> x = y.
+Lemma val_inj : injective val.
Proof.
intros [x Hx] [y Hy]; simpl; intros; subst; f_equal; apply proof_irrel.
Qed.
@@ -790,8 +790,8 @@ Context {G1 G2 : AbelianMonoid}.
Context {PG1 : G1 -> Prop}.
Context {PG2 : G2 -> Prop}.
-Hypothesis HPG1 : compatible_m PG1.
-Hypothesis HPG2 : compatible_m PG2.
+Context {HPG1 : compatible_m PG1}.
+Context {HPG2 : compatible_m PG2}.
Context {f : G1 -> G2}.
Context {fS : sub_struct HPG1 -> sub_struct HPG2}.
@@ -845,7 +845,7 @@ intros [Hf1 Hf2]; split;
[apply (sub_m_f_plus_compat Hf1) | apply (sub_m_f_zero_compat Hf2)].
Qed.
-Lemma sub_Ker_equiv :
+Lemma Ker_sub_KerS_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.
@@ -853,11 +853,26 @@ split; [apply in_sub | apply val_zero_equiv; easy].
apply val_inj; easy.
Qed.
-Lemma KerS_sub_equiv :
+Lemma KerS_Ker_sub_equiv :
forall {x1} (Hx1 : PG1 x1), KerS PG1 f x1 <-> Ker fS (mk_sub Hx1).
-Proof. intros; rewrite sub_Ker_equiv; easy. Qed.
+Proof. intros; rewrite Ker_sub_KerS_equiv; easy. Qed.
+
+Lemma Ker_sub_zero_equiv :
+ morphism_m f ->
+ Ker fS = zero_sub_struct <-> KerS PG1 f = zero_sub_struct.
+Proof.
+intros Hf; split; intros H; apply subset_ext_equiv; split.
+(* *)
+intros x1; destruct (classic_dec (PG1 x1)) as [Hx1 | Hx1].
+move=> /(KerS_Ker_sub_equiv Hx1); rewrite H; move=> /mk_sub_zero_equiv; easy.
+intros [Hx1a _]; easy.
+(* *)
+move=> x1 ->; apply compatible_m_zero, KerS_compatible_m; easy.
+move=> x1 /Ker_sub_KerS_equiv Hx1; rewrite H in Hx1; apply val_inj; easy.
+move=> x1 ->; apply (compatible_m_zero (Ker_compatible_m (sub_m_morphism Hf))).
+Qed.
-Lemma sub_Rg_equiv :
+Lemma Rg_sub_RgS_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 |].
@@ -865,9 +880,9 @@ 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 :
+Lemma RgS_Rg_sub_equiv :
forall {x2} (Hx2 : PG2 x2), RgS PG1 f x2 <-> Rg fS (mk_sub Hx2).
-Proof. intros; rewrite sub_Rg_equiv; easy. Qed.
+Proof. intros; rewrite Rg_sub_RgS_equiv; easy. Qed.
End Sub_Monoid_Morphism_Facts2a.
@@ -1405,6 +1420,13 @@ Proof. easy. Qed.
Lemma val_minus : forall (x y : sub_g HPG), val (x - y) = val x - val y.
Proof. easy. Qed.
+Lemma mk_sub_g_zero : mk_sub_g (compatible_g_zero HPG) = (0 : sub_g HPG).
+Proof. apply val_inj; easy. Qed.
+
+Lemma mk_sub_g_zero_equiv :
+ forall {x} (Hx : PG x), mk_sub_g Hx = 0 :> sub_g HPG <-> x = 0.
+Proof. apply mk_sub_zero_equiv. Qed.
+
Lemma mk_sub_opp :
forall (x : G) (Hx : PG x), - mk_sub Hx = mk_sub (compatible_g_opp HPG _ Hx).
Proof. easy. Qed.
@@ -1423,6 +1445,11 @@ Lemma sub_minus_eq :
x - y = mk_sub (compatible_g_minus HPG _ _ (in_sub x) (in_sub y)).
Proof. intros; apply mk_sub_minus. Qed.
+Lemma mk_sub_g_inj :
+ forall {x y} (Hx : PG x) (Hy : PG y),
+ mk_sub_g Hx = mk_sub_g Hy :> sub_g HPG -> x = y.
+Proof. apply mk_sub_inj. Qed.
+
End Sub_Group_Def.
@@ -1432,8 +1459,8 @@ Context {G1 G2 : AbelianGroup}.
Context {PG1 : G1 -> Prop}.
Context {PG2 : G2 -> Prop}.
-Hypothesis HPG1 : compatible_g PG1.
-Hypothesis HPG2 : compatible_g PG2.
+Context {HPG1 : compatible_g PG1}.
+Context {HPG2 : compatible_g PG2}.
Context {f : G1 -> G2}.
Context {fS : sub_g HPG1 -> sub_g HPG2}.
@@ -1478,18 +1505,59 @@ 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 Ker_sub_g_KerS_zero_equiv :
+ morphism_g f ->
+ Ker fS = zero_sub_struct <-> KerS PG1 f = zero_sub_struct.
+Proof. move=> /morphism_g_m; apply Ker_sub_zero_equiv, HfS. Qed.
+
+Lemma KerS_g_zero_equiv_alt :
+ morphism_g f ->
+ KerS PG1 f = zero_sub_struct <->
+ forall (x1 : sub_g HPG1), f (val x1) = 0 -> x1 = 0.
+Proof.
+move=>>; rewrite subset_ext_equiv; split; [intros [Hf1 _] | intros Hf1; split].
+intros [x1 Hx1] Hx1a; apply val_inj, Hf1; easy.
+intros x1 [Hx1 Hx1a]; apply (mk_sub_g_inj HPG1 Hx1 (compatible_g_zero HPG1)).
+rewrite mk_sub_g_zero; apply Hf1; easy.
+move=> x1 ->; apply compatible_g_zero, KerS_compatible_g; easy.
+Qed.
+
+Lemma Ker_sub_g_zero_equiv :
+ morphism_g f ->
+ Ker fS = zero_sub_struct <->
+ forall (x1 : sub_g HPG1), f (val x1) = 0 -> x1 = 0.
+Proof.
+intros; rewrite Ker_sub_g_KerS_zero_equiv//; apply KerS_g_zero_equiv_alt; easy.
+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.
+rewrite (Ker_sub_KerS_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.
+rewrite (KerS_Ker_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.
+Lemma gmS_injS_sub_equiv_alt :
+ morphism_g f ->
+ injS PG1 f <-> forall (x1 : sub_g HPG1), f (val x1) = 0 -> x1 = 0.
+Proof.
+intros H; rewrite (gmS_injS_sub_equiv H); apply (Ker_sub_g_zero_equiv H).
+Qed.
+
+Lemma gmS_bijS_sub_equiv :
+ morphism_g f -> bijS PG1 (RgS PG1 f) f <-> Ker fS = zero_sub_struct.
+Proof. rewrite gmS_bijS_injS_equiv; apply gmS_injS_sub_equiv. Qed.
+
+Lemma gmS_bijS_sub_equiv_alt :
+ morphism_g f ->
+ bijS PG1 (RgS PG1 f) f <-> forall (x1 : sub_g HPG1), f (val x1) = 0 -> x1 = 0.
+Proof. rewrite gmS_bijS_injS_equiv; apply gmS_injS_sub_equiv_alt. Qed.
+
End Sub_Group_Morphism_Facts2a.
@@ -1544,10 +1612,25 @@ 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 Ker_fct_sub_g_KerS_zero_equiv :
+ morphism_g f ->
+ Ker fct_sub_g = zero_sub_struct <-> KerS PG1 f = zero_sub_struct.
+Proof. apply Ker_sub_g_KerS_zero_equiv, fct_sub_correct. Qed.
+
+Lemma Ker_fct_sub_g_zero_equiv :
+ morphism_g f ->
+ Ker fct_sub_g = zero_sub_struct <->
+ forall (x1 : sub_g HPG1), f (val x1) = 0 -> x1 = 0.
+Proof. apply Ker_sub_g_zero_equiv, 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.
+Lemma gmS_bijS_fct_sub_equiv :
+ morphism_g f -> bijS PG1 (RgS PG1 f) f <-> Ker fct_sub_g = zero_sub_struct.
+Proof. apply gmS_bijS_sub_equiv, fct_sub_correct. Qed.
+
End Sub_Group_Morphism_Facts2b.
@@ -1745,6 +1828,11 @@ Lemma sub_mult_eq :
x * y = mk_sub (compatible_r_mult HPK _ _ (in_sub x) (in_sub y)).
Proof. easy. Qed.
+Lemma mk_sub_r_inj :
+ forall {x y} (Hx : PK x) (Hy : PK y),
+ mk_sub_r Hx = mk_sub_r Hy :> sub_r HPK -> x = y.
+Proof. apply mk_sub_g_inj. Qed.
+
End Sub_Ring_Def.
@@ -1828,7 +1916,7 @@ Proof. intros Hf; apply val_inj; rewrite HfS Hf; easy. Qed.
Lemma sub_r_morphism : morphism_r f -> morphism_r fS.
Proof.
-intros [Hf1 [Hf2 Hf3]]; repeat split; [apply (sub_g_morphism _ _ HfS Hf1) |
+intros [Hf1 [Hf2 Hf3]]; repeat split; [apply (sub_g_morphism HfS Hf1) |
apply (sub_r_f_mult_compat Hf2) | apply (sub_r_f_one_compat Hf3)].
Qed.
@@ -2539,6 +2627,11 @@ Lemma sub_comb_lin_eq :
mk_sub_ms (compatible_ms_comb_lin HPE _ L _ (fun i => in_sub (B i))).
Proof. intros; apply mk_sub_comb_lin. Qed.
+Lemma mk_sub_ms_inj :
+ forall {x y} (Hx : PE x) (Hy : PE y),
+ mk_sub_ms Hx = mk_sub_ms Hy :> sub_ms HPE -> x = y.
+Proof. apply mk_sub_g_inj. Qed.
+
End Sub_ModuleSpace_Def.
@@ -2602,15 +2695,60 @@ 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) |
+intros [Hf1 Hf2]; split; [apply (sub_g_morphism HfS Hf1) |
move=>>; apply sub_ms_f_scal_compat; move=>>; easy].
Qed.
+Lemma Ker_sub_ms_KerS_zero_equiv :
+ is_linear_mapping f ->
+ Ker fS = zero_sub_struct <-> KerS PE1 f = zero_sub_struct.
+Proof.
+intros Hf; apply (Ker_sub_g_KerS_zero_equiv HfS),
+ is_linear_mapping_morphism_g, Hf.
+Qed.
+
+Lemma KerS_ms_zero_equiv_alt :
+ is_linear_mapping f ->
+ KerS PE1 f = zero_sub_struct <->
+ forall (x1 : sub_ms HPE1), f (val x1) = 0 -> x1 = 0.
+Proof.
+intros H; apply: KerS_g_zero_equiv_alt; apply is_linear_mapping_morphism_g, H.
+Qed.
+
+Lemma Ker_sub_ms_zero_equiv :
+ is_linear_mapping f ->
+ Ker fS = zero_sub_struct <->
+ forall (x1 : sub_ms HPE1), f (val x1) = 0 -> x1 = 0.
+Proof.
+intros Hf; apply (Ker_sub_g_zero_equiv HfS), is_linear_mapping_morphism_g, Hf.
+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].
+intros Hf; apply (gmS_injS_sub_equiv HfS), is_linear_mapping_morphism_g, Hf.
+Qed.
+
+Lemma lmS_injS_sub_equiv_alt :
+ is_linear_mapping f ->
+ injS PE1 f <-> forall (x1 : sub_ms HPE1), f (val x1) = 0 -> x1 = 0.
+Proof.
+intros Hf; apply: (gmS_injS_sub_equiv_alt HfS);
+ apply is_linear_mapping_morphism_g, Hf.
+Qed.
+
+Lemma lmS_bijS_sub_equiv :
+ is_linear_mapping f -> bijS PE1 (RgS PE1 f) f <-> Ker fS = zero_sub_struct.
+Proof.
+intros Hf; apply (gmS_bijS_sub_equiv HfS), is_linear_mapping_morphism_g, Hf.
+Qed.
+
+Lemma lmS_bijS_sub_equiv_alt :
+ is_linear_mapping f ->
+ bijS PE1 (RgS PE1 f) f <-> forall (x1 : sub_ms HPE1), f (val x1) = 0 -> x1 = 0.
+Proof.
+intros Hf; apply: (gmS_bijS_sub_equiv_alt HfS);
+ apply is_linear_mapping_morphism_g, Hf.
Qed.
End Sub_Linear_Mapping_Facts2a.
@@ -2670,10 +2808,26 @@ 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 Ker_fct_sub_ms_KerS_zero_equiv :
+ is_linear_mapping f ->
+ Ker fct_sub_ms = zero_sub_struct <-> KerS PE1 f = zero_sub_struct.
+Proof. apply Ker_sub_ms_KerS_zero_equiv, fct_sub_correct. Qed.
+
+Lemma Ker_fct_sub_ms_zero_equiv :
+ is_linear_mapping f ->
+ Ker fct_sub_ms = zero_sub_struct <->
+ forall (x1 : sub_ms HPE1), f (val x1) = 0 -> x1 = 0.
+Proof. apply Ker_sub_ms_zero_equiv, 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.
+Lemma lmS_bijS_fct_sub_equiv :
+ is_linear_mapping f ->
+ bijS PE1 (RgS PE1 f) f <-> Ker fct_sub_ms = zero_sub_struct.
+Proof. apply lmS_bijS_sub_equiv, fct_sub_correct. Qed.
+
End Sub_Linear_Mapping_Facts2b.
--
GitLab