# 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 ssrfun ssrbool eqtype choice ssrnat.
From mathcomp Require Import 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.
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.
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.
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 quot := {eq_quot equiv}.
#[export]
HB.instance Definition _ : EqQuotient R equiv quot := EqQuotient.on quot.
#[export]
HB.instance Definition _ := Choice.on quot.
Lemma idealrBE x y : (x - y) \in I = (x == y %[mod quot]).
Lemma idealrDE x y : (x + y) \in I = (x == - y %[mod quot]).
Definition zero : quot := lift_cst quot 0.
Definition add := lift_op2 quot +%R.
Definition opp := lift_op1 quot -%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 quot addqA addqC add0q addNq.
#[export]
HB.instance Definition _ := @isZmodQuotient.Build R equiv 0 -%R +%R quot
(lock _) pi_opp pi_add.
End ZmodQuotient.
Arguments quot R%type I%type.
Notation "{ 'quot' I }" := (quot I) : 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 mulq_addl: left_distributive mul +%R.
Lemma nonzero1q: one != 0.
#[export]
HB.instance Definition _ := GRing.Zmodule_isComRing.Build (quot idealI)
mulqA mulqC mul1q mulq_addl nonzero1q.
#[export]
HB.instance Definition _ := @isRingQuotient.Build
R (equiv idealI) 0 -%R +%R 1%R *%R (quot idealI) (lock _) pi_mul.
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.quot _ I) : 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.