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

Quotients of algebraic structures This file defines a join hierarchy mixing the structures defined in file ssralg (up to unit ring type) and the quotType quotient structure defined in generic_quotient.v. 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 The HB class is called ZmodQuotient. 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 The HB class is called RingQuotient. unitRingQuotType ... u i == As in the previous cases, instance of unit ring whose unit predicate is obtained from u and the inverse from i The HB class is called UnitRingQuotient. idealr R == {pred R} is a non-trivial, decidable, right ideal of the ring R (join of GRing.ZmodClosed and ProperIdeal) The HB class is called Idealr. prime_idealr R == {pred R} is a non-trivial, decidable, right, prime ideal of the ring R The HB class is called PrimeIdealr. The formalization of ideals features the following constructions: proper_ideal R == the collective predicate (S : pred R) on the ring R is stable by the ring product and does contain R's one The HB class is called ProperIdeal. idealr R == join of GRing.ZmodClosed and ProperIdeal 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. {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

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.

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

Variable (T : Type). Variable eqT : rel T. Variables (zeroT : T) (oppT : T -> T) (addT : T -> T -> T). Variables (oneT : T) (mulT : T -> T -> T).
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="proper_ideal")]
HB.structure Definition ProperIdeal R := {S of isProperIdeal R S}.

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

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

Section IdealTheory.
Variables (R : ringType) (idealrI : idealr R).
Local Notation I := (idealrI : pred 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 : prime_idealr R).
Local Notation I := (pidealI : pred 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.
Local Notation quot := (type_of (Phant R)).

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

#[export]
#[export]
HB.instance Definition _ := GRing.Zmodule.on quot.
#[export]
HB.instance Definition _ := @isZmodQuotient.Build R equiv 0 -%R +%R type
#[export]
HB.instance Definition _ := @ZmodQuotient.on quot.

End ZmodQuotient.

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

Section RingQuotient.

Variables (R : comRingType) (idealI : idealr R).
Local Notation I := (idealI : pred 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 nonzero1q: one != 0.

#[export]
HB.instance Definition _ := GRing.Zmodule_isComRing.Build (type idealI)
#[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 : prime_idealr 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.