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.

Brief description

Support for subgroups.

Description

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.

Additional support for group morphism

Let G1 G2 : AbelianGroup. Let PG1 : G1 Prop. Let f : G1 G2.

Additional support for subgroup

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.

Bibliography

[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.

Used logic axioms

  • classic, the weak form of excluded middle.

Usage

This module mat be used through the import of Algebra.Group.Group, Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

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.

[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.

[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.

[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.
movex1 ->; 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.