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.
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.
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
Definition equivf x y := equivf_notation x y.
Lemma equivfE x y : equivf x y = equivf_notation x y.
Lemma equivf_refl : reflexive equivf.
Lemma equivf_sym : symmetric equivf.
Lemma equivf_trans : transitive equivf.
Lemma equivfE x y : equivf x y = equivf_notation x y.
Lemma equivf_refl : reflexive equivf.
Lemma equivf_sym : symmetric equivf.
Lemma equivf_trans : transitive equivf.
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.
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 : R ⇒ Ratio 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.
= (\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 : R ⇒ Ratio 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
Lemma mulA : associative mul.
Lemma mulC : commutative mul.
Lemma mul1_l : left_id 1%:F mul.
Lemma mul_addl : left_distributive mul add.
Lemma nonzero1 : 1%:F != 0%:F :> type.
fractions form a commutative ring
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.
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.