Library Algebra.Ring.Ring_sub
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 subrings.
Let K : Ring.
Let PK : K → Prop.
Lemmas about predicate compatible_r have "cr" in their names, usually as
prefix "cr_", sometimes as suffix "_cr".
Let gen : K → Prop.
Let K : Ring.
Let PK : K → Prop.
Let HPK : compatible_r PK.
Let K1 K2 : Ring.
Let PK1 : K1 → Prop and PK2 : K2 → Prop.
Let HPK1 : compatible_r PK1 and HPK2 : compatible_r PK2.
Let f : K1 → K2.
Let Hf : funS PK1 PK2 f.
Bernard Gostiaux,
Cours de mathématiques spéciales - 1. Algèbre,
Mathématiques, Presses Universitaires de France, Paris, 1993,
https://www.puf.com/cours-de-mathematiques-speciales-tome-1-algebre.
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
- mult_closed PK states that PK is closed under the multiplicative law mult;
- one_closed PK states that PK contains the multiplicative identity element one;
- compatible_r PK states that PK is closed under the ring laws plus and mult and contains identity elements zero and one, ie is compatible with the Ring structure.
- span_r gen is the specialization span compatible_r gen (see Algebra.Sub_struct), ie it is the intersection of all subsets (= the smallest) compatible with the Ring structure that also contain gen.
Additional support for subring
- fct_sub_r HPK1 HPK2 Hf is the function fct_sub Hf with type sub_Ring HPK1 → sub_Ring HPK2 (see Subsets.Sub_type).
Bibliography
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 Sub_struct.
From Algebra Require Import Monoid Group Ring_compl Ring_morphism.
Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.
Section Compatible_Ring_Def.
Context {K : Ring}.
Definition mult_closed (PK : K → Prop) : Prop :=
∀ x y, PK x → PK y → PK (x × y).
Definition one_closed (PK : K → Prop) : Prop := PK one.
Definition compatible_r (PK : K → Prop) : Prop:=
compatible_g PK ∧ mult_closed PK ∧ one_closed PK.
End Compatible_Ring_Def.
Section Compatible_Ring_Facts.
Context {K : Ring}.
Lemma cr_cg : ∀ {PK : K → Prop}, compatible_r PK → compatible_g PK.
Proof. move=>> H; apply H. Qed.
Lemma cr_cm : ∀ {PK : K → Prop}, compatible_r PK → compatible_m PK.
Proof. move=>> /cr_cg; apply: cg_cm. Qed.
Lemma cr_nonempty : ∀ {PK : K → Prop}, compatible_r PK → nonempty PK.
Proof. move=>> /cr_cg; apply cg_nonempty. Qed.
Lemma cr_zero : ∀ {PK : K → Prop}, compatible_r PK → zero_closed PK.
Proof. move=>> /cr_cg; apply: cg_zero. Qed.
Lemma cr_plus : ∀ {PK : K → Prop}, compatible_r PK → plus_closed PK.
Proof. move=>> /cr_cg; apply: cg_plus. Qed.
Lemma cr_sum : ∀ {PK : K → Prop}, compatible_r PK → sum_closed PK.
Proof.
intros; apply plus_zero_sum_closed; [apply cr_plus | apply cr_zero]; easy.
Qed.
Lemma cr_opp : ∀ {PK : K → Prop}, compatible_r PK → opp_closed PK.
Proof. move=>> /cr_cg; apply cg_opp. Qed.
Lemma cr_minus : ∀ {PK : K → Prop}, compatible_r PK → minus_closed PK.
Proof. move=>> /cr_cg; apply cg_minus. Qed.
Lemma cr_one : ∀ {PK : K → Prop}, compatible_r PK → one_closed PK.
Proof. move=>> H; apply H. Qed.
Lemma cr_mult : ∀ {PK : K → Prop}, compatible_r PK → mult_closed PK.
Proof. move=>> H; apply H. Qed.
Lemma cr_full : ∀ {PK : K → Prop}, full PK → compatible_r PK.
Proof.
intros; split; [apply cg_full; easy |]; split; [| unfold one_closed]; easy.
Qed.
Lemma cr_fullset : compatible_r (@fullset K).
Proof. apply cr_full; easy. Qed.
Lemma mult_closed_inter :
∀ {PK QK : K → Prop},
mult_closed PK → mult_closed QK → mult_closed (inter PK QK).
Proof.
move=>> HPK HQK x y [HxP HxQ] [HyP HyQ]; split; [apply HPK | apply HQK]; easy.
Qed.
Lemma one_closed_inter :
∀ {PK QK : K → Prop},
one_closed PK → one_closed QK → one_closed (inter PK QK).
Proof. easy. Qed.
Lemma cr_inter :
∀ {PK QK : K → Prop},
compatible_r PK → compatible_r QK → compatible_r (inter PK QK).
Proof.
move=>> HPK HQK; split; [apply cg_inter; apply cr_cg; easy | split].
apply mult_closed_inter; [apply HPK | apply HQK].
apply one_closed_inter; [apply HPK | apply HQK].
Qed.
[GostiauxT1]
Th 5.12, p. 133.
Lemma mult_closed_inter_any :
∀ {Idx : Type} {PK : Idx → K → Prop},
(∀ i, mult_closed (PK i)) → mult_closed (inter_any PK).
Proof. move=>> HPK; move=>> Hx Hy i; apply HPK; easy. Qed.
∀ {Idx : Type} {PK : Idx → K → Prop},
(∀ i, mult_closed (PK i)) → mult_closed (inter_any PK).
Proof. move=>> HPK; move=>> Hx Hy i; apply HPK; easy. Qed.
[GostiauxT1]
Th 5.12, p. 133.
Lemma one_closed_inter_any :
∀ {Idx : Type} {PK : Idx → K → Prop},
(∀ i, one_closed (PK i)) → one_closed (inter_any PK).
Proof. move=>> HPK i; apply HPK. Qed.
∀ {Idx : Type} {PK : Idx → K → Prop},
(∀ i, one_closed (PK i)) → one_closed (inter_any PK).
Proof. move=>> HPK i; apply HPK. Qed.
[GostiauxT1]
Th 5.12, p. 133.
Lemma cr_inter_any :
∀ {Idx : Type} {PK : Idx → K → Prop},
(∀ i, compatible_r (PK i)) → compatible_r (inter_any PK).
Proof.
move=>> HPK; split; [ | split].
apply cg_inter_any; intro; apply cr_cg; easy.
apply mult_closed_inter_any; intro; apply HPK.
apply one_closed_inter_any; intro; apply HPK.
Qed.
Definition span_r (gen : K → Prop) := span compatible_r gen.
Lemma span_r_cr : ∀ gen, compatible_r (span_r gen).
Proof. apply span_compatible; move=>>; apply cr_inter_any. Qed.
Lemma span_r_nonempty : ∀ gen, nonempty (span_r gen).
Proof. intros; apply cr_nonempty, span_r_cr. Qed.
Lemma span_r_zero : ∀ gen, zero_closed (span_r gen).
Proof. intros; apply cr_zero, span_r_cr. Qed.
Lemma span_r_plus : ∀ gen, plus_closed (span_r gen).
Proof. intros; apply cr_plus, span_r_cr. Qed.
Lemma span_r_opp : ∀ gen, opp_closed (span_r gen).
Proof. intros; apply cr_opp, span_r_cr. Qed.
Lemma span_r_minus : ∀ gen, minus_closed (span_r gen).
Proof. intros; apply cr_minus, span_r_cr. Qed.
Lemma span_r_one : ∀ gen, one_closed (span_r gen).
Proof. intros; apply cr_one, span_r_cr. Qed.
Lemma span_r_mult : ∀ gen, mult_closed (span_r gen).
Proof. intros; apply cr_mult, span_r_cr. Qed.
Lemma span_r_sum : ∀ gen, sum_closed (span_r gen).
Proof. intros; apply cr_sum, span_r_cr. Qed.
Lemma span_r_incl : ∀ gen, incl gen (span_r gen).
Proof. apply span_incl. Qed.
Lemma span_r_lub :
∀ {gen PK}, compatible_r PK → incl gen PK → incl (span_r gen) PK.
Proof. apply span_lub. Qed.
Lemma span_r_full : ∀ {PK}, compatible_r PK → span_r PK = PK.
Proof. apply span_full. Qed.
End Compatible_Ring_Facts.
Section Compatible_Ring_Morphism_Facts.
Context {K1 K2 : Ring}.
Context {PK1 : K1 → Prop}.
Context {PK2 : K2 → Prop}.
Context {f : K1 → K2}.
Hypothesis Hf : morphism_r f.
Lemma cr_image : compatible_r PK1 → compatible_r (image f PK1).
Proof.
intros [HPK1a [HPK1b HPK1c]]; split; [| split].
apply cg_image; [apply mr_mg |]; easy.
intros _ _ [x1 Hx1] [y1 Hy1]; rewrite -(mr_mult Hf); apply Im; auto.
unfold one_closed; rewrite -(mr_one Hf); easy.
Qed.
Lemma cr_preimage : compatible_r PK2 → compatible_r (preimage f PK2).
Proof.
intros [HPK2a [HPK2b HPK2c]]; split; [| split; unfold preimage].
apply cg_preimage; [apply mr_mg |]; easy.
move=>> Hx1 Hy1; rewrite (mr_mult Hf); auto.
unfold one_closed; rewrite (mr_one Hf); easy.
Qed.
End Compatible_Ring_Morphism_Facts.
Section Sub_Ring_Def.
Context {K : Ring}.
Context {PK : K → Prop}.
Hypothesis HPK : compatible_r PK.
Let PK_g := sub_AbelianGroup (cr_cg HPK).
Definition sub_mult (x y : PK_g) : PK_g :=
mk_sub (cr_mult HPK _ _ (in_sub x) (in_sub y)).
Definition sub_one : PK_g := mk_sub (cr_one HPK : PK 1).
Lemma sub_mult_assoc:
∀ x y z, sub_mult x (sub_mult y z) = sub_mult (sub_mult x y) z.
Proof. intros; apply val_inj, mult_assoc. Qed.
Lemma sub_mult_one_r : ∀ x, sub_mult x sub_one = x.
Proof. intros; apply val_inj, mult_one_r. Qed.
Lemma sub_mult_one_l : ∀ x, sub_mult sub_one x = x.
Proof. intros; apply val_inj, mult_one_l. Qed.
Lemma sub_mult_distr_r :
∀ x y z, sub_mult (x + y) z = sub_mult x z + sub_mult y z.
Proof. intros; apply val_inj, mult_distr_r. Qed.
Lemma sub_mult_distr_l :
∀ x y z, sub_mult x (y + z) = sub_mult x y + sub_mult x z.
Proof. intros; apply val_inj, mult_distr_l. Qed.
Definition sub_Ring_mixin :=
Ring.Mixin _ _ _
sub_mult_assoc sub_mult_one_r sub_mult_one_l
sub_mult_distr_r sub_mult_distr_l.
Canonical Structure sub_Ring :=
Ring.Pack _ (Ring.Class _ _ sub_Ring_mixin) PK_g.
Lemma val_one : f_one_compat val.
Proof. easy. Qed.
Lemma val_mult : f_mult_compat val.
Proof. easy. Qed.
Lemma val_mr : morphism_r val.
Proof. easy. Qed.
Lemma mk_sub_one_equiv :
∀ {x} (Hx : PK x), mk_sub Hx = 1 :> sub_Ring ↔ x = 1.
Proof. intros; split; [move⇒ /val_eq | intros; apply val_inj]; easy. Qed.
Lemma mk_sub_mult :
∀ (x y : K) (Hx : PK x) (Hy : PK y),
mk_sub Hx × mk_sub Hy = mk_sub (cr_mult HPK _ _ Hx Hy).
Proof. easy. Qed.
Lemma sub_one_eq : (1 : sub_Ring) = mk_sub (cr_one HPK : PK 1).
Proof. easy. Qed.
Lemma sub_mult_eq :
∀ (x y : sub_Ring),
x × y = mk_sub (cr_mult HPK _ _ (in_sub x) (in_sub y)).
Proof. easy. Qed.
Lemma val_r_inv_r : ∀ {x} (Hx : PK x), val (mk_sub Hx : sub_Ring) = x.
Proof. apply val_g_inv_r, cr_cg; easy. Qed.
Lemma mk_sub_r_inv_r : ∀ {x}, mk_sub (in_sub x) = x :> sub_Ring.
Proof. intros; apply mk_sub_inv_r. Qed.
Lemma mk_sub_r_inj :
∀ {x y} (Hx : PK x) (Hy : PK y),
mk_sub Hx = mk_sub Hy :> sub_Ring → x = y.
Proof. intros x y; apply mk_sub_inj. Qed.
End Sub_Ring_Def.
Section Sub_Ring_Morphism_Facts1.
Context {K1 K2 : Ring}.
Context {PK1 : K1 → Prop}.
Context {PK2 : K2 → Prop}.
Context {HPK1 : compatible_r PK1}.
Context {HPK2 : compatible_r PK2}.
Let PK1_r := sub_Ring HPK1.
Let PK2_r := sub_Ring HPK2.
Context {f : K1 → K2}.
Context {fS : PK1_r → PK2_r}.
Hypothesis HfS : ∀ x, val (fS x) = f (val x).
Lemma sub_r_f_mult_compat : f_mult_compat f → f_mult_compat fS.
Proof. intros Hf x1 y1; apply val_inj; rewrite HfS Hf -!HfS; easy. Qed.
Lemma sub_r_f_one_compat : f_one_compat f → f_one_compat fS.
Proof. intros Hf; apply val_inj; rewrite HfS Hf; easy. Qed.
Lemma sub_r_morphism : morphism_r f → morphism_r fS.
Proof.
intros [Hf1 [Hf2 Hf3]]; repeat split; [apply (sub_g_morphism HfS Hf1) |
apply (sub_r_f_mult_compat Hf2) | apply (sub_r_f_one_compat Hf3)].
Qed.
End Sub_Ring_Morphism_Facts1.
Section Sub_Ring_Morphism_Facts2.
Context {K1 K2 : Ring}.
Context {PK1 : K1 → Prop}.
Context {PK2 : K2 → Prop}.
Hypothesis HPK1 : compatible_r PK1.
Hypothesis HPK2 : compatible_r PK2.
Let PK1_r := sub_Ring HPK1.
Let PK2_r := sub_Ring HPK2.
Context {f : K1 → K2}.
Hypothesis Hf : funS PK1 PK2 f.
Definition fct_sub_r : PK1_r → PK2_r := fct_sub Hf.
Lemma fct_sub_r_inj : injS PK1 f → injective fct_sub_r.
Proof. apply fct_sub_inj. Qed.
Lemma fct_sub_r_inj_rev : injective fct_sub_r → injS PK1 f.
Proof. apply fct_sub_inj_rev. Qed.
Lemma fct_sub_r_inj_equiv : injective fct_sub_r ↔ injS PK1 f.
Proof. apply fct_sub_inj_equiv. Qed.
Lemma fct_sub_r_surj : surjS PK1 PK2 f → surjective fct_sub_r.
Proof. apply fct_sub_surj. Qed.
Lemma fct_sub_r_surj_rev : surjective fct_sub_r → surjS PK1 PK2 f.
Proof. apply fct_sub_surj_rev. Qed.
Lemma fct_sub_r_surj_equiv : surjective fct_sub_r ↔ surjS PK1 PK2 f.
Proof. apply fct_sub_surj_equiv. Qed.
Lemma fct_sub_r_bij : bijS PK1 PK2 f → bijective fct_sub_r.
Proof. apply fct_sub_bij, inhabited_r. Qed.
Lemma fct_sub_r_bij_rev : bijective fct_sub_r → bijS PK1 PK2 f.
Proof. apply fct_sub_bij_rev, inhabited_r. Qed.
Lemma fct_sub_r_bij_equiv : bijective fct_sub_r ↔ bijS PK1 PK2 f.
Proof. apply fct_sub_bij_equiv, inhabited_r. Qed.
Lemma fct_sub_r_f_mult_compat : f_mult_compat f → f_mult_compat fct_sub_r.
Proof. apply sub_r_f_mult_compat, fct_sub_correct. Qed.
Lemma fct_sub_r_f_one_compat : f_one_compat f → f_one_compat fct_sub_r.
Proof. apply sub_r_f_one_compat, fct_sub_correct. Qed.
Lemma fct_sub_r_mr : morphism_r f → morphism_r fct_sub_r.
Proof. apply sub_r_morphism, fct_sub_correct. Qed.
Lemma fct_sub_r_f_inv_mr :
∀ (Hfb : bijS PK1 PK2 f),
morphism_r f → morphism_r (f_inv (fct_sub_r_bij Hfb)).
Proof. intros; apply mr_bij_compat, fct_sub_r_mr; easy. Qed.
End Sub_Ring_Morphism_Facts2.
∀ {Idx : Type} {PK : Idx → K → Prop},
(∀ i, compatible_r (PK i)) → compatible_r (inter_any PK).
Proof.
move=>> HPK; split; [ | split].
apply cg_inter_any; intro; apply cr_cg; easy.
apply mult_closed_inter_any; intro; apply HPK.
apply one_closed_inter_any; intro; apply HPK.
Qed.
Definition span_r (gen : K → Prop) := span compatible_r gen.
Lemma span_r_cr : ∀ gen, compatible_r (span_r gen).
Proof. apply span_compatible; move=>>; apply cr_inter_any. Qed.
Lemma span_r_nonempty : ∀ gen, nonempty (span_r gen).
Proof. intros; apply cr_nonempty, span_r_cr. Qed.
Lemma span_r_zero : ∀ gen, zero_closed (span_r gen).
Proof. intros; apply cr_zero, span_r_cr. Qed.
Lemma span_r_plus : ∀ gen, plus_closed (span_r gen).
Proof. intros; apply cr_plus, span_r_cr. Qed.
Lemma span_r_opp : ∀ gen, opp_closed (span_r gen).
Proof. intros; apply cr_opp, span_r_cr. Qed.
Lemma span_r_minus : ∀ gen, minus_closed (span_r gen).
Proof. intros; apply cr_minus, span_r_cr. Qed.
Lemma span_r_one : ∀ gen, one_closed (span_r gen).
Proof. intros; apply cr_one, span_r_cr. Qed.
Lemma span_r_mult : ∀ gen, mult_closed (span_r gen).
Proof. intros; apply cr_mult, span_r_cr. Qed.
Lemma span_r_sum : ∀ gen, sum_closed (span_r gen).
Proof. intros; apply cr_sum, span_r_cr. Qed.
Lemma span_r_incl : ∀ gen, incl gen (span_r gen).
Proof. apply span_incl. Qed.
Lemma span_r_lub :
∀ {gen PK}, compatible_r PK → incl gen PK → incl (span_r gen) PK.
Proof. apply span_lub. Qed.
Lemma span_r_full : ∀ {PK}, compatible_r PK → span_r PK = PK.
Proof. apply span_full. Qed.
End Compatible_Ring_Facts.
Section Compatible_Ring_Morphism_Facts.
Context {K1 K2 : Ring}.
Context {PK1 : K1 → Prop}.
Context {PK2 : K2 → Prop}.
Context {f : K1 → K2}.
Hypothesis Hf : morphism_r f.
Lemma cr_image : compatible_r PK1 → compatible_r (image f PK1).
Proof.
intros [HPK1a [HPK1b HPK1c]]; split; [| split].
apply cg_image; [apply mr_mg |]; easy.
intros _ _ [x1 Hx1] [y1 Hy1]; rewrite -(mr_mult Hf); apply Im; auto.
unfold one_closed; rewrite -(mr_one Hf); easy.
Qed.
Lemma cr_preimage : compatible_r PK2 → compatible_r (preimage f PK2).
Proof.
intros [HPK2a [HPK2b HPK2c]]; split; [| split; unfold preimage].
apply cg_preimage; [apply mr_mg |]; easy.
move=>> Hx1 Hy1; rewrite (mr_mult Hf); auto.
unfold one_closed; rewrite (mr_one Hf); easy.
Qed.
End Compatible_Ring_Morphism_Facts.
Section Sub_Ring_Def.
Context {K : Ring}.
Context {PK : K → Prop}.
Hypothesis HPK : compatible_r PK.
Let PK_g := sub_AbelianGroup (cr_cg HPK).
Definition sub_mult (x y : PK_g) : PK_g :=
mk_sub (cr_mult HPK _ _ (in_sub x) (in_sub y)).
Definition sub_one : PK_g := mk_sub (cr_one HPK : PK 1).
Lemma sub_mult_assoc:
∀ x y z, sub_mult x (sub_mult y z) = sub_mult (sub_mult x y) z.
Proof. intros; apply val_inj, mult_assoc. Qed.
Lemma sub_mult_one_r : ∀ x, sub_mult x sub_one = x.
Proof. intros; apply val_inj, mult_one_r. Qed.
Lemma sub_mult_one_l : ∀ x, sub_mult sub_one x = x.
Proof. intros; apply val_inj, mult_one_l. Qed.
Lemma sub_mult_distr_r :
∀ x y z, sub_mult (x + y) z = sub_mult x z + sub_mult y z.
Proof. intros; apply val_inj, mult_distr_r. Qed.
Lemma sub_mult_distr_l :
∀ x y z, sub_mult x (y + z) = sub_mult x y + sub_mult x z.
Proof. intros; apply val_inj, mult_distr_l. Qed.
Definition sub_Ring_mixin :=
Ring.Mixin _ _ _
sub_mult_assoc sub_mult_one_r sub_mult_one_l
sub_mult_distr_r sub_mult_distr_l.
Canonical Structure sub_Ring :=
Ring.Pack _ (Ring.Class _ _ sub_Ring_mixin) PK_g.
Lemma val_one : f_one_compat val.
Proof. easy. Qed.
Lemma val_mult : f_mult_compat val.
Proof. easy. Qed.
Lemma val_mr : morphism_r val.
Proof. easy. Qed.
Lemma mk_sub_one_equiv :
∀ {x} (Hx : PK x), mk_sub Hx = 1 :> sub_Ring ↔ x = 1.
Proof. intros; split; [move⇒ /val_eq | intros; apply val_inj]; easy. Qed.
Lemma mk_sub_mult :
∀ (x y : K) (Hx : PK x) (Hy : PK y),
mk_sub Hx × mk_sub Hy = mk_sub (cr_mult HPK _ _ Hx Hy).
Proof. easy. Qed.
Lemma sub_one_eq : (1 : sub_Ring) = mk_sub (cr_one HPK : PK 1).
Proof. easy. Qed.
Lemma sub_mult_eq :
∀ (x y : sub_Ring),
x × y = mk_sub (cr_mult HPK _ _ (in_sub x) (in_sub y)).
Proof. easy. Qed.
Lemma val_r_inv_r : ∀ {x} (Hx : PK x), val (mk_sub Hx : sub_Ring) = x.
Proof. apply val_g_inv_r, cr_cg; easy. Qed.
Lemma mk_sub_r_inv_r : ∀ {x}, mk_sub (in_sub x) = x :> sub_Ring.
Proof. intros; apply mk_sub_inv_r. Qed.
Lemma mk_sub_r_inj :
∀ {x y} (Hx : PK x) (Hy : PK y),
mk_sub Hx = mk_sub Hy :> sub_Ring → x = y.
Proof. intros x y; apply mk_sub_inj. Qed.
End Sub_Ring_Def.
Section Sub_Ring_Morphism_Facts1.
Context {K1 K2 : Ring}.
Context {PK1 : K1 → Prop}.
Context {PK2 : K2 → Prop}.
Context {HPK1 : compatible_r PK1}.
Context {HPK2 : compatible_r PK2}.
Let PK1_r := sub_Ring HPK1.
Let PK2_r := sub_Ring HPK2.
Context {f : K1 → K2}.
Context {fS : PK1_r → PK2_r}.
Hypothesis HfS : ∀ x, val (fS x) = f (val x).
Lemma sub_r_f_mult_compat : f_mult_compat f → f_mult_compat fS.
Proof. intros Hf x1 y1; apply val_inj; rewrite HfS Hf -!HfS; easy. Qed.
Lemma sub_r_f_one_compat : f_one_compat f → f_one_compat fS.
Proof. intros Hf; apply val_inj; rewrite HfS Hf; easy. Qed.
Lemma sub_r_morphism : morphism_r f → morphism_r fS.
Proof.
intros [Hf1 [Hf2 Hf3]]; repeat split; [apply (sub_g_morphism HfS Hf1) |
apply (sub_r_f_mult_compat Hf2) | apply (sub_r_f_one_compat Hf3)].
Qed.
End Sub_Ring_Morphism_Facts1.
Section Sub_Ring_Morphism_Facts2.
Context {K1 K2 : Ring}.
Context {PK1 : K1 → Prop}.
Context {PK2 : K2 → Prop}.
Hypothesis HPK1 : compatible_r PK1.
Hypothesis HPK2 : compatible_r PK2.
Let PK1_r := sub_Ring HPK1.
Let PK2_r := sub_Ring HPK2.
Context {f : K1 → K2}.
Hypothesis Hf : funS PK1 PK2 f.
Definition fct_sub_r : PK1_r → PK2_r := fct_sub Hf.
Lemma fct_sub_r_inj : injS PK1 f → injective fct_sub_r.
Proof. apply fct_sub_inj. Qed.
Lemma fct_sub_r_inj_rev : injective fct_sub_r → injS PK1 f.
Proof. apply fct_sub_inj_rev. Qed.
Lemma fct_sub_r_inj_equiv : injective fct_sub_r ↔ injS PK1 f.
Proof. apply fct_sub_inj_equiv. Qed.
Lemma fct_sub_r_surj : surjS PK1 PK2 f → surjective fct_sub_r.
Proof. apply fct_sub_surj. Qed.
Lemma fct_sub_r_surj_rev : surjective fct_sub_r → surjS PK1 PK2 f.
Proof. apply fct_sub_surj_rev. Qed.
Lemma fct_sub_r_surj_equiv : surjective fct_sub_r ↔ surjS PK1 PK2 f.
Proof. apply fct_sub_surj_equiv. Qed.
Lemma fct_sub_r_bij : bijS PK1 PK2 f → bijective fct_sub_r.
Proof. apply fct_sub_bij, inhabited_r. Qed.
Lemma fct_sub_r_bij_rev : bijective fct_sub_r → bijS PK1 PK2 f.
Proof. apply fct_sub_bij_rev, inhabited_r. Qed.
Lemma fct_sub_r_bij_equiv : bijective fct_sub_r ↔ bijS PK1 PK2 f.
Proof. apply fct_sub_bij_equiv, inhabited_r. Qed.
Lemma fct_sub_r_f_mult_compat : f_mult_compat f → f_mult_compat fct_sub_r.
Proof. apply sub_r_f_mult_compat, fct_sub_correct. Qed.
Lemma fct_sub_r_f_one_compat : f_one_compat f → f_one_compat fct_sub_r.
Proof. apply sub_r_f_one_compat, fct_sub_correct. Qed.
Lemma fct_sub_r_mr : morphism_r f → morphism_r fct_sub_r.
Proof. apply sub_r_morphism, fct_sub_correct. Qed.
Lemma fct_sub_r_f_inv_mr :
∀ (Hfb : bijS PK1 PK2 f),
morphism_r f → morphism_r (f_inv (fct_sub_r_bij Hfb)).
Proof. intros; apply mr_bij_compat, fct_sub_r_mr; easy. Qed.
End Sub_Ring_Morphism_Facts2.