QuotientGroup.v

Require Import Basics Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core.
Require Import Algebra.Congruence.
Require Import Algebra.Groups.Group.
Require Import Algebra.Groups.Subgroup.
Require Export Colimits.Quotient.
Require Import HSet.
Require Import Spaces.Finite.Finite.
Require Import WildCat.
Require Import Modalities.Modality.

(** * Quotient groups *)

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.
Local Open Scope wc_iso_scope.

(** ** Congruence quotients *)

Section GroupCongruenceQuotient.

  (** A congruence on a group is a relation satisfying [R x x' -> R y y' -> R (x * y) (x' * y')].  Because we also require that [R] is reflexive, we also know that [R y y' -> R (x * y) (x * y')] for any [x], and similarly for multiplication on the right by [x].  We don't need to assume that [R] is symmetric or transitive. *)
  Context {G : Group} {R : Relation G} `{!IsCongruence R, !Reflexive R}.

  (** The type underlying the quotient group is [Quotient R]. *)
  Definition CongruenceQuotient := G / R.

  #[export] Instance congquot_sgop : SgOp CongruenceQuotient.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
SgOp CongruenceQuotient
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
SgOp CongruenceQuotient
    srapply Quotient_rec2.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
G -> G -> CongruenceQuotient
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a a' b : G,
R a a' -> ?dclass a b = ?dclass a' b
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a b b' : G,
R b b' -> ?dclass a b = ?dclass a b'
    -G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
G -> G -> CongruenceQuotient intros x y.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
CongruenceQuotient
      exact (class_of _ (x * y)).
    -G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a a' b : G,
R a a' ->
(fun x y : G => class_of R (x * y)) a b =
(fun x y : G => class_of R (x * y)) a' b intros x x' y p.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, x', y: G
p: R x x'
(fun x y : G => class_of R (x * y)) x y =
(fun x y : G => class_of R (x * y)) x' y apply qglue.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, x', y: G
p: R x x'
R (x * y) (x' * y) by apply iscong.
    -G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a b b' : G,
R b b' ->
(fun x y : G => class_of R (x * y)) a b =
(fun x y : G => class_of R (x * y)) a b' intros x y y' q.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y, y': G
q: R y y'
(fun x y : G => class_of R (x * y)) x y =
(fun x y : G => class_of R (x * y)) x y' apply qglue.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y, y': G
q: R y y'
R (x * y) (x * y') by apply iscong.
  Defined.

  #[export] Instance congquot_mon_unit : MonUnit CongruenceQuotient.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
MonUnit CongruenceQuotient
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
MonUnit CongruenceQuotient
    apply class_of, mon_unit.
  Defined.

  #[export] Instance congquot_inverse : Inverse CongruenceQuotient.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Inverse CongruenceQuotient
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Inverse CongruenceQuotient
    srapply Quotient_rec.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
G -> CongruenceQuotient
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a b : G, R a b -> ?pclass a = ?pclass b
    1: exact (class_of R o (^)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
forall a b : G,
R a b -> (class_of R o inv) a = (class_of R o inv) b
    intros x y p; cbn beta.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R y^
    transitivity (class_of R (y^ * (y * x^))).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R (y^ * (y * x^))
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (y * x^)) = class_of R y^
    -G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R (y^ * (y * x^)) rewrite grp_assoc.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R (y^ * y * x^)
      rewrite grp_inv_l.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R (1 * x^)
      rewrite grp_unit_l.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R x^ = class_of R x^
      reflexivity.
    -G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (y * x^)) = class_of R y^ transitivity (class_of R (y^ * (x * x^))).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (y * x^)) =
class_of R (y^ * (x * x^))
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (x * x^)) = class_of R y^
      +G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (y * x^)) =
class_of R (y^ * (x * x^)) symmetry; apply qglue; repeat apply iscong.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
R y^ y^
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
R x y
G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
R x^ x^
        1,3: reflexivity.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
R x y
        exact p.
      +G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * (x * x^)) = class_of R y^ rewrite grp_inv_r.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R (y^ * 1) = class_of R y^
        rewrite grp_unit_r.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y: G
p: R x y
class_of R y^ = class_of R y^
        reflexivity.
  Defined.

  #[export] Instance congquot_sgop_associative : Associative congquot_sgop.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Associative congquot_sgop
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
Associative congquot_sgop
    srapply Quotient_ind3_hprop; intros x y z.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y, z: G
(fun x y z : G / R =>
 congquot_sgop x (congquot_sgop y z) =
 congquot_sgop (congquot_sgop x y) z) (class_of R x)
  (class_of R y) (class_of R z)
    snapply (ap (class_of R)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x, y, z: G
x * (y * z) = x * y * z
    rapply associativity.
  Defined.
  Global Opaque congquot_sgop_associative.

  #[export] Instance issemigroup_congquot : IsSemiGroup CongruenceQuotient := {}.

  #[export] Instance congquot_leftidentity : LeftIdentity (.*.) mon_unit.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
LeftIdentity sg_op 1
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
LeftIdentity sg_op 1
    srapply Quotient_ind_hprop; intro x.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
(fun x : G / R => 1 * x = x) (class_of R x)
    snapply (ap (class_of R)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
1 * x = x
    rapply left_identity.
  Defined.
  Global Opaque congquot_leftidentity.

  #[export] Instance congquot_rightidentity : RightIdentity (.*.) mon_unit.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
RightIdentity sg_op 1
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
RightIdentity sg_op 1
    srapply Quotient_ind_hprop; intro x.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
(fun x : G / R => x * 1 = x) (class_of R x)
    snapply (ap (class_of R)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
x * 1 = x
    rapply right_identity.
  Defined.
  Global Opaque congquot_rightidentity.

  #[export] Instance ismonoid_quotientgroup : IsMonoid CongruenceQuotient := {}.

  #[export] Instance quotientgroup_leftinverse : LeftInverse (.*.) (^) mon_unit.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
LeftInverse sg_op inv 1
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
LeftInverse sg_op inv 1
    srapply Quotient_ind_hprop; intro x; cbn beta.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
(class_of R x)^ * class_of R x = 1
    snapply (ap (class_of R)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
x^ * x = 1
    rapply left_inverse.
  Defined.
  Global Opaque quotientgroup_leftinverse.

  #[export] Instance quotientgroup_rightinverse : RightInverse (.*.) (^) mon_unit.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
RightInverse sg_op inv 1
  Proof.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
RightInverse sg_op inv 1
    srapply Quotient_ind_hprop; intro x; cbn beta.G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
class_of R x * (class_of R x)^ = 1
    snapply (ap (class_of R)).G: Group
R: Relation G
IsCongruence0: IsCongruence R
Reflexive0: Reflexive R
x: G
x * x^ = 1
    rapply right_inverse.
  Defined.
  Global Opaque quotientgroup_rightinverse.

  #[export] Instance isgroup_quotientgroup : IsGroup CongruenceQuotient := {}.

End GroupCongruenceQuotient.

(** ** Sets of cosets *)

Section Cosets.

  Context (G : Group) (H : Subgroup G).

  Definition LeftCoset := G / in_cosetL H.

  (** TODO: Way too many universes, needs fixing *)
  (** The set of left cosets of a finite subgroup of a finite group is finite. *)
  #[export] Instance finite_leftcoset `{Univalence, Finite G, Finite H}
    : Finite LeftCoset.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite LeftCoset
  Proof.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite LeftCoset
    napply finite_quotient.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite G
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
is_mere_relation G (in_cosetL H)
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Reflexive (in_cosetL H)
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Transitive (in_cosetL H)
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Symmetric (in_cosetL H)
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
forall x y : G, Decidable (in_cosetL H x y)
    1-5: exact _.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
forall x y : G, Decidable (in_cosetL H x y)
    intros x y.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
x, y: G
Decidable (in_cosetL H x y)
    apply (detachable_finite_subset H).
  Defined.

  (** The index of a subgroup is the number of cosets of the subgroup. *)
  Definition subgroup_index `{Univalence, Finite G, Finite H} : nat
    := fcard LeftCoset.

  Definition RightCoset := G / in_cosetR H.

  (** The set of left cosets is equivalent to the set of right coset. *)
  Definition equiv_leftcoset_rightcoset
    : LeftCoset <~> RightCoset.G: Group
H: Subgroup G
LeftCoset <~> RightCoset
  Proof.G: Group
H: Subgroup G
LeftCoset <~> RightCoset
    snapply equiv_quotient_functor.G: Group
H: Subgroup G
G -> G
G: Group
H: Subgroup G
IsEquiv ?f
G: Group
H: Subgroup G
forall a b : G,
in_cosetL H a b <-> in_cosetR H (?f a) (?f b)
    -G: Group
H: Subgroup G
G -> G exact inv.
    -G: Group
H: Subgroup G
IsEquiv inv exact _.
    -G: Group
H: Subgroup G
forall a b : G, in_cosetL H a b <-> in_cosetR H a^ b^ intros x y; simpl.G: Group
H: Subgroup G
x, y: G
H (x^ * y) <-> H (x^ * (y^)^)
      by rewrite grp_inv_inv.
  Defined.

  (** The set of right cosets of a finite subgroup of a finite group is finite since it is equivalent to the set of left cosets. *)
  #[export] Instance finite_rightcoset `{Univalence, Finite G, Finite H}
    : Finite RightCoset.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite RightCoset
  Proof.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite RightCoset
    napply finite_equiv'.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
?Goal <~> RightCoset
G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite ?Goal
    1: exact equiv_leftcoset_rightcoset.G: Group
H: Subgroup G
H0: Univalence
H1: Finite G
H2: Finite H
Finite LeftCoset
    exact _.
  Defined.

End Cosets.

(** ** Quotient groups *)

(** Now we can define the quotient group by a normal subgroup. *)

Section QuotientGroup.

  Context (G : Group) (N : NormalSubgroup G).

  #[export] Instance iscongruence_in_cosetL : IsCongruence (in_cosetL N).G: Group
N: NormalSubgroup G
IsCongruence (in_cosetL N)
  Proof.G: Group
N: NormalSubgroup G
IsCongruence (in_cosetL N)
    srapply Build_IsCongruence.G: Group
N: NormalSubgroup G
forall x x' y y' : G,
in_cosetL N x x' ->
in_cosetL N y y' -> in_cosetL N (x * y) (x' * y')
    intros; by apply in_cosetL_cong.
  Defined.

  #[export] Instance iscongruence_in_cosetR: IsCongruence (in_cosetR N).G: Group
N: NormalSubgroup G
IsCongruence (in_cosetR N)
  Proof.G: Group
N: NormalSubgroup G
IsCongruence (in_cosetR N)
    srapply Build_IsCongruence.G: Group
N: NormalSubgroup G
forall x x' y y' : G,
in_cosetR N x x' ->
in_cosetR N y y' -> in_cosetR N (x * y) (x' * y')
    intros; by apply in_cosetR_cong.
  Defined.

  (** Now we have to make a choice whether to pick the left or right cosets. Due to existing convention we shall pick left cosets but we note that we could equally have picked right. *)
  Definition QuotientGroup : Group
    := Build_Group (LeftCoset G N) _ _ _ _.

  Definition grp_quotient_map : G $-> QuotientGroup.G: Group
N: NormalSubgroup G
G $-> QuotientGroup
  Proof.G: Group
N: NormalSubgroup G
G $-> QuotientGroup
    snapply Build_GroupHomomorphism.G: Group
N: NormalSubgroup G
G -> QuotientGroup
G: Group
N: NormalSubgroup G
IsSemiGroupPreserving ?grp_homo_map
    1: exact (class_of _).G: Group
N: NormalSubgroup G
IsSemiGroupPreserving (class_of (in_cosetL N))
    intros ??; reflexivity.
  Defined.

  Definition grp_quotient_rec {A : Group} (f : G $-> A)
             (h : forall n : G, N n -> f n = mon_unit)
    : QuotientGroup $-> A.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
QuotientGroup $-> A
  Proof.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
QuotientGroup $-> A
    snapply Build_GroupHomomorphism.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
QuotientGroup -> A
G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
IsSemiGroupPreserving ?grp_homo_map
    -G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
QuotientGroup -> A srapply Quotient_rec.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
G -> A
G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
forall a b : G,
in_cosetL N a b -> ?pclass a = ?pclass b
      +G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
G -> A exact f.
      +G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
forall a b : G, in_cosetL N a b -> f a = f b cbn; intros x y n.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
x, y: G
n: N (x^ * y)
f x = f y
        apply grp_moveR_M1.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
x, y: G
n: N (x^ * y)
1 = (f x)^ * f y
        rhs_V napply (ap (.* f y) (grp_homo_inv _ _)).G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
x, y: G
n: N (x^ * y)
1 = f x^ * f y
        rhs_V napply grp_homo_op.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
x, y: G
n: N (x^ * y)
1 = f (x^ * y)
        symmetry; apply h; assumption.
    -G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
IsSemiGroupPreserving
  (Quotient_rec (in_cosetL N) A f
     ((fun (x y : G) (n : N (x^ * y)) =>
       let X := equiv_fun grp_moveR_M1 in
       X
         (((h (inv x * y) n)^ @
           grp_homo_op f (inv x) y) @
          ap (fun y0 : A => y0 * f y)
            (grp_homo_inv f x)))
      :
      forall a b : G, in_cosetL N a b -> f a = f b)) intro x.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
x: QuotientGroup
forall y : QuotientGroup,
Quotient_rec (in_cosetL N) A f
  (fun (x y0 : G) (n : N (x^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y0) n)^ @ grp_homo_op f (inv x) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x)))
  (x * y) =
Quotient_rec (in_cosetL N) A f
  (fun (x y0 : G) (n : N (x^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y0) n)^ @ grp_homo_op f (inv x) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x)))
  x *
Quotient_rec (in_cosetL N) A f
  (fun (x y0 : G) (n : N (x^ * y0)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y0) n)^ @ grp_homo_op f (inv x) y0) @
      ap (fun y1 : A => y1 * f y0) (grp_homo_inv f x)))
  y
      refine (Quotient_ind_hprop _ _ _).G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
x: QuotientGroup
forall a : G,
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (x^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y) n)^ @ grp_homo_op f (inv x) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x)))
  (x * class_of (in_cosetL N) a) =
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (x^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y) n)^ @ grp_homo_op f (inv x) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x)))
  x *
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (x^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y) n)^ @ grp_homo_op f (inv x) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x)))
  (class_of (in_cosetL N) a)
      intro y.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
x: QuotientGroup
y: G
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (x^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y) n)^ @ grp_homo_op f (inv x) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x)))
  (x * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (x^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y) n)^ @ grp_homo_op f (inv x) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x)))
  x *
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (x^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y) n)^ @ grp_homo_op f (inv x) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x)))
  (class_of (in_cosetL N) y) revert x.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
y: G
forall x : QuotientGroup,
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (x0^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y) n)^ @ grp_homo_op f (inv x0) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x0)))
  (x * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (x0^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y) n)^ @ grp_homo_op f (inv x0) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x0)))
  x *
Quotient_rec (in_cosetL N) A f
  (fun (x0 y : G) (n : N (x0^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x0 * y) n)^ @ grp_homo_op f (inv x0) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x0)))
  (class_of (in_cosetL N) y)
      refine (Quotient_ind_hprop _ _ _).G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
y: G
forall a : G,
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (x^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y) n)^ @ grp_homo_op f (inv x) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x)))
  (class_of (in_cosetL N) a * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (x^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y) n)^ @ grp_homo_op f (inv x) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x)))
  (class_of (in_cosetL N) a) *
Quotient_rec (in_cosetL N) A f
  (fun (x y : G) (n : N (x^ * y)) =>
   let X := equiv_fun grp_moveR_M1 in
   X
     (((h (inv x * y) n)^ @ grp_homo_op f (inv x) y) @
      ap (fun y0 : A => y0 * f y) (grp_homo_inv f x)))
  (class_of (in_cosetL N) y)
      intro x; simpl.G: Group
N: NormalSubgroup G
A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
y, x: G
f (x * y) = f x * f y
      apply grp_homo_op.
  Defined.

  Definition grp_quotient_ind_hprop (P : QuotientGroup -> Type)
    `{forall x, IsHProp (P x)}
    (H1 : forall x, P (grp_quotient_map x))
    : forall x, P x.G: Group
N: NormalSubgroup G
P: QuotientGroup -> Type
H: forall x : QuotientGroup, IsHProp (P x)
H1: forall x : G, P (grp_quotient_map x)
forall x : QuotientGroup, P x
  Proof.G: Group
N: NormalSubgroup G
P: QuotientGroup -> Type
H: forall x : QuotientGroup, IsHProp (P x)
H1: forall x : G, P (grp_quotient_map x)
forall x : QuotientGroup, P x
    srapply Quotient_ind_hprop.G: Group
N: NormalSubgroup G
P: QuotientGroup -> Type
H: forall x : QuotientGroup, IsHProp (P x)
H1: forall x : G, P (grp_quotient_map x)
forall a : G, P (class_of (in_cosetL N) a)
    exact H1.
  Defined.

End QuotientGroup.

Arguments QuotientGroup G N : simpl never.
Arguments grp_quotient_map {_ _}.

Notation "G / N" := (QuotientGroup G N) : group_scope.

(** Rephrasing that lets you specify the normality proof *)
Definition QuotientGroup' (G : Group) (N : Subgroup G) (H : IsNormalSubgroup N)
  := QuotientGroup G (Build_NormalSubgroup G N H).

Local Open Scope group_scope.

(** Computation rule for [grp_quotient_rec]. *)
Corollary grp_quotient_rec_beta `{F : Funext} {G : Group}
          (N : NormalSubgroup G) (H : Group)
          {A : Group} (f : G $-> A)
          (h : forall n:G, N n -> f n = mon_unit)
  : (grp_quotient_rec G N f h) $o grp_quotient_map = f.F: Funext
G: Group
N: NormalSubgroup G
H, A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
grp_quotient_rec G N f h $o grp_quotient_map = f
Proof.F: Funext
G: Group
N: NormalSubgroup G
H, A: Group
f: G $-> A
h: forall n : G, N n -> f n = 1
grp_quotient_rec G N f h $o grp_quotient_map = f
  apply equiv_path_grouphomomorphism; reflexivity.
Defined.

(** Computation rule for [grp_quotient_rec]. *)
Definition grp_quotient_rec_beta' {G : Group}
          (N : NormalSubgroup G) (H : Group)
          {A : Group} (f : G $-> A)
          (h : forall n:G, N n -> f n = mon_unit)
  : (grp_quotient_rec G N f h) $o grp_quotient_map == f
    := fun _ => idpath.

(** The proof of normality is irrelevant up to equivalence. It is unfortunate that it doesn't hold definitionally. *)
Definition grp_iso_quotient_normal (G : Group) (H : Subgroup G)
  {k k' : IsNormalSubgroup H}
  : QuotientGroup' G H k ≅ QuotientGroup' G H k'.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
QuotientGroup' G H k ≅ QuotientGroup' G H k'
Proof.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
QuotientGroup' G H k ≅ QuotientGroup' G H k'
  snapply Build_GroupIsomorphism'.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
QuotientGroup' G H k <~> QuotientGroup' G H k'
G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
IsSemiGroupPreserving ?f
  1: reflexivity.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
IsSemiGroupPreserving 1%equiv
  intro x.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
x: QuotientGroup' G H k
forall y : QuotientGroup' G H k,
1%equiv (x * y) = 1%equiv x * 1%equiv y
  srapply Quotient_ind_hprop; intro y; revert x.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
y: G
forall x : QuotientGroup' G H k,
(fun
   x0 : Quotient
          (in_cosetL
             {|
               normalsubgroup_subgroup := H;
               normalsubgroup_isnormal := k
             |}) =>
 1%equiv (x * x0) = 1%equiv x * 1%equiv x0)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := H;
          normalsubgroup_isnormal := k
        |}) y)
  srapply Quotient_ind_hprop; intro x.G: Group
H: Subgroup G
k, k': IsNormalSubgroup H
y, x: G
(fun
   x : Quotient
         (in_cosetL
            {|
              normalsubgroup_subgroup := H;
              normalsubgroup_isnormal := k
            |}) =>
 (fun
    x0 : Quotient
           (in_cosetL
              {|
                normalsubgroup_subgroup := H;
                normalsubgroup_isnormal := k
              |}) =>
  1%equiv (x * x0) = 1%equiv x * 1%equiv x0)
   (class_of
      (in_cosetL
         {|
           normalsubgroup_subgroup := H;
           normalsubgroup_isnormal := k
         |}) y))
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := H;
          normalsubgroup_isnormal := k
        |}) x)
  reflexivity.
Defined.

(** The universal mapping property for groups *)
Theorem equiv_grp_quotient_ump {F : Funext} {G : Group} (N : NormalSubgroup G) (H : Group)
  : {f : G $-> H & forall (n : G), N n -> f n = mon_unit}
    <~> (G / N $-> H).F: Funext
G: Group
N: NormalSubgroup G
H: Group
{f : G $-> H & forall n : G, N n -> f n = 1} <~>
(G / N $-> H)
Proof.F: Funext
G: Group
N: NormalSubgroup G
H: Group
{f : G $-> H & forall n : G, N n -> f n = 1} <~>
(G / N $-> H)
  srapply equiv_adjointify.F: Funext
G: Group
N: NormalSubgroup G
H: Group
{f : G $-> H & forall n : G, N n -> f n = 1} ->
G / N $-> H
F: Funext
G: Group
N: NormalSubgroup G
H: Group
(G / N $-> H) ->
{f : G $-> H & forall n : G, N n -> f n = 1}
F: Funext
G: Group
N: NormalSubgroup G
H: Group
?f o ?g == idmap
F: Funext
G: Group
N: NormalSubgroup G
H: Group
?g o ?f == idmap
  -F: Funext
G: Group
N: NormalSubgroup G
H: Group
{f : G $-> H & forall n : G, N n -> f n = 1} ->
G / N $-> H intros [f p].F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G $-> H
p: forall n : G, N n -> f n = 1
G / N $-> H
    exact (grp_quotient_rec _ _ f p).
  -F: Funext
G: Group
N: NormalSubgroup G
H: Group
(G / N $-> H) ->
{f : G $-> H & forall n : G, N n -> f n = 1} intro f.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
{f : G $-> H & forall n : G, N n -> f n = 1}
    exists (f $o grp_quotient_map).F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
forall n : G, N n -> (f $o grp_quotient_map) n = 1
    intros n h; cbn.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
f (class_of (fun x y : G => N (x^ * y)) n) = 1
    refine (_ @ grp_homo_unit f).F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
f (class_of (fun x y : G => N (x^ * y)) n) = f 1
    apply ap.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
class_of (fun x y : G => N (x^ * y)) n = 1
    apply qglue; cbn.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
n: G
h: N n
N (n^ * 1)
    rewrite right_identity;
      by apply issubgroup_in_inv.
  -F: Funext
G: Group
N: NormalSubgroup G
H: Group
(fun X : {f : G $-> H & forall n : G, N n -> f n = 1}
 =>
 (fun (f : G $-> H) (p : forall n : G, N n -> f n = 1)
  => grp_quotient_rec G N f p) X.1 X.2)
o (fun f : G / N $-> H =>
   (f $o grp_quotient_map;
   fun (n : G) (h : N n) =>
   ap f
     (qglue
        (internal_paths_rew_r (fun g : G => N g)
           (issubgroup_in_inv n h)
           (right_identity (inv n))
         :
         in_cosetL N n mon_unit)) @ grp_homo_unit f
   :
   (f $o grp_quotient_map) n = 1)) == idmap intros f.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
grp_quotient_rec G N (f $o grp_quotient_map)
  (fun (n : G) (h : N n) =>
   ap f
     (qglue
        (internal_paths_rew_r (fun g : G => N g)
           (issubgroup_in_inv n h)
           (right_identity (inv n)))) @
   grp_homo_unit f) = f
    rapply equiv_path_grouphomomorphism.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G / N $-> H
grp_quotient_rec G N (f $o grp_quotient_map)
  (fun (n : G) (h : N n) =>
   ap f
     (qglue
        (internal_paths_rew_r (fun g : G => N g)
           (issubgroup_in_inv n h)
           (right_identity (inv n)))) @
   grp_homo_unit f) == f
      by srapply Quotient_ind_hprop.
  -F: Funext
G: Group
N: NormalSubgroup G
H: Group
(fun f : G / N $-> H =>
 (f $o grp_quotient_map;
 fun (n : G) (h : N n) =>
 ap f
   (qglue
      (internal_paths_rew_r (fun g : G => N g)
         (issubgroup_in_inv n h)
         (right_identity (inv n))
       :
       in_cosetL N n mon_unit)) @ grp_homo_unit f
 :
 (f $o grp_quotient_map) n = 1))
o (fun
     X : {f : G $-> H & forall n : G, N n -> f n = 1}
   =>
   (fun (f : G $-> H)
      (p : forall n : G, N n -> f n = 1) =>
    grp_quotient_rec G N f p) X.1 X.2) == idmap intros [f p].F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G $-> H
p: forall n : G, N n -> f n = 1
(grp_quotient_rec G N f p $o grp_quotient_map;
fun (n : G) (h : N n) =>
ap (grp_quotient_rec G N f p)
  (qglue
     (internal_paths_rew_r (fun g : G => N g)
        (issubgroup_in_inv n h)
        (right_identity (inv n)))) @
grp_homo_unit (grp_quotient_rec G N f p)) = (f; p)
    srapply path_sigma_hprop; simpl.F: Funext
G: Group
N: NormalSubgroup G
H: Group
f: G $-> H
p: forall n : G, N n -> f n = 1
grp_homo_compose (grp_quotient_rec G N f p)
  grp_quotient_map = f
    exact (grp_quotient_rec_beta N H f p).
Defined.

Section FirstIso.

  Context `{Funext} {A B : Group} (phi : A $-> B).

  (** First we define a map from the quotient by the kernel of phi into the image of phi *)
  Definition grp_image_quotient
    : A / grp_kernel phi $-> grp_image phi.H: Funext
A, B: Group
phi: A $-> B
A / grp_kernel phi $-> grp_image phi
  Proof.H: Funext
A, B: Group
phi: A $-> B
A / grp_kernel phi $-> grp_image phi
    srapply grp_quotient_rec.H: Funext
A, B: Group
phi: A $-> B
A $-> grp_image phi
H: Funext
A, B: Group
phi: A $-> B
forall n : A, grp_kernel phi n -> ?f n = 1
    +H: Funext
A, B: Group
phi: A $-> B
A $-> grp_image phi srapply grp_homo_image_in.
    +H: Funext
A, B: Group
phi: A $-> B
forall n : A,
grp_kernel phi n -> grp_homo_image_in phi n = 1 intros n x.H: Funext
A, B: Group
phi: A $-> B
n: A
x: grp_kernel phi n
grp_homo_image_in phi n = 1
      by apply path_sigma_hprop.
  Defined.

  (** The underlying map of this homomorphism is an equivalence *)
  #[export] Instance isequiv_grp_image_quotient
    : IsEquiv grp_image_quotient.H: Funext
A, B: Group
phi: A $-> B
IsEquiv grp_image_quotient
  Proof.H: Funext
A, B: Group
phi: A $-> B
IsEquiv grp_image_quotient
    snapply isequiv_surj_emb.H: Funext
A, B: Group
phi: A $-> B
IsConnMap (Tr (-1)) grp_image_quotient
H: Funext
A, B: Group
phi: A $-> B
IsEmbedding grp_image_quotient
    1: srapply cancelR_conn_map.H: Funext
A, B: Group
phi: A $-> B
IsEmbedding grp_image_quotient
    srapply isembedding_isinj_hset.H: Funext
A, B: Group
phi: A $-> B
IsInjective grp_image_quotient
    srapply Quotient_ind2_hprop.H: Funext
A, B: Group
phi: A $-> B
forall a b : A,
(fun x y : Quotient (in_cosetL (grp_kernel phi)) =>
 grp_image_quotient x = grp_image_quotient y -> x = y)
  (class_of (in_cosetL (grp_kernel phi)) a)
  (class_of (in_cosetL (grp_kernel phi)) b)
    intros x y h; simpl in h.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: (phi x; grp_image_in phi x) =
(phi y; grp_image_in phi y)
class_of (in_cosetL (grp_kernel phi)) x =
class_of (in_cosetL (grp_kernel phi)) y
    apply qglue; cbn.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: (phi x; grp_image_in phi x) =
(phi y; grp_image_in phi y)
phi (x^ * y) = 1
    apply (equiv_path_sigma_hprop _ _)^-1%equiv in h; cbn in h.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: phi x = phi y
phi (x^ * y) = 1
    cbn.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: phi x = phi y
phi (x^ * y) = 1 rewrite grp_homo_op, grp_homo_inv, h.H: Funext
A, B: Group
phi: A $-> B
x, y: A
h: phi x = phi y
(phi y)^ * phi y = 1
    apply grp_inv_l.
  Defined.

  (** First isomorphism theorem for groups *)
  Theorem grp_first_iso : A / grp_kernel phi ≅ grp_image phi.H: Funext
A, B: Group
phi: A $-> B
A / grp_kernel phi ≅ grp_image phi
  Proof.H: Funext
A, B: Group
phi: A $-> B
A / grp_kernel phi ≅ grp_image phi
    exact (Build_GroupIsomorphism _ _ grp_image_quotient _).
  Defined.

End FirstIso.

(** Quotient groups are finite. *)
(** Note that we cannot constructively conclude that the normal subgroup [H] must be finite since [G] is, therefore we keep it as an assumption. *)
Instance finite_quotientgroup {U : Univalence} (G : Group) (H : NormalSubgroup G)
  (fin_G : Finite G) (fin_H : Finite H)
  : Finite (QuotientGroup G H).U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Finite (G / H)
Proof.U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Finite (G / H)
  napply finite_quotient.U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Finite G
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
is_mere_relation G (in_cosetL H)
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Reflexive (in_cosetL H)
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Transitive (in_cosetL H)
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
Symmetric (in_cosetL H)
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
forall x y : G, Decidable (in_cosetL H x y)
  1-5: exact _.U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
forall x y : G, Decidable (in_cosetL H x y)
  intros x y.U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
x, y: G
Decidable (in_cosetL H x y)
  pose (dec_H := detachable_finite_subset H).U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
x, y: G
dec_H:= detachable_finite_subset H: forall x : G, Decidable (H x)
Decidable (in_cosetL H x y)
  apply dec_H.
Defined.

Definition grp_kernel_quotient_iso `{Univalence} {G : Group} (N : NormalSubgroup G)
  : GroupIsomorphism N (grp_kernel (@grp_quotient_map G N)).H: Univalence
G: Group
N: NormalSubgroup G
GroupIsomorphism N (grp_kernel grp_quotient_map)
Proof.H: Univalence
G: Group
N: NormalSubgroup G
GroupIsomorphism N (grp_kernel grp_quotient_map)
  srapply Build_GroupIsomorphism.H: Univalence
G: Group
N: NormalSubgroup G
GroupHomomorphism N (grp_kernel grp_quotient_map)
H: Univalence
G: Group
N: NormalSubgroup G
IsEquiv ?grp_iso_homo
  -H: Univalence
G: Group
N: NormalSubgroup G
GroupHomomorphism N (grp_kernel grp_quotient_map) srapply (grp_kernel_corec (subgroup_incl N)).H: Univalence
G: Group
N: NormalSubgroup G
grp_quotient_map $o subgroup_incl N == grp_homo_const
    intro x; cbn.H: Univalence
G: Group
N: NormalSubgroup G
x: N
class_of (fun x y : G => N (x^ * y)) x.1 = group_unit
    apply qglue.H: Univalence
G: Group
N: NormalSubgroup G
x: N
in_cosetL N x.1 1
    apply issubgroup_in_op.H: Univalence
G: Group
N: NormalSubgroup G
x: N
N (x.1)^
H: Univalence
G: Group
N: NormalSubgroup G
x: N
N 1
    +H: Univalence
G: Group
N: NormalSubgroup G
x: N
N (x.1)^ exact (issubgroup_in_inv _ x.2).
    +H: Univalence
G: Group
N: NormalSubgroup G
x: N
N 1 exact issubgroup_in_unit.
  -H: Univalence
G: Group
N: NormalSubgroup G
IsEquiv
  (grp_kernel_corec (subgroup_incl N)
     ((fun x : N =>
       qglue
         (issubgroup_in_op (x.1)^ 1
            (issubgroup_in_inv x.1 x.2)
            issubgroup_in_unit)
       :
       (grp_quotient_map $o subgroup_incl N) x =
       grp_homo_const x)
      :
      grp_quotient_map $o subgroup_incl N ==
      grp_homo_const)) apply isequiv_surj_emb.H: Univalence
G: Group
N: NormalSubgroup G
IsConnMap (Tr (-1))
  (grp_kernel_corec (subgroup_incl N)
     (fun x : N =>
      qglue
        (issubgroup_in_op (x.1)^ 1
           (issubgroup_in_inv x.1 x.2)
           issubgroup_in_unit)))
H: Univalence
G: Group
N: NormalSubgroup G
IsEmbedding
  (grp_kernel_corec (subgroup_incl N)
     (fun x : N =>
      qglue
        (issubgroup_in_op (x.1)^ 1
           (issubgroup_in_inv x.1 x.2)
           issubgroup_in_unit)))
    2: exact (cancelL_isembedding (g:=pr1)).H: Univalence
G: Group
N: NormalSubgroup G
IsConnMap (Tr (-1))
  (grp_kernel_corec (subgroup_incl N)
     (fun x : N =>
      qglue
        (issubgroup_in_op (x.1)^ 1
           (issubgroup_in_inv x.1 x.2)
           issubgroup_in_unit)))
    intros [g p].H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
IsConnected (Tr (-1))
  (hfiber
     (grp_kernel_corec (subgroup_incl N)
        (fun x : N =>
         qglue
           (issubgroup_in_op (x.1)^ 1
              (issubgroup_in_inv x.1 x.2)
              issubgroup_in_unit))) (g; p))
    rapply contr_inhabited_hprop.H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
Tr (-1)
  (hfiber
     (grp_kernel_corec (subgroup_incl N)
        (fun x : N =>
         qglue
           (issubgroup_in_op (x.1)^ 1
              (issubgroup_in_inv x.1 x.2)
              issubgroup_in_unit))) (g; p))
    srefine (tr ((g; _); _)).H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
N g
H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
(fun x : N =>
 grp_kernel_corec (subgroup_incl N)
   (fun x0 : N =>
    qglue
      (issubgroup_in_op (x0.1)^ 1
         (issubgroup_in_inv x0.1 x0.2)
         issubgroup_in_unit)) x = (g; p)) (g; ?proj2)
    +H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
N g rewrite <- grp_unit_l, <- inverse_mon_unit.H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
N (1^ * g)
      apply (related_quotient_paths (fun x y => N (x^ * y))).H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
class_of (fun x y : G => N (x^ * y)) 1 =
class_of (fun x y : G => N (x^ * y)) g
      exact p^%path.
    +H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
(fun x : N =>
 grp_kernel_corec (subgroup_incl N)
   (fun x0 : N =>
    qglue
      (issubgroup_in_op (x0.1)^ 1
         (issubgroup_in_inv x0.1 x0.2)
         issubgroup_in_unit)) x = (g; p))
  (g;
  internal_paths_rew N
    (internal_paths_rew (fun g0 : G => N (g0 * g))
       (related_quotient_paths
          (fun x y : G => N (x^ * y)) 1 g p^)
       inverse_mon_unit) (grp_unit_l g)) srapply path_sigma_hprop.H: Univalence
G: Group
N: NormalSubgroup G
g: G
p: grp_kernel grp_quotient_map g
(grp_kernel_corec (subgroup_incl N)
   (fun x : N =>
    qglue
      (issubgroup_in_op (x.1)^ 1
         (issubgroup_in_inv x.1 x.2)
         issubgroup_in_unit))
   (g;
   internal_paths_rew N
     (internal_paths_rew (fun g0 : G => N (g0 * g))
        (related_quotient_paths
           (fun x y : G => N (x^ * y)) 1 g p^)
        inverse_mon_unit) (grp_unit_l g))).1 =
(g; p).1
      reflexivity.
Defined.

(** When the normal subgroup [N] is trivial, the inclusion map [G $-> G / N] is an isomorphism. *)
Instance catie_grp_quotient_map_trivial {G : Group} (N : NormalSubgroup G)
  (triv : IsTrivialGroup N)
  : CatIsEquiv (@grp_quotient_map G N).G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
CatIsEquiv grp_quotient_map
Proof.G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
CatIsEquiv grp_quotient_map
  snapply catie_adjointify.G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
G / N $-> G
G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
grp_quotient_map $o ?g $== Id (G / N)
G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
?g $o grp_quotient_map $== Id G
  -G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
G / N $-> G srapply (grp_quotient_rec _ _ (Id _)).G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
forall n : G, N n -> Id G n = 1
    exact triv.
  -G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
grp_quotient_map $o grp_quotient_rec G N (Id G) triv $==
Id (G / N) by srapply grp_quotient_ind_hprop.
  -G: Group
N: NormalSubgroup G
triv: IsTrivialGroup N
grp_quotient_rec G N (Id G) triv $o grp_quotient_map $==
Id G reflexivity.
Defined.

(** The group quotient by a trivial group is isomorphic to the original group. *)
Definition grp_quotient_trivial (G : Group) (N : NormalSubgroup G)
  (triv : IsTrivialGroup N)
  : G $<~> G / N
  := Build_CatEquiv grp_quotient_map.

(** A quotient by a maximal subgroup is trivial. *)
Instance istrivial_grp_quotient_maximal
  (G : Group) (N : NormalSubgroup G)
  : IsMaximalSubgroup N -> IsTrivialGroup (G / N).G: Group
N: NormalSubgroup G
IsMaximalSubgroup N ->
IsTrivialGroup (maximal_subgroup (G / N))
Proof.G: Group
N: NormalSubgroup G
IsMaximalSubgroup N ->
IsTrivialGroup (maximal_subgroup (G / N))
  intros max x _; revert x.G: Group
N: NormalSubgroup G
max: IsMaximalSubgroup N
forall x : G / N, trivial_subgroup (G / N) x
  rapply grp_quotient_ind_hprop.G: Group
N: NormalSubgroup G
max: IsMaximalSubgroup N
forall x : G,
trivial_subgroup (G / N) (grp_quotient_map x)
  intros x.G: Group
N: NormalSubgroup G
max: IsMaximalSubgroup N
x: G
trivial_subgroup (G / N) (grp_quotient_map x)
  apply qglue, max.
Defined.

(** Conversely, a trivial quotient means the subgroup is maximal. *)
Definition ismaximalsubgroup_istrivial_grp_quotient `{Univalence}
  (G : Group) (N : NormalSubgroup G)
  : IsTrivialGroup (G / N) -> IsMaximalSubgroup N.H: Univalence
G: Group
N: NormalSubgroup G
IsTrivialGroup (maximal_subgroup (G / N)) ->
IsMaximalSubgroup N
Proof.H: Univalence
G: Group
N: NormalSubgroup G
IsTrivialGroup (maximal_subgroup (G / N)) ->
IsMaximalSubgroup N
  intros triv x.H: Univalence
G: Group
N: NormalSubgroup G
triv: IsTrivialGroup (maximal_subgroup (G / N))
x: G
N x
  specialize (triv (grp_quotient_map x) tt).H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: trivial_subgroup (G / N) (grp_quotient_map x)
N x
  simpl in triv.H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: class_of (fun x y : G => N (x^ * y)) x = 1
N x
  apply related_quotient_paths in triv.H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: N (x^ * 1)
N x
H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: class_of (fun x y : G => N (x^ * y)) x = 1
forall x y : G, IsHProp (N (x^ * y))
H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: class_of (fun x y : G => N (x^ * y)) x = 1
Transitive (fun x y : G => N (x^ * y))
H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: class_of (fun x y : G => N (x^ * y)) x = 1
Symmetric (fun x y : G => N (x^ * y))
H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: class_of (fun x y : G => N (x^ * y)) x = 1
Reflexive (fun x y : G => N (x^ * y))
  2-5: exact _.H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: N (x^ * 1)
N x
  apply equiv_subgroup_inv.H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: N (x^ * 1)
N x^
  napply (subgroup_in_op_l _ _ 1 triv) .H: Univalence
G: Group
N: NormalSubgroup G
x: G
triv: N (x^ * 1)
N 1
  apply subgroup_in_unit.
Defined.