(** * Division Rig *) (** Definition of an algebraic structure (F,0,1,+,*,/) where: - (F,0,+,* ) is a commutative - / is a multiplicative inverse - * distribute over + on both sides *) (** Examples of such structure : non-negative rationnal numbers, non-negative real numbers *) (** Catherine Lelay. Sep. 2015 *) Unset Kernel Term Sharing. Require Export UniMath.Foundations.Sets. Require Export UniMath.Algebra.RigsAndRings. Require Export UniMath.Algebra.Domains_and_Fields. Require Import UniMath.MoreFoundations.Tactics. (** ** Definition of a DivRig *) Definition isnonzerorig (X : rig) : UU := (1%rig : X) != 0%rig. Definition isDivRig (X : rig) : UU := isnonzerorig X × (∏ x : X, x != 0%rig -> multinvpair X x). Lemma isaprop_isDivRig (X : rig) : isaprop (isDivRig X). Proof. apply isofhleveldirprod. - now apply isapropneg. - apply impred_isaprop ; intro. apply isapropimpl. now apply isapropinvpair. Qed. Definition isDivRig_zero {X : rig} (is : isDivRig X) : X := 0%rig. Definition isDivRig_one {X : rig} (is : isDivRig X) : X := 1%rig. Definition isDivRig_plus {X : rig} (is : isDivRig X) : binop X := λ x y : X, (x + y)%rig. Definition isDivRig_mult {X : rig} (is : isDivRig X) : binop X := λ x y : X, (x * y)%rig. Definition isDivRig_inv {X : rig} (is : isDivRig X) : (∑ x : X, x != isDivRig_zero is) -> X := λ x, pr1 ((pr2 is) (pr1 x) (pr2 x)). Definition isDivRig_isassoc_plus {X : rig} (is : isDivRig X) : isassoc (isDivRig_plus is) := rigassoc1 X. Definition isDivRig_islunit_x0 {X : rig} (is : isDivRig X) : islunit (isDivRig_plus is) (isDivRig_zero is) := riglunax1 X. Definition isDivRig_isrunit_x0 {X : rig} (is : isDivRig X) : isrunit (isDivRig_plus is) (isDivRig_zero is) := rigrunax1 X. Definition isDivRig_iscomm_plus {X : rig} (is : isDivRig X) : iscomm (isDivRig_plus is) := rigcomm1 X. Definition isDivRig_isassoc_mult {X : rig} (is : isDivRig X) : isassoc (isDivRig_mult is) := rigassoc2 X. Definition isDivRig_islunit_x1 {X : rig} (is : isDivRig X) : islunit (isDivRig_mult is) (isDivRig_one is) := riglunax2 X. Definition isDivRig_isrunit_x1 {X : rig} (is : isDivRig X) : isrunit (isDivRig_mult is) (isDivRig_one is) := rigrunax2 X. Definition isDivRig_islinv {X : rig} (is : isDivRig X) : ∏ (x : X) (Hx : x != isDivRig_zero is), isDivRig_mult is (isDivRig_inv is (x,, Hx)) x = isDivRig_one is := λ (x : X) (Hx : x != isDivRig_zero is), pr1 (pr2 (pr2 is x Hx)). Definition isDivRig_isrinv {X : rig} (is : isDivRig X) : ∏ (x : X) (Hx : x != isDivRig_zero is), isDivRig_mult is x (isDivRig_inv is (x,, Hx)) = isDivRig_one is := λ (x : X) (Hx : x != isDivRig_zero is), pr2 (pr2 (pr2 is x Hx)). Definition isDivRig_isldistr {X : rig} (is : isDivRig X) : isldistr (isDivRig_plus is) (isDivRig_mult is) := rigldistr X. Definition isDivRig_isrdistr {X : rig} (is : isDivRig X) : isrdistr (isDivRig_plus is) (isDivRig_mult is) := rigrdistr X. (** DivRig *) Definition DivRig : UU := ∑ (X : rig), isDivRig X. Definition pr1DivRig (F : DivRig) : hSet := pr1 F. Coercion pr1DivRig : DivRig >-> hSet. Definition zeroDivRig {F : DivRig} : F := isDivRig_zero (pr2 F). Definition oneDivRig {F : DivRig} : F := isDivRig_one (pr2 F). Definition plusDivRig {F : DivRig} : binop F := isDivRig_plus (pr2 F). Definition multDivRig {F : DivRig} : binop F := isDivRig_mult (pr2 F). Definition invDivRig {F : DivRig} : (∑ x : F, x != zeroDivRig) -> F := isDivRig_inv (pr2 F). Definition divDivRig {F : DivRig} : F -> (∑ x : F, x != zeroDivRig) -> F := λ x y, multDivRig x (invDivRig y). Definition DivRig_isDivRig (F : DivRig) : isDivRig (pr1 F) := (pr2 F). Definition isDivRig_DivRig {X : rig} : isDivRig X -> DivRig := λ is : isDivRig X, X ,, is. Declare Scope dr_scope. Delimit Scope dr_scope with dr. Local Open Scope dr_scope. Notation "0" := zeroDivRig : dr_scope. Notation "1" := oneDivRig : dr_scope. Notation "x + y" := (plusDivRig x y) : dr_scope. Notation "x * y" := (multDivRig x y) : dr_scope. Notation "/ x" := (invDivRig x) : dr_scope. Notation "x / y" := (divDivRig x y) : dr_scope. Section DivRig_pty. Context {F : DivRig}. Definition DivRig_isassoc_plus: ∏ x y z : F, x + y + z = x + (y + z) := isDivRig_isassoc_plus (DivRig_isDivRig F). Definition DivRig_islunit_zero: ∏ x : F, 0 + x = x := isDivRig_islunit_x0 (DivRig_isDivRig F). Definition DivRig_isrunit_zero: ∏ x : F, x + 0 = x := isDivRig_isrunit_x0 (DivRig_isDivRig F). Definition DivRig_iscomm_plus: ∏ x y : F, x + y = y + x := isDivRig_iscomm_plus (DivRig_isDivRig F). Definition DivRig_isassoc_mult: ∏ x y z : F, x * y * z = x * (y * z) := isDivRig_isassoc_mult (DivRig_isDivRig F). Definition DivRig_islunit_one: ∏ x : F, 1 * x = x := isDivRig_islunit_x1 (DivRig_isDivRig F). Definition DivRig_isrunit_one: ∏ x : F, x * 1 = x := isDivRig_isrunit_x1 (DivRig_isDivRig F). Definition DivRig_islinv: ∏ (x : F) (Hx : x != 0), / (x,, Hx) * x = 1 := isDivRig_islinv (DivRig_isDivRig F). Definition DivRig_isrinv: ∏ (x : F) (Hx : x != 0), x * / (x,, Hx) = 1 := isDivRig_isrinv (DivRig_isDivRig F). Definition DivRig_isldistr: ∏ x y z : F, z * (x + y) = z * x + z * y := isDivRig_isldistr (DivRig_isDivRig F). Definition DivRig_isrdistr: ∏ x y z : F, (x + y) * z = x * z + y * z := isDivRig_isrdistr (DivRig_isDivRig F). End DivRig_pty. (** ** Definition of a Commutative DivRig *) Definition CommDivRig : UU := ∑ (X : commrig), isDivRig X. Definition CommDivRig_DivRig (F : CommDivRig) : DivRig := commrigtorig (pr1 F) ,, pr2 F. Coercion CommDivRig_DivRig : CommDivRig >-> DivRig. Section CommDivRig_pty. Local Open Scope dr_scope. Context {F : CommDivRig}. Definition CommDivRig_isassoc_plus: ∏ x y z : F, x + y + z = x + (y + z) := DivRig_isassoc_plus. Definition CommDivRig_islunit_zero: ∏ x : F, 0 + x = x := DivRig_islunit_zero. Definition CommDivRig_isrunit_zero: ∏ x : F, x + 0 = x := DivRig_isrunit_zero. Definition CommDivRig_iscomm_plus: ∏ x y : F, x + y = y + x := DivRig_iscomm_plus. Definition CommDivRig_isassoc_mult: ∏ x y z : F, x * y * z = x * (y * z) := DivRig_isassoc_mult. Definition CommDivRig_islunit_one: ∏ x : F, 1 * x = x := DivRig_islunit_one. Definition CommDivRig_isrunit_one: ∏ x : F, x * 1 = x := DivRig_isrunit_one. Definition CommDivRig_iscomm_mult: ∏ x y : F, x * y = y * x := rigcomm2 (pr1 F). Definition CommDivRig_islinv: ∏ (x : F) (Hx : x != 0), / (x,, Hx) * x = 1 := DivRig_islinv. Definition CommDivRig_isrinv: ∏ (x : F) (Hx : x != 0), x * / (x,, Hx) = 1 := DivRig_isrinv. Definition CommDivRig_isldistr: ∏ x y z : F, z * (x + y) = z * x + z * y := DivRig_isldistr. Definition CommDivRig_isrdistr: ∏ x y z : F, (x + y) * z = x * z + y * z := DivRig_isrdistr. Close Scope dr_scope. End CommDivRig_pty.