Library mathcomp.algebra.fraction

(* (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 ssrnat div seq.
From mathcomp Require Import ssrAC choice tuple bigop ssralg poly polydiv.
From mathcomp Require Import generic_quotient.

This file builds the field of fraction of any integral domain. The main result of this file is the existence of the field and of the tofrac function which is a injective ring morphism from R to its fraction field {fraction R}

Set Implicit Arguments.

Import GRing.Theory.
Local Open Scope ring_scope.
Local Open Scope quotient_scope.

Reserved Notation "{ 'ratio' T }" (at level 0, format "{ 'ratio' T }").
Reserved Notation "{ 'fraction' T }" (at level 0, format "{ 'fraction' T }").
Reserved Notation "x %:F" (at level 2, format "x %:F").

Section FracDomain.
Variable R : ringType.

ratios are pairs of R, such that the second member is nonzero
Inductive ratio := mkRatio { frac :> R × R; _ : frac.2 != 0 }.
Definition ratio_of of phant R := ratio.


Lemma denom_ratioP : f : ratio, f.2 != 0.

Definition ratio0 := (@mkRatio (0, 1) (oner_neq0 _)).
Definition Ratio x y : {ratio R} := insubd ratio0 (x, y).

Lemma numer_Ratio x y : y != 0 (Ratio x y).1 = x.

Lemma denom_Ratio x y : y != 0 (Ratio x y).2 = y.

Definition numden_Ratio := (numer_Ratio, denom_Ratio).

Variant Ratio_spec (n d : R) : {ratio R} R R Type :=
  | RatioNull of d = 0 : Ratio_spec n d ratio0 n 0
  | RatioNonNull (d_neq0 : d != 0) :
    Ratio_spec n d (@mkRatio (n, d) d_neq0) n d.

Lemma RatioP n d : Ratio_spec n d (Ratio n d) n d.

Lemma Ratio0 x : Ratio x 0 = ratio0.

End FracDomain.

Notation "{ 'ratio' T }" := (ratio_of (Phant T)) : type_scope.
Identity Coercion type_fracdomain_of : ratio_of >-> ratio.

Notation "'\n_' x" := (frac x).1
  (at level 8, x at level 2, format "'\n_' x").
Notation "'\d_' x" := (frac x).2
  (at level 8, x at level 2, format "'\d_' x").

Module FracField.
Section FracField.

Variable R : idomainType.


Implicit Types x y z : dom.

We define a relation in ratios
we show that equivf is an equivalence
Canonical equivf_equiv := EquivRel equivf equivf_refl equivf_sym equivf_trans.

Definition type := {eq_quot equivf}.
Definition type_of of phant R := type.
Notation "{ 'fraction' T }" := (type_of (Phant T)) : type_scope.

we recover some structure for the quotient

we explain what was the equivalence on the quotient
Lemma equivf_def (x y : ratio R) : x == y %[mod type]
                                    = (\n_x × \d_y == \d_x × \n_y).

Lemma equivf_r x : \n_x × \d_(repr (\pi_type x)) = \d_x × \n_(repr (\pi_type x)).

Lemma equivf_l x : \n_(repr (\pi_type x)) × \d_x = \d_(repr (\pi_type x)) × \n_x.

Lemma numer0 x : (\n_x == 0) = (x == (ratio0 R) %[mod_eq equivf]).

Lemma Ratio_numden : x, Ratio \n_x \d_x = x.

Definition tofrac := lift_embed {fraction R} (fun x : RRatio x 1).
Canonical tofrac_pi_morph := PiEmbed tofrac.

Notation "x %:F" := (@tofrac x).

Implicit Types a b c : type.

Definition addf x y : dom := Ratio (\n_x × \d_y + \n_y × \d_x) (\d_x × \d_y).
Definition add := lift_op2 {fraction R} addf.

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

Definition oppf x : dom := Ratio (- \n_x) \d_x.
Definition opp := lift_op1 {fraction R} oppf.
Lemma pi_opp : {morph \pi : x / oppf x >-> opp x}.
Canonical pi_opp_morph := PiMorph1 pi_opp.

Definition mulf x y : dom := Ratio (\n_x × \n_y) (\d_x × \d_y).
Definition mul := lift_op2 {fraction R} mulf.

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

Definition invf x : dom := Ratio \d_x \n_x.
Definition inv := lift_op1 {fraction R} invf.

Lemma pi_inv : {morph \pi : x / invf x >-> inv x}.
Canonical pi_inv_morph := PiMorph1 pi_inv.

Lemma addA : associative add.

Lemma addC : commutative add.

Lemma add0_l : left_id 0%:F add.

Lemma addN_l : left_inverse 0%:F opp add.

fracions form an abelian group
fractions form a commutative ring

Lemma mulV_l : a, a != 0%:F mul (inv a) a = 1%:F.

Lemma inv0 : inv 0%:F = 0%:F.

fractions form a ring with explicit unit fractions form a field

End FracField.
End FracField.

Notation "{ 'fraction' T }" := (FracField.type_of (Phant T)).
Notation equivf := (@FracField.equivf _).
#[global] Hint Resolve denom_ratioP : core.


Section FracFieldTheory.

Import FracField.

Variable R : idomainType.

Lemma Ratio_numden (x : {ratio R}) : Ratio \n_x \d_x = x.

exporting the embeding from R to {fraction R}
tests
Lemma tofrac0 : 0%:F = 0.
Lemma tofracN : {morph tofrac: x / - x}.
Lemma tofracD : {morph tofrac: x y / x + y}.
Lemma tofracB : {morph tofrac: x y / x - y}.
Lemma tofracMn n : {morph tofrac: x / x *+ n}.
Lemma tofracMNn n : {morph tofrac: x / x *- n}.
Lemma tofrac1 : 1%:F = 1.
Lemma tofracM : {morph tofrac: x y / x × y}.
Lemma tofracX n : {morph tofrac: x / x ^+ n}.

Lemma tofrac_eq (p q : R): (p%:F == q%:F) = (p == q).

Lemma tofrac_eq0 (p : R): (p%:F == 0) = (p == 0).
End FracFieldTheory.