Library mathcomp.algebra.fraction
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
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 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.
Canonical ratio_subType := Eval hnf in [subType for frac].
Canonical ratio_of_subType := Eval hnf in [subType of {ratio R}].
Definition ratio_EqMixin := [eqMixin of ratio by <:].
Canonical ratio_eqType := EqType ratio ratio_EqMixin.
Canonical ratio_of_eqType := Eval hnf in [eqType of {ratio R}].
Definition ratio_ChoiceMixin := [choiceMixin of ratio by <:].
Canonical ratio_choiceType := ChoiceType ratio ratio_ChoiceMixin.
Canonical ratio_of_choiceType := Eval hnf in [choiceType of {ratio R}].
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.
Canonical ratio_subType := Eval hnf in [subType for frac].
Canonical ratio_of_subType := Eval hnf in [subType of {ratio R}].
Definition ratio_EqMixin := [eqMixin of ratio by <:].
Canonical ratio_eqType := EqType ratio ratio_EqMixin.
Canonical ratio_of_eqType := Eval hnf in [eqType of {ratio R}].
Definition ratio_ChoiceMixin := [choiceMixin of ratio by <:].
Canonical ratio_choiceType := ChoiceType ratio ratio_ChoiceMixin.
Canonical ratio_of_choiceType := Eval hnf in [choiceType of {ratio R}].
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
Canonical frac_quotType := [quotType of type].
Canonical frac_eqType := [eqType of type].
Canonical frac_choiceType := [choiceType of type].
Canonical frac_eqQuotType := [eqQuotType equivf of type].
Canonical frac_of_quotType := [quotType of {fraction R}].
Canonical frac_of_eqType := [eqType of {fraction R}].
Canonical frac_of_choiceType := [choiceType of {fraction R}].
Canonical frac_of_eqQuotType := [eqQuotType equivf of {fraction R}].
Canonical frac_eqType := [eqType of type].
Canonical frac_choiceType := [choiceType of type].
Canonical frac_eqQuotType := [eqQuotType equivf of type].
Canonical frac_of_quotType := [quotType of {fraction R}].
Canonical frac_of_eqType := [eqType of {fraction R}].
Canonical frac_of_choiceType := [choiceType of {fraction R}].
Canonical frac_of_eqQuotType := [eqQuotType equivf of {fraction R}].
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
Definition frac_zmodMixin := ZmodMixin addA addC add0_l addN_l.
Canonical frac_zmodType := Eval hnf in ZmodType type frac_zmodMixin.
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.
Canonical frac_zmodType := Eval hnf in ZmodType type frac_zmodMixin.
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.
fracions form a commutative ring
Definition frac_comRingMixin := ComRingMixin mulA mulC mul1_l mul_addl nonzero1.
Canonical frac_ringType := Eval hnf in RingType type frac_comRingMixin.
Canonical frac_comRingType := Eval hnf in ComRingType type mulC.
Lemma mulV_l : ∀ a, a != 0%:F → mul (inv a) a = 1%:F.
Lemma inv0 : inv 0%:F = 0%:F.
Canonical frac_ringType := Eval hnf in RingType type frac_comRingMixin.
Canonical frac_comRingType := Eval hnf in ComRingType type mulC.
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
Definition RatFieldUnitMixin := FieldUnitMixin mulV_l inv0.
Canonical frac_unitRingType := Eval hnf in UnitRingType type RatFieldUnitMixin.
Canonical frac_comUnitRingType := [comUnitRingType of type].
Lemma field_axiom : GRing.Field.mixin_of frac_unitRingType.
Canonical frac_unitRingType := Eval hnf in UnitRingType type RatFieldUnitMixin.
Canonical frac_comUnitRingType := [comUnitRingType of type].
Lemma field_axiom : GRing.Field.mixin_of frac_unitRingType.
fractions form a field
Definition RatFieldIdomainMixin := (FieldIdomainMixin field_axiom).
Canonical frac_idomainType :=
Eval hnf in IdomainType type (FieldIdomainMixin field_axiom).
Canonical frac_fieldType := FieldType type field_axiom.
End FracField.
End FracField.
Notation "{ 'fraction' T }" := (FracField.type_of (Phant T)).
Notation equivf := (@FracField.equivf _).
#[global] Hint Resolve denom_ratioP : core.
Section Canonicals.
Variable R : idomainType.
Canonical frac_idomainType :=
Eval hnf in IdomainType type (FieldIdomainMixin field_axiom).
Canonical frac_fieldType := FieldType type field_axiom.
End FracField.
End FracField.
Notation "{ 'fraction' T }" := (FracField.type_of (Phant T)).
Notation equivf := (@FracField.equivf _).
#[global] Hint Resolve denom_ratioP : core.
Section Canonicals.
Variable R : idomainType.
reexporting the structures
Canonical FracField.frac_quotType.
Canonical FracField.frac_eqType.
Canonical FracField.frac_choiceType.
Canonical FracField.frac_zmodType.
Canonical FracField.frac_ringType.
Canonical FracField.frac_comRingType.
Canonical FracField.frac_unitRingType.
Canonical FracField.frac_comUnitRingType.
Canonical FracField.frac_idomainType.
Canonical FracField.frac_fieldType.
Canonical FracField.tofrac_pi_morph.
Canonical frac_of_quotType := Eval hnf in [quotType of {fraction R}].
Canonical frac_of_eqType := Eval hnf in [eqType of {fraction R}].
Canonical frac_of_choiceType := Eval hnf in [choiceType of {fraction R}].
Canonical frac_of_zmodType := Eval hnf in [zmodType of {fraction R}].
Canonical frac_of_ringType := Eval hnf in [ringType of {fraction R}].
Canonical frac_of_comRingType := Eval hnf in [comRingType of {fraction R}].
Canonical frac_of_unitRingType := Eval hnf in [unitRingType of {fraction R}].
Canonical frac_of_comUnitRingType := Eval hnf in [comUnitRingType of {fraction R}].
Canonical frac_of_idomainType := Eval hnf in [idomainType of {fraction R}].
Canonical frac_of_fieldType := Eval hnf in [fieldType of {fraction R}].
End Canonicals.
Section FracFieldTheory.
Import FracField.
Variable R : idomainType.
Lemma Ratio_numden (x : {ratio R}) : Ratio \n_x \d_x = x.
Canonical FracField.frac_eqType.
Canonical FracField.frac_choiceType.
Canonical FracField.frac_zmodType.
Canonical FracField.frac_ringType.
Canonical FracField.frac_comRingType.
Canonical FracField.frac_unitRingType.
Canonical FracField.frac_comUnitRingType.
Canonical FracField.frac_idomainType.
Canonical FracField.frac_fieldType.
Canonical FracField.tofrac_pi_morph.
Canonical frac_of_quotType := Eval hnf in [quotType of {fraction R}].
Canonical frac_of_eqType := Eval hnf in [eqType of {fraction R}].
Canonical frac_of_choiceType := Eval hnf in [choiceType of {fraction R}].
Canonical frac_of_zmodType := Eval hnf in [zmodType of {fraction R}].
Canonical frac_of_ringType := Eval hnf in [ringType of {fraction R}].
Canonical frac_of_comRingType := Eval hnf in [comRingType of {fraction R}].
Canonical frac_of_unitRingType := Eval hnf in [unitRingType of {fraction R}].
Canonical frac_of_comUnitRingType := Eval hnf in [comUnitRingType of {fraction R}].
Canonical frac_of_idomainType := Eval hnf in [idomainType of {fraction R}].
Canonical frac_of_fieldType := Eval hnf in [fieldType of {fraction R}].
End Canonicals.
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}
Lemma tofrac_is_additive: additive tofrac.
Canonical tofrac_additive := Additive tofrac_is_additive.
Lemma tofrac_is_multiplicative: multiplicative tofrac.
Canonical tofrac_rmorphism := AddRMorphism tofrac_is_multiplicative.
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.