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.

Brief description

Support for morphisms on rings.

Description

Results needing a commutative Ring are only stated for the ring of real numbers R_Ring.
Let K1 K2 : Ring. Let f : K1 K2.
  • 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.
Lemmas about predicate morphism_r have "mr" in their names, usually as prefix "mr_", sometimes as suffix "_mr".

Usage

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

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^nB1 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 K3g \o f).
Proof. easy. Qed.

Lemma f_one_compat_comp_l :
   (f : K1 K2), f_one_compat (fun g : K2 K3g \o f).
Proof. easy. Qed.

Lemma mr_comp_l :
   (f : K1 K2), morphism_r (fun g : K2 K3g \o f).
Proof. easy. Qed.

Lemma f_mult_compat_comp_r :
   {g : K2 K3},
    f_mult_compat g f_mult_compat (fun f : K1 K2g \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 K2g \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 K2g \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.