Library mathcomp.algebra.ring_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

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

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