Library UniMath.Algebra.Groups

Algebra I. Part C. Groups, abelian groups. Vladimir Voevodsky. Aug. 2011 - .

Contents

  • Groups
    • Basic definitions
    • Univalence for groups
    • Computation lemmas for groups
    • Relations on groups
    • Subobjects
    • Quotient objects
    • Cosets
    • Normal Subgroups
    • Direct products
    • Group of invertible elements in a monoid
  • Abelian groups
    • Basic definitions
    • Univalence for abelian groups
    • Subobjects
    • Kernels
    • Quotient objects
    • Direct products
    • Abelian group of fractions of an abelian unitary monoid
    • Abelian group of fractions and abelian monoid of fractions
    • Canonical homomorphism to the abelian group of fractions
    • Abelian group of fractions in the case when all elements are cancelable
    • Relations on the abelian group of fractions
    • Relations and the canonical homomorphism to abgrdiff

Require Import UniMath.MoreFoundations.Orders.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.Subtypes.
Require Export UniMath.Algebra.BinaryOperations.
Require Export UniMath.Algebra.Monoids.

Local Open Scope logic.

Groups

Basic definitions


Definition gr : UU := total2 (λ X : setwithbinop, isgrop (@op X)).

Definition make_gr :
  ∏ (t : setwithbinop), (λ X : setwithbinop, isgrop op) t → ∑ X : setwithbinop, isgrop op :=
  tpair (λ X : setwithbinop, isgrop (@op X)).

Definition grtomonoid : gr -> monoid := λ X : _, make_monoid (pr1 X) (pr1 (pr2 X)).
Coercion grtomonoid : gr >-> monoid.

Definition grinv (X : gr) : X -> X := pr1 (pr2 (pr2 X)).

Definition grlinvax (X : gr) : islinv (@op X) (unel X) (grinv X) := pr1 (pr2 (pr2 (pr2 X))).

Definition grrinvax (X : gr) : isrinv (@op X) (unel X) (grinv X) := pr2 (pr2 (pr2 (pr2 X))).

Definition gr_of_monoid (X : monoid) (H : invstruct (@op X) (pr2 X)) : gr :=
  make_gr X (make_isgrop (pr2 X) H).

Lemma monoidfuninvtoinv {X Y : gr} (f : monoidfun X Y) (x : X) :
  f (grinv X x) = grinv Y (f x).
Show proof.
  intros.
  apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is (pr2 Y) (f x)))).
  simpl.
  change (paths (op (pr1 f (grinv X x)) (pr1 f x)) (op (grinv Y (pr1 f x)) (pr1 f x))).
  rewrite (grlinvax Y (pr1 f x)).
  destruct (pr1 (pr2 f) (grinv X x) x).
  rewrite (grlinvax X x).
  apply (pr2 (pr2 f)).

Lemma grinv_path_from_op_path {X : gr} {x y : X} (p : (x * y)%multmonoid = unel X) :
  grinv X x = y.
Show proof.
  now rewrite <- (lunax X y), <- (grlinvax X x), assocax, p, runax.

Construction of the trivial abmonoid consisting of one element given by unit.


Definition unitgr_isgrop : isgrop (@op unitmonoid).
Show proof.
  use make_isgrop.
  - exact unitmonoid_ismonoid.
  - use make_invstruct.
    + intros i. exact i.
    + use make_isinv.
      * intros x. use isProofIrrelevantUnit.
      * intros x. use isProofIrrelevantUnit.

Definition unitgr : gr := make_gr unitmonoid unitgr_isgrop.

Lemma grfuntounit_ismonoidfun (X : gr) : ismonoidfun (λ x : X, (unel unitgr)).
Show proof.
  use make_ismonoidfun.
  - use make_isbinopfun. intros x x'. use isProofIrrelevantUnit.
  - use isProofIrrelevantUnit.

Definition grfuntounit (X : gr) : monoidfun X unitgr := monoidfunconstr (grfuntounit_ismonoidfun X).

Lemma grfunfromunit_ismonoidfun (X : gr) : ismonoidfun (λ x : unitgr, (unel X)).
Show proof.
  use make_ismonoidfun.
  - use make_isbinopfun. intros x x'. use pathsinv0. use (runax X).
  - use idpath.

Definition grfunfromunit (X : gr) : monoidfun unitmonoid X :=
  monoidfunconstr (monoidfunfromunit_ismonoidfun X).

Lemma unelgrfun_ismonoidfun (X Y : gr) : ismonoidfun (λ x : X, (unel Y)).
Show proof.
  use make_ismonoidfun.
  - use make_isbinopfun. intros x x'. use pathsinv0. use lunax.
  - use idpath.

Definition unelgrfun (X Y : gr) : monoidfun X Y :=
  monoidfunconstr (unelgrfun_ismonoidfun X Y).

(X = Y) ≃ (monoidiso X Y)

The idea is to use the composition
(X = Y) ≃ (make_gr' X = make_gr' Y) ≃ ((gr'_to_monoid (make_gr' X)) = (gr'_to_monoid (make_gr' Y))) ≃ (monoidiso X Y).
The reason why we use gr' is that then we can use univalence for monoids. See gr_univalence_weq3.

Local Definition gr' : UU :=
  ∑ g : (∑ X : setwithbinop, ismonoidop (@op X)), invstruct (@op (pr1 g)) (pr2 g).

Local Definition make_gr' (X : gr) : gr' := tpair _ (tpair _ (pr1 X) (pr1 (pr2 X))) (pr2 (pr2 X)).

Local Definition gr'_to_monoid (X : gr') : monoid := pr1 X.

Definition gr_univalence_weq1 : gr ≃ gr' :=
  weqtotal2asstol
    (λ Z : setwithbinop, ismonoidop (@op Z))
    (fun y : (∑ (x : setwithbinop), ismonoidop (@op x)) => invstruct (@op (pr1 y)) (pr2 y)).

Definition gr_univalence_weq1' (X Y : gr) : (X = Y) ≃ (make_gr' X = make_gr' Y) :=
  make_weq _ (@isweqmaponpaths gr gr' gr_univalence_weq1 X Y).

Definition gr_univalence_weq2 (X Y : gr) :
  ((make_gr' X) = (make_gr' Y)) ≃ ((gr'_to_monoid (make_gr' X)) = (gr'_to_monoid (make_gr' Y))).
Show proof.
  use subtypeInjectivity.
  intros w. use isapropinvstruct.
Opaque gr_univalence_weq2.

Definition gr_univalence_weq3 (X Y : gr) :
  ((gr'_to_monoid (make_gr' X)) = (gr'_to_monoid (make_gr' Y))) ≃ (monoidiso X Y) :=
  monoid_univalence (gr'_to_monoid (make_gr' X)) (gr'_to_monoid (make_gr' Y)).

Definition gr_univalence_map (X Y : gr) : (X = Y) -> (monoidiso X Y).
Show proof.
  intro e. induction e. exact (idmonoidiso X).

Lemma gr_univalence_isweq (X Y : gr) : isweq (gr_univalence_map X Y).
Show proof.
  use isweqhomot.
  - exact (weqcomp (gr_univalence_weq1' X Y)
                   (weqcomp (gr_univalence_weq2 X Y) (gr_univalence_weq3 X Y))).
  - intros e. induction e.
    use (pathscomp0 weqcomp_to_funcomp_app).
    use weqcomp_to_funcomp_app.
  - use weqproperty.
Opaque gr_univalence_isweq.

Definition gr_univalence (X Y : gr) : (X = Y) ≃ (monoidiso X Y).
Show proof.
  use make_weq.
  - exact (gr_univalence_map X Y).
  - exact (gr_univalence_isweq X Y).
Opaque gr_univalence.

Computation lemmas for groups


Definition weqlmultingr (X : gr) (x0 : X) : pr1 X ≃ pr1 X :=
  make_weq _ (isweqlmultingr_is (pr2 X) x0).

Definition weqrmultingr (X : gr) (x0 : X) : pr1 X ≃ pr1 X :=
  make_weq _ (isweqrmultingr_is (pr2 X) x0).

Lemma grlcan (X : gr) {a b : X} (c : X) (e : paths (op c a) (op c b)) : a = b.
Show proof.
apply (invmaponpathsweq (weqlmultingr X c) _ _ e).

Lemma grrcan (X : gr) {a b : X} (c : X) (e : paths (op a c) (op b c)) : a = b.
Show proof.
apply (invmaponpathsweq (weqrmultingr X c) _ _ e).

Lemma grinvunel (X : gr) : paths (grinv X (unel X)) (unel X).
Show proof.
  apply (grrcan X (unel X)).
  rewrite (grlinvax X). rewrite (runax X).
  apply idpath.

Lemma grinvinv (X : gr) (a : X) : paths (grinv X (grinv X a)) a.
Show proof.
  apply (grlcan X (grinv X a)).
  rewrite (grlinvax X a). rewrite (grrinvax X _).
  apply idpath.

Lemma grinvmaponpathsinv (X : gr) {a b : X} (e : paths (grinv X a) (grinv X b)) : a = b.
Show proof.
  assert (e' := maponpaths (λ x, grinv X x) e).
  simpl in e'. rewrite (grinvinv X _) in e'.
  rewrite (grinvinv X _) in e'. apply e'.

Lemma grinvandmonoidfun (X Y : gr) {f : X -> Y} (is : ismonoidfun f) (x : X) :
  paths (f (grinv X x)) (grinv Y (f x)).
Show proof.
  apply (grrcan Y (f x)).
  rewrite (pathsinv0 (pr1 is _ _)). rewrite (grlinvax X).
  rewrite (grlinvax Y).
  apply (pr2 is).

Lemma grinvop (Y : gr) :
  ∏ y1 y2 : Y, grinv Y (@op Y y1 y2) = @op Y (grinv Y y2) (grinv Y y1).
Show proof.
  intros y1 y2.
  apply (grrcan Y y1).
  rewrite (assocax Y). rewrite (grlinvax Y). rewrite (runax Y).
  apply (grrcan Y y2).
  rewrite (grlinvax Y). rewrite (assocax Y). rewrite (grlinvax Y).
  apply idpath.

Relations on groups


Lemma isinvbinophrelgr (X : gr) {R : hrel X} (is : isbinophrel R) : isinvbinophrel R.
Show proof.
  set (is1 := pr1 is). set (is2 := pr2 is). split.
  - intros a b c r. set (r' := is1 _ _ (grinv X c) r).
    clearbody r'. rewrite (pathsinv0 (assocax X _ _ a)) in r'.
    rewrite (pathsinv0 (assocax X _ _ b)) in r'.
    rewrite (grlinvax X c) in r'.
    rewrite (lunax X a) in r'.
    rewrite (lunax X b) in r'.
    apply r'.
  - intros a b c r. set (r' := is2 _ _ (grinv X c) r).
    clearbody r'. rewrite ((assocax X a _ _)) in r'.
    rewrite ((assocax X b _ _)) in r'.
    rewrite (grrinvax X c) in r'.
    rewrite (runax X a) in r'.
    rewrite (runax X b) in r'.
    apply r'.
Opaque isinvbinophrelgr.

Lemma isbinophrelgr (X : gr) {R : hrel X} (is : isinvbinophrel R) : isbinophrel R.
Show proof.
  set (is1 := pr1 is). set (is2 := pr2 is). split.
  - intros a b c r. rewrite (pathsinv0 (lunax X a)) in r.
    rewrite (pathsinv0 (lunax X b)) in r.
    rewrite (pathsinv0 (grlinvax X c)) in r.
    rewrite (assocax X _ _ a) in r.
    rewrite (assocax X _ _ b) in r.
    apply (is1 _ _ (grinv X c) r).
  - intros a b c r. rewrite (pathsinv0 (runax X a)) in r.
    rewrite (pathsinv0 (runax X b)) in r.
    rewrite (pathsinv0 (grrinvax X c)) in r.
    rewrite (pathsinv0 (assocax X a _ _)) in r.
    rewrite (pathsinv0 (assocax X b _ _)) in r.
    apply (is2 _ _ (grinv X c) r).
Opaque isbinophrelgr.

Lemma grfromgtunel (X : gr) {R : hrel X} (is : isbinophrel R) {x : X} (isg : R x (unel X)) :
  R (unel X) (grinv X x).
Show proof.
  intros.
  set (r := (pr2 is) _ _ (grinv X x) isg).
  rewrite (grrinvax X x) in r.
  rewrite (lunax X _) in r.
  apply r.

Lemma grtogtunel (X : gr) {R : hrel X} (is : isbinophrel R) {x : X} (isg : R (unel X) (grinv X x)) :
  R x (unel X).
Show proof.
  assert (r := (pr2 is) _ _ x isg).
  rewrite (grlinvax X x) in r.
  rewrite (lunax X _) in r.
  apply r.

Lemma grfromltunel (X : gr) {R : hrel X} (is : isbinophrel R) {x : X} (isg : R (unel X) x) :
  R (grinv X x) (unel X).
Show proof.
  assert (r := (pr1 is) _ _ (grinv X x) isg).
  rewrite (grlinvax X x) in r.
  rewrite (runax X _) in r.
  apply r.

Lemma grtoltunel (X : gr) {R : hrel X} (is : isbinophrel R) {x : X} (isg : R (grinv X x) (unel X)) :
  R (unel X) x.
Show proof.
  assert (r := (pr1 is) _ _ x isg).
  rewrite (grrinvax X x) in r. rewrite (runax X _) in r.
  apply r.

Subobjects


Definition issubgr {X : gr} (A : hsubtype X) : UU :=
  dirprod (issubmonoid A) (∏ x : X, A x -> A (grinv X x)).

Definition make_issubgr {X : gr} {A : hsubtype X} (H1 : issubmonoid A)
           (H2 : ∏ x : X, A x -> A (grinv X x)) : issubgr A := make_dirprod H1 H2.

Lemma isapropissubgr {X : gr} (A : hsubtype X) : isaprop (issubgr A).
Show proof.
  apply (isofhleveldirprod 1).
  - apply isapropissubmonoid.
  - apply impred. intro x.
    apply impred. intro a.
    apply (pr2 (A (grinv X x))).

Definition subgr (X : gr) : UU := total2 (λ A : hsubtype X, issubgr A).

Definition make_subgr {X : gr} :
  ∏ (t : hsubtype X), (λ A : hsubtype X, issubgr A) t → ∑ A : hsubtype X, issubgr A :=
  tpair (λ A : hsubtype X, issubgr A).

Definition subgrconstr {X : gr} :
  ∏ (t : hsubtype X), (λ A : hsubtype X, issubgr A) t → ∑ A : hsubtype X, issubgr A :=
  @make_subgr X.

Definition subgrtosubmonoid (X : gr) : subgr X -> submonoid X :=
  λ A : _, make_submonoid (pr1 A) (pr1 (pr2 A)).
Coercion subgrtosubmonoid : subgr >-> submonoid.

Definition totalsubgr (X : gr) : subgr X.
Show proof.
  split with (@totalsubtype X).
  split.
  - exact (pr2 (totalsubmonoid X)).
  - exact (fun _ _ => tt).

Definition trivialsubgr (X : gr) : subgr X.
Show proof.
  exists (λ x, x = @unel X)%logic.
  split.
  - exact (pr2 (@trivialsubmonoid X)).
  - intro.
    intro eq_1.
    induction (!eq_1).
    apply grinvunel.

Lemma isinvoncarrier {X : gr} (A : subgr X) :
  isinv (@op A) (unel A) (λ a : A, make_carrier _ (grinv X (pr1 a)) (pr2 (pr2 A) (pr1 a) (pr2 a))).
Show proof.
  split.
  - intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)).
    simpl. apply (grlinvax X (pr1 a)).
  - intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)).
    simpl. apply (grrinvax X (pr1 a)).

Definition isgrcarrier {X : gr} (A : subgr X) : isgrop (@op A) :=
  tpair _ (ismonoidcarrier A)
        (tpair _ (λ a : A, make_carrier _ (grinv X (pr1 a)) (pr2 (pr2 A) (pr1 a) (pr2 a)))
               (isinvoncarrier A)).

Definition carrierofasubgr {X : gr} (A : subgr X) : gr.
Show proof.
split with A. apply (isgrcarrier A).
Coercion carrierofasubgr : subgr >-> gr.

Lemma intersection_subgr : forall {X : gr} {I : UU} (S : I -> hsubtype X)
                                  (each_is_subgr : ∏ i : I, issubgr (S i)),
    issubgr (subtype_intersection S).
Show proof.
  intros.
  use make_issubgr.
  - exact (intersection_submonoid S (λ i, (pr1 (each_is_subgr i)))).
  - exact (λ x x_in_S i, pr2 (each_is_subgr i) x (x_in_S i)).

Definition subgr_incl {X : gr} (A : subgr X) : monoidfun A X :=
submonoid_incl A.

Quotient objects


Lemma grquotinvcomp {X : gr} (R : binopeqrel X) : iscomprelrelfun R R (grinv X).
Show proof.
  destruct R as [ R isb ].
  set (isc := iscompbinoptransrel _ (eqreltrans _) isb).
  unfold iscomprelrelfun. intros x x' r.
  destruct R as [ R iseq ]. destruct iseq as [ ispo0 symm0 ].
  destruct ispo0 as [ trans0 refl0 ]. unfold isbinophrel in isb.
  set (r0 := isc _ _ _ _ (isc _ _ _ _ (refl0 (grinv X x')) r) (refl0 (grinv X x))).
  rewrite (grlinvax X x') in r0.
  rewrite (assocax X (grinv X x') x (grinv X x)) in r0.
  rewrite (grrinvax X x) in r0. rewrite (lunax X _) in r0.
  rewrite (runax X _) in r0.
  apply (symm0 _ _ r0).
Opaque grquotinvcomp.

Definition invongrquot {X : gr} (R : binopeqrel X) : setquot R -> setquot R :=
  setquotfun R R (grinv X) (grquotinvcomp R).

Lemma isinvongrquot {X : gr} (R : binopeqrel X) :
  isinv (@op (setwithbinopquot R)) (setquotpr R (unel X)) (invongrquot R).
Show proof.
  split.
  - unfold islinv.
    apply (setquotunivprop R (λ x, _ = _)).
    intro x.
    apply (@maponpaths _ _ (setquotpr R) (@op X (grinv X x) x) (unel X)).
    apply (grlinvax X).
  - unfold isrinv.
    apply (setquotunivprop R (λ x, _ = _)).
    intro x.
    apply (@maponpaths _ _ (setquotpr R) (@op X x (grinv X x)) (unel X)).
    apply (grrinvax X).
Opaque isinvongrquot.

Definition isgrquot {X : gr} (R : binopeqrel X) : isgrop (@op (setwithbinopquot R)) :=
  tpair _ (ismonoidquot R) (tpair _ (invongrquot R) (isinvongrquot R)).

Definition grquot {X : gr} (R : binopeqrel X) : gr.
Show proof.
split with (setwithbinopquot R). apply isgrquot.

Cosets


Section GrCosets.
  Context {X : gr}.

  Local Open Scope multmonoid.

  Local Lemma isaprop_mult_eq_r (x y : X) : isaprop (∑ z : X, x * z = y).
  Show proof.
    apply invproofirrelevance; intros z1 z2.
    apply subtypePath.
    { intros x'. apply setproperty. }
    refine (!lunax _ _ @ _ @ lunax _ _).
    refine (maponpaths (λ z, z * _) (!grlinvax X x) @ _ @
            maponpaths (λ z, z * _) (grlinvax X x)).
    refine (assocax _ _ _ _ @ _ @ !assocax _ _ _ _).
    refine (maponpaths _ (pr2 z1) @ _ @ !maponpaths _ (pr2 z2)).
    reflexivity.

  Local Lemma isaprop_mult_eq_l (x y : X) : isaprop (∑ z : X, z * x = y).
  Show proof.
    apply invproofirrelevance; intros z1 z2.
    apply subtypePath.
    { intros x'. apply setproperty. }
    refine (!runax _ _ @ _ @ runax _ _).
    refine (maponpaths (λ z, _ * z) (!grrinvax X x) @ _ @
            maponpaths (λ z, _ * z) (grrinvax X x)).
    refine (!assocax _ _ _ _ @ _ @ assocax _ _ _ _).
    refine (maponpaths (λ z, z * _) (pr2 z1) @ _ @ !maponpaths (λ z, z * _) (pr2 z2)).
    reflexivity.

  Context (Y : subgr X).

  Lemma isaprop_in_same_left_coset (x1 x2 : X) :
    isaprop (in_same_left_coset Y x1 x2).
  Show proof.
    unfold in_same_left_coset.
    apply invproofirrelevance; intros p q.
    apply subtypePath.
    { intros x'. apply setproperty. }
    apply subtypePath.
    { intros x'. apply propproperty. }
    pose (p' := (pr11 p,, pr2 p) : ∑ y : X, x1 * y = x2).
    pose (q' := (pr11 q,, pr2 q) : ∑ y : X, x1 * y = x2).
    apply (maponpaths pr1 (iscontrpr1 (isaprop_mult_eq_r _ _ p' q'))).

  Lemma isaprop_in_same_right_coset (x1 x2 : X) :
    isaprop (in_same_right_coset Y x1 x2).
  Show proof.
    apply invproofirrelevance.
    intros p q.
    apply subtypePath; [intros x; apply setproperty|].
    apply subtypePath; [intros x; apply propproperty|].
    pose (p' := (pr11 p,, pr2 p) : ∑ y : X, y * x1 = x2).
    pose (q' := (pr11 q,, pr2 q) : ∑ y : X, y * x1 = x2).
    apply (maponpaths pr1 (iscontrpr1 (isaprop_mult_eq_l _ _ p' q'))).

The property of being in the same coset defines an equivalence relation.

  Definition in_same_left_coset_prop : X -> X -> hProp.
  Show proof.
    intros x1 x2.
    use make_hProp.
    + exact (in_same_left_coset Y x1 x2).
    + apply isaprop_in_same_left_coset.

  Definition in_same_right_coset_prop : X -> X -> hProp.
  Show proof.
    intros x1 x2.
    use make_hProp.
    + exact (in_same_right_coset Y x1 x2).
    + apply isaprop_in_same_right_coset.

  Definition in_same_left_coset_eqrel : eqrel X.
    use make_eqrel.
    - exact in_same_left_coset_prop.
    - use iseqrelconstr.
      +
Transitivity
        intros ? ? ?; cbn; intros inxy inyz.
        unfold in_same_left_coset in *.
        use tpair.
        * exists (pr11 inxy * pr11 inyz).
          apply (pr2 Y).
        * cbn.
          refine (_ @ pr2 inyz).
          refine (_ @ maponpaths (λ z, z * _) (pr2 inxy)).
          apply pathsinv0, assocax.
      +
Reflexivity
        intro; cbn.
        use tpair.
        * exists 1; apply (pr2 Y).
        * apply runax.
      +
Symmetry
        intros x y inxy.
        use tpair.
        * exists (grinv X (pr1 (pr1 inxy))).
          apply (pr2 Y).
          exact (pr2 (pr1 inxy)).
        * cbn in *.
          refine (!maponpaths (λ z, z * _) (pr2 inxy) @ _).
          refine (assocax _ _ _ _ @ _).
          refine (maponpaths _ (grrinvax _ _) @ _).
          apply runax.
  Defined.

x₁ and x₂ are in the same Y-coset if and only if x₁⁻¹ * x₂ is in Y. (Proposition 4 in Dummit and Foote)

  Definition in_same_coset_test (x1 x2 : X) :
             (Y ((grinv _ x1) * x2)) ≃ in_same_left_coset Y x1 x2.
  Show proof.
    apply weqimplimpl; unfold in_same_left_coset in *.
    - intros yx1x2.
      exists ((grinv _ x1) * x2,, yx1x2); cbn.
      refine (!assocax X _ _ _ @ _).
      refine (maponpaths (λ z, z * _) (grrinvax X _) @ _).
      apply lunax.
    - intros y.
      use (transportf (pr1 Y)).
      + exact (pr11 y).
      + refine (_ @ maponpaths _ (pr2 y)).
        refine (_ @ assocax _ _ _ _).
        refine (_ @ !maponpaths (λ z, z * _) (grlinvax X _)).
        apply pathsinv0, lunax.
      + exact (pr2 (pr1 y)).
    - apply propproperty.
    - apply isaprop_in_same_left_coset.
End GrCosets.

Normal Subgroups


Section NormalSubGroups.
  Local Open Scope multmonoid.

  Definition isnormalsubgr {X : gr} (N : subgr X) : hProp :=
    ∀ g : X, ∀ n1 : N, N ((g * (pr1 n1)) * (grinv X g)).

  Definition normalsubgr (X : gr) : UU := ∑ N : subgr X, isnormalsubgr N.

  Definition normalsubgrtosubgr (X : gr) : normalsubgr X -> subgr X := pr1.
  Coercion normalsubgrtosubgr : normalsubgr >-> subgr.

  Definition normalsubgrprop {X : gr} (N : normalsubgr X) : isnormalsubgr N := pr2 N.

  Definition lcoset_in_rcoset {X : gr} (N : subgr X) : UU :=
    ∏ g : X, ∏ n1 : N, ∑ n2 : N, g * (pr1 n1) = (pr1 n2) * g.
  Definition lcoset_in_rcoset_witness {X : gr} {N : subgr X} :
    lcoset_in_rcoset N -> (X -> N -> N) := fun H g n1 => pr1 (H g n1).
  Definition lcoset_in_rcoset_property {X : gr} {N : subgr X}
      (H : lcoset_in_rcoset N) (g : X) (n1 : N) :
    N (pr1 (lcoset_in_rcoset_witness H g n1)) := pr2 (lcoset_in_rcoset_witness H g n1).
  Definition lcoset_in_rcoset_equation {X : gr} {N : subgr X}
      (H : lcoset_in_rcoset N) (g : X) (n1 : N) :
    g * (pr1 n1) = (pr1 (lcoset_in_rcoset_witness H g n1)) * g := pr2 (H g n1).

  Definition rcoset_in_lcoset {X : gr} (N : subgr X) : UU :=
    ∏ g : X, ∏ n1 : N, ∑ n2 : N, (pr1 n1) * g = g * (pr1 n2).
  Definition rcoset_in_lcoset_witness {X : gr} {N : subgr X} :
    rcoset_in_lcoset N -> (X -> N -> N) := fun H g n1 => pr1 (H g n1).
  Definition rcoset_in_lcoset_property {X : gr} {N : subgr X}
      (H : rcoset_in_lcoset N) (g : X) (n1 : N) :
    N (pr1 (rcoset_in_lcoset_witness H g n1)) := pr2 (rcoset_in_lcoset_witness H g n1).
  Definition rcoset_in_lcoset_equation {X : gr} {N : subgr X}
      (H : rcoset_in_lcoset N) (g : X) (n1 : N) :
    (pr1 n1) * g = g * (pr1 (rcoset_in_lcoset_witness H g n1)) := pr2 (H g n1).

  Definition lcoset_equal_rcoset {X : gr} (N : subgr X) : UU :=
    lcoset_in_rcoset N × rcoset_in_lcoset N.

  Lemma lcoset_in_rcoset_impl_normal {X : gr} (N : subgr X) :
    lcoset_in_rcoset N -> isnormalsubgr N.
  Show proof.
    intros lcinrc.
    unfold isnormalsubgr.
    intros g n1.
    refine (@transportb _ (fun x => N x) _ _ _ _).
    { etrans. { apply maponpaths_2, (lcoset_in_rcoset_equation lcinrc). }
      etrans. { apply assocax. }
      etrans. { apply maponpaths, grrinvax. }
      apply runax.
    }
    apply lcoset_in_rcoset_property.

  Lemma lcoset_equal_rcoset_impl_normal {X : gr} (N : subgr X) :
    lcoset_equal_rcoset N -> isnormalsubgr N.
  Show proof.
    intros H. apply lcoset_in_rcoset_impl_normal. exact (pr1 H).

  Lemma normal_lcoset_in_rcoset {X : gr} (N : normalsubgr X) : lcoset_in_rcoset N.
  Show proof.
    unfold normalsubgr in N.
    induction N as [N normalprop].
    simpl.
    unfold lcoset_in_rcoset.
    intros g n1.
    use tpair.
    - exact (tpair _ (g * (pr1 n1) * (grinv X g)) (normalprop g n1)).
    - simpl.
      rewrite (assocax _ _ _ g).
      rewrite (grlinvax X _).
      rewrite (runax X).
      reflexivity.

  Definition normal_rcoset_in_lcoset {X : gr} (N : normalsubgr X) : rcoset_in_lcoset N.
  Show proof.
    induction N as [N normalprop].
    simpl.
    unfold rcoset_in_lcoset.
    intros g n1.
    use tpair.
    - exists ((grinv X g) * (pr1 n1) * (grinv X (grinv X g))). use normalprop.
    - simpl.
      rewrite (assocax _ (grinv X g) _ _).
      rewrite (!assocax _ g _ _).
      rewrite (grrinvax X).
      rewrite (lunax X).
      rewrite (grinvinv X).
      reflexivity.

  Definition normal_lcoset_equal_rcoset {X : gr} (N : normalsubgr X) : lcoset_equal_rcoset N :=
    (normal_lcoset_in_rcoset N,,normal_rcoset_in_lcoset N).

  Lemma in_same_coset_isbinophrel {X : gr} (N : normalsubgr X) :
    isbinophrel (in_same_left_coset_eqrel N).
  Show proof.
    unfold isbinophrel.
    split.
    - intros a b c.
      unfold in_same_left_coset_eqrel.
      simpl.
      unfold in_same_left_coset.
      intros ab_same_lcoset.
      use tpair.
      + exact (pr1 ab_same_lcoset).
      + simpl.
        rewrite (assocax _ c _ _).
        apply maponpaths.
        exact (pr2 ab_same_lcoset).
    - intros a b c.
      unfold in_same_left_coset_eqrel.
      simpl.
      unfold in_same_left_coset.
      intros ab_same_lcoset.
      use tpair.
      + refine (rcoset_in_lcoset_witness _ c (pr1 ab_same_lcoset));
          apply normal_rcoset_in_lcoset.
      + simpl.
        rewrite (grinvinv _).
        rewrite (assocax _ a _ _).
        rewrite (assocax _ (grinv X c) _ _).
        rewrite (!assocax _ c _ _).
        rewrite (grrinvax _).
        rewrite (lunax _).
        rewrite (!assocax _ a _ _).
        apply maponpaths_2.
        exact (pr2 ab_same_lcoset).

  Definition in_same_coset_binopeqrel {X : gr} (N : normalsubgr X) : binopeqrel X :=
    tpair _ (in_same_left_coset_eqrel N) (in_same_coset_isbinophrel N).

  Definition grquot_by_normal_subgr (X : gr) (N : normalsubgr X) : gr :=
    grquot (in_same_coset_binopeqrel N).

End NormalSubGroups.

Direct products


Lemma isgrdirprod (X Y : gr) : isgrop (@op (setwithbinopdirprod X Y)).
Show proof.
  split with (ismonoiddirprod X Y).
  split with (λ xy : _, make_dirprod (grinv X (pr1 xy)) (grinv Y (pr2 xy))).
  split.
  - intro xy. destruct xy as [ x y ].
    unfold unel_is. simpl. apply pathsdirprod.
    apply (grlinvax X x). apply (grlinvax Y y).
  - intro xy. destruct xy as [ x y ].
    unfold unel_is. simpl. apply pathsdirprod.
    apply (grrinvax X x). apply (grrinvax Y y).

Definition grdirprod (X Y : gr) : gr.
Show proof.
split with (setwithbinopdirprod X Y). apply isgrdirprod.

Group of invertible elements in a monoid


Local Open Scope multmonoid.

Definition invertible_submonoid_grop X : isgrop (@op (invertible_submonoid X)).
Show proof.
  pose (submon := invertible_submonoid X).
  pose (submon_carrier := ismonoidcarrier submon).

We know that if each element has an inverse, it's a grop
  apply (isgropif submon_carrier).

  intros xpair.
  pose (x := pr1 xpair).
  pose (unel := (unel_is submon_carrier)).

We can use other hProps when proving an hProp (assume it has an inverse)
  apply (squash_to_prop (pr2 xpair) (propproperty _)).

  intros xinv.
  unfold haslinv.
  apply hinhpr.
  refine ((pr1 xinv,, inverse_in_submonoid _ x (pr1 xinv) (pr2 xpair) (pr2 xinv)),, _).
  apply subtypePath_prop.
  exact (pr2 (pr2 xinv)).

Local Close Scope multmonoid.

Definition gr_merely_invertible_elements : monoid -> gr :=
  fun X => (carrierofasubsetwithbinop
             (submonoidtosubsetswithbinop
                _ (invertible_submonoid X)),, invertible_submonoid_grop X).

Abelian groups

Basic definitions


Definition abgr : UU := total2 (λ X : setwithbinop, isabgrop (@op X)).

Definition make_abgr (X : setwithbinop) (is : isabgrop (@op X)) : abgr :=
  tpair (λ X : setwithbinop, isabgrop (@op X)) X is.

Definition abgrconstr (X : abmonoid) (inv0 : X -> X) (is : isinv (@op X) (unel X) inv0) : abgr :=
  make_abgr X (make_dirprod (make_isgrop (pr2 X) (tpair _ inv0 is)) (commax X)).

Definition abgrtogr : abgr -> gr := λ X : _, make_gr (pr1 X) (pr1 (pr2 X)).
Coercion abgrtogr : abgr >-> gr.

Definition abgrtoabmonoid : abgr -> abmonoid :=
  λ X : _, make_abmonoid (pr1 X) (make_dirprod (pr1 (pr1 (pr2 X))) (pr2 (pr2 X))).
Coercion abgrtoabmonoid : abgr >-> abmonoid.

Definition abgr_of_gr (X : gr) (H : iscomm (@op X)) : abgr :=
  make_abgr X (make_isabgrop (pr2 X) H).

Declare Scope abgr.
Delimit Scope abgr with abgr.
Notation "x - y" := (op x (grinv _ y)) : abgr.
Notation "- y" := (grinv _ y) : abgr.

Construction of the trivial abgr consisting of one element given by unit.


Definition unitabgr_isabgrop : isabgrop (@op unitabmonoid).
Show proof.
  use make_isabgrop.
  - exact unitgr_isgrop.
  - exact (commax unitabmonoid).

Definition unitabgr : abgr := make_abgr unitabmonoid unitabgr_isabgrop.

Lemma abgrfuntounit_ismonoidfun (X : abgr) : ismonoidfun (λ x : X, (unel unitabgr)).
Show proof.
  use make_ismonoidfun.
  - use make_isbinopfun. intros x x'. use isProofIrrelevantUnit.
  - use isProofIrrelevantUnit.

Definition abgrfuntounit (X : abgr) : monoidfun X unitabgr :=
  monoidfunconstr (abgrfuntounit_ismonoidfun X).

Lemma abgrfunfromunit_ismonoidfun (X : abgr) : ismonoidfun (λ x : unitabgr, (unel X)).
Show proof.
  use make_ismonoidfun.
  - use make_isbinopfun. intros x x'. use pathsinv0. use (runax X).
  - use idpath.

Definition abgrfunfromunit (X : abgr) : monoidfun unitabgr X :=
  monoidfunconstr (abgrfunfromunit_ismonoidfun X).

Lemma unelabgrfun_ismonoidfun (X Y : abgr) : ismonoidfun (λ x : X, (unel Y)).
Show proof.
  use make_ismonoidfun.
  - use make_isbinopfun. intros x x'. use pathsinv0. use lunax.
  - use idpath.

Definition unelabgrfun (X Y : abgr) : monoidfun X Y :=
  monoidfunconstr (unelgrfun_ismonoidfun X Y).

Abelian group structure on morphism between abelian groups


Definition abgrshombinop_inv_ismonoidfun {X Y : abgr} (f : monoidfun X Y) :
  ismonoidfun (λ x : X, grinv Y (pr1 f x)).
Show proof.
  use make_ismonoidfun.
  - use make_isbinopfun. intros x x'. cbn.
    rewrite (pr1 (pr2 f)). rewrite (pr2 (pr2 Y)). use (grinvop Y).
  - use (pathscomp0 (maponpaths (λ y : Y, grinv Y y) (monoidfununel f))).
    use grinvunel.

Definition abgrshombinop_inv {X Y : abgr} (f : monoidfun X Y) : monoidfun X Y :=
  monoidfunconstr (abgrshombinop_inv_ismonoidfun f).

Definition abgrshombinop_linvax {X Y : abgr} (f : monoidfun X Y) :
  @abmonoidshombinop X Y (abgrshombinop_inv f) f = unelmonoidfun X Y.
Show proof.
  use monoidfun_paths. use funextfun. intros x. use (@grlinvax Y).

Definition abgrshombinop_rinvax {X Y : abgr} (f : monoidfun X Y) :
  @abmonoidshombinop X Y f (abgrshombinop_inv f) = unelmonoidfun X Y.
Show proof.
  use monoidfun_paths. use funextfun. intros x. use (grrinvax Y).

Lemma abgrshomabgr_isabgrop (X Y : abgr) :
  @isabgrop (abmonoidshomabmonoid X Y) (λ f g : monoidfun X Y, @abmonoidshombinop X Y f g).
Show proof.
  use make_isabgrop.
  - use make_isgrop.
    + exact (abmonoidshomabmonoid_ismonoidop X Y).
    + use make_invstruct.
      * intros f. exact (abgrshombinop_inv f).
      * use make_isinv.
          intros f. exact (abgrshombinop_linvax f).
          intros f. exact (abgrshombinop_rinvax f).
  - intros f g. exact (abmonoidshombinop_comm f g).

Definition abgrshomabgr (X Y : abgr) : abgr.
Show proof.
  use make_abgr.
  - exact (abmonoidshomabmonoid X Y).
  - exact (abgrshomabgr_isabgrop X Y).

(X = Y) ≃ (monoidiso X Y)

The idea is to use the following composition
(X = Y) ≃ (make_abgr' X = make_abgr' Y) ≃ (pr1 (make_abgr' X) = pr1 (make_abgr' Y)) ≃ (monoidiso X Y)
We use abgr' so that we can use univalence for groups, gr_univalence. See abgr_univalence_weq3.

Local Definition abgr' : UU :=
  ∑ g : (∑ X : setwithbinop, isgrop (@op X)), iscomm (pr2 (pr1 g)).

Local Definition make_abgr' (X : abgr) : abgr' :=
  tpair _ (tpair _ (pr1 X) (dirprod_pr1 (pr2 X))) (dirprod_pr2 (pr2 X)).

Local Definition abgr_univalence_weq1 : abgr ≃ abgr' :=
  weqtotal2asstol (λ Z : setwithbinop, isgrop (@op Z))
                  (fun y : (∑ x : setwithbinop, isgrop (@op x)) => iscomm (@op (pr1 y))).

Definition abgr_univalence_weq1' (X Y : abgr) : (X = Y) ≃ (make_abgr' X = make_abgr' Y) :=
  make_weq _ (@isweqmaponpaths abgr abgr' abgr_univalence_weq1 X Y).

Definition abgr_univalence_weq2 (X Y : abgr) :
  (make_abgr' X = make_abgr' Y) ≃ (pr1 (make_abgr' X) = pr1 (make_abgr' Y)).
Show proof.
  use subtypeInjectivity.
  intros w. use isapropiscomm.
Opaque abgr_univalence_weq2.

Definition abgr_univalence_weq3 (X Y : abgr) :
  (pr1 (make_abgr' X) = pr1 (make_abgr' Y)) ≃ (monoidiso X Y) :=
  gr_univalence (pr1 (make_abgr' X)) (pr1 (make_abgr' Y)).

Definition abgr_univalence_map (X Y : abgr) : (X = Y) -> (monoidiso X Y).
Show proof.
  intro e. induction e. exact (idmonoidiso X).

Lemma abgr_univalence_isweq (X Y : abgr) : isweq (abgr_univalence_map X Y).
Show proof.
  use isweqhomot.
  - exact (weqcomp (abgr_univalence_weq1' X Y)
                   (weqcomp (abgr_univalence_weq2 X Y) (abgr_univalence_weq3 X Y))).
  - intros e. induction e.
    use (pathscomp0 weqcomp_to_funcomp_app).
    use weqcomp_to_funcomp_app.
  - use weqproperty.
Opaque abgr_univalence_isweq.

Definition abgr_univalence (X Y : abgr) : (X = Y) ≃ (monoidiso X Y).
Show proof.
  use make_weq.
  - exact (abgr_univalence_map X Y).
  - exact (abgr_univalence_isweq X Y).
Opaque abgr_univalence.

Subobjects


Definition subabgr (X : abgr) := subgr X.
Identity Coercion id_subabgr : subabgr >-> subgr.

Lemma isabgrcarrier {X : abgr} (A : subgr X) : isabgrop (@op A).
Show proof.
  split with (isgrcarrier A).
  apply (pr2 (@isabmonoidcarrier X A)).

Definition carrierofasubabgr {X : abgr} (A : subabgr X) : abgr.
Show proof.
split with A. apply isabgrcarrier.
Coercion carrierofasubabgr : subabgr >-> abgr.

Definition subabgr_incl {X : abgr} (A : subabgr X) : monoidfun A X :=
  submonoid_incl A.

Definition abgr_kernel_hsubtype {A B : abgr} (f : monoidfun A B) : hsubtype A :=
  monoid_kernel_hsubtype f.

Definition abgr_image_hsubtype {A B : abgr} (f : monoidfun A B) : hsubtype B :=
  (λ y : B, ∃ x : A, (f x) = y).

Kernels

Let f : X -> Y be a morphism of abelian groups. A kernel of f is given by the subgroup of X consisting of elements x such that f x = unel Y.

Kernel as abelian group


Definition abgr_Kernel_subabgr_issubgr {A B : abgr} (f : monoidfun A B) :
  issubgr (abgr_kernel_hsubtype f).
Show proof.
  use make_issubgr.
  - apply kernel_issubmonoid.
  - intros x a.
    apply (grrcan B (f x)).
    apply (pathscomp0 (! (binopfunisbinopfun f (grinv A x) x))).
    apply (pathscomp0 (maponpaths (λ a : A, f a) (grlinvax A x))).
    apply (pathscomp0 (monoidfununel f)).
    apply pathsinv0.
    apply (pathscomp0 (lunax B (f x))).
    exact a.

Definition abgr_Kernel_subabgr {A B : abgr} (f : monoidfun A B) : @subabgr A :=
  subgrconstr (@abgr_kernel_hsubtype A B f) (abgr_Kernel_subabgr_issubgr f).

The inclusion Kernel f --> X is a morphism of abelian groups


Definition abgr_Kernel_monoidfun_ismonoidfun {A B : abgr} (f : monoidfun A B) :
  @ismonoidfun (abgr_Kernel_subabgr f) A
               (make_incl (pr1carrier (abgr_kernel_hsubtype f))
                         (isinclpr1carrier (abgr_kernel_hsubtype f))).
Show proof.
  use make_ismonoidfun.
  - use make_isbinopfun. intros x x'. use idpath.
  - use idpath.

Image of f is a subgroup


Definition abgr_image_issubgr {A B : abgr} (f : monoidfun A B) : issubgr (abgr_image_hsubtype f).
Show proof.
  use make_issubgr.
  - use make_issubmonoid.
    + intros a a'.
      use (hinhuniv _ (pr2 a)). intros ae.
      use (hinhuniv _ (pr2 a')). intros a'e.
      use hinhpr.
      use tpair.
      * exact (@op A (pr1 ae) (pr1 a'e)).
      * use (pathscomp0 (binopfunisbinopfun f (pr1 ae) (pr1 a'e))).
        use two_arg_paths.
          exact (pr2 ae).
          exact (pr2 a'e).
    + use hinhpr. use tpair.
      * exact (unel A).
      * exact (monoidfununel f).
  - intros b b'.
    use (hinhuniv _ b'). intros eb.
    use hinhpr.
    use tpair.
    + exact (grinv A (pr1 eb)).
    + use (pathscomp0 _ (maponpaths (λ bb : B, (grinv B bb)) (pr2 eb))).
      use monoidfuninvtoinv.

Definition abgr_image {A B : abgr} (f : monoidfun A B) : @subabgr B :=
  @subgrconstr B (@abgr_image_hsubtype A B f) (abgr_image_issubgr f).

Quotient objects


Lemma isabgrquot {X : abgr} (R : binopeqrel X) : isabgrop (@op (setwithbinopquot R)).
Show proof.
  split with (isgrquot R).
  apply (pr2 (@isabmonoidquot X R)).

Definition abgrquot {X : abgr} (R : binopeqrel X) : abgr.
Show proof.
split with (setwithbinopquot R). apply isabgrquot.

Direct products


Lemma isabgrdirprod (X Y : abgr) : isabgrop (@op (setwithbinopdirprod X Y)).
Show proof.
  split with (isgrdirprod X Y).
  apply (pr2 (isabmonoiddirprod X Y)).

Definition abgrdirprod (X Y : abgr) : abgr.
Show proof.
  split with (setwithbinopdirprod X Y).
  apply isabgrdirprod.

Abelian group of fractions of an abelian unitary monoid


Section Fractions.
Import UniMath.Algebra.Monoids.AddNotation.
Local Open Scope addmonoid.

Definition hrelabgrdiff (X : abmonoid) : hrel (X × X) :=
  λ xa1 xa2,
    hexists (λ x0 : X, paths (((pr1 xa1) + (pr2 xa2)) + x0) (((pr1 xa2) + (pr2 xa1)) + x0)).

Definition abgrdiffphi (X : abmonoid) (xa : dirprod X X) :
  dirprod X (totalsubtype X) := make_dirprod (pr1 xa) (make_carrier (λ x : X, htrue) (pr2 xa) tt).

Definition hrelabgrdiff' (X : abmonoid) : hrel (X × X) :=
  λ xa1 xa2, eqrelabmonoidfrac X (totalsubmonoid X) (abgrdiffphi X xa1) (abgrdiffphi X xa2).

Lemma logeqhrelsabgrdiff (X : abmonoid) : hrellogeq (hrelabgrdiff' X) (hrelabgrdiff X).
Show proof.
  split. simpl. apply hinhfun. intro t2.
  set (a0 := pr1 (pr1 t2)). split with a0. apply (pr2 t2). simpl.
  apply hinhfun. intro t2. set (x0 := pr1 t2). split with (tpair _ x0 tt).
  apply (pr2 t2).

Lemma iseqrelabgrdiff (X : abmonoid) : iseqrel (hrelabgrdiff X).
Show proof.
  apply (iseqrellogeqf (logeqhrelsabgrdiff X)).
  apply (iseqrelconstr).
  intros xx' xx'' xx'''.
  intros r1 r2.
  apply (eqreltrans (eqrelabmonoidfrac X (totalsubmonoid X)) _ _ _ r1 r2).
  intro xx. apply (eqrelrefl (eqrelabmonoidfrac X (totalsubmonoid X)) _).
  intros xx xx'. intro r.
  apply (eqrelsymm (eqrelabmonoidfrac X (totalsubmonoid X)) _ _ r).
Opaque iseqrelabgrdiff.

Definition eqrelabgrdiff (X : abmonoid) : @eqrel (abmonoiddirprod X X) :=
  make_eqrel _ (iseqrelabgrdiff X).

Lemma isbinophrelabgrdiff (X : abmonoid) : @isbinophrel (abmonoiddirprod X X) (hrelabgrdiff X).
Show proof.
  apply (@isbinophrellogeqf (abmonoiddirprod X X) _ _ (logeqhrelsabgrdiff X)).
  split. intros a b c r.
  apply (pr1 (isbinophrelabmonoidfrac X (totalsubmonoid X)) _ _
             (make_dirprod (pr1 c) (make_carrier (λ x : X, htrue) (pr2 c) tt))
             r).
  intros a b c r.
  apply (pr2 (isbinophrelabmonoidfrac X (totalsubmonoid X)) _ _
             (make_dirprod (pr1 c) (make_carrier (λ x : X, htrue) (pr2 c) tt))
             r).
Opaque isbinophrelabgrdiff.

Definition binopeqrelabgrdiff (X : abmonoid) : binopeqrel (abmonoiddirprod X X) :=
  make_binopeqrel (eqrelabgrdiff X) (isbinophrelabgrdiff X).

Definition abgrdiffcarrier (X : abmonoid) : abmonoid := @abmonoidquot (abmonoiddirprod X X)
                                                                      (binopeqrelabgrdiff X).

Definition abgrdiffinvint (X : abmonoid) : dirprod X X -> dirprod X X :=
  λ xs : _, make_dirprod (pr2 xs) (pr1 xs).

Lemma abgrdiffinvcomp (X : abmonoid) :
  iscomprelrelfun (hrelabgrdiff X) (eqrelabgrdiff X) (abgrdiffinvint X).
Show proof.
  unfold iscomprelrelfun. unfold eqrelabgrdiff. unfold hrelabgrdiff.
  unfold eqrelabmonoidfrac. unfold hrelabmonoidfrac. simpl. intros xs xs'.
  apply (hinhfun). intro tt0.
  set (x := pr1 xs). set (s := pr2 xs).
  set (x' := pr1 xs'). set (s' := pr2 xs').
  split with (pr1 tt0).
  destruct tt0 as [ a eq ]. change (paths (s + x' + a) (s' + x + a)).
  apply pathsinv0. simpl.
  set(e := commax X s' x). simpl in e. rewrite e. clear e.
  set (e := commax X s x'). simpl in e. rewrite e. clear e.
  apply eq.
Opaque abgrdiffinvcomp.

Definition abgrdiffinv (X : abmonoid) : abgrdiffcarrier X -> abgrdiffcarrier X :=
  setquotfun (hrelabgrdiff X) (eqrelabgrdiff X) (abgrdiffinvint X) (abgrdiffinvcomp X).

Lemma abgrdiffisinv (X : abmonoid) :
  isinv (@op (abgrdiffcarrier X)) (unel (abgrdiffcarrier X)) (abgrdiffinv X).
Show proof.
  set (R := eqrelabgrdiff X).
  assert (isl : islinv (@op (abgrdiffcarrier X)) (unel (abgrdiffcarrier X)) (abgrdiffinv X)).
  {
    unfold islinv.
    apply (setquotunivprop R (λ x, _ = _)).
    intro xs.
    set (x := pr1 xs). set (s := pr2 xs).
    apply (iscompsetquotpr R (@op (abmonoiddirprod X X) (abgrdiffinvint X xs) xs) (unel _)).
    simpl. apply hinhpr. split with (unel X).
    change (paths (s + x + (unel X) + (unel X)) ((unel X) + (x + s) + (unel X))).
    destruct (commax X x s). destruct (commax X (unel X) (x + s)).
    apply idpath.
  }
  apply (make_dirprod isl (weqlinvrinv (@op (abgrdiffcarrier X)) (commax (abgrdiffcarrier X))
                                      (unel (abgrdiffcarrier X)) (abgrdiffinv X) isl)).
Opaque abgrdiffisinv.

Definition abgrdiff (X : abmonoid) : abgr := abgrconstr (abgrdiffcarrier X) (abgrdiffinv X)
                                                        (abgrdiffisinv X).

Definition prabgrdiff (X : abmonoid) : X -> X -> abgrdiff X :=
  λ x x' : X, setquotpr (eqrelabgrdiff X) (make_dirprod x x').

Abelian group of fractions and abelian monoid of fractions


Definition weqabgrdiffint (X : abmonoid) : weq (X × X) (dirprod X (totalsubtype X)) :=
  weqdirprodf (idweq X) (invweq (weqtotalsubtype X)).

Definition weqabgrdiff (X : abmonoid) : weq (abgrdiff X) (abmonoidfrac X (totalsubmonoid X)).
Show proof.
  intros.
  apply (weqsetquotweq (eqrelabgrdiff X)
                       (eqrelabmonoidfrac X (totalsubmonoid X)) (weqabgrdiffint X)).
  - simpl. intros x x'. destruct x as [ x1 x2 ]. destruct x' as [ x1' x2' ].
    simpl in *. apply hinhfun. intro tt0. destruct tt0 as [ xx0 is0 ].
    split with (make_carrier (λ x : X, htrue) xx0 tt). apply is0.
  - simpl. intros x x'. destruct x as [ x1 x2 ]. destruct x' as [ x1' x2' ].
    simpl in *. apply hinhfun. intro tt0. destruct tt0 as [ xx0 is0 ].
    split with (pr1 xx0). apply is0.

Canonical homomorphism to the abelian group of fractions


Definition toabgrdiff (X : abmonoid) (x : X) : abgrdiff X := setquotpr _ (make_dirprod x (unel X)).

Lemma isbinopfuntoabgrdiff (X : abmonoid) : isbinopfun (toabgrdiff X).
Show proof.
  unfold isbinopfun. intros x1 x2.
  change (paths (setquotpr _ (make_dirprod (x1 + x2) (unel X)))
                (setquotpr (eqrelabgrdiff X) (make_dirprod (x1 + x2) ((unel X) + (unel X))))).
  apply (maponpaths (setquotpr _)).
  apply (@pathsdirprod X X).
  apply idpath.
  apply (pathsinv0 (lunax X 0)).

Lemma isunitalfuntoabgrdiff (X : abmonoid) : paths (toabgrdiff X (unel X)) (unel (abgrdiff X)).
Show proof.
apply idpath.

Definition ismonoidfuntoabgrdiff (X : abmonoid) : ismonoidfun (toabgrdiff X) :=
  make_dirprod (isbinopfuntoabgrdiff X) (isunitalfuntoabgrdiff X).

Abelian group of fractions in the case when all elements are cancelable


Lemma isinclprabgrdiff (X : abmonoid) (iscanc : ∏ x : X, isrcancelable (@op X) x) :
  ∏ x' : X, isincl (λ x, prabgrdiff X x x').
Show proof.
  intros.
  set (int := isinclprabmonoidfrac X (totalsubmonoid X) (λ a : totalsubmonoid X, iscanc (pr1 a))
                                   (make_carrier (λ x : X, htrue) x' tt)).
  set (int1 := isinclcomp (make_incl _ int) (weqtoincl (invweq (weqabgrdiff X)))).
  apply int1.

Definition isincltoabgrdiff (X : abmonoid) (iscanc : ∏ x : X, isrcancelable (@op X) x) :
  isincl (toabgrdiff X) := isinclprabgrdiff X iscanc (unel X).

Lemma isdeceqabgrdiff (X : abmonoid) (iscanc : ∏ x : X, isrcancelable (@op X) x) (is : isdeceq X) :
  isdeceq (abgrdiff X).
Show proof.
  intros.
  apply (isdeceqweqf (invweq (weqabgrdiff X))).
  apply (isdeceqabmonoidfrac X (totalsubmonoid X) (λ a : totalsubmonoid X, iscanc (pr1 a)) is).

Relations on the abelian group of fractions


Definition abgrdiffrelint (X : abmonoid) (L : hrel X) : hrel (setwithbinopdirprod X X) :=
  λ xa yb, hexists (λ c0 : X, L (((pr1 xa) + (pr2 yb)) + c0) (((pr1 yb) + (pr2 xa)) + c0)).

Definition abgrdiffrelint' (X : abmonoid) (L : hrel X) : hrel (setwithbinopdirprod X X) :=
  λ xa1 xa2, abmonoidfracrelint _ (totalsubmonoid X) L (abgrdiffphi X xa1) (abgrdiffphi X xa2).

Lemma logeqabgrdiffrelints (X : abmonoid) (L : hrel X) :
  hrellogeq (abgrdiffrelint' X L) (abgrdiffrelint X L).
Show proof.
  split. unfold abgrdiffrelint. unfold abgrdiffrelint'.
  simpl. apply hinhfun. intro t2. set (a0 := pr1 (pr1 t2)).
  split with a0. apply (pr2 t2). simpl. apply hinhfun.
  intro t2. set (x0 := pr1 t2). split with (tpair _ x0 tt). apply (pr2 t2).

Lemma iscomprelabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) :
  iscomprelrel (eqrelabgrdiff X) (abgrdiffrelint X L).
Show proof.
  apply (iscomprelrellogeqf1 _ (logeqhrelsabgrdiff X)).
  apply (iscomprelrellogeqf2 _ (logeqabgrdiffrelints X L)).
  intros x x' x0 x0' r r0.
  apply (iscomprelabmonoidfracrelint
           _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is) _ _ _ _ r r0).
Opaque iscomprelabgrdiffrelint.

Definition abgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) :=
  quotrel (iscomprelabgrdiffrelint X is).

Definition abgrdiffrel' (X : abmonoid) {L : hrel X} (is : isbinophrel L) : hrel (abgrdiff X) :=
  λ x x', abmonoidfracrel X (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
                           (weqabgrdiff X x) (weqabgrdiff X x').

Definition logeqabgrdiffrels (X : abmonoid) {L : hrel X} (is : isbinophrel L) :
  hrellogeq (abgrdiffrel' X is) (abgrdiffrel X is).
Show proof.
  intros x1 x2. split.
  - assert (int : ∏ x x', isaprop (abgrdiffrel' X is x x' -> abgrdiffrel X is x x')).
    {
      intros x x'.
      apply impred. intro.
      apply (pr2 _).
    }
    generalize x1 x2. clear x1 x2.
    apply (setquotuniv2prop _ (λ x x', make_hProp _ (int x x'))).
    intros x x'.
    change ((abgrdiffrelint' X L x x') -> (abgrdiffrelint _ L x x')).
    apply (pr1 (logeqabgrdiffrelints X L x x')).
  - assert (int : ∏ x x', isaprop (abgrdiffrel X is x x' -> abgrdiffrel' X is x x')).
    intros x x'.
    apply impred. intro.
    apply (pr2 _).
    generalize x1 x2. clear x1 x2.
    apply (setquotuniv2prop _ (λ x x', make_hProp _ (int x x'))).
    intros x x'.
    change ((abgrdiffrelint X L x x') -> (abgrdiffrelint' _ L x x')).
    apply (pr2 (logeqabgrdiffrelints X L x x')).

Lemma istransabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : istrans L) :
  istrans (abgrdiffrelint X L).
Show proof.
  apply (istranslogeqf (logeqabgrdiffrelints X L)).
  intros a b c rab rbc.
  apply (istransabmonoidfracrelint
           _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is) isl _ _ _ rab rbc).
Opaque istransabgrdiffrelint.

Lemma istransabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : istrans L) :
  istrans (abgrdiffrel X is).
Show proof.
  refine (istransquotrel _ _). apply istransabgrdiffrelint.
  - apply is.
  - apply isl.

Lemma issymmabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : issymm L) :
  issymm (abgrdiffrelint X L).
Show proof.
  apply (issymmlogeqf (logeqabgrdiffrelints X L)).
  intros a b rab.
  apply (issymmabmonoidfracrelint _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is) isl _ _ rab).
Opaque issymmabgrdiffrelint.

Lemma issymmabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : issymm L) :
  issymm (abgrdiffrel X is).
Show proof.
  refine (issymmquotrel _ _). apply issymmabgrdiffrelint.
  - apply is.
  - apply isl.

Lemma isreflabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : isrefl L) :
  isrefl (abgrdiffrelint X L).
Show proof.
  intro xa. unfold abgrdiffrelint. simpl.
  apply hinhpr. split with (unel X). apply (isl _).

Lemma isreflabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : isrefl L) :
  isrefl (abgrdiffrel X is).
Show proof.
  refine (isreflquotrel _ _). apply isreflabgrdiffrelint.
  - apply is.
  - apply isl.

Lemma ispoabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : ispreorder L) :
  ispreorder (abgrdiffrelint X L).
Show proof.
  split with (istransabgrdiffrelint X is (pr1 isl)).
  apply (isreflabgrdiffrelint X is (pr2 isl)).

Lemma ispoabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : ispreorder L) :
  ispreorder (abgrdiffrel X is).
Show proof.
  refine (ispoquotrel _ _). apply ispoabgrdiffrelint.
  - apply is.
  - apply isl.

Lemma iseqrelabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : iseqrel L) :
  iseqrel (abgrdiffrelint X L).
Show proof.
  split with (ispoabgrdiffrelint X is (pr1 isl)).
  apply (issymmabgrdiffrelint X is (pr2 isl)).

Lemma iseqrelabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : iseqrel L) :
  iseqrel (abgrdiffrel X is).
Show proof.
  refine (iseqrelquotrel _ _). apply iseqrelabgrdiffrelint.
  - apply is.
  - apply isl.

Lemma isantisymmnegabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L)
      (isl : isantisymmneg L) : isantisymmneg (abgrdiffrel X is).
Show proof.
  apply (isantisymmneglogeqf (logeqabgrdiffrels X is)).
  intros a b rab rba.
  set (int := isantisymmnegabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
                                           isl (weqabgrdiff X a) (weqabgrdiff X b) rab rba).
  apply (invmaponpathsweq _ _ _ int).

Lemma isantisymmabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : isantisymm L) :
  isantisymm (abgrdiffrel X is).
Show proof.
  apply (isantisymmlogeqf (logeqabgrdiffrels X is)).
  intros a b rab rba.
  set (int := isantisymmabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
                                        isl (weqabgrdiff X a) (weqabgrdiff X b) rab rba).
  apply (invmaponpathsweq _ _ _ int).
Opaque isantisymmabgrdiffrel.

Lemma isirreflabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : isirrefl L) :
  isirrefl (abgrdiffrel X is).
Show proof.
  apply (isirrefllogeqf (logeqabgrdiffrels X is)).
  intros a raa.
  apply (isirreflabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
                                 isl (weqabgrdiff X a) raa).
Opaque isirreflabgrdiffrel.

Lemma isasymmabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : isasymm L) :
  isasymm (abgrdiffrel X is).
Show proof.
  apply (isasymmlogeqf (logeqabgrdiffrels X is)).
  intros a b rab rba.
  apply (isasymmabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
                                isl (weqabgrdiff X a) (weqabgrdiff X b) rab rba).
Opaque isasymmabgrdiffrel.

Lemma iscoasymmabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : iscoasymm L) :
  iscoasymm (abgrdiffrel X is).
Show proof.
  apply (iscoasymmlogeqf (logeqabgrdiffrels X is)).
  intros a b rab.
  apply (iscoasymmabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
                                  isl (weqabgrdiff X a) (weqabgrdiff X b) rab).
Opaque iscoasymmabgrdiffrel.

Lemma istotalabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : istotal L) :
  istotal (abgrdiffrel X is).
Show proof.
  apply (istotallogeqf (logeqabgrdiffrels X is)).
  intros a b.
  apply (istotalabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
                                isl (weqabgrdiff X a) (weqabgrdiff X b)).
Opaque istotalabgrdiffrel.

Lemma iscotransabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : iscotrans L) :
  iscotrans (abgrdiffrel X is).
Show proof.
  apply (iscotranslogeqf (logeqabgrdiffrels X is)).
  intros a b c.
  apply (iscotransabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
                                  isl (weqabgrdiff X a) (weqabgrdiff X b) (weqabgrdiff X c)).
Opaque iscotransabgrdiffrel.

Lemma isStrongOrder_abgrdiff {X : abmonoid} (gt : hrel X)
      (Hgt : isbinophrel gt) :
  isStrongOrder gt → isStrongOrder (abgrdiffrel X Hgt).
Show proof.
  intros H.
  repeat split.
  - apply istransabgrdiffrel, (istrans_isStrongOrder H).
  - apply iscotransabgrdiffrel, (iscotrans_isStrongOrder H).
  - apply isirreflabgrdiffrel, (isirrefl_isStrongOrder H).
Opaque isStrongOrder_abgrdiff.

Definition StrongOrder_abgrdiff {X : abmonoid} (gt : StrongOrder X)
           (Hgt : isbinophrel gt) : StrongOrder (abgrdiff X) :=
  abgrdiffrel X Hgt,, isStrongOrder_abgrdiff gt Hgt (pr2 gt).

Lemma abgrdiffrelimpl (X : abmonoid) {L L' : hrel X} (is : isbinophrel L) (is' : isbinophrel L')
      (impl : ∏ x x', L x x' -> L' x x') (x x' : abgrdiff X) (ql : abgrdiffrel X is x x') :
  abgrdiffrel X is' x x'.
Show proof.
  generalize ql. refine (quotrelimpl _ _ _ _ _).
  intros x0 x0'. simpl. apply hinhfun. intro t2. split with (pr1 t2).
  apply (impl _ _ (pr2 t2)).
Opaque abgrdiffrelimpl.

Lemma abgrdiffrellogeq (X : abmonoid) {L L' : hrel X} (is : isbinophrel L) (is' : isbinophrel L')
      (lg : ∏ x x', L x x' <-> L' x x') (x x' : abgrdiff X) :
  (abgrdiffrel X is x x') <-> (abgrdiffrel X is' x x').
Show proof.
  refine (quotrellogeq _ _ _ _ _). intros x0 x0'. split.
  - simpl. apply hinhfun. intro t2. split with (pr1 t2).
    apply (pr1 (lg _ _) (pr2 t2)).
  - simpl. apply hinhfun. intro t2. split with (pr1 t2).
    apply (pr2 (lg _ _) (pr2 t2)).
Opaque abgrdiffrellogeq.

Lemma isbinopabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) :
  @isbinophrel (setwithbinopdirprod X X) (abgrdiffrelint X L).
Show proof.
  apply (isbinophrellogeqf (logeqabgrdiffrelints X L)). split.
  - intros a b c lab.
    apply (pr1 (ispartbinopabmonoidfracrelint _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is))
               (abgrdiffphi X a) (abgrdiffphi X b) (abgrdiffphi X c) tt lab).
  - intros a b c lab.
    apply (pr2 (ispartbinopabmonoidfracrelint _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is))
               (abgrdiffphi X a) (abgrdiffphi X b) (abgrdiffphi X c) tt lab).
Opaque isbinopabgrdiffrelint.

Lemma isbinopabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) :
  @isbinophrel (abgrdiff X) (abgrdiffrel X is).
Show proof.
  intros.
  apply (isbinopquotrel (binopeqrelabgrdiff X) (iscomprelabgrdiffrelint X is)).
  apply (isbinopabgrdiffrelint X is).

Definition isdecabgrdiffrelint (X : abmonoid) {L : hrel X}
           (is : isinvbinophrel L) (isl : isdecrel L) : isdecrel (abgrdiffrelint X L).
Show proof.
  intros xa1 xa2.
  set (x1 := pr1 xa1). set (a1 := pr2 xa1).
  set (x2 := pr1 xa2). set (a2 := pr2 xa2).
  assert (int : coprod (L (x1 + a2) (x2 + a1)) (neg (L (x1 + a2) (x2 + a1)))) by apply (isl _ _).
  destruct int as [ l | nl ].
  - apply ii1. unfold abgrdiffrelint. apply hinhpr. split with (unel X).
    rewrite (runax X _). rewrite (runax X _). apply l.
  - apply ii2. generalize nl. clear nl. apply negf. unfold abgrdiffrelint.
    simpl. apply (@hinhuniv _ (make_hProp _ (pr2 (L _ _)))).
    intro t2l. destruct t2l as [ c0a l ]. simpl. apply ((pr2 is) _ _ c0a l).

Definition isdecabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L)
           (isi : isinvbinophrel L) (isl : isdecrel L) : isdecrel (abgrdiffrel X is).
Show proof.
  refine (isdecquotrel _ _). apply isdecabgrdiffrelint.
  - apply isi.
  - apply isl.

Relations and the canonical homomorphism to abgrdiff


Lemma iscomptoabgrdiff (X : abmonoid) {L : hrel X} (is : isbinophrel L) :
  iscomprelrelfun L (abgrdiffrel X is) (toabgrdiff X).
Show proof.
  unfold iscomprelrelfun.
  intros x x' l.
  change (abgrdiffrelint X L (make_dirprod x (unel X)) (make_dirprod x' (unel X))).
  simpl. apply (hinhpr). split with (unel X).
  apply ((pr2 is) _ _ 0). apply ((pr2 is) _ _ 0).
  apply l.
Opaque iscomptoabgrdiff.

Close Scope addmonoid_scope.
End Fractions.