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.
Support for morphisms on commutative monoids.
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".
This module may be used through the import of Algebra.Monoid.Monoid,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- f_plus_compat f states that f transports the monoid law plus;
- f_zero_compat f states that f transports the identity element zero;
- morphism_m f states that f transports the monoid structure.
Usage
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^n ⇒ B1 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 → G3 ⇒ g \o f).
Proof. easy. Qed.
Lemma f_zero_compat_comp_l :
∀ (f : G1 → G2), f_zero_compat (fun g : G2 → G3 ⇒ g \o f).
Proof. easy. Qed.
Lemma mm_comp_l :
∀ (f : G1 → G2), morphism_m (fun g : G2 → G3 ⇒ g \o f).
Proof. easy. Qed.
Lemma f_plus_compat_comp_r :
∀ {g : G2 → G3},
f_plus_compat g → f_plus_compat (fun f : G1 → G2 ⇒ g \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 → G2 ⇒ g \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 → G2 ⇒ g \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^n ⇒ sum 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.