Library UniMath.Algebra.DivisionRig

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.