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.

Brief description

Support for subrings.

Description

Let K : Ring. Let PK : K Prop.
  • 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.
Lemmas about predicate compatible_r have "cr" in their names, usually as prefix "cr_", sometimes as suffix "_cr".
Let gen : K Prop.
  • 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

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.

Bibliography

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.

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 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.

[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.

[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.