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.
Field of fraction of an integral domain
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 }.
Lemma denom_ratioP : ∀ f : ratio, f.2 != 0.
Definition ratio0 := (@mkRatio (0, 1) (oner_neq0 _)).
Definition Ratio x y : ratio := 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 → 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.
Arguments ratio R%type.
Notation "{ 'ratio' T }" := (ratio T) : type_scope.
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.
Lemma denom_ratioP : ∀ f : ratio, f.2 != 0.
Definition ratio0 := (@mkRatio (0, 1) (oner_neq0 _)).
Definition Ratio x y : ratio := 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 → 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.
Arguments ratio R%type.
Notation "{ 'ratio' T }" := (ratio T) : type_scope.
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 := {eq_quot equivf}.
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 type (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 type 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 type 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 type 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 type 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 type (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 type 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 type 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 type 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 type 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.
Arguments FracField.type R%type.
Notation "{ 'fraction' T }" := (FracField.type 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 tofracXn 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.
#[deprecated(since="mathcomp 1.17.0", note="Use tofracXn instead.")]
Notation tofracX := tofracXn.
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 tofracXn 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.
#[deprecated(since="mathcomp 1.17.0", note="Use tofracXn instead.")]
Notation tofracX := tofracXn.