Library mathcomp.algebra.fraction
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
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).
CoInductive 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)).
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).
CoInductive 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)).
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)).
Definition type := {eq_quot equivf}.
Definition type_of of phant R := type.
Notation "{ 'fraction' T }" := (type_of (Phant T)).
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 _).
Hint Resolve denom_ratioP.
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 _).
Hint Resolve denom_ratioP.
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.