Library Algebra.Group.Group_sub
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Support for subgroups.
Let G : AbelianGroup.
Let PG : G → Prop.
Lemmas about predicate compatible_g have "cg" in their names, usually as
prefix "cg_", sometimes as suffix "_cg".
Let gen : G → Prop.
Let G1 G2 : AbelianGroup.
Let PG1 : G1 → Prop.
Let f : G1 → G2.
Let G : AbelianGroup.
Let PG : G → Prop.
Let HPG : compatible_g PG.
Let G1 G2 : AbelianGroup.
Let PG1 : G1 → Prop and PG2 : G2 → Prop.
Let HPG1 : compatible_g PG1 and HPG2 : compatible_g PG2.
Let f : G1 → G2.
Let Hf : funS PG1 PG2 f.
[GostiauxT1]
Bernard Gostiaux,
Cours de mathématiques spéciales - 1. Algèbre,
Mathématiques, Presses Universitaires de France, Paris, 1993,
https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre.
This module mat be used through the import of Algebra.Group.Group,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- opp_closed PG states that PG is closed under the opposite law opp;
- minus_closed PG states that PG is closed under the minus law minus.
- span_g gen is the specialization span compatible_g gen (see Algebra.Sub_struct), ie it is the intersection of all subsets (= the smallest) compatible with the AbelianGroup structure that also contain gen.
Additional support for group morphism
Additional support for subgroup
- sub_AbelianGroup HPG is the type sub PG endowed with the AbelianGroup structure (see Subsets..Sub_type).
- fct_sub_g HPG1 HPG2 Hf is the function fct_sub Hf with type sub_AbelianGroup HPG1 → sub_AbelianGroup HPG2 (see Subsets.Sub_type).
Bibliography
Used logic axioms
- classic, the weak form of excluded middle.
Usage
From Requisite Require Import ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Sub_struct.
From Algebra Require Import Monoid Group_compl Group_morphism.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Section Compatible_Group_Def.
Context {G : AbelianGroup}.
Definition opp_closed (PG : G → Prop) : Prop := ∀ x, PG x → PG (- x).
Definition minus_closed (PG : G → Prop) : Prop :=
∀ x y, PG x → PG y → PG (x - y).
Definition compatible_g (PG : G → Prop) : Prop :=
compatible_m PG ∧ opp_closed PG.
End Compatible_Group_Def.
Section Compatible_Group_Facts.
Context {G : AbelianGroup}.
Lemma plus_opp_minus_closed :
∀ {PG : G → Prop}, plus_closed PG → opp_closed PG → minus_closed PG.
Proof. intros PG H1 H2 x y; rewrite minus_eq; auto. Qed.
Lemma minus_zero_closed :
∀ {PG : G → Prop}, nonempty PG → minus_closed PG → zero_closed PG.
Proof.
move=>> [x Hx]; unfold zero_closed; rewrite -(minus_eq_zero x); auto.
Qed.
Lemma plus_opp_zero_closed :
∀ {PG : G → Prop},
nonempty PG → plus_closed PG → opp_closed PG → zero_closed PG.
Proof. intros; apply minus_zero_closed, plus_opp_minus_closed; easy. Qed.
Lemma minus_opp_closed :
∀ {PG : G → Prop}, nonempty PG → minus_closed PG → opp_closed PG.
Proof.
intros PG HPG0 HPG1 x; rewrite -(minus_zero_l x).
apply HPG1, minus_zero_closed; easy.
Qed.
Lemma minus_plus_closed :
∀ {PG : G → Prop}, nonempty PG → minus_closed PG → plus_closed PG.
Proof.
intros PG HPG0 HPG1 x y Hx Hy.
rewrite -minus_opp; apply HPG1; try easy.
apply minus_opp_closed; easy.
Qed.
Lemma minus_plus_opp_closed_equiv :
∀ {PG : G → Prop},
nonempty PG → minus_closed PG ↔ plus_closed PG ∧ opp_closed PG.
Proof.
intros; split.
intros; split; [apply minus_plus_closed | apply minus_opp_closed]; easy.
intros; apply plus_opp_minus_closed; easy.
Qed.
Lemma minus_closed_cg :
∀ {PG : G → Prop}, nonempty PG → minus_closed PG → compatible_g PG.
Proof.
intros; repeat split; [apply minus_plus_closed | apply minus_zero_closed |
apply minus_opp_closed]; easy.
Qed.
Lemma plus_opp_closed_cg :
∀ {PG : G → Prop},
nonempty PG → plus_closed PG → opp_closed PG → compatible_g PG.
Proof.
intros; apply minus_closed_cg; [| apply plus_opp_minus_closed]; easy.
Qed.
Lemma cg_cm : ∀ {PG : G → Prop}, compatible_g PG → compatible_m PG.
Proof. move=>> H; apply H. Qed.
Lemma cm_cg :
∀ {PG : G → Prop}, opp_closed PG → compatible_m PG → compatible_g PG.
Proof.
intros; apply plus_opp_closed_cg; [apply cm_nonempty | apply cm_plus | ]; easy.
Qed.
Lemma cg_cm_equiv :
∀ {PG : G → Prop},
opp_closed PG → compatible_g PG ↔ compatible_m PG.
Proof. intros; split; [apply cg_cm | apply cm_cg; easy]. Qed.
Lemma cg_nonempty : ∀ {PG : G → Prop}, compatible_g PG → nonempty PG.
Proof. move=>> /cg_cm; apply cm_nonempty. Qed.
Lemma cg_zero : ∀ {PG : G → Prop}, compatible_g PG → zero_closed PG.
Proof. move=>> /cg_cm; apply cm_zero. Qed.
Lemma cg_plus : ∀ {PG : G → Prop}, compatible_g PG → plus_closed PG.
Proof. move=>> /cg_cm; apply cm_plus. Qed.
Lemma cg_sum : ∀ {PG : G → Prop}, compatible_g PG → sum_closed PG.
Proof. move=>> /cg_cm; apply cm_sum. Qed.
Lemma cg_opp : ∀ {PG : G → Prop}, compatible_g PG → opp_closed PG.
Proof. move=>> H; apply H. Qed.
Lemma cg_minus : ∀ {PG : G → Prop}, compatible_g PG → minus_closed PG.
Proof. move=>> H; apply plus_opp_minus_closed; apply H. Qed.
Lemma cg_plus_opp_equiv :
∀ {PG : G → Prop},
compatible_g PG ↔ nonempty PG ∧ plus_closed PG ∧ opp_closed PG.
Proof.
intros; split; intros H; [| apply plus_opp_closed_cg; apply H].
repeat split; [apply cg_nonempty | apply cg_plus | apply cg_opp]; easy.
Qed.
Lemma cg_minus_equiv :
∀ {PG : G → Prop}, compatible_g PG ↔ nonempty PG ∧ minus_closed PG.
Proof.
intros; split; intros; [split |];
[apply cg_nonempty | apply cg_minus | apply minus_closed_cg]; easy.
Qed.
Lemma cg_zero_sub_struct : compatible_g (@zero_sub_struct G).
Proof.
split; [apply cm_zero_sub_struct | intros x Hx; rewrite Hx opp_zero; easy].
Qed.
Lemma cg_full : ∀ {PG : G → Prop}, full PG → compatible_g PG.
Proof. intros; split; [apply cm_full |]; easy. Qed.
Lemma cg_fullset : compatible_g (@fullset G).
Proof. apply cg_full; easy. Qed.
Lemma opp_closed_inter :
∀ {PG QG : G → Prop},
opp_closed PG → opp_closed QG → opp_closed (inter PG QG).
Proof. move=>> HPG HQG x Hx; split; [apply HPG, Hx | apply HQG, Hx]. Qed.
Lemma cg_inter :
∀ {PG QG : G → Prop},
compatible_g PG → compatible_g QG → compatible_g (inter PG QG).
Proof.
move=>> HPG HQG; split; [apply cm_inter; apply cg_cm; easy |].
apply opp_closed_inter; [apply HPG | apply HQG].
Qed.
[GostiauxT1]
Th 4.6, p. 89.
Lemma opp_closed_inter_any :
∀ {Idx : Type} {PG : Idx → G → Prop},
(∀ i, opp_closed (PG i)) → opp_closed (inter_any PG).
Proof. move=>> HPG; move=>> Hx i; apply HPG, Hx. Qed.
∀ {Idx : Type} {PG : Idx → G → Prop},
(∀ i, opp_closed (PG i)) → opp_closed (inter_any PG).
Proof. move=>> HPG; move=>> Hx i; apply HPG, Hx. Qed.
[GostiauxT1]
Th 4.6, p. 89.
Lemma cg_inter_any :
∀ {Idx : Type} {PG : Idx → G → Prop},
(∀ i, compatible_g (PG i)) → compatible_g (inter_any PG).
Proof.
move=>> HPG; split.
apply cm_inter_any; intro; apply cg_cm; easy.
apply opp_closed_inter_any; intro; apply HPG.
Qed.
∀ {Idx : Type} {PG : Idx → G → Prop},
(∀ i, compatible_g (PG i)) → compatible_g (inter_any PG).
Proof.
move=>> HPG; split.
apply cm_inter_any; intro; apply cg_cm; easy.
apply opp_closed_inter_any; intro; apply HPG.
Qed.
[GostiauxT1]
Th 4.10, pp. 89-91.
Definition span_g (gen : G → Prop) := span compatible_g gen.
Lemma span_g_cg : ∀ gen, compatible_g (span_g gen).
Proof. apply span_compatible; move=>>; apply cg_inter_any. Qed.
Lemma span_g_nonempty : ∀ gen, nonempty (span_g gen).
Proof. intros; apply cg_nonempty, span_g_cg. Qed.
Lemma span_g_zero : ∀ gen, zero_closed (span_g gen).
Proof. intros; apply cg_zero, span_g_cg. Qed.
Lemma span_g_plus : ∀ gen, plus_closed (span_g gen).
Proof. intros; apply cg_plus, span_g_cg. Qed.
Lemma span_g_opp : ∀ gen, opp_closed (span_g gen).
Proof. intros; apply cg_opp, span_g_cg. Qed.
Lemma span_g_minus : ∀ gen, minus_closed (span_g gen).
Proof. intros; apply cg_minus, span_g_cg. Qed.
Lemma span_g_incl : ∀ gen, incl gen (span_g gen).
Proof. apply span_incl. Qed.
Lemma span_g_cg : ∀ gen, compatible_g (span_g gen).
Proof. apply span_compatible; move=>>; apply cg_inter_any. Qed.
Lemma span_g_nonempty : ∀ gen, nonempty (span_g gen).
Proof. intros; apply cg_nonempty, span_g_cg. Qed.
Lemma span_g_zero : ∀ gen, zero_closed (span_g gen).
Proof. intros; apply cg_zero, span_g_cg. Qed.
Lemma span_g_plus : ∀ gen, plus_closed (span_g gen).
Proof. intros; apply cg_plus, span_g_cg. Qed.
Lemma span_g_opp : ∀ gen, opp_closed (span_g gen).
Proof. intros; apply cg_opp, span_g_cg. Qed.
Lemma span_g_minus : ∀ gen, minus_closed (span_g gen).
Proof. intros; apply cg_minus, span_g_cg. Qed.
Lemma span_g_incl : ∀ gen, incl gen (span_g gen).
Proof. apply span_incl. Qed.
[GostiauxT1]
Def 4.9, p. 90.
Lemma span_g_lub :
∀ {gen PG}, compatible_g PG → incl gen PG → incl (span_g gen) PG.
Proof. apply span_lub. Qed.
Lemma span_g_full : ∀ {PG}, compatible_g PG → span_g PG = PG.
Proof. apply span_full. Qed.
End Compatible_Group_Facts.
Section Compatible_Group_Morphism_Facts0.
Context {G1 G2 : AbelianGroup}.
Lemma cg_mg : compatible_g (@morphism_g G1 G2).
Proof.
repeat split; [move=>>; apply mg_fct_plus | apply mg_fct_zero |
move=>>; apply mg_fct_opp].
Qed.
End Compatible_Group_Morphism_Facts0.
Section Compatible_Group_Morphism_Facts1.
Context {G1 G2 : AbelianGroup}.
Context {PG1 : G1 → Prop}.
Context {PG2 : G2 → Prop}.
Context {f : G1 → G2}.
Hypothesis Hf : morphism_g f.
Lemma cg_image : compatible_g PG1 → compatible_g (image f PG1).
Proof.
intros [HPG1a HPG1b]; split.
apply cm_image; [apply mg_mm |]; easy.
intros _ [x1 Hx1]; rewrite -(mg_opp Hf); apply Im; auto.
Qed.
Lemma cg_preimage : compatible_g PG2 → compatible_g (preimage f PG2).
Proof.
intros [HPG2a HPG2b]; split.
apply cm_preimage; [apply mg_mm; easy | apply HPG2a].
intros x1 Hx1; unfold preimage; rewrite (mg_opp Hf); apply HPG2b; easy.
Qed.
End Compatible_Group_Morphism_Facts1.
Section Compatible_Group_Morphism_Def.
Context {G1 G2 : AbelianGroup}.
Variable PG1 : G1 → Prop.
Variable f : G1 → G2.
Definition mg_sub : Prop := f_plus_compat_sub PG1 f.
End Compatible_Group_Morphism_Def.
Section Compatible_Group_Morphism_Facts2a.
Context {G1 G2 : AbelianGroup}.
Context {PG1 : G1 → Prop}.
Hypothesis HPG1 : compatible_g PG1.
Context {PG2 : G2 → Prop}.
Hypothesis HPG2 : compatible_g PG2.
Context {f : G1 → G2}.
Hypothesis Hf : morphism_g f.
Lemma KerS_cg : compatible_g (KerS PG1 f).
Proof. apply cg_inter, cg_preimage, cg_zero_sub_struct; easy. Qed.
Lemma RgS_gen_cg : compatible_g (RgS_gen PG1 PG2 f).
Proof. apply cg_inter, cg_image; easy. Qed.
Lemma RgS_cg : compatible_g (RgS PG1 f).
Proof. apply cg_image; easy. Qed.
Lemma KerS_g_zero_equiv :
KerS PG1 f = zero_sub_struct ↔ incl (KerS PG1 f) zero_sub_struct.
Proof. apply KerS_m_zero_equiv; [apply cg_cm | apply mg_mm]; easy. Qed.
Lemma gmS_injS : incl (KerS PG1 f) zero_sub_struct → injS PG1 f.
Proof.
intros Hf1 x1 y1 Hx1 Hy1; rewrite -2!minus_zero_equiv -(mg_minus Hf).
intros H1; apply Hf1, KerS_equiv; split; [apply cg_minus |]; easy.
Qed.
Lemma gmS_injS_rev : injS PG1 f → KerS PG1 f = zero_sub_struct.
Proof. apply mmS_injS_rev; [apply cg_cm | apply mg_mm]; easy. Qed.
Lemma gmS_injS_equiv : injS PG1 f ↔ KerS PG1 f = zero_sub_struct.
Proof.
split; [apply gmS_injS_rev | rewrite KerS_g_zero_equiv; apply gmS_injS].
Qed.
Lemma gmS_bijS_gen :
funS PG1 PG2 f → incl (KerS PG1 f) zero_sub_struct → incl PG2 (RgS PG1 f) →
bijS PG1 PG2 f.
Proof.
intros; apply bijS_equiv; [apply inhabited_g | repeat split];
[| apply gmS_injS | apply surjS_correct]; easy.
Qed.
Lemma gmS_bijS_gen_rev :
bijS PG1 PG2 f →
funS PG1 PG2 f ∧ KerS PG1 f = zero_sub_struct ∧ RgS_gen PG1 PG2 f = PG2.
Proof. apply mmS_bijS_gen_rev; [apply cg_cm | apply mg_mm]; easy. Qed.
Lemma gmS_bijS_gen_equiv :
bijS PG1 PG2 f ↔
funS PG1 PG2 f ∧ KerS PG1 f = zero_sub_struct ∧ RgS_gen PG1 PG2 f = PG2.
Proof.
split; [apply gmS_bijS_gen_rev | rewrite KerS_g_zero_equiv RgS_gen_full_equiv].
intros; apply gmS_bijS_gen; easy.
Qed.
Lemma gmS_bijS : incl (KerS PG1 f) zero_sub_struct → bijS PG1 (RgS PG1 f) f.
Proof.
rewrite bijS_RgS_equiv; [| apply inhabited_g]; apply gmS_injS; easy.
Qed.
Lemma gmS_bijS_rev : bijS PG1 (RgS PG1 f) f → KerS PG1 f = zero_sub_struct.
Proof. apply mmS_bijS_rev; [apply cg_cm | apply mg_mm]; easy. Qed.
Lemma gmS_bijS_equiv : bijS PG1 (RgS PG1 f) f ↔ KerS PG1 f = zero_sub_struct.
Proof.
split; [apply gmS_bijS_rev | rewrite KerS_g_zero_equiv//; apply gmS_bijS].
Qed.
Lemma gmS_bijS_injS_equiv : bijS PG1 (RgS PG1 f) f ↔ injS PG1 f.
Proof. apply mmS_bijS_injS_equiv. Qed.
End Compatible_Group_Morphism_Facts2a.
Section Compatible_Group_Morphism_Facts2b.
Context {G1 G2 : AbelianGroup}.
Context {f : G1 → G2}.
Hypothesis Hf : morphism_g f.
Lemma Ker_cg : compatible_g (Ker f).
Proof. rewrite -KerS_full; apply (KerS_cg cg_fullset Hf). Qed.
Lemma Rg_cg : compatible_g (Rg f).
Proof. rewrite -RgS_full; apply (RgS_cg cg_fullset Hf). Qed.
Lemma Ker_g_zero_equiv :
Ker f = zero_sub_struct ↔ incl (Ker f) zero_sub_struct.
Proof. apply Ker_m_zero_equiv, mg_mm; easy. Qed.
Lemma gm_inj : incl (Ker f) zero_sub_struct → injective f.
Proof. rewrite -KerS_full inj_S_equiv; apply (gmS_injS cg_fullset Hf). Qed.
Lemma gm_inj_rev : injective f → Ker f = zero_sub_struct.
Proof. apply mm_inj_rev, mg_mm; easy. Qed.
Lemma gm_inj_equiv : injective f ↔ Ker f = zero_sub_struct.
Proof.
rewrite -KerS_full inj_S_equiv; apply (gmS_injS_equiv cg_fullset Hf).
Qed.
Lemma gm_bij :
incl (Ker f) zero_sub_struct → incl fullset (Rg f) → bijective f.
Proof.
rewrite -KerS_full -RgS_full bij_S_equiv; [| apply inhabited_g].
apply (gmS_bijS_gen cg_fullset Hf), funS_full.
Qed.
Lemma gm_bij_rev : bijective f → Ker f = zero_sub_struct ∧ Rg f = fullset.
Proof. apply mm_bij_rev, mg_mm; easy. Qed.
Lemma gm_bij_equiv : bijective f ↔ Ker f = zero_sub_struct ∧ Rg f = fullset.
Proof.
rewrite -KerS_full -RgS_gen_full bij_S_equiv; [| apply inhabited_g].
rewrite (gmS_bijS_gen_equiv cg_fullset Hf); easy.
Qed.
End Compatible_Group_Morphism_Facts2b.
Section Compatible_Group_Morphism_Facts3.
Context {E1 E2 E3 : AbelianGroup}.
Context {f : E1 → E2}.
Hypothesis Hf : morphism_g f.
Context {g : E2 → E3}.
Hypothesis Hg : morphism_g g.
Lemma Ker_g_comp_r : injective g → RgS (Ker (g \o f)) f = Ker g.
Proof. apply Ker_m_comp_r; apply mg_mm; easy. Qed.
Lemma Ker_g_comp_r_alt :
∀ h x2, injective g → h = g \o f →
(∃ x1, h x1 = 0 ∧ f x1 = x2) ↔ g x2 = 0.
Proof. apply Ker_m_comp_r_alt; apply mg_mm; easy. Qed.
End Compatible_Group_Morphism_Facts3.
Section Compatible_Group_Morphism_Facts4a.
Context {G1 G2 : AbelianGroup}.
Variable PG1 : G1 → Prop.
Lemma mg_sub_id : mg_sub PG1 ssrfun.id.
Proof. easy. Qed.
Lemma mg_is_sub : ∀ {f : G1 → G2}, morphism_g f → mg_sub PG1 f.
Proof. easy. Qed.
End Compatible_Group_Morphism_Facts4a.
Section Compatible_Group_Morphism_Facts4b.
Context {G1 G2 G3 : AbelianGroup}.
Context {PG1 : G1 → Prop}.
Variable PG2 : G2 → Prop.
Context {f : G1 → G2}.
Hypothesis Hf : funS PG1 PG2 f.
Variable g : G2 → G3.
Lemma mg_comp_sub : mg_sub PG1 f → mg_sub PG2 g → mg_sub PG1 (g \o f).
Proof. apply f_plus_compat_comp_sub; easy. Qed.
End Compatible_Group_Morphism_Facts4b.
Section Sub_Group_Def.
Context {G : AbelianGroup}.
Context {PG : G → Prop}.
Hypothesis HPG : compatible_g PG.
Let PG_m := sub_AbelianMonoid (cg_cm HPG).
Definition sub_opp (x : PG_m) : PG_m := mk_sub (cg_opp HPG _ (in_sub x)).
Lemma sub_plus_opp_r : ∀ x, x + (sub_opp x) = 0.
Proof. intros; apply val_inj, plus_opp_r. Qed.
Definition sub_AbelianGroup_mixin := AbelianGroup.Mixin _ _ sub_plus_opp_r.
Canonical Structure sub_AbelianGroup :=
AbelianGroup.Pack _ (AbelianGroup.Class _ _ sub_AbelianGroup_mixin) PG_m.
Lemma val_opp : f_opp_compat val.
Proof. easy. Qed.
Lemma val_minus : f_minus_compat val.
Proof. easy. Qed.
Lemma val_mg : morphism_g val.
Proof. easy. Qed.
Lemma mk_sub_g_zero : mk_sub (cg_zero HPG : PG 0) = 0 :> sub_AbelianGroup.
Proof. apply val_inj; easy. Qed.
Lemma mk_sub_g_zero_equiv :
∀ {x} (Hx : PG x), mk_sub Hx = 0 :> sub_AbelianGroup ↔ x = 0.
Proof. apply mk_sub_zero_equiv. Qed.
Lemma mk_sub_opp :
∀ (x : G) (Hx : PG x), - mk_sub Hx = mk_sub (cg_opp HPG _ Hx).
Proof. easy. Qed.
Lemma mk_sub_minus :
∀ (x y : G) (Hx : PG x) (Hy : PG y),
mk_sub Hx - mk_sub Hy = mk_sub (cg_minus HPG _ _ Hx Hy).
Proof. intros; apply val_inj; easy. Qed.
Lemma sub_opp_eq :
∀ (x : sub_AbelianGroup), - x = mk_sub (cg_opp HPG _ (in_sub x)).
Proof. easy. Qed.
Lemma sub_minus_eq :
∀ (x y : sub_AbelianGroup),
x - y = mk_sub (cg_minus HPG _ _ (in_sub x) (in_sub y)).
Proof. intros; apply mk_sub_minus. Qed.
Lemma val_g_inv_r :
∀ {x} (Hx : PG x), val (mk_sub Hx : sub_AbelianGroup) = x.
Proof. intros; apply val_inv_r. Qed.
Lemma mk_sub_g_inv_r : ∀ {x}, mk_sub (in_sub x) = x :> sub_AbelianGroup.
Proof. intros; apply mk_sub_inv_r. Qed.
Lemma mk_sub_g_inj :
∀ {x y} (Hx : PG x) (Hy : PG y),
mk_sub Hx = mk_sub Hy :> sub_AbelianGroup → x = y.
Proof. intros x y; apply mk_sub_inj. Qed.
End Sub_Group_Def.
Section Sub_Group_Facts1.
Context {G : AbelianGroup}.
Context {PGa PG : G → Prop}.
Hypothesis HPGa : incl PGa PG.
Hypothesis HPG : compatible_g PG.
Let PG_g := sub_AbelianGroup HPG.
Let PGa' : PG_g → Prop := preimage val PGa.
Lemma RgS_val_g_eq : RgS PGa' val = PGa.
Proof. apply RgS_val_eq; easy. Qed.
Lemma preimage_val_cg : compatible_g PGa → compatible_g PGa'.
Proof. intros; apply cg_preimage; easy. Qed.
Lemma preimage_val_cg_rev : compatible_g PGa' → compatible_g PGa.
Proof. intros; rewrite -RgS_val_g_eq; apply RgS_cg; easy. Qed.
Lemma preimage_val_cg_equiv : compatible_g PGa' ↔ compatible_g PGa.
Proof. split; [apply preimage_val_cg_rev | apply preimage_val_cg]. Qed.
End Sub_Group_Facts1.
Section Sub_Group_Facts2.
Context {G : AbelianGroup}.
Context {PG : G → Prop}.
Hypothesis HPG : compatible_g PG.
Let PG_g := sub_AbelianGroup HPG.
Variable PGa : PG_g → Prop.
Let PGa' := RgS PGa val.
Lemma preimage_val_g_eq : preimage val PGa' = PGa.
Proof. apply preimage_val_eq. Qed.
Lemma RgS_val_cg : compatible_g PGa → compatible_g PGa'.
Proof. intros; apply RgS_cg; easy. Qed.
Lemma RgS_val_cg_rev : compatible_g PGa' → compatible_g PGa.
Proof. intros; rewrite -preimage_val_g_eq; apply cg_preimage; easy. Qed.
Lemma RgS_val_cg_equiv : compatible_g PGa' ↔ compatible_g PGa.
Proof. split; [apply RgS_val_cg_rev | apply RgS_val_cg]. Qed.
End Sub_Group_Facts2.
Section Sub_Group_Morphism_Facts1.
Context {G1 G2 : AbelianGroup}.
Context {PG1 : G1 → Prop}.
Context {PG2 : G2 → Prop}.
Context {HPG1 : compatible_g PG1}.
Context {HPG2 : compatible_g PG2}.
Let PG1_g := sub_AbelianGroup HPG1.
Let PG2_g := sub_AbelianGroup HPG2.
Context {f : G1 → G2}.
Context {fS : PG1_g → PG2_g}.
Hypothesis HfS : ∀ x, val (fS x) = f (val x).
Lemma sub_g_f_opp_compat : f_opp_compat f → f_opp_compat fS.
Proof. intros Hf x1; apply val_inj; rewrite HfS Hf -HfS; easy. Qed.
Lemma sub_g_f_minus_compat : f_minus_compat f → f_minus_compat fS.
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⇒ /mg_mm; apply Ker_sub_zero_equiv, HfS. Qed.
Lemma KerS_g_zero_equiv_alt :
morphism_g f →
KerS PG1 f = zero_sub_struct ↔
∀ (x1 : sub_AbelianGroup 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 (cg_zero HPG1)).
rewrite mk_sub_g_zero; apply Hf1; easy.
move⇒ x1 ->; apply cg_zero, KerS_cg; easy.
Qed.
Lemma Ker_sub_g_zero_equiv :
morphism_g f →
Ker fS = zero_sub_struct ↔
∀ (x1 : sub_AbelianGroup 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 (Ker_sub_KerS_equiv HfS) Hf1; apply val_zero_equiv.
destruct (classic (PG1 x1)) as [Hx1 | Hx1a].
rewrite (KerS_Ker_sub_equiv HfS Hx1) Hf1; apply mk_sub_zero_equiv.
split; intros Hx1b; contradict Hx1a;
[apply Hx1b | rewrite Hx1b; apply cg_zero, HPG1].
Qed.
Lemma gmS_injS_val_equiv :
morphism_g f →
injS PG1 f ↔ ∀ (x1 : sub_AbelianGroup 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_val_equiv :
morphism_g f →
bijS PG1 (RgS PG1 f) f ↔
∀ (x1 : sub_AbelianGroup HPG1), f (val x1) = 0 → x1 = 0.
Proof. rewrite gmS_bijS_injS_equiv; apply gmS_injS_val_equiv. Qed.
End Sub_Group_Morphism_Facts1.
Section Sub_Group_Morphism_Facts2.
Context {G1 G2 : AbelianGroup}.
Context {PG1 : G1 → Prop}.
Context {PG2 : G2 → Prop}.
Hypothesis HPG1 : compatible_g PG1.
Hypothesis HPG2 : compatible_g PG2.
Let PG1_g := sub_AbelianGroup HPG1.
Let PG2_g := sub_AbelianGroup HPG2.
Context {f : G1 → G2}.
Hypothesis Hf : funS PG1 PG2 f.
Definition fct_sub_g : PG1_g → PG2_g := fct_sub Hf.
Lemma fct_sub_g_inj : injS PG1 f → injective fct_sub_g.
Proof. apply fct_sub_inj. Qed.
Lemma fct_sub_g_inj_rev : injective fct_sub_g → injS PG1 f.
Proof. apply fct_sub_inj_rev. Qed.
Lemma fct_sub_g_inj_equiv : injective fct_sub_g ↔ injS PG1 f.
Proof. apply fct_sub_inj_equiv. Qed.
Lemma fct_sub_g_surj : surjS PG1 PG2 f → surjective fct_sub_g.
Proof. apply fct_sub_surj. Qed.
Lemma fct_sub_g_surj_rev : surjective fct_sub_g → surjS PG1 PG2 f.
Proof. apply fct_sub_surj_rev. Qed.
Lemma fct_sub_g_surj_equiv : surjective fct_sub_g ↔ surjS PG1 PG2 f.
Proof. apply fct_sub_surj_equiv. Qed.
Lemma fct_sub_g_bij : bijS PG1 PG2 f → bijective fct_sub_g.
Proof. apply fct_sub_bij, inhabited_g. Qed.
Lemma fct_sub_g_bij_rev : bijective fct_sub_g → bijS PG1 PG2 f.
Proof. apply fct_sub_bij_rev, inhabited_g. Qed.
Lemma fct_sub_g_bij_equiv : bijective fct_sub_g ↔ bijS PG1 PG2 f.
Proof. apply fct_sub_bij_equiv, inhabited_g. Qed.
Lemma fct_sub_g_f_opp_compat : f_opp_compat f → f_opp_compat fct_sub_g.
Proof. apply sub_g_f_opp_compat, fct_sub_correct. Qed.
Lemma fct_sub_g_f_minus_compat : f_minus_compat f → f_minus_compat fct_sub_g.
Proof. apply sub_g_f_minus_compat, fct_sub_correct. Qed.
Lemma fct_sub_g_mg : morphism_g f → morphism_g fct_sub_g.
Proof. apply sub_g_morphism, fct_sub_correct. Qed.
Lemma fct_sub_g_f_inv_mg :
∀ (Hfb : bijS PG1 PG2 f),
morphism_g f → morphism_g (f_inv (fct_sub_g_bij Hfb)).
Proof. intros; apply mg_bij_compat, fct_sub_g_mg; easy. 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 ↔
∀ (x1 : sub_AbelianGroup 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_Facts2.
Section Compose_n_Group_Facts.
Context {E : AbelianGroup}.
Context {PE : E → Prop}.
Context {n : nat}.
Variable f : '(E → E)^n.
Hypothesis Hf : ∀ i, funS PE PE (f i).
Lemma comp_n_mg_sub : (∀ i, mg_sub PE (f i)) → mg_sub PE (comp_n f).
Proof.
intros Hf1; induction n as [| n1 Hn1];
[rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply (mg_comp_sub PE);
[apply comp_n_funS | apply Hn1 |]; unfold liftF_S; easy.
Qed.
End Compose_n_Group_Facts.
Section Compose_n_part_Group_Facts.
Context {E : AbelianGroup}.
Context {PE : E → Prop}.
Context {n : nat}.
Variable f : '(E → E)^n.
Variable j : 'I_n.+1.
Hypothesis Hf : ∀ i, funS PE PE (widenF (leq_ord j) f i).
Lemma comp_n_part_mg_sub :
(∀ i, mg_sub PE (widenF (leq_ord j) f i)) →
mg_sub PE (comp_n_part f j).
Proof.
intros Hf1; induction n as [| n1 Hn1]; [rewrite comp_n_part_nil; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
[rewrite (comp_n_part_0 _ _ Hj0); easy |].
rewrite comp_n_part_ind_l; apply (mg_comp_sub PE).
apply comp_n_part_funS; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply Hn1; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply (widenF_0_P_compat Hj0 Hf1).
Qed.
End Compose_n_part_Group_Facts.
∀ {gen PG}, compatible_g PG → incl gen PG → incl (span_g gen) PG.
Proof. apply span_lub. Qed.
Lemma span_g_full : ∀ {PG}, compatible_g PG → span_g PG = PG.
Proof. apply span_full. Qed.
End Compatible_Group_Facts.
Section Compatible_Group_Morphism_Facts0.
Context {G1 G2 : AbelianGroup}.
Lemma cg_mg : compatible_g (@morphism_g G1 G2).
Proof.
repeat split; [move=>>; apply mg_fct_plus | apply mg_fct_zero |
move=>>; apply mg_fct_opp].
Qed.
End Compatible_Group_Morphism_Facts0.
Section Compatible_Group_Morphism_Facts1.
Context {G1 G2 : AbelianGroup}.
Context {PG1 : G1 → Prop}.
Context {PG2 : G2 → Prop}.
Context {f : G1 → G2}.
Hypothesis Hf : morphism_g f.
Lemma cg_image : compatible_g PG1 → compatible_g (image f PG1).
Proof.
intros [HPG1a HPG1b]; split.
apply cm_image; [apply mg_mm |]; easy.
intros _ [x1 Hx1]; rewrite -(mg_opp Hf); apply Im; auto.
Qed.
Lemma cg_preimage : compatible_g PG2 → compatible_g (preimage f PG2).
Proof.
intros [HPG2a HPG2b]; split.
apply cm_preimage; [apply mg_mm; easy | apply HPG2a].
intros x1 Hx1; unfold preimage; rewrite (mg_opp Hf); apply HPG2b; easy.
Qed.
End Compatible_Group_Morphism_Facts1.
Section Compatible_Group_Morphism_Def.
Context {G1 G2 : AbelianGroup}.
Variable PG1 : G1 → Prop.
Variable f : G1 → G2.
Definition mg_sub : Prop := f_plus_compat_sub PG1 f.
End Compatible_Group_Morphism_Def.
Section Compatible_Group_Morphism_Facts2a.
Context {G1 G2 : AbelianGroup}.
Context {PG1 : G1 → Prop}.
Hypothesis HPG1 : compatible_g PG1.
Context {PG2 : G2 → Prop}.
Hypothesis HPG2 : compatible_g PG2.
Context {f : G1 → G2}.
Hypothesis Hf : morphism_g f.
Lemma KerS_cg : compatible_g (KerS PG1 f).
Proof. apply cg_inter, cg_preimage, cg_zero_sub_struct; easy. Qed.
Lemma RgS_gen_cg : compatible_g (RgS_gen PG1 PG2 f).
Proof. apply cg_inter, cg_image; easy. Qed.
Lemma RgS_cg : compatible_g (RgS PG1 f).
Proof. apply cg_image; easy. Qed.
Lemma KerS_g_zero_equiv :
KerS PG1 f = zero_sub_struct ↔ incl (KerS PG1 f) zero_sub_struct.
Proof. apply KerS_m_zero_equiv; [apply cg_cm | apply mg_mm]; easy. Qed.
Lemma gmS_injS : incl (KerS PG1 f) zero_sub_struct → injS PG1 f.
Proof.
intros Hf1 x1 y1 Hx1 Hy1; rewrite -2!minus_zero_equiv -(mg_minus Hf).
intros H1; apply Hf1, KerS_equiv; split; [apply cg_minus |]; easy.
Qed.
Lemma gmS_injS_rev : injS PG1 f → KerS PG1 f = zero_sub_struct.
Proof. apply mmS_injS_rev; [apply cg_cm | apply mg_mm]; easy. Qed.
Lemma gmS_injS_equiv : injS PG1 f ↔ KerS PG1 f = zero_sub_struct.
Proof.
split; [apply gmS_injS_rev | rewrite KerS_g_zero_equiv; apply gmS_injS].
Qed.
Lemma gmS_bijS_gen :
funS PG1 PG2 f → incl (KerS PG1 f) zero_sub_struct → incl PG2 (RgS PG1 f) →
bijS PG1 PG2 f.
Proof.
intros; apply bijS_equiv; [apply inhabited_g | repeat split];
[| apply gmS_injS | apply surjS_correct]; easy.
Qed.
Lemma gmS_bijS_gen_rev :
bijS PG1 PG2 f →
funS PG1 PG2 f ∧ KerS PG1 f = zero_sub_struct ∧ RgS_gen PG1 PG2 f = PG2.
Proof. apply mmS_bijS_gen_rev; [apply cg_cm | apply mg_mm]; easy. Qed.
Lemma gmS_bijS_gen_equiv :
bijS PG1 PG2 f ↔
funS PG1 PG2 f ∧ KerS PG1 f = zero_sub_struct ∧ RgS_gen PG1 PG2 f = PG2.
Proof.
split; [apply gmS_bijS_gen_rev | rewrite KerS_g_zero_equiv RgS_gen_full_equiv].
intros; apply gmS_bijS_gen; easy.
Qed.
Lemma gmS_bijS : incl (KerS PG1 f) zero_sub_struct → bijS PG1 (RgS PG1 f) f.
Proof.
rewrite bijS_RgS_equiv; [| apply inhabited_g]; apply gmS_injS; easy.
Qed.
Lemma gmS_bijS_rev : bijS PG1 (RgS PG1 f) f → KerS PG1 f = zero_sub_struct.
Proof. apply mmS_bijS_rev; [apply cg_cm | apply mg_mm]; easy. Qed.
Lemma gmS_bijS_equiv : bijS PG1 (RgS PG1 f) f ↔ KerS PG1 f = zero_sub_struct.
Proof.
split; [apply gmS_bijS_rev | rewrite KerS_g_zero_equiv//; apply gmS_bijS].
Qed.
Lemma gmS_bijS_injS_equiv : bijS PG1 (RgS PG1 f) f ↔ injS PG1 f.
Proof. apply mmS_bijS_injS_equiv. Qed.
End Compatible_Group_Morphism_Facts2a.
Section Compatible_Group_Morphism_Facts2b.
Context {G1 G2 : AbelianGroup}.
Context {f : G1 → G2}.
Hypothesis Hf : morphism_g f.
Lemma Ker_cg : compatible_g (Ker f).
Proof. rewrite -KerS_full; apply (KerS_cg cg_fullset Hf). Qed.
Lemma Rg_cg : compatible_g (Rg f).
Proof. rewrite -RgS_full; apply (RgS_cg cg_fullset Hf). Qed.
Lemma Ker_g_zero_equiv :
Ker f = zero_sub_struct ↔ incl (Ker f) zero_sub_struct.
Proof. apply Ker_m_zero_equiv, mg_mm; easy. Qed.
Lemma gm_inj : incl (Ker f) zero_sub_struct → injective f.
Proof. rewrite -KerS_full inj_S_equiv; apply (gmS_injS cg_fullset Hf). Qed.
Lemma gm_inj_rev : injective f → Ker f = zero_sub_struct.
Proof. apply mm_inj_rev, mg_mm; easy. Qed.
Lemma gm_inj_equiv : injective f ↔ Ker f = zero_sub_struct.
Proof.
rewrite -KerS_full inj_S_equiv; apply (gmS_injS_equiv cg_fullset Hf).
Qed.
Lemma gm_bij :
incl (Ker f) zero_sub_struct → incl fullset (Rg f) → bijective f.
Proof.
rewrite -KerS_full -RgS_full bij_S_equiv; [| apply inhabited_g].
apply (gmS_bijS_gen cg_fullset Hf), funS_full.
Qed.
Lemma gm_bij_rev : bijective f → Ker f = zero_sub_struct ∧ Rg f = fullset.
Proof. apply mm_bij_rev, mg_mm; easy. Qed.
Lemma gm_bij_equiv : bijective f ↔ Ker f = zero_sub_struct ∧ Rg f = fullset.
Proof.
rewrite -KerS_full -RgS_gen_full bij_S_equiv; [| apply inhabited_g].
rewrite (gmS_bijS_gen_equiv cg_fullset Hf); easy.
Qed.
End Compatible_Group_Morphism_Facts2b.
Section Compatible_Group_Morphism_Facts3.
Context {E1 E2 E3 : AbelianGroup}.
Context {f : E1 → E2}.
Hypothesis Hf : morphism_g f.
Context {g : E2 → E3}.
Hypothesis Hg : morphism_g g.
Lemma Ker_g_comp_r : injective g → RgS (Ker (g \o f)) f = Ker g.
Proof. apply Ker_m_comp_r; apply mg_mm; easy. Qed.
Lemma Ker_g_comp_r_alt :
∀ h x2, injective g → h = g \o f →
(∃ x1, h x1 = 0 ∧ f x1 = x2) ↔ g x2 = 0.
Proof. apply Ker_m_comp_r_alt; apply mg_mm; easy. Qed.
End Compatible_Group_Morphism_Facts3.
Section Compatible_Group_Morphism_Facts4a.
Context {G1 G2 : AbelianGroup}.
Variable PG1 : G1 → Prop.
Lemma mg_sub_id : mg_sub PG1 ssrfun.id.
Proof. easy. Qed.
Lemma mg_is_sub : ∀ {f : G1 → G2}, morphism_g f → mg_sub PG1 f.
Proof. easy. Qed.
End Compatible_Group_Morphism_Facts4a.
Section Compatible_Group_Morphism_Facts4b.
Context {G1 G2 G3 : AbelianGroup}.
Context {PG1 : G1 → Prop}.
Variable PG2 : G2 → Prop.
Context {f : G1 → G2}.
Hypothesis Hf : funS PG1 PG2 f.
Variable g : G2 → G3.
Lemma mg_comp_sub : mg_sub PG1 f → mg_sub PG2 g → mg_sub PG1 (g \o f).
Proof. apply f_plus_compat_comp_sub; easy. Qed.
End Compatible_Group_Morphism_Facts4b.
Section Sub_Group_Def.
Context {G : AbelianGroup}.
Context {PG : G → Prop}.
Hypothesis HPG : compatible_g PG.
Let PG_m := sub_AbelianMonoid (cg_cm HPG).
Definition sub_opp (x : PG_m) : PG_m := mk_sub (cg_opp HPG _ (in_sub x)).
Lemma sub_plus_opp_r : ∀ x, x + (sub_opp x) = 0.
Proof. intros; apply val_inj, plus_opp_r. Qed.
Definition sub_AbelianGroup_mixin := AbelianGroup.Mixin _ _ sub_plus_opp_r.
Canonical Structure sub_AbelianGroup :=
AbelianGroup.Pack _ (AbelianGroup.Class _ _ sub_AbelianGroup_mixin) PG_m.
Lemma val_opp : f_opp_compat val.
Proof. easy. Qed.
Lemma val_minus : f_minus_compat val.
Proof. easy. Qed.
Lemma val_mg : morphism_g val.
Proof. easy. Qed.
Lemma mk_sub_g_zero : mk_sub (cg_zero HPG : PG 0) = 0 :> sub_AbelianGroup.
Proof. apply val_inj; easy. Qed.
Lemma mk_sub_g_zero_equiv :
∀ {x} (Hx : PG x), mk_sub Hx = 0 :> sub_AbelianGroup ↔ x = 0.
Proof. apply mk_sub_zero_equiv. Qed.
Lemma mk_sub_opp :
∀ (x : G) (Hx : PG x), - mk_sub Hx = mk_sub (cg_opp HPG _ Hx).
Proof. easy. Qed.
Lemma mk_sub_minus :
∀ (x y : G) (Hx : PG x) (Hy : PG y),
mk_sub Hx - mk_sub Hy = mk_sub (cg_minus HPG _ _ Hx Hy).
Proof. intros; apply val_inj; easy. Qed.
Lemma sub_opp_eq :
∀ (x : sub_AbelianGroup), - x = mk_sub (cg_opp HPG _ (in_sub x)).
Proof. easy. Qed.
Lemma sub_minus_eq :
∀ (x y : sub_AbelianGroup),
x - y = mk_sub (cg_minus HPG _ _ (in_sub x) (in_sub y)).
Proof. intros; apply mk_sub_minus. Qed.
Lemma val_g_inv_r :
∀ {x} (Hx : PG x), val (mk_sub Hx : sub_AbelianGroup) = x.
Proof. intros; apply val_inv_r. Qed.
Lemma mk_sub_g_inv_r : ∀ {x}, mk_sub (in_sub x) = x :> sub_AbelianGroup.
Proof. intros; apply mk_sub_inv_r. Qed.
Lemma mk_sub_g_inj :
∀ {x y} (Hx : PG x) (Hy : PG y),
mk_sub Hx = mk_sub Hy :> sub_AbelianGroup → x = y.
Proof. intros x y; apply mk_sub_inj. Qed.
End Sub_Group_Def.
Section Sub_Group_Facts1.
Context {G : AbelianGroup}.
Context {PGa PG : G → Prop}.
Hypothesis HPGa : incl PGa PG.
Hypothesis HPG : compatible_g PG.
Let PG_g := sub_AbelianGroup HPG.
Let PGa' : PG_g → Prop := preimage val PGa.
Lemma RgS_val_g_eq : RgS PGa' val = PGa.
Proof. apply RgS_val_eq; easy. Qed.
Lemma preimage_val_cg : compatible_g PGa → compatible_g PGa'.
Proof. intros; apply cg_preimage; easy. Qed.
Lemma preimage_val_cg_rev : compatible_g PGa' → compatible_g PGa.
Proof. intros; rewrite -RgS_val_g_eq; apply RgS_cg; easy. Qed.
Lemma preimage_val_cg_equiv : compatible_g PGa' ↔ compatible_g PGa.
Proof. split; [apply preimage_val_cg_rev | apply preimage_val_cg]. Qed.
End Sub_Group_Facts1.
Section Sub_Group_Facts2.
Context {G : AbelianGroup}.
Context {PG : G → Prop}.
Hypothesis HPG : compatible_g PG.
Let PG_g := sub_AbelianGroup HPG.
Variable PGa : PG_g → Prop.
Let PGa' := RgS PGa val.
Lemma preimage_val_g_eq : preimage val PGa' = PGa.
Proof. apply preimage_val_eq. Qed.
Lemma RgS_val_cg : compatible_g PGa → compatible_g PGa'.
Proof. intros; apply RgS_cg; easy. Qed.
Lemma RgS_val_cg_rev : compatible_g PGa' → compatible_g PGa.
Proof. intros; rewrite -preimage_val_g_eq; apply cg_preimage; easy. Qed.
Lemma RgS_val_cg_equiv : compatible_g PGa' ↔ compatible_g PGa.
Proof. split; [apply RgS_val_cg_rev | apply RgS_val_cg]. Qed.
End Sub_Group_Facts2.
Section Sub_Group_Morphism_Facts1.
Context {G1 G2 : AbelianGroup}.
Context {PG1 : G1 → Prop}.
Context {PG2 : G2 → Prop}.
Context {HPG1 : compatible_g PG1}.
Context {HPG2 : compatible_g PG2}.
Let PG1_g := sub_AbelianGroup HPG1.
Let PG2_g := sub_AbelianGroup HPG2.
Context {f : G1 → G2}.
Context {fS : PG1_g → PG2_g}.
Hypothesis HfS : ∀ x, val (fS x) = f (val x).
Lemma sub_g_f_opp_compat : f_opp_compat f → f_opp_compat fS.
Proof. intros Hf x1; apply val_inj; rewrite HfS Hf -HfS; easy. Qed.
Lemma sub_g_f_minus_compat : f_minus_compat f → f_minus_compat fS.
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⇒ /mg_mm; apply Ker_sub_zero_equiv, HfS. Qed.
Lemma KerS_g_zero_equiv_alt :
morphism_g f →
KerS PG1 f = zero_sub_struct ↔
∀ (x1 : sub_AbelianGroup 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 (cg_zero HPG1)).
rewrite mk_sub_g_zero; apply Hf1; easy.
move⇒ x1 ->; apply cg_zero, KerS_cg; easy.
Qed.
Lemma Ker_sub_g_zero_equiv :
morphism_g f →
Ker fS = zero_sub_struct ↔
∀ (x1 : sub_AbelianGroup 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 (Ker_sub_KerS_equiv HfS) Hf1; apply val_zero_equiv.
destruct (classic (PG1 x1)) as [Hx1 | Hx1a].
rewrite (KerS_Ker_sub_equiv HfS Hx1) Hf1; apply mk_sub_zero_equiv.
split; intros Hx1b; contradict Hx1a;
[apply Hx1b | rewrite Hx1b; apply cg_zero, HPG1].
Qed.
Lemma gmS_injS_val_equiv :
morphism_g f →
injS PG1 f ↔ ∀ (x1 : sub_AbelianGroup 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_val_equiv :
morphism_g f →
bijS PG1 (RgS PG1 f) f ↔
∀ (x1 : sub_AbelianGroup HPG1), f (val x1) = 0 → x1 = 0.
Proof. rewrite gmS_bijS_injS_equiv; apply gmS_injS_val_equiv. Qed.
End Sub_Group_Morphism_Facts1.
Section Sub_Group_Morphism_Facts2.
Context {G1 G2 : AbelianGroup}.
Context {PG1 : G1 → Prop}.
Context {PG2 : G2 → Prop}.
Hypothesis HPG1 : compatible_g PG1.
Hypothesis HPG2 : compatible_g PG2.
Let PG1_g := sub_AbelianGroup HPG1.
Let PG2_g := sub_AbelianGroup HPG2.
Context {f : G1 → G2}.
Hypothesis Hf : funS PG1 PG2 f.
Definition fct_sub_g : PG1_g → PG2_g := fct_sub Hf.
Lemma fct_sub_g_inj : injS PG1 f → injective fct_sub_g.
Proof. apply fct_sub_inj. Qed.
Lemma fct_sub_g_inj_rev : injective fct_sub_g → injS PG1 f.
Proof. apply fct_sub_inj_rev. Qed.
Lemma fct_sub_g_inj_equiv : injective fct_sub_g ↔ injS PG1 f.
Proof. apply fct_sub_inj_equiv. Qed.
Lemma fct_sub_g_surj : surjS PG1 PG2 f → surjective fct_sub_g.
Proof. apply fct_sub_surj. Qed.
Lemma fct_sub_g_surj_rev : surjective fct_sub_g → surjS PG1 PG2 f.
Proof. apply fct_sub_surj_rev. Qed.
Lemma fct_sub_g_surj_equiv : surjective fct_sub_g ↔ surjS PG1 PG2 f.
Proof. apply fct_sub_surj_equiv. Qed.
Lemma fct_sub_g_bij : bijS PG1 PG2 f → bijective fct_sub_g.
Proof. apply fct_sub_bij, inhabited_g. Qed.
Lemma fct_sub_g_bij_rev : bijective fct_sub_g → bijS PG1 PG2 f.
Proof. apply fct_sub_bij_rev, inhabited_g. Qed.
Lemma fct_sub_g_bij_equiv : bijective fct_sub_g ↔ bijS PG1 PG2 f.
Proof. apply fct_sub_bij_equiv, inhabited_g. Qed.
Lemma fct_sub_g_f_opp_compat : f_opp_compat f → f_opp_compat fct_sub_g.
Proof. apply sub_g_f_opp_compat, fct_sub_correct. Qed.
Lemma fct_sub_g_f_minus_compat : f_minus_compat f → f_minus_compat fct_sub_g.
Proof. apply sub_g_f_minus_compat, fct_sub_correct. Qed.
Lemma fct_sub_g_mg : morphism_g f → morphism_g fct_sub_g.
Proof. apply sub_g_morphism, fct_sub_correct. Qed.
Lemma fct_sub_g_f_inv_mg :
∀ (Hfb : bijS PG1 PG2 f),
morphism_g f → morphism_g (f_inv (fct_sub_g_bij Hfb)).
Proof. intros; apply mg_bij_compat, fct_sub_g_mg; easy. 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 ↔
∀ (x1 : sub_AbelianGroup 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_Facts2.
Section Compose_n_Group_Facts.
Context {E : AbelianGroup}.
Context {PE : E → Prop}.
Context {n : nat}.
Variable f : '(E → E)^n.
Hypothesis Hf : ∀ i, funS PE PE (f i).
Lemma comp_n_mg_sub : (∀ i, mg_sub PE (f i)) → mg_sub PE (comp_n f).
Proof.
intros Hf1; induction n as [| n1 Hn1];
[rewrite comp_n_nil; easy | rewrite comp_n_ind_l].
apply (mg_comp_sub PE);
[apply comp_n_funS | apply Hn1 |]; unfold liftF_S; easy.
Qed.
End Compose_n_Group_Facts.
Section Compose_n_part_Group_Facts.
Context {E : AbelianGroup}.
Context {PE : E → Prop}.
Context {n : nat}.
Variable f : '(E → E)^n.
Variable j : 'I_n.+1.
Hypothesis Hf : ∀ i, funS PE PE (widenF (leq_ord j) f i).
Lemma comp_n_part_mg_sub :
(∀ i, mg_sub PE (widenF (leq_ord j) f i)) →
mg_sub PE (comp_n_part f j).
Proof.
intros Hf1; induction n as [| n1 Hn1]; [rewrite comp_n_part_nil; easy |].
destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
[rewrite (comp_n_part_0 _ _ Hj0); easy |].
rewrite comp_n_part_ind_l; apply (mg_comp_sub PE).
apply comp_n_part_funS; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply Hn1; intros; apply (widenF_liftF_S_P_compat _ Hj0); easy.
apply (widenF_0_P_compat Hj0 Hf1).
Qed.
End Compose_n_part_Group_Facts.