Library Algebra.Ring.Ring_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 rings.
Results needing a commutative Ring are only stated for the ring of
real numbers R_Ring.
Let K1 K2 : Ring.
Let f : K1 → K2.
Lemmas about predicate morphism_r have "mr" in their names, usually as
prefix "mr_", sometimes as suffix "_mr".
This module may be used through the import of Algebra.Ring.Ring,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
- f_mult_compat f states that f transports the multiplicative law mult;
- f_one_compat f states that f transports the multiplicative identity element one;
- morphism_r f states that f transports the ring structure.
Usage
From Requisite Require Import ssr.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Section Ring_Morphism_Def.
Context {K1 K2 : Ring}.
Definition f_mult_compat (f : K1 → K2) : Prop :=
∀ x1 y1, f (x1 × y1) = f x1 × f y1.
Definition f_one_compat (f : K1 → K2) : Prop := f 1 = 1.
Definition morphism_r f : Prop :=
f_plus_compat f ∧ f_mult_compat f ∧ f_one_compat f.
End Ring_Morphism_Def.
Section Ring_Morphism_Facts1a.
Context {K1 K2 : Ring}.
Lemma mr_mg : ∀ {f : K1 → K2}, morphism_r f → morphism_g f.
Proof. move=>> H; apply H. Qed.
Lemma mr_mult : ∀ {f : K1 → K2}, morphism_r f → f_mult_compat f.
Proof. move=>> H; apply H. Qed.
Lemma mr_one : ∀ {f : K1 → K2}, morphism_r f → f_one_compat f.
Proof. move=>> H; apply H. Qed.
Lemma mr_m : ∀ {f : K1 → K2}, morphism_r f → morphism_m f.
Proof. move=>> /mr_mg; apply: mg_mm. Qed.
Lemma mr_plus : ∀ {f : K1 → K2}, morphism_r f → f_plus_compat f.
Proof. move=>> /mr_mg; apply: mg_plus. Qed.
Lemma mr_zero : ∀ {f : K1 → K2}, morphism_r f → f_zero_compat f.
Proof. move=>> /mr_mg; apply: mg_zero. Qed.
Lemma mr_sum : ∀ {f : K1 → K2}, morphism_r f → f_sum_compat f.
Proof. move=>> /mr_mg; apply: mg_sum. Qed.
Lemma mr_opp : ∀ {f : K1 → K2}, morphism_r f → f_opp_compat f.
Proof. move=>> /mr_mg; apply mg_opp. Qed.
Lemma mr_minus : ∀ {f : K1 → K2}, morphism_r f → f_minus_compat f.
Proof. move=>> /mr_mg; apply mg_minus. Qed.
Lemma mr_ext :
∀ f g : K1 → K2, same_fun f g → morphism_r f → morphism_r g.
Proof. move=>> /fun_ext H; subst; easy. Qed.
End Ring_Morphism_Facts1a.
Section Ring_Morphism_Facts1b.
Context {K1 K2 K3 : Ring}.
Lemma mr_pt_eval : ∀ (u : K1), morphism_r (pt_eval K2 u).
Proof. easy. Qed.
Lemma mr_component : ∀ {n} i, morphism_r (fun B1 : 'K1^n ⇒ B1 i).
Proof. easy. Qed.
Lemma f_mult_compat_mapF :
∀ {n} {f : K1 → K2},
f_mult_compat f → f_mult_compat (mapF f : 'K1^n → 'K2^n).
Proof. move=>> Hf x1 y1; apply extF; intro; rewrite mapF_correct Hf; easy. Qed.
Lemma f_one_compat_mapF :
∀ {n} {f : K1 → K2},
f_one_compat f → f_one_compat (mapF f : 'K1^n → 'K2^n).
Proof. move=>> Hf; apply extF; intro; rewrite mapF_correct Hf; easy. Qed.
Lemma mr_mapF :
∀ {n} {f : K1 → K2},
morphism_r f → morphism_r (mapF f : 'K1^n → 'K2^n).
Proof.
move=>> [Hf1 [Hf2 Hf3]]; repeat split; [apply mg_mapF |
apply f_mult_compat_mapF | apply f_one_compat_mapF]; easy.
Qed.
Lemma mr_map2F :
∀ {n} {f : K1 → K2 → K3} (u1 : 'K1^n),
(∀ i1, morphism_r (f (u1 i1))) → morphism_r (map2F f u1).
Proof.
move=>> Hf; repeat split.
apply mg_map2F; intros; apply mr_mg; easy.
intros x1 y1; apply extF; intros i1; destruct (Hf i1) as [_ [Hf2 _]].
rewrite map2F_correct Hf2; easy.
apply extF; intros i1; destruct (Hf i1) as [_ [_ Hf3]].
rewrite map2F_correct Hf3; easy.
Qed.
End Ring_Morphism_Facts1b.
Section Ring_Morphism_Facts2.
Context {K1 K2 K3 : Ring}.
Lemma f_mult_compat_comp :
∀ {f : K1 → K2} {g : K2 → K3},
f_mult_compat f → f_mult_compat g → f_mult_compat (g \o f).
Proof. intros f g Hf Hg x1 y1; rewrite !comp_correct Hf; easy. Qed.
Lemma f_one_compat_comp :
∀ {f : K1 → K2} {g : K2 → K3},
f_one_compat f → f_one_compat g → f_one_compat (g \o f).
Proof.
intros f g; unfold f_one_compat; rewrite comp_correct; move⇒ ->; easy.
Qed.
Lemma mr_comp :
∀ {f : K1 → K2} {g : K2 → K3},
morphism_r f → morphism_r g → morphism_r (g \o f).
Proof.
intros f g [Hfa [Hfb Hfc]] [Hga [Hgb Hgc]]; repeat split;
[apply f_plus_compat_comp | apply f_mult_compat_comp |
apply f_one_compat_comp]; easy.
Qed.
Lemma f_mult_compat_comp_l :
∀ (f : K1 → K2), f_mult_compat (fun g : K2 → K3 ⇒ g \o f).
Proof. easy. Qed.
Lemma f_one_compat_comp_l :
∀ (f : K1 → K2), f_one_compat (fun g : K2 → K3 ⇒ g \o f).
Proof. easy. Qed.
Lemma mr_comp_l :
∀ (f : K1 → K2), morphism_r (fun g : K2 → K3 ⇒ g \o f).
Proof. easy. Qed.
Lemma f_mult_compat_comp_r :
∀ {g : K2 → K3},
f_mult_compat g → f_mult_compat (fun f : K1 → K2 ⇒ g \o f).
Proof.
intros g Hg; move=>>; apply fun_ext; intro;
rewrite comp_correct fct_mult_eq Hg; easy.
Qed.
Lemma f_one_compat_comp_r :
∀ {g : K2 → K3},
f_one_compat g → f_one_compat (fun f : K1 → K2 ⇒ g \o f).
Proof. intros g Hg; apply fun_ext; easy. Qed.
Lemma mr_comp_r :
∀ {g : K2 → K3},
morphism_r g → morphism_r (fun f : K1 → K2 ⇒ g \o f).
Proof.
intros g [Hga [Hgb Hgc]]; repeat split; [apply mg_comp_r |
apply f_mult_compat_comp_r | apply f_one_compat_comp_r]; easy.
Qed.
Lemma mr_bij_compat :
∀ {f : K1 → K2} (Hf : bijective f),
morphism_r f → morphism_r (f_inv Hf).
Proof.
intros f Hf1 [Hf2 [Hf3 Hf4]]; repeat split; move=>>;
apply (bij_inj Hf1); [rewrite Hf2 | rewrite Hf3 | rewrite Hf4];
rewrite !f_inv_can_r; easy.
Qed.
End Ring_Morphism_Facts2.