Library mathcomp.algebra.ring_quotient

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

From HB Require Import structures.
From mathcomp Require Import ssreflect eqtype choice ssreflect ssrbool ssrnat.
From mathcomp Require Import ssrfun seq ssralg generic_quotient.

This file describes quotients of algebraic structures.
It defines a join hierarchy mixing the structures defined in file ssralg (up to unit ring type) and the quotType quotient structure defined in file generic_quotient. Every structure in that (join) hierarchy is parametrized by a base type T and the constants and operations on the base type that will be used to confer its algebraic structure to the quotient. Note that T itself is in general not an instance of an algebraic structure. The canonical surjection from T onto its quotient should be compatible with the parameter operations.
The second part of the file provides a definition of (non trivial) decidable ideals (resp. prime ideals) of an arbitrary instance of ring structure and a construction of the quotient of a ring by such an ideal. These definitions extend the hierarchy of sub-structures defined in file ssralg (see Module Pred in ssralg), following a similar methodology. Although the definition of the (structure of) quotient of a ring by an ideal is a general one, we do not provide infrastructure for the case of non commutative ring and left or two-sided ideals.
The file defines the following Structures: zmodQuotType T e z n a == Z-module obtained by quotienting type T with the relation e and whose neutral, opposite and addition are the images in the quotient of the parameters z, n and a, respectively. ringQuotType T e z n a o m == ring obtained by quotienting type T with the relation e and whose zero opposite, addition, one, and multiplication are the images in the quotient of the parameters z, n, a, o, m, respectively. unitRingQuotType ... u i == As in the previous cases, instance of unit ring whose unit predicate is obtained from u and the inverse from i. idealr R S == S : {pred R} is a non-trivial, decidable, right ideal of the ring R. prime_idealr R S == S : {pred R} is a non-trivial, decidable, right, prime ideal of the ring R.
The formalization of ideals features the following constructions: proper_ideal S == the collective predicate (S : pred R) on the ring R is stable by the ring product and does contain R's one. prime_idealr_closed S := u * v \in S -> (u \in S) || (v \in S) idealr_closed S == the collective predicate (S : pred R) on the ring R represents a (right) ideal. This implies its being a proper_ideal.
MkIdeal idealS == packs idealS : proper_ideal S into an idealr S interface structure associating the idealr_closed property to the canonical pred_key S (see ssrbool), which must already be a zmodPred (see ssralg). MkPrimeIdeal pidealS == packs pidealS : prime_idealr_closed S into a prime_idealr S interface structure associating the prime_idealr_closed property to the canonical pred_key S (see ssrbool), which must already be an idealr (see above). {ideal_quot kI} == quotient by the keyed (right) ideal predicate kI of a commutative ring R. Note that we only provide canonical structures of ring quotients for commutative rings, in which a right ideal is obviously a two-sided ideal.
Note : if (I : pred R) is a predicate over a ring R and (ideal : idealr I) is an instance of (right) ideal, in order to quantify over an arbitrary (keyed) predicate describing ideal, use type (keyed_pred ideal), as in: forall (kI : keyed_pred ideal),...

Import GRing.Theory.

Set Implicit Arguments.

Local Open Scope ring_scope.
Local Open Scope quotient_scope.

Reserved Notation "{ 'ideal_quot' I }"
  (at level 0, format "{ 'ideal_quot' I }").
Reserved Notation "m = n %[ 'mod_ideal' I ]" (at level 70, n at next level,
  format "'[hv ' m '/' = n '/' %[ 'mod_ideal' I ] ']'").
Reserved Notation "m == n %[ 'mod_ideal' I ]" (at level 70, n at next level,
  format "'[hv ' m '/' == n '/' %[ 'mod_ideal' I ] ']'").
Reserved Notation "m <> n %[ 'mod_ideal' I ]" (at level 70, n at next level,
  format "'[hv ' m '/' <> n '/' %[ 'mod_ideal' I ] ']'").
Reserved Notation "m != n %[ 'mod_ideal' I ]" (at level 70, n at next level,
  format "'[hv ' m '/' != n '/' %[ 'mod_ideal' I ] ']'").

Variable (T : Type). Variable eqT : rel T. Variables (zeroT : T) (oppT : T -> T) (addT : T -> T -> T).


#[short(type="zmodQuotType")]
HB.structure Definition ZmodQuotient T eqT zeroT oppT addT :=
  {Q of isZmodQuotient T eqT zeroT oppT addT Q &
        GRing.Zmodule Q & EqQuotient T eqT Q}.

Section ZModQuotient.

Variable (T : Type).
Variable eqT : rel T.
Variables (zeroT : T) (oppT : T T) (addT : T T T).
Implicit Type zqT : ZmodQuotient.type eqT zeroT oppT addT.

Canonical pi_zero_quot_morph zqT := PiMorph (@pi_zeror _ _ _ _ _ zqT).
Canonical pi_opp_quot_morph zqT := PiMorph1 (@pi_oppr _ _ _ _ _ zqT).
Canonical pi_add_quot_morph zqT := PiMorph2 (@pi_addr _ _ _ _ _ zqT).

End ZModQuotient.

Module ZModQuotientExports.
Notation "[ 'zmodQuotType' z , o & a 'of' Q ]" :=
  (@ZmodQuotient.clone _ _ z o%function a%function Q%type _)
  (at level 0, format "[ 'zmodQuotType' z , o & a 'of' Q ]") : form_scope.
End ZModQuotientExports.

Section PiAdditive.

Variables (V : zmodType) (equivV : rel V) (zeroV : V).
Variable Q : @zmodQuotType V equivV zeroV -%R +%R.

Lemma pi_is_additive : additive \pi_Q.


End PiAdditive.

Variable (T : Type). Variable eqT : rel T. Variables (zeroT : T) (oppT : T -> T) (addT : T -> T -> T). Variables (oneT : T) (mulT : T -> T -> T).

#[short(type="ringQuotType")]
HB.structure Definition RingQuotient T eqT zeroT oppT addT oneT mulT :=
  {Q of isRingQuotient T eqT zeroT oppT addT oneT mulT Q &
   ZmodQuotient T eqT zeroT oppT addT Q & GRing.Ring Q }.

Section ringQuotient.
Clash with the module name RingQuotient

Variable (T : Type).
Variable eqT : rel T.
Variables (zeroT : T) (oppT : T T) (addT : T T T) (oneT : T) (mulT : T T T).
Implicit Type rqT : RingQuotient.type eqT zeroT oppT addT oneT mulT.

Canonical pi_one_quot_morph rqT := PiMorph (@pi_oner _ _ _ _ _ _ _ rqT).
Canonical pi_mul_quot_morph rqT := PiMorph2 (@pi_mulr _ _ _ _ _ _ _ rqT).

End ringQuotient.
Module RingQuotientExports.
Notation "[ 'ringQuotType' o & m 'of' Q ]" :=
  (@RingQuotient.clone _ _ _ _ _ o m%function Q%type _)
  (at level 0, format "[ 'ringQuotType' o & m 'of' Q ]") : form_scope.
End RingQuotientExports.

Section PiRMorphism.

Variables (R : ringType) (equivR : rel R) (zeroR : R).

Variable Q : @ringQuotType R equivR zeroR -%R +%R 1 *%R.

Lemma pi_is_multiplicative : multiplicative \pi_Q.


End PiRMorphism.


#[short(type="unitRingQuotType")]
HB.structure Definition UnitRingQuotient T eqT zeroT oppT addT oneT mulT unitT invT :=
  {Q of isUnitRingQuotient T eqT zeroT oppT addT oneT mulT unitT invT Q & GRing.UnitRing Q & isQuotient T Q & isEqQuotient T eqT Q & isZmodQuotient T eqT zeroT oppT addT Q & isRingQuotient T eqT zeroT oppT addT oneT mulT Q}.

Section UnitRingQuot.
Variable (T : Type).
Variable eqT : rel T.
Variables (zeroT : T) (oppT : T T) (addT : T T T).
Variables (oneT : T) (mulT : T T T).
Variables (unitT : pred T) (invT : T T).
Implicit Type urqT : UnitRingQuotient.type eqT zeroT oppT addT oneT mulT unitT invT.

Canonical pi_unit_quot_morph urqT := PiMono1 (@pi_unitr _ _ _ _ _ _ _ _ _ urqT).
Canonical pi_inv_quot_morph urqT := PiMorph1 (@pi_invr _ _ _ _ _ _ _ _ _ urqT).

End UnitRingQuot.

Module UnitRingQuotientExports.
Notation "[ 'unitRingQuotType' u & i 'of' Q ]" :=
  (@UnitRingQuotient.clone _ _ _ _ _ _ _ u i%function Q%type _)
  (at level 0, format "[ 'unitRingQuotType' u & i 'of' Q ]") : form_scope.
End UnitRingQuotientExports.

Definition proper_ideal (R : ringType) (S : {pred R}) : Prop :=
  1 \notin S a, {in S, u, a × u \in S}.

Definition prime_idealr_closed (R : ringType) (S : {pred R}) : Prop :=
   u v, u × v \in S (u \in S) || (v \in S).

Definition idealr_closed (R : ringType) (S : {pred R}) :=
  [/\ 0 \in S, 1 \notin S & a, {in S &, u v, a × u + v \in S}].

Lemma idealr_closed_nontrivial R S : @idealr_closed R S proper_ideal S.

Lemma idealr_closedB R S : @idealr_closed R S zmod_closed S.


#[short(type="properIdealPred")]
HB.structure Definition ProperIdeal R := {S of isProperIdeal R S}.

#[short(type="idealrPred")]
HB.structure Definition Idealr (R : ringType) :=
  {S of GRing.ZmodClosed R S & ProperIdeal R S}.


#[short(type="primeIdealrPred")]
HB.structure Definition PrimeIdealr (R : ringType) :=
  {S of Idealr R S & isPrimeIdealrClosed R S}.



Section IdealTheory.
Variables (R : ringType) (idealrI : idealrPred R).

Lemma idealr1 : 1 \in I = false.

Lemma idealMr a u : u \in I a × u \in I.

Lemma idealr0 : 0 \in I.

End IdealTheory.

Section PrimeIdealTheory.

Variables (R : comRingType) (pidealI : primeIdealrPred R).

Lemma prime_idealrM u v : (u × v \in I) = (u \in I) || (v \in I).

End PrimeIdealTheory.

Module Quotient.
Section ZmodQuotient.
Variables (R : zmodType) (I : zmodClosed R).

Definition equiv (x y : R) := (x - y) \in I.

Lemma equivE x y : (equiv x y) = (x - y \in I).

Lemma equiv_is_equiv : equiv_class_of equiv.

Canonical equiv_equiv := EquivRelPack equiv_is_equiv.
Canonical equiv_encModRel := defaultEncModRel equiv.

Definition type := {eq_quot equiv}.
Definition type_of of phant R := type.

#[export]
HB.instance Definition _ : EqQuotient R equiv type := EqQuotient.on type.
#[export]
HB.instance Definition _ := Choice.on type.
#[export]
HB.instance Definition _ := EqQuotient.on quot.
#[export]
HB.instance Definition _ := Choice.on quot.

Lemma idealrBE x y : (x - y) \in I = (x == y %[mod type]).

Lemma idealrDE x y : (x + y) \in I = (x == - y %[mod type]).

Definition zero : type := lift_cst type 0.
Definition add := lift_op2 type +%R.
Definition opp := lift_op1 type -%R.

Canonical pi_zero_morph := PiConst zero.

Lemma pi_opp : {morph \pi : x / - x >-> opp x}.
Canonical pi_opp_morph := PiMorph1 pi_opp.

Lemma pi_add : {morph \pi : x y / x + y >-> add x y}.
Canonical pi_add_morph := PiMorph2 pi_add.

Lemma addqA: associative add.

Lemma addqC: commutative add.

Lemma add0q: left_id zero add.

Lemma addNq: left_inverse zero opp add.

#[export]
HB.instance Definition _ := GRing.isZmodule.Build type addqA addqC add0q addNq.
#[export]
HB.instance Definition _ := GRing.Zmodule.on quot.
#[export]
HB.instance Definition _ := @isZmodQuotient.Build R equiv 0 -%R +%R type
  (lock _) pi_opp pi_add.
#[export]
HB.instance Definition _ := @ZmodQuotient.on quot.

End ZmodQuotient.

Notation "{ 'quot' I }" := (@type_of _ I (Phant _)) : type_scope.

Section RingQuotient.

Variables (R : comRingType) (idealI : idealrPred R).

Definition one : {quot idealI} := lift_cst {quot idealI} 1.
Definition mul := lift_op2 {quot idealI} *%R.

Canonical pi_one_morph := PiConst one.

Lemma pi_mul: {morph \pi : x y / x × y >-> mul x y}.
Canonical pi_mul_morph := PiMorph2 pi_mul.

Lemma mulqA: associative mul.

Lemma mulqC: commutative mul.

Lemma mul1q: left_id one mul.

Lemma mulq_addl: left_distributive mul +%R.

Lemma nonzero1q: one != 0.

#[export]
HB.instance Definition _ := GRing.Zmodule_isComRing.Build (type idealI)
  mulqA mulqC mul1q mulq_addl nonzero1q.
#[export]
HB.instance Definition _ := GRing.ComRing.on {quot idealI}.

#[export]
HB.instance Definition _ := @isRingQuotient.Build
  R (equiv idealI) 0 -%R +%R 1%R *%R (type idealI) (lock _) pi_mul.
#[export]
HB.instance Definition _ := @RingQuotient.on {quot idealI}.

End RingQuotient.

Section IDomainQuotient.

Variables (R : comRingType) (I : primeIdealrPred R).

Lemma rquot_IdomainAxiom (x y : {quot I}): x × y = 0 (x == 0) || (y == 0).

End IDomainQuotient.

Module Exports. End Exports.
End Quotient.

Export Quotient.Exports.

Notation "{ 'ideal_quot' I }" :=
  (@Quotient.type_of _ I (Phant _)) : type_scope.
Notation "x == y %[ 'mod_ideal' I ]" :=
  (x == y %[mod {ideal_quot I}]) : quotient_scope.
Notation "x = y %[ 'mod_ideal' I ]" :=
  (x = y %[mod {ideal_quot I}]) : quotient_scope.
Notation "x != y %[ 'mod_ideal' I ]" :=
  (x != y %[mod {ideal_quot I}]) : quotient_scope.
Notation "x <> y %[ 'mod_ideal' I ]" :=
  (x y %[mod {ideal_quot I}]) : quotient_scope.