Library mathcomp.algebra.ring_quotient

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
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),...