Library Algebra.Monoid.Monoid_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 monoids.

Description

Let G1 G2 : AbelianMonoid. Let f : G1 G2.
Lemmas about predicate morphism_m have "mm" in their names, usually as prefix "mm_", sometimes as suffix "_mm".

Usage

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

From Requisite Require Import stdlib_wR ssr_wMC.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid_sum.

Local Open Scope Monoid_scope.

Section Monoid_Morphism_Def.

Context {G1 G2 : AbelianMonoid}.

Definition f_plus_compat (f : G1 G2) : Prop :=
   x1 y1, f (x1 + y1) = f x1 + f y1.

Definition f_zero_compat (f : G1 G2) : Prop := f 0 = 0.

Definition f_sum_compat (f : G1 G2) : Prop :=
   n (u1 : 'G1^n), f (sum u1) = sum (mapF f u1).

Definition morphism_m f : Prop := f_plus_compat f f_zero_compat f.

End Monoid_Morphism_Def.

Section Monoid_Morphism_Facts1a.

Context {G1 G2 : AbelianMonoid}.

Lemma mm_plus : {f : G1 G2}, morphism_m f f_plus_compat f.
Proof. move=>> H; apply H. Qed.

Lemma mm_zero : {f : G1 G2}, morphism_m f f_zero_compat f.
Proof. move=>> H; apply H. Qed.

Lemma mm_fct_plus :
   {f g : G1 G2}, morphism_m f morphism_m g morphism_m (f + g).
Proof.
move=>> [Hfa Hfb] [Hga Hgb]; split.
intros x1 y1; rewrite 3!fct_plus_eq Hfa Hga 2!plus_assoc; f_equal;
    rewrite -2!plus_assoc; f_equal; apply plus_comm.
unfold f_zero_compat; rewrite fct_plus_eq Hfb Hgb plus_zero_r; easy.
Qed.

Lemma mm_fct_zero : morphism_m (0 : G1 G2).
Proof.
split; try easy; intros x1 y1; rewrite 2!fct_zero_eq plus_zero_l; easy.
Qed.

Lemma mm_ext :
   (f g : G1 G2), same_fun f g morphism_m f morphism_m g.
Proof. move=>> /fun_ext H; subst; easy. Qed.

End Monoid_Morphism_Facts1a.

Section Monoid_Morphism_Facts1b.

Context {G1 G2 G3 : AbelianMonoid}.

Lemma mm_pt_eval : (u : G1), morphism_m (pt_eval G2 u).
Proof. easy. Qed.

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

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

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

Lemma mm_mapF :
   {n} {f : G1 G2},
    morphism_m f morphism_m (mapF f : 'G1^n 'G2^n).
Proof.
move=>> [Hf1 Hf2]; split;
    [apply f_plus_compat_mapF | apply f_zero_compat_mapF]; easy.
Qed.

Lemma mm_map2F :
   {n} {f : G1 G2 G3} (u1 : 'G1^n),
    ( i1, morphism_m (f (u1 i1))) morphism_m (map2F f u1).
Proof.
move=>> Hf; split.
intros x1 y1; apply extF; intros i1; destruct (Hf i1) as [Hf1 _].
rewrite map2F_correct Hf1; easy.
apply extF; intros i1; destruct (Hf i1) as [_ Hf2].
rewrite map2F_correct Hf2; easy.
Qed.

End Monoid_Morphism_Facts1b.

Section Monoid_Morphism_Facts2.

Context {G1 G2 G3 : AbelianMonoid}.

Lemma f_plus_compat_comp :
   {f : G1 G2} {g : G2 G3},
    f_plus_compat f f_plus_compat g f_plus_compat (g \o f).
Proof. intros f g Hf Hg x1 y1; rewrite !comp_correct Hf; easy. Qed.

Lemma f_zero_compat_comp :
   {f : G1 G2} {g : G2 G3},
    f_zero_compat f f_zero_compat g f_zero_compat (g \o f).
Proof.
intros f g; unfold f_zero_compat; rewrite comp_correct; move⇒ ->; easy.
Qed.

Lemma mm_comp :
   {f : G1 G2} {g : G2 G3},
    morphism_m f morphism_m g morphism_m (g \o f).
Proof.
intros f g [Hfa Hfb] [Hga Hgb]; split;
    [apply f_plus_compat_comp | apply f_zero_compat_comp]; easy.
Qed.

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

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

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

Lemma f_plus_compat_comp_r :
   {g : G2 G3},
    f_plus_compat g f_plus_compat (fun f : G1 G2g \o f).
Proof.
intros g Hg; move=>>; apply fun_ext; intro;
    rewrite comp_correct fct_plus_eq Hg; easy.
Qed.

Lemma f_zero_compat_comp_r :
   {g : G2 G3},
    f_zero_compat g f_zero_compat (fun f : G1 G2g \o f).
Proof. intros g Hg; apply fun_ext; easy. Qed.

Lemma mm_comp_r :
   {g : G2 G3},
    morphism_m g morphism_m (fun f : G1 G2g \o f).
Proof.
intros g [Hga Hgb]; split;
    [apply f_plus_compat_comp_r | apply f_zero_compat_comp_r]; easy.
Qed.

Lemma mm_bij_compat :
   {f : G1 G2} (Hf : bijective f),
    morphism_m f morphism_m (f_inv Hf).
Proof.
intros f Hf1 [Hf2 Hf3]; split; move=>>;
    apply (bij_inj Hf1); [rewrite Hf2 | rewrite Hf3];
    rewrite !f_inv_can_r; easy.
Qed.

End Monoid_Morphism_Facts2.

Section Monoid_Morphism_Sum_Facts1.

Context {G1 G2 : AbelianMonoid}.

Lemma sum_mapF :
   {n} {f : G1 G2} (u1 : 'G1^n),
    morphism_m f sum (mapF f u1) = f (sum u1).
Proof.
intros n f u1 [Hf1 Hf2]; induction n as [| n Hn].
rewrite !sum_nil Hf2; easy.
rewrite !sum_ind_l liftF_S_mapF Hn Hf1; easy.
Qed.

Lemma sum_mm : {f : G1 G2}, f_sum_compat f morphism_m f.
Proof.
intros f Hf; split.
move=>>; rewrite -!sum_coupleF -mapF_coupleF; auto.
unfold f_zero_compat; rewrite -(sum_nil (fun _ ⇒ 0)) Hf mapF_constF sum_nil//.
Qed.

Lemma mm_sum : {f : G1 G2}, morphism_m f f_sum_compat f.
Proof.
move=>> [Hfa Hfb] n; induction n as [| n Hn]; intros.
rewrite 2!sum_nil; easy.
rewrite 2!sum_ind_l Hfa Hn; easy.
Qed.

Lemma mm_sum_equiv : (f : G1 G2), morphism_m f f_sum_compat f.
Proof. intros; split; [apply mm_sum | apply sum_mm]. Qed.

Lemma mm_fct_sum :
   {n} {f : '(G1 G2)^n},
    ( i, morphism_m (f i)) morphism_m (sum f).
Proof.
intros n f Hf; induction n as [| n Hn].
rewrite sum_nil; apply mm_fct_zero.
rewrite sum_ind_l; apply mm_fct_plus; auto.
apply Hn; intros i; apply Hf.
Qed.

Lemma sum_fun_sum :
   {n p} {f : '(G1 G2)^n} (u : 'G1^p),
    ( i, morphism_m (f i)) sum f (sum u) = sum (mapF (sum f) u).
Proof. intros; rewrite mm_sum; [| apply mm_fct_sum]; easy. Qed.

End Monoid_Morphism_Sum_Facts1.

Section Monoid_Morphism_Sum_Facts2.

Context {G : AbelianMonoid}.

Lemma mm_component_sum : {n}, morphism_m (fun u : 'G^nsum u).
Proof.
intros; eapply mm_ext.
2: eapply mm_fct_sum, mm_component.
move=>>; rewrite sum_fun_compat; easy.
Qed.

End Monoid_Morphism_Sum_Facts2.

Section Monoid_Morphism_Sum_Facts3.

Context {G1 G2 : AbelianMonoid}.
Context {T : Type}.

Lemma sum_compF_r:
   {n} (u : G1 G2) (f : '(T G1)^n),
    morphism_m u sum (compF_r u f) = u \o sum f.
Proof.
intros; apply fun_ext; intro;
    rewrite comp_correct (fct_sum_eq f) -sum_mapF// fct_sum_eq; easy.
Qed.

End Monoid_Morphism_Sum_Facts3.

Section Monoid_Morphism_R_Facts.

Lemma INR_mm : morphism_m INR.
Proof. split; [intro; apply plus_INR | easy]. Qed.

Lemma sum_INR : {n} (x : 'nat^n), sum (mapF INR x) = INR (sum x).
Proof. intros; apply sum_mapF, INR_mm. Qed.

End Monoid_Morphism_R_Facts.