Module mathcomp.algebra.fraction
From HB Require Import structures.From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import ssrAC generic_quotient nmodule.
From mathcomp Require Import rings_modules_and_algebras divalg.
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.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory.
Local Open Scope ring_scope.
Local Open Scope quotient_scope.
Reserved Notation "{ 'ratio' T }" (format "{ 'ratio' T }").
Reserved Notation "{ 'fraction' T }" (format "{ 'fraction' T }").
Reserved Notation "x %:F" (format "x %:F").
Section FracDomain.
Variable R : nzRingType.
Inductive ratio := mkRatio { frac :> R * R; _ : frac.2 != 0 }.
HB.instance Definition _ := [isSub for frac].
HB.instance Definition _ := [Choice of ratio by <:].
Lemma denom_ratioP : forall f : ratio, f.2 != 0
Proof.
by case. Qed.
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.
Proof.
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.
Local Notation frac := (R * R).
Local Notation dom := (ratio R).
Local Notation domP := denom_ratioP.
Implicit Types x y z : dom.
Local Notation equivf_notation x y := (\n_x * \d_y == \d_x * \n_y).
Definition equivf x y := equivf_notation x y.
Lemma equivfE x y : equivf x y = equivf_notation x y.
Proof.
by []. Qed.
Lemma equivf_refl : reflexive equivf.
Lemma equivf_sym : symmetric equivf.
Lemma equivf_trans : transitive equivf.
Proof.
Canonical equivf_equiv := EquivRel equivf equivf_refl equivf_sym equivf_trans.
Definition type := {eq_quot equivf}.
HB.instance Definition _ : EqQuotient _ equivf type := EqQuotient.on type.
HB.instance Definition _ := Choice.on type.
Lemma equivf_def (x y : ratio R) :
(x == y %[mod type]) = (\n_x * \d_y == \d_x * \n_y).
Proof.
Lemma equivf_r x : \n_x * \d_(repr (\pi_type x)) = \d_x * \n_(repr (\pi_type x)).
Proof.
Lemma equivf_l x : \n_(repr (\pi_type x)) * \d_x = \d_(repr (\pi_type x)) * \n_x.
Proof.
Lemma numer0 x : (\n_x == 0) = (x == (ratio0 R) %[mod_eq equivf]).
Lemma Ratio_numden : forall x, Ratio \n_x \d_x = x.
Proof.
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}.
Proof.
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}.
Proof.
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}.
Proof.
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}.
Proof.
Lemma addA : associative add.
Proof.
Lemma addC : commutative add.
Lemma add0_l : left_id 0%:F add.
Proof.
elim/quotW=> x; rewrite !piE /addf !numden_Ratio ?oner_eq0 //.
by rewrite mul0r mul1r mulr1 add0r Ratio_numden.
Qed.
by rewrite mul0r mul1r mulr1 add0r Ratio_numden.
Qed.
Lemma addN_l : left_inverse 0%:F opp add.
Proof.
HB.instance Definition _ := GRing.isZmodule.Build type addA addC add0_l addN_l.
Lemma mulA : associative mul.
Proof.
Lemma mulC : commutative mul.
Proof.
Lemma mul1_l : left_id 1%:F mul.
Proof.
Lemma mul_addl : left_distributive mul add.
Proof.
Lemma nonzero1 : 1%:F != 0%:F :> type.
Proof.
HB.instance Definition _ :=
GRing.Zmodule_isComNzRing.Build type mulA mulC mul1_l mul_addl nonzero1.
Lemma mulV_l : forall a, a != 0%:F -> mul (inv a) a = 1%:F.
Proof.
Lemma inv0 : inv 0%:F = 0%:F.
Proof.
HB.instance Definition _ := GRing.ComNzRing_isField.Build type mulV_l inv0.
End FracField.
End FracField.
HB.export 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.
Proof.
Local Notation tofrac := (@FracField.tofrac R).
Local Notation "x %:F" := (tofrac x).
Lemma tofrac_is_zmod_morphism: zmod_morphism tofrac.
Proof.
use=tofrac_is_zmod_morphism)]
Definition tofrac_is_additive := tofrac_is_zmod_morphism.
HB.instance Definition _ := GRing.isZmodMorphism.Build R {fraction R} tofrac
tofrac_is_zmod_morphism.
Lemma tofrac_is_monoid_morphism: monoid_morphism tofrac.
Proof.
use=tofrac_is_monoid_morphism)]
Definition tofrac_is_multiplicative := tofrac_is_monoid_morphism.
HB.instance Definition _ := GRing.isMonoidMorphism.Build R {fraction R} tofrac
tofrac_is_monoid_morphism.
Lemma tofrac0 : 0%:F = 0
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Lemma tofrac_eq (p q : R): (p%:F == q%:F) = (p == q).
Proof.
Lemma tofrac_eq0 (p : R): (p%:F == 0) = (p == 0).