Library Algebra.Group.Group_morphism

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 morphisms on commutative groups.

Description

Let G1 G2 : AbelianGroup. Let f : G1 G2.
Lemmas about predicate morphism_g have "mg" in their names, usually as prefix "mg_", sometimes as suffix "_mg".

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 Monoid Group_compl.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.

Section Group_Morphism_Def.

Context {G1 G2 : AbelianGroup}.

Definition morphism_g (f : G1 G2) : Prop := f_plus_compat f.

Definition f_opp_compat (f : G1 G2) : Prop := x1, f (- x1) = - f x1.

Definition f_minus_compat (f : G1 G2) : Prop :=
   x1 y1, f (x1 - y1) = f x1 - f y1.

End Group_Morphism_Def.

Section Group_Morphism_Facts1a.

Context {G1 G2 : AbelianGroup}.

Lemma f_zero_minus_opp_compat :
   {f : G1 G2}, f_zero_compat f f_minus_compat f f_opp_compat f.
Proof.
intros f Hf0 Hf1 x1; rewrite -(plus_zero_l (- x1)) Hf1 Hf0 minus_zero_l; easy.
Qed.

Lemma f_opp_minus_plus_compat :
   {f : G1 G2}, f_opp_compat f f_minus_compat f f_plus_compat f.
Proof. intros f Hf1 Hf2 x1 y1; rewrite -(opp_opp y1) Hf1 Hf2; easy. Qed.

Lemma f_plus_opp_minus_compat :
   {f : G1 G2}, f_plus_compat f f_opp_compat f f_minus_compat f.
Proof. intros f Hf1 Hf2 x1 y1; rewrite minus_eq Hf1 Hf2; easy. Qed.

Lemma mg_plus : {f : G1 G2}, morphism_g f f_plus_compat f.
Proof. easy. Qed.

Lemma mg_zero : {f : G1 G2}, morphism_g f f_zero_compat f.
Proof.
intros f Hf; apply (plus_reg_l (f 0)); rewrite -Hf 2!plus_zero_r; easy.
Qed.

Lemma mg_mm : {f : G1 G2}, morphism_g f morphism_m f.
Proof. intros; split; try apply mg_zero; easy. Qed.

Lemma mg_mm_equiv : {f : G1 G2}, morphism_g f morphism_m f.
Proof. intros; split. apply mg_mm. intros [Hf _]; easy. Qed.

Lemma mg_sum : {f : G1 G2}, morphism_g f f_sum_compat f.
Proof. intros; apply mm_sum, mg_mm; easy. Qed.

Lemma mg_opp : {f : G1 G2}, morphism_g f f_opp_compat f.
Proof.
intros f Hf x1; apply (plus_reg_l (f x1)); rewrite -Hf 2!plus_opp_r.
apply mg_zero; easy.
Qed.

Lemma mg_minus : {f : G1 G2}, morphism_g f f_minus_compat f.
Proof. move=>> Hf x1 y1; rewrite Hf mg_opp; easy. Qed.

Lemma mg_fct_plus :
   {f g : G1 G2}, morphism_g f morphism_g g morphism_g (f + g).
Proof. move=>>; rewrite !mg_mm_equiv; apply mm_fct_plus. Qed.

Lemma mg_fct_zero : morphism_g (0 : G1 G2).
Proof. rewrite mg_mm_equiv; apply mm_fct_zero. Qed.

Lemma mg_fct_sum :
   {n} {f : '(G1 G2)^n},
    ( i, morphism_g (f i)) morphism_g (sum f).
Proof.
intros; rewrite mg_mm_equiv; apply mm_fct_sum.
intros; apply mg_mm; easy.
Qed.

Lemma mg_fct_opp : {f : G1 G2}, morphism_g f morphism_g (- f).
Proof. move=>> H; intros x1 y1; rewrite 3!fct_opp_eq H; apply opp_plus. Qed.

Lemma mg_fct_minus :
   {f g : G1 G2}, morphism_g f morphism_g g morphism_g (f - g).
Proof. intros; rewrite minus_eq; apply mg_fct_plus, mg_fct_opp; easy. Qed.

Lemma mg_ext :
   f g : G1 G2, ( x, f x = g x) morphism_g f morphism_g g.
Proof. move=>> /fun_ext H; subst; easy. Qed.

End Group_Morphism_Facts1a.

Section Group_Morphism_Facts1b.

Context {G1 G2 G3 : AbelianGroup}.

Lemma mg_pt_eval : (u : G1), morphism_g (pt_eval G2 u).
Proof. easy. Qed.

Lemma mg_component : {n} i, morphism_g (fun B1 : 'G1^nB1 i).
Proof. easy. Qed.

Lemma f_opp_compat_mapF :
   {n} {f : G1 G2},
    f_opp_compat f f_opp_compat (mapF f : 'G1^n 'G2^n).
Proof. move=>> Hf x1; apply extF; intro; rewrite mapF_correct Hf; easy. Qed.

Lemma f_minus_compat_mapF :
   {n} {f : G1 G2},
    f_minus_compat f f_minus_compat (mapF f : 'G1^n 'G2^n).
Proof. move=>> Hf x1 y1; apply extF; intro; rewrite mapF_correct Hf; easy. Qed.

Lemma mg_mapF :
   {n} {f : G1 G2},
    morphism_g f morphism_g (mapF f : 'G1^n 'G2^n).
Proof. move=>>; rewrite !mg_mm_equiv; apply mm_mapF. Qed.

Lemma mg_map2F :
   {n} {f : G1 G2 G3} (u1 : 'G1^n),
    ( i1, morphism_g (f (u1 i1))) morphism_g (map2F f u1).
Proof.
move=>> Hf; apply mg_mm.
apply mm_map2F; intros; apply mg_mm; easy.
Qed.

End Group_Morphism_Facts1b.

Section Group_Morphism_Facts2.

Context {G1 G2 G3 : AbelianGroup}.

Lemma mg_comp :
   {f : G1 G2} {g : G2 G3},
    morphism_g f morphism_g g morphism_g (g \o f).
Proof. move=>>; apply f_plus_compat_comp. Qed.

Lemma mg_comp_l :
   (f : G1 G2), morphism_g (fun g : G2 G3g \o f).
Proof. easy. Qed.

Lemma mg_comp_r :
   {g : G2 G3},
    morphism_g g morphism_g (fun f : G1 G2g \o f).
Proof. move=>>; apply f_plus_compat_comp_r. Qed.

Lemma mg_bij_compat :
   {f : G1 G2} (Hf : bijective f),
    morphism_g f morphism_g (f_inv Hf).
Proof.
intros f Hf1 Hf2; move=>>; apply (bij_inj Hf1); rewrite Hf2 !f_inv_can_r; easy.
Qed.

End Group_Morphism_Facts2.

Section Compose_n_Group_Facts.

Context {E : AbelianGroup}.

Lemma comp_n_mg :
   {n} (f : '(E E)^n),
    ( i, morphism_g (f i)) morphism_g (comp_n f).
Proof. move=>>; apply comp_n_f_plus_compat. Qed.

End Compose_n_Group_Facts.

Section Compose_n_part_Group_Facts.

Context {E : AbelianGroup}.

Lemma comp_n_part_mg :
   {n} (f : '(E E)^n) j,
    ( i, morphism_g (widenF (leq_ord j) f i))
    morphism_g (comp_n_part f j).
Proof. move=>>; apply comp_n_part_f_plus_compat. Qed.

End Compose_n_part_Group_Facts.