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.
Support for morphisms on commutative groups.
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".
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
- f_opp_compat f states that f transports the opposite law opp;
- f_minus_compat f states that f transports the minus law minus;
- morphism_g f states that f transports the group structure.
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 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^n ⇒ B1 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 → G3 ⇒ g \o f).
Proof. easy. Qed.
Lemma mg_comp_r :
∀ {g : G2 → G3},
morphism_g g → morphism_g (fun f : G1 → G2 ⇒ g \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.