Subgroup.v

Require Import Basics Types HFiber WildCat.Core WildCat.Equiv.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core Modalities.Modality.
Require Export Modalities.Modality (conn_map_factor1_image).
Require Import Algebra.Groups.Group Universes.TruncType Universes.HSet.

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

Generalizable Variables G H A B C N f g.

(** * Subgroups *)

(** ** Definition of being a subgroup *)

(** A subgroup H of a group G is a predicate (i.e. an hProp-valued type family) on G which is closed under the group operations. The group underlying H is given by the total space { g : G & H g }, defined in [subgroup_group] below. *)
Class IsSubgroup {G : Group} (H : G -> Type) := {
  issubgroup_predicate :: forall x, IsHProp (H x) ;
  issubgroup_in_unit : H mon_unit ;
  issubgroup_in_op : forall x y, H x -> H y -> H (x * y) ;
  issubgroup_in_inv : forall x, H x -> H x^ ;
}.

Definition issig_issubgroup {G : Group} (H : G -> Type) : _ <~> IsSubgroup H
  := ltac:(issig).

(** Basic properties of subgroups *)

(** Smart constructor for subgroups.  *)
Definition Build_IsSubgroup' {G : Group}
  (H : G -> Type) `{forall x, IsHProp (H x)}
  (unit : H mon_unit)
  (c : forall x y, H x -> H y -> H (x * y^))
  : IsSubgroup H.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
IsSubgroup H
Proof.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
IsSubgroup H
  refine (Build_IsSubgroup G H _ unit _ _).G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
forall x y : G, H x -> H y -> H (x * y)
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
forall x : G, H x -> H x^
  -G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
forall x y : G, H x -> H y -> H (x * y) intros x y.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
x, y: G
H x -> H y -> H (x * y)
    intros hx hy.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
x, y: G
hx: H x
hy: H y
H (x * y)
    pose (c' := c mon_unit y).G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
x, y: G
hx: H x
hy: H y
c':= c 1 y: H 1 -> H y -> H (1 * y^)
H (x * y)
    specialize (c' unit).G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
x, y: G
hx: H x
hy: H y
c': H y -> H (1 * y^)
H (x * y)
    specialize (c x y^).G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
x, y: G
c: H x -> H y^ -> H (x * (y^)^)
hx: H x
hy: H y
c': H y -> H (1 * y^)
H (x * y)
    rewrite (grp_inv_inv y) in c.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
x, y: G
c: H x -> H y^ -> H (x * y)
hx: H x
hy: H y
c': H y -> H (1 * y^)
H (x * y)
    rewrite left_identity in c'.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
x, y: G
c: H x -> H y^ -> H (x * y)
hx: H x
hy: H y
c': H y -> H y^
H (x * y)
    apply c.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
x, y: G
c: H x -> H y^ -> H (x * y)
hx: H x
hy: H y
c': H y -> H y^
H x
G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
x, y: G
c: H x -> H y^ -> H (x * y)
hx: H x
hy: H y
c': H y -> H y^
H y^
    1: assumption.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
x, y: G
c: H x -> H y^ -> H (x * y)
hx: H x
hy: H y
c': H y -> H y^
H y^
    exact (c' hy).
  -G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
forall x : G, H x -> H x^ intro g.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
g: G
H g -> H g^
    specialize (c _ g unit).G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
g: G
c: H g -> H (1 * g^)
H g -> H g^
    rewrite left_identity in c.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
g: G
c: H g -> H g^
H g -> H g^
    assumption.
Defined.

(** Additional lemmas about being elements in a subgroup *)
Section IsSubgroupElements.
  Context  {G : Group} {H : G -> Type} `{IsSubgroup G H}.

  Definition issubgroup_in_op_inv (x y : G) : H x -> H y -> H (x * y^).G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H y -> H (x * y^)
  Proof.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H y -> H (x * y^)
    intros p q.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H (x * y^)
    apply issubgroup_in_op.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H x
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H y^
    1: assumption.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H y^
    by apply issubgroup_in_inv.
  Defined.

  Definition issubgroup_in_inv' (x : G) : H x^ -> H x.G: Group
H: G -> Type
H0: IsSubgroup H
x: G
H x^ -> H x
  Proof.G: Group
H: G -> Type
H0: IsSubgroup H
x: G
H x^ -> H x
    intros p; rewrite <- (inverse_involutive x); revert p.G: Group
H: G -> Type
H0: IsSubgroup H
x: G
H x^ -> H (x^)^
    apply issubgroup_in_inv.
  Defined.

  Definition issubgroup_in_inv_op (x y : G) : H x -> H y -> H (x^ * y).G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H y -> H (x^ * y)
  Proof.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H y -> H (x^ * y)
    intros p q.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H (x^ * y)
    rewrite <- (inverse_involutive y).G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H (x^ * (y^)^)
    apply issubgroup_in_op_inv.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H x^
G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H x
q: H y
H y^
    1,2: by apply issubgroup_in_inv.
  Defined.

  Definition issubgroup_in_op_l (x y : G) : H (x * y) -> H y -> H x.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H y -> H x
  Proof.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H y -> H x
    intros p q.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H (x * y)
q: H y
H x
    rewrite <- (grp_unit_r x).G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H (x * y)
q: H y
H (x * 1)
    revert p q.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H y -> H (x * 1)
    rewrite <- (grp_inv_r y).G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H y -> H (x * (y * y^))
    rewrite grp_assoc.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H y -> H (x * y * y^)
    apply issubgroup_in_op_inv.
  Defined.

  Definition issubgroup_in_op_r (x y : G) : H (x * y) -> H x -> H y.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H x -> H y
  Proof.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H (x * y) -> H x -> H y
    intros p q.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H (x * y)
q: H x
H y
    rewrite <- (grp_unit_l y).G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
p: H (x * y)
q: H x
H (1 * y)
    revert q p.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H (x * y) -> H (1 * y)
    rewrite <- (grp_inv_l x).G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H (x * y) -> H (x^ * x * y)
    rewrite <- grp_assoc.G: Group
H: G -> Type
H0: IsSubgroup H
x, y: G
H x -> H (x * y) -> H (x^ * (x * y))
    apply issubgroup_in_inv_op.
  Defined.

End IsSubgroupElements.

(** Given a predicate H on a group G, being a subgroup is a property. *)
Instance ishprop_issubgroup `{F : Funext} {G : Group} {H : G -> Type}
  : IsHProp (IsSubgroup H).F: Funext
G: Group
H: G -> Type
IsHProp (IsSubgroup H)
Proof.F: Funext
G: Group
H: G -> Type
IsHProp (IsSubgroup H)
  exact (istrunc_equiv_istrunc _ (issig_issubgroup H)).
Defined.

(** Transporting being a subgroup across a pointwise equivalence. *)
Definition issubgroup_equiv {G : Group} {H K : G -> Type}
  (p : forall g, H g <~> K g)
  : IsSubgroup H -> IsSubgroup K.G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
IsSubgroup H -> IsSubgroup K
Proof.G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
IsSubgroup H -> IsSubgroup K
  intros H1.G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
IsSubgroup K
  snapply Build_IsSubgroup.G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
forall x : G, IsHProp (K x)
G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
K 1
G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
forall x y : G, K x -> K y -> K (x * y)
G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
forall x : G, K x -> K x^
  -G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
forall x : G, IsHProp (K x) intros x.G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
x: G
IsHProp (K x)
    rapply (istrunc_equiv_istrunc (H x)).G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
x: G
H x <~> K x
    apply p.
  -G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
K 1 apply p, issubgroup_in_unit.
  -G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
forall x y : G, K x -> K y -> K (x * y) intros x y inx iny.G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
x, y: G
inx: K x
iny: K y
K (x * y)
    apply (p _)^-1 in inx, iny.G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
x, y: G
inx: H x
iny: H y
K (x * y)
    exact (p _ (issubgroup_in_op x y inx iny)).
  -G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
forall x : G, K x -> K x^ intros x inx.G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
x: G
inx: K x
K x^
    apply (p _)^-1 in inx.G: Group
H, K: G -> Type
p: forall g : G, H g <~> K g
H1: IsSubgroup H
x: G
inx: H x
K x^
    exact (p _ (issubgroup_in_inv x inx)).
Defined.

(** ** Definition of subgroup *) 

(** The type (set) of subgroups of a group G. *)
Record Subgroup (G : Group) := {
  subgroup_pred : G -> Type ;
  subgroup_issubgroup :: IsSubgroup subgroup_pred ;
}.

Coercion subgroup_pred : Subgroup >-> Funclass.

Definition issig_subgroup {G : Group} : _ <~> Subgroup G
  := ltac:(issig).

(** ** Basics properties of subgroups *)

Definition Build_Subgroup' {G : Group}
  (H : G -> Type) `{forall x, IsHProp (H x)}
  (unit : H mon_unit)
  (c : forall x y, H x -> H y -> H (x * y^))
  : Subgroup G.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
Subgroup G
Proof.G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
Subgroup G
  refine (Build_Subgroup G H _).G: Group
H: G -> Type
H0: forall x : G, IsHProp (H x)
unit: H 1
c: forall x y : G, H x -> H y -> H (x * y^)
IsSubgroup H
  rapply Build_IsSubgroup'; assumption.
Defined.

Section SubgroupElements.
  Context {G : Group} (H : Subgroup G) (x y : G).
  Definition subgroup_in_unit : H 1 := issubgroup_in_unit.
  Definition subgroup_in_inv : H x -> H x^ := issubgroup_in_inv x.
  Definition subgroup_in_inv' : H x^ -> H x := issubgroup_in_inv' x.
  Definition subgroup_in_op : H x -> H y -> H (x * y) := issubgroup_in_op x y.
  Definition subgroup_in_op_inv : H x -> H y -> H (x * y^) := issubgroup_in_op_inv x y.
  Definition subgroup_in_inv_op : H x -> H y -> H (x^ * y) := issubgroup_in_inv_op x y.
  Definition subgroup_in_op_l : H (x * y) -> H y -> H x := issubgroup_in_op_l x y.
  Definition subgroup_in_op_r : H (x * y) -> H x -> H y := issubgroup_in_op_r x y.
End SubgroupElements.

Instance isequiv_subgroup_in_inv `(H : Subgroup G) (x : G)
  : IsEquiv (subgroup_in_inv H x).G: Group
H: Subgroup G
x: G
IsEquiv (subgroup_in_inv H x)
Proof.G: Group
H: Subgroup G
x: G
IsEquiv (subgroup_in_inv H x)
  srapply isequiv_iff_hprop.G: Group
H: Subgroup G
x: G
H x^ -> H x
  apply subgroup_in_inv'.
Defined.

Definition equiv_subgroup_inv {G : Group} (H : Subgroup G) (x : G)
  : H x <~> H x^ := Build_Equiv _ _ (subgroup_in_inv H x) _.

Definition equiv_subgroup_op_inv {G : Group} (H : Subgroup G) (x y : G)
  : H (x * y^) <~> H (y * x^).G: Group
H: Subgroup G
x, y: G
H (x * y^) <~> H (y * x^)
Proof.G: Group
H: Subgroup G
x, y: G
H (x * y^) <~> H (y * x^)
  nrefine (_ oE equiv_subgroup_inv _ _).G: Group
H: Subgroup G
x, y: G
H (x * y^)^ <~> H (y * x^)
  by rewrite grp_inv_op, grp_inv_inv.
Defined.

(** Paths between subgroups correspond to homotopies between the underlying predicates. *) 
Proposition equiv_path_subgroup `{F : Funext} {G : Group} (H K : Subgroup G)
  : (H == K) <~> (H = K).F: Funext
G: Group
H, K: Subgroup G
H == K <~> H = K
Proof.F: Funext
G: Group
H, K: Subgroup G
H == K <~> H = K
  refine ((equiv_ap' issig_subgroup^-1%equiv _ _)^-1%equiv oE _); cbn.F: Funext
G: Group
H, K: Subgroup G
H == K <~>
(H; subgroup_issubgroup G H) =
(K; subgroup_issubgroup G K)
  refine (equiv_path_sigma_hprop _ _ oE _); cbn.F: Funext
G: Group
H, K: Subgroup G
H == K <~> H = K
  apply equiv_path_arrow.
Defined.

Proposition equiv_path_subgroup' `{U : Univalence} {G : Group} (H K : Subgroup G)
  : (forall g:G, H g <-> K g) <~> (H = K).U: Univalence
G: Group
H, K: Subgroup G
(forall g : G, H g <-> K g) <~> H = K
Proof.U: Univalence
G: Group
H, K: Subgroup G
(forall g : G, H g <-> K g) <~> H = K
  refine (equiv_path_subgroup _ _ oE _).U: Univalence
G: Group
H, K: Subgroup G
(forall g : G, H g <-> K g) <~> H == K
  apply equiv_functor_forall_id; intro g.U: Univalence
G: Group
H, K: Subgroup G
g: G
(H g <-> K g) <~> H g = K g
  exact equiv_path_iff_ishprop.
Defined.

Instance ishset_subgroup `{Univalence} {G : Group} : IsHSet (Subgroup G).H: Univalence
G: Group
IsHSet (Subgroup G)
Proof.H: Univalence
G: Group
IsHSet (Subgroup G)
  nrefine (istrunc_equiv_istrunc _ issig_subgroup).H: Univalence
G: Group
IsHSet {H : G -> Type & IsSubgroup H}
  nrefine (istrunc_equiv_istrunc _ (equiv_functor_sigma_id _)).H: Univalence
G: Group
forall a : G -> Type, ?Goal a <~> IsSubgroup a
H: Univalence
G: Group
IsHSet {x : _ & ?Goal x}
  -H: Univalence
G: Group
forall a : G -> Type, ?Goal a <~> IsSubgroup a intro P; apply issig_issubgroup.
  -H: Univalence
G: Group
IsHSet
  {P : G -> Type &
  {_ : forall x : G, IsHProp (P x) &
  {_ : P 1 &
  {_ : forall x y : G, P x -> P y -> P (x * y) &
  forall x : G, P x -> P x^}}}} nrefine (istrunc_equiv_istrunc _ (equiv_sigma_assoc' _ _)^-1%equiv).H: Univalence
G: Group
IsHSet
  {ap : {a : G -> Type & forall x : G, IsHProp (a x)}
  &
  {_ : ap.1 1 &
  {_
  : forall x y : G, ap.1 x -> ap.1 y -> ap.1 (x * y) &
  forall x : G, ap.1 x -> ap.1 x^}}}
    napply istrunc_sigma.H: Univalence
G: Group
IsHSet {a : G -> Type & forall x : G, IsHProp (a x)}
H: Univalence
G: Group
forall
a : {a : G -> Type & forall x : G, IsHProp (a x)},
IsHSet
  {_ : a.1 1 &
  {_ : forall x y : G, a.1 x -> a.1 y -> a.1 (x * y) &
  forall x : G, a.1 x -> a.1 x^}}
    2: intros []; apply istrunc_hprop.H: Univalence
G: Group
IsHSet {a : G -> Type & forall x : G, IsHProp (a x)}
    nrefine (istrunc_equiv_istrunc
               _ (equiv_sig_coind (fun g:G => Type) (fun g x => IsHProp x))^-1%equiv).H: Univalence
G: Group
IsHSet (G -> {x : Type & IsHProp x})
    apply istrunc_forall.
Defined.

(** ** Underlying group of a subgroup *)

(** The group given by a subgroup *)
Definition subgroup_group {G : Group} (H : Subgroup G) : Group.G: Group
H: Subgroup G
Group
Proof.G: Group
H: Subgroup G
Group
  apply (Build_Group (sig H)
      (fun x y => (x.1 * y.1 ; issubgroup_in_op x.1 y.1 x.2 y.2))
      (1; issubgroup_in_unit)
      (fun x => (- x.1 ; issubgroup_in_inv _ x.2))).G: Group
H: Subgroup G
IsGroup {x : _ & H x}
  1: repeat split.G: Group
H: Subgroup G
IsHSet {x : _ & H x}
G: Group
H: Subgroup G
Associative sg_op
G: Group
H: Subgroup G
LeftIdentity sg_op 1
G: Group
H: Subgroup G
RightIdentity sg_op 1
G: Group
H: Subgroup G
LeftInverse sg_op inv 1
G: Group
H: Subgroup G
RightInverse sg_op inv 1
  1: exact _.G: Group
H: Subgroup G
Associative sg_op
G: Group
H: Subgroup G
LeftIdentity sg_op 1
G: Group
H: Subgroup G
RightIdentity sg_op 1
G: Group
H: Subgroup G
LeftInverse sg_op inv 1
G: Group
H: Subgroup G
RightInverse sg_op inv 1
  1-5: grp_auto.
Defined.

Coercion subgroup_group : Subgroup >-> Group.

(** The underlying group of a subgroup of [G] has an inclusion map into [G]. *) 
Definition subgroup_incl {G : Group} (H : Subgroup G)
  : subgroup_group H $-> G.G: Group
H: Subgroup G
H $-> G
Proof.G: Group
H: Subgroup G
H $-> G
  snapply Build_GroupHomomorphism.G: Group
H: Subgroup G
H -> G
G: Group
H: Subgroup G
IsSemiGroupPreserving ?grp_homo_map
  1: exact pr1.G: Group
H: Subgroup G
IsSemiGroupPreserving pr1
  hnf; reflexivity.
Defined.

(** The inclusion map is an embedding. *)
Instance isembedding_subgroup_incl {G : Group} (H : Subgroup G)
  : IsEmbedding (subgroup_incl H)
  := fun _ => istrunc_equiv_istrunc _ (hfiber_fibration _ _).

(** Restriction of a group homomorphism to a subgroup. *)
Definition grp_homo_restr {G H : Group} (f : G $-> H) (K : Subgroup G)
  : subgroup_group K $-> H
  := f $o subgroup_incl _.

(** Corestriction of a group homomorphism to a subgroup. *)
Definition subgroup_corec {G H : Group} {K : Subgroup H}
  (f : G $-> H) (g : forall x, K (f x))
  : G $-> subgroup_group K.G, H: Group
K: Subgroup H
f: G $-> H
g: forall x : G, K (f x)
G $-> K
Proof.G, H: Group
K: Subgroup H
f: G $-> H
g: forall x : G, K (f x)
G $-> K
  snapply Build_GroupHomomorphism.G, H: Group
K: Subgroup H
f: G $-> H
g: forall x : G, K (f x)
G -> K
G, H: Group
K: Subgroup H
f: G $-> H
g: forall x : G, K (f x)
IsSemiGroupPreserving ?grp_homo_map
  -G, H: Group
K: Subgroup H
f: G $-> H
g: forall x : G, K (f x)
G -> K exact (fun x => (f x; g x)).
  -G, H: Group
K: Subgroup H
f: G $-> H
g: forall x : G, K (f x)
IsSemiGroupPreserving (fun x : G => (f x; g x)) intros x y.G, H: Group
K: Subgroup H
f: G $-> H
g: forall x : G, K (f x)
x, y: G
(f (x * y); g (x * y)) = (f x; g x) * (f y; g y)
    rapply path_sigma_hprop.G, H: Group
K: Subgroup H
f: G $-> H
g: forall x : G, K (f x)
x, y: G
(f (x * y); g (x * y)).1 = ((f x; g x) * (f y; g y)).1
    snapply grp_homo_op.
Defined.

(** Corestriction is an equivalence on group homomorphisms. *)
Definition equiv_subgroup_corec {F : Funext}
  (G : Group) {H : Group} (K : Subgroup H)
  : {f : G $-> H & forall x, K (f x)} <~> (G $-> subgroup_group K).F: Funext
G, H: Group
K: Subgroup H
{f : G $-> H & forall x : G, K (f x)} <~> (G $-> K)
Proof.F: Funext
G, H: Group
K: Subgroup H
{f : G $-> H & forall x : G, K (f x)} <~> (G $-> K)
  snapply equiv_adjointify.F: Funext
G, H: Group
K: Subgroup H
{f : G $-> H & forall x : G, K (f x)} -> G $-> K
F: Funext
G, H: Group
K: Subgroup H
(G $-> K) -> {f : G $-> H & forall x : G, K (f x)}
F: Funext
G, H: Group
K: Subgroup H
?f o ?g == idmap
F: Funext
G, H: Group
K: Subgroup H
?g o ?f == idmap
  -F: Funext
G, H: Group
K: Subgroup H
{f : G $-> H & forall x : G, K (f x)} -> G $-> K exact (sig_rec subgroup_corec).
  -F: Funext
G, H: Group
K: Subgroup H
(G $-> K) -> {f : G $-> H & forall x : G, K (f x)} intros g.F: Funext
G, H: Group
K: Subgroup H
g: G $-> K
{f : G $-> H & forall x : G, K (f x)}
    exists (subgroup_incl _ $o g).F: Funext
G, H: Group
K: Subgroup H
g: G $-> K
forall x : G, K ((subgroup_incl K $o g) x)
    intros x.F: Funext
G, H: Group
K: Subgroup H
g: G $-> K
x: G
K ((subgroup_incl K $o g) x)
    exact (g x).2.
  -F: Funext
G, H: Group
K: Subgroup H
sig_rec subgroup_corec
o (fun g : G $-> K =>
   (subgroup_incl K $o g; fun x : G => (g x).2)) ==
idmap intros g.F: Funext
G, H: Group
K: Subgroup H
g: G $-> K
sig_rec subgroup_corec
  (subgroup_incl K $o g; fun x : G => (g x).2) = g
    by snapply equiv_path_grouphomomorphism.
  -F: Funext
G, H: Group
K: Subgroup H
(fun g : G $-> K =>
 (subgroup_incl K $o g; fun x : G => (g x).2))
o sig_rec subgroup_corec == idmap intros [f p].F: Funext
G, H: Group
K: Subgroup H
f: G $-> H
p: forall x : G, K (f x)
(subgroup_incl K $o sig_rec subgroup_corec (f; p);
fun x : G => (sig_rec subgroup_corec (f; p) x).2) =
(f; p)
    rapply path_sigma_hprop.F: Funext
G, H: Group
K: Subgroup H
f: G $-> H
p: forall x : G, K (f x)
(subgroup_incl K $o sig_rec subgroup_corec (f; p);
fun x : G => (sig_rec subgroup_corec (f; p) x).2).1 =
(f; p).1
    by snapply equiv_path_grouphomomorphism.
Defined.

(** Functoriality on subgroups. *)
Definition functor_subgroup_group {G H : Group} {J : Subgroup G} {K : Subgroup H}
  (f : G $-> H) (g : forall x, J x -> K (f x))
  : subgroup_group J $-> subgroup_group K
  := subgroup_corec (grp_homo_restr f J) (sig_ind _ g).

Definition grp_iso_subgroup_group {G H : Group@{i}}
  {J : Subgroup@{i i} G} {K : Subgroup@{i i} H}
  (e : G $<~> H) (f : forall x, J x <-> K (e x))
  : subgroup_group J $<~> subgroup_group K.G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
J $<~> K
Proof.G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
J $<~> K
  snapply cate_adjointify.G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
J $-> K
G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
K $-> J
G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
?f $o ?g $== Id K
G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
?g $o ?f $== Id J
  -G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
J $-> K exact (functor_subgroup_group e (fun x => fst (f x))).
  -G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
K $-> J nrefine (functor_subgroup_group e^-1$ _).G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
forall x : H, K x -> J (e^-1$ x)
    equiv_intro e x.G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
x: G
K (e x) -> J (e^-1$ (e x)) 
    intros k.G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
x: G
k: K (e x)
J (e^-1$ (e x))
    nrefine ((eissect e _)^ # _).G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
x: G
k: K (e x)
J x
    exact (snd (f x) k).
  -G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
functor_subgroup_group e (fun x : G => fst (f x)) $o
functor_subgroup_group e^-1$
  (equiv_ind e (fun x : H => K x -> J (e^-1$ x))
     (fun (x : G) (k : K (e x)) =>
      transport J (eissect e x)^ (snd (f x) k))
   :
   forall x : H, K x -> J (e^-1$ x)) $== Id K intros x.G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
x: K
(functor_subgroup_group e (fun x : G => fst (f x)) $o
 functor_subgroup_group e^-1$
   (equiv_ind e (fun x : H => K x -> J (e^-1$ x))
      (fun (x : G) (k : K (e x)) =>
       transport J (eissect e x)^ (snd (f x) k)))) x =
Id K x
    rapply path_sigma_hprop.G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
x: K
((functor_subgroup_group e (fun x : G => fst (f x)) $o
  functor_subgroup_group e^-1$
    (equiv_ind e (fun x : H => K x -> J (e^-1$ x))
       (fun (x : G) (k : K (e x)) =>
        transport J (eissect e x)^ (snd (f x) k)))) x).1 =
(Id K x).1
    napply eisretr.
  -G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
functor_subgroup_group e^-1$
  (equiv_ind e (fun x : H => K x -> J (e^-1$ x))
     (fun (x : G) (k : K (e x)) =>
      transport J (eissect e x)^ (snd (f x) k))
   :
   forall x : H, K x -> J (e^-1$ x)) $o
functor_subgroup_group e (fun x : G => fst (f x)) $==
Id J intros x.G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
x: J
(functor_subgroup_group e^-1$
   (equiv_ind e (fun x : H => K x -> J (e^-1$ x))
      (fun (x : G) (k : K (e x)) =>
       transport J (eissect e x)^ (snd (f x) k))) $o
 functor_subgroup_group e (fun x : G => fst (f x))) x =
Id J x
    rapply path_sigma_hprop.G, H: Group
J: Subgroup G
K: Subgroup H
e: G $<~> H
f: forall x : G, J x <-> K (e x)
x: J
((functor_subgroup_group e^-1$
    (equiv_ind e (fun x : H => K x -> J (e^-1$ x))
       (fun (x : G) (k : K (e x)) =>
        transport J (eissect e x)^ (snd (f x) k))) $o
  functor_subgroup_group e (fun x : G => fst (f x))) x).1 =
(Id J x).1
    napply eissect.
Defined.

(** ** Cosets of subgroups *)

Section Cosets.

  (** Left and right cosets give equivalence relations. *)

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

  (** The relation of being in a left coset represented by an element. *)
  Definition in_cosetL : Relation G := fun x y => H (x^ * y).
  (** The relation of being in a right coset represented by an element. *)
  Definition in_cosetR : Relation G := fun x y => H (x * y^).

  Hint Extern 4 => progress unfold in_cosetL : typeclass_instances.
  Hint Extern 4 => progress unfold in_cosetR : typeclass_instances.

  Global Arguments in_cosetL /.
  Global Arguments in_cosetR /.

  (** These are props *)
  #[export] Instance ishprop_in_cosetL : is_mere_relation G in_cosetL := _.
  #[export] Instance ishprop_in_cosetR : is_mere_relation G in_cosetR := _.

  (** In fact, they are both equivalence relations. *)
  #[export] Instance reflexive_in_cosetL : Reflexive in_cosetL.G: Group
H: Subgroup G
Reflexive in_cosetL
  Proof.G: Group
H: Subgroup G
Reflexive in_cosetL
    intro x; hnf.G: Group
H: Subgroup G
x: G
H (x^ * x)
    rewrite left_inverse.G: Group
H: Subgroup G
x: G
H 1
    exact issubgroup_in_unit.
  Defined.

  #[export] Instance reflexive_in_cosetR : Reflexive in_cosetR.G: Group
H: Subgroup G
Reflexive in_cosetR
  Proof.G: Group
H: Subgroup G
Reflexive in_cosetR
    intro x; hnf.G: Group
H: Subgroup G
x: G
H (x * x^)
    rewrite right_inverse.G: Group
H: Subgroup G
x: G
H 1
    exact issubgroup_in_unit.
  Defined.

  #[export] Instance symmetric_in_cosetL : Symmetric in_cosetL.G: Group
H: Subgroup G
Symmetric in_cosetL
  Proof.G: Group
H: Subgroup G
Symmetric in_cosetL
    intros x y h; cbn; cbn in h.G: Group
H: Subgroup G
x, y: G
h: H (x^ * y)
H (y^ * x)
    rewrite <- (grp_inv_inv x).G: Group
H: Subgroup G
x, y: G
h: H (x^ * y)
H (y^ * (x^)^)
    rewrite <- grp_inv_op.G: Group
H: Subgroup G
x, y: G
h: H (x^ * y)
H (x^ * y)^
    apply issubgroup_in_inv; assumption.
  Defined.

  #[export] Instance symmetric_in_cosetR : Symmetric in_cosetR.G: Group
H: Subgroup G
Symmetric in_cosetR
  Proof.G: Group
H: Subgroup G
Symmetric in_cosetR
    intros x y h; cbn; cbn in h.G: Group
H: Subgroup G
x, y: G
h: H (x * y^)
H (y * x^)
    rewrite <- (grp_inv_inv y).G: Group
H: Subgroup G
x, y: G
h: H (x * y^)
H ((y^)^ * x^)
    rewrite <- grp_inv_op.G: Group
H: Subgroup G
x, y: G
h: H (x * y^)
H (x * y^)^
    apply issubgroup_in_inv; assumption.
  Defined.

  #[export] Instance transitive_in_cosetL : Transitive in_cosetL.G: Group
H: Subgroup G
Transitive in_cosetL
  Proof.G: Group
H: Subgroup G
Transitive in_cosetL
    intros x y z h k; cbn; cbn in h; cbn in k.G: Group
H: Subgroup G
x, y, z: G
h: H (x^ * y)
k: H (y^ * z)
H (x^ * z)
    rewrite <- (right_identity x^).G: Group
H: Subgroup G
x, y, z: G
h: H (x^ * y)
k: H (y^ * z)
H (x^ * 1 * z)
    rewrite <- (right_inverse y : y * y^ = mon_unit).G: Group
H: Subgroup G
x, y, z: G
h: H (x^ * y)
k: H (y^ * z)
H (x^ * (y * y^) * z)
    rewrite (associativity x^ _ _).G: Group
H: Subgroup G
x, y, z: G
h: H (x^ * y)
k: H (y^ * z)
H (x^ * y * y^ * z)
    rewrite <- simple_associativity.G: Group
H: Subgroup G
x, y, z: G
h: H (x^ * y)
k: H (y^ * z)
H (x^ * y * (y^ * z))
    apply issubgroup_in_op; assumption.
  Defined.

  #[export] Instance transitive_in_cosetR : Transitive in_cosetR.G: Group
H: Subgroup G
Transitive in_cosetR
  Proof.G: Group
H: Subgroup G
Transitive in_cosetR
    intros x y z h k; cbn; cbn in h; cbn in k.G: Group
H: Subgroup G
x, y, z: G
h: H (x * y^)
k: H (y * z^)
H (x * z^)
    rewrite <- (right_identity x).G: Group
H: Subgroup G
x, y, z: G
h: H (x * y^)
k: H (y * z^)
H (x * 1 * z^)
    rewrite <- (left_inverse y : y^ * y = mon_unit).G: Group
H: Subgroup G
x, y, z: G
h: H (x * y^)
k: H (y * z^)
H (x * (y^ * y) * z^)
    rewrite (simple_associativity x).G: Group
H: Subgroup G
x, y, z: G
h: H (x * y^)
k: H (y * z^)
H (x * y^ * y * z^)
    rewrite <- (associativity _ _ z^).G: Group
H: Subgroup G
x, y, z: G
h: H (x * y^)
k: H (y * z^)
H (x * y^ * (y * z^))
    apply issubgroup_in_op; assumption.
  Defined.

End Cosets.

(** ** Properties of left and right cosets *)

Definition in_cosetL_unit {G : Group} {N : Subgroup G}
  : forall x y, in_cosetL N (x^ * y) mon_unit <~> in_cosetL N x y.G: Group
N: Subgroup G
forall x y : G,
in_cosetL N (x^ * y) 1 <~> in_cosetL N x y
Proof.G: Group
N: Subgroup G
forall x y : G,
in_cosetL N (x^ * y) 1 <~> in_cosetL N x y
  intros x y; cbn.G: Group
N: Subgroup G
x, y: G
N ((x^ * y)^ * 1) <~> N (x^ * y)
  rewrite (right_identity _^).G: Group
N: Subgroup G
x, y: G
N (x^ * y)^ <~> N (x^ * y)
  rewrite (inverse_sg_op _).G: Group
N: Subgroup G
x, y: G
N (y^ * (x^)^) <~> N (x^ * y)
  rewrite (inverse_involutive _).G: Group
N: Subgroup G
x, y: G
N (y^ * x) <~> N (x^ * y)
  apply equiv_iff_hprop; apply symmetric_in_cosetL.
Defined.

Definition in_cosetR_unit {G : Group} {N : Subgroup G}
  : forall x y, in_cosetR N (x * y^) mon_unit <~> in_cosetR N x y.G: Group
N: Subgroup G
forall x y : G,
in_cosetR N (x * y^) 1 <~> in_cosetR N x y
Proof.G: Group
N: Subgroup G
forall x y : G,
in_cosetR N (x * y^) 1 <~> in_cosetR N x y
  intros x y; cbn.G: Group
N: Subgroup G
x, y: G
N (x * y^ * 1^) <~> N (x * y^)
  rewrite inverse_mon_unit.G: Group
N: Subgroup G
x, y: G
N (x * y^ * 1) <~> N (x * y^)
  rewrite (right_identity (x * y^)).G: Group
N: Subgroup G
x, y: G
N (x * y^) <~> N (x * y^)
  reflexivity.
Defined.

(** Symmetry is an equivalence. *)
Definition equiv_in_cosetL_symm {G : Group} {N : Subgroup G}
  : forall x y, in_cosetL N x y <~> in_cosetL N y x.G: Group
N: Subgroup G
forall x y : G, in_cosetL N x y <~> in_cosetL N y x
Proof.G: Group
N: Subgroup G
forall x y : G, in_cosetL N x y <~> in_cosetL N y x
  intros x y.G: Group
N: Subgroup G
x, y: G
in_cosetL N x y <~> in_cosetL N y x
  srapply equiv_iff_hprop.G: Group
N: Subgroup G
x, y: G
in_cosetL N x y -> in_cosetL N y x
G: Group
N: Subgroup G
x, y: G
in_cosetL N y x -> in_cosetL N x y
  all: by intro.
Defined.

Definition equiv_in_cosetR_symm {G : Group} {N : Subgroup G}
  : forall x y, in_cosetR N x y <~> in_cosetR N y x.G: Group
N: Subgroup G
forall x y : G, in_cosetR N x y <~> in_cosetR N y x
Proof.G: Group
N: Subgroup G
forall x y : G, in_cosetR N x y <~> in_cosetR N y x
  intros x y.G: Group
N: Subgroup G
x, y: G
in_cosetR N x y <~> in_cosetR N y x
  srapply equiv_iff_hprop.G: Group
N: Subgroup G
x, y: G
in_cosetR N x y -> in_cosetR N y x
G: Group
N: Subgroup G
x, y: G
in_cosetR N y x -> in_cosetR N x y
  all: by intro.
Defined.

(** The sigma type of a left coset is equivalent to the sigma type of the subgroup. *)
Definition equiv_sigma_in_cosetL_subgroup (G : Group) (H : Subgroup G) (x : G)
  : sig (in_cosetL H x) <~> sig H.G: Group
H: Subgroup G
x: G
{x0 : _ & in_cosetL H x x0} <~> {x : _ & H x}
Proof.G: Group
H: Subgroup G
x: G
{x0 : _ & in_cosetL H x x0} <~> {x : _ & H x}
  snapply equiv_functor_sigma'.G: Group
H: Subgroup G
x: G
G <~> G
G: Group
H: Subgroup G
x: G
forall a : G, in_cosetL H x a <~> H (?f a)
  -G: Group
H: Subgroup G
x: G
G <~> G rapply (Build_Equiv _ _ (x^ *.)).
  -G: Group
H: Subgroup G
x: G
forall a : G,
in_cosetL H x a <~>
H
  ({|
     equiv_fun := sg_op x^;
     equiv_isequiv := isequiv_group_left_op x^
   |} a) reflexivity.
Defined.

(** The sigma type of a right coset is equivalent to the sigma type of the subgroup. *)
Definition equiv_sigma_in_cosetR_subgroup (G : Group) (H : Subgroup G) (x : G)
  : sig (in_cosetR H x) <~> sig H.G: Group
H: Subgroup G
x: G
{x0 : _ & in_cosetR H x x0} <~> {x : _ & H x}
Proof.G: Group
H: Subgroup G
x: G
{x0 : _ & in_cosetR H x x0} <~> {x : _ & H x}
  snapply equiv_functor_sigma'.G: Group
H: Subgroup G
x: G
G <~> G
G: Group
H: Subgroup G
x: G
forall a : G, in_cosetR H x a <~> H (?f a)
  -G: Group
H: Subgroup G
x: G
G <~> G rapply (Build_Equiv _ _ (.* x ^)).
  -G: Group
H: Subgroup G
x: G
forall a : G,
in_cosetR H x a <~>
H
  ({|
     equiv_fun := fun y : G => y * x^;
     equiv_isequiv := isequiv_group_right_op G x^
   |} a) simpl; intros y.G: Group
H: Subgroup G
x, y: G
H (x * y^) <~> H (y * x^)
    apply equiv_subgroup_op_inv.
Defined.

(** ** Normal subgroups *)

(** A normal subgroup is a subgroup closed under conjugation. *)
Class IsNormalSubgroup {G : Group} (N : Subgroup G)
  := isnormal : forall {x y}, N (x * y) -> N (y * x).

Record NormalSubgroup (G : Group) := {
  normalsubgroup_subgroup : Subgroup G ;
  normalsubgroup_isnormal :: IsNormalSubgroup normalsubgroup_subgroup ;
}.

Arguments Build_NormalSubgroup G N _ : rename.

Coercion normalsubgroup_subgroup : NormalSubgroup >-> Subgroup.

Definition equiv_symmetric_in_normalsubgroup {G : Group}
  (N : Subgroup G) `{!IsNormalSubgroup N}
  : forall x y, N (x * y) <~> N (y * x).G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
forall x y : G, N (x * y) <~> N (y * x)
Proof.G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
forall x y : G, N (x * y) <~> N (y * x)
  intros x y.G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x, y: G
N (x * y) <~> N (y * x)
  rapply equiv_iff_hprop.G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x, y: G
N (x * y) -> N (y * x)
G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x, y: G
N (y * x) -> N (x * y)
  all: exact isnormal.
Defined.

(** Our definition of normal subgroup implies the usual definition of invariance under conjugation. *)
Definition isnormal_conj {G : Group} (N : Subgroup G)
  `{!IsNormalSubgroup N} {x y : G}
  : N x <~> N (y * x * y^).G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x, y: G
N x <~> N (y * x * y^)
Proof.G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x, y: G
N x <~> N (y * x * y^)
  srefine (equiv_symmetric_in_normalsubgroup N _ _ oE _).G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x, y: G
N x <~> N (y^ * (y * x))
  by rewrite grp_inv_V_gg.
Defined.

(** We can show a subgroup is normal if it is invariant under conjugation. *)
Definition Build_IsNormalSubgroup' (G : Group) (N : Subgroup G)
  (isnormal : forall x y, N x -> N (y * x * y^))
  : IsNormalSubgroup N.G: Group
N: Subgroup G
isnormal: forall x y : G, N x -> N (y * x * y^)
IsNormalSubgroup N
Proof.G: Group
N: Subgroup G
isnormal: forall x y : G, N x -> N (y * x * y^)
IsNormalSubgroup N
  intros x y n.G: Group
N: Subgroup G
isnormal: forall x y : G, N x -> N (y * x * y^)
x, y: G
n: N (x * y)
N (y * x)
  nrefine (transport N (grp_unit_r _) _).G: Group
N: Subgroup G
isnormal: forall x y : G, N x -> N (y * x * y^)
x, y: G
n: N (x * y)
N (y * x * 1)
  nrefine (transport (fun z => N (_ * z)) (grp_inv_r y) _).G: Group
N: Subgroup G
isnormal: forall x y : G, N x -> N (y * x * y^)
x, y: G
n: N (x * y)
N (y * x * (y * y^))
  nrefine (transport N (grp_assoc _ _ _)^ _).G: Group
N: Subgroup G
isnormal: forall x y : G, N x -> N (y * x * y^)
x, y: G
n: N (x * y)
N (y * x * y * y^)
  nrefine (transport (fun z => N (z * _)) (grp_assoc _ _ _) _).G: Group
N: Subgroup G
isnormal: forall x y : G, N x -> N (y * x * y^)
x, y: G
n: N (x * y)
N (y * (x * y) * y^)
  by apply isnormal.
Defined.

(** Under funext, being a normal subgroup is a hprop. *)
Instance ishprop_isnormalsubgroup `{Funext} {G : Group} (N : Subgroup G)
  : IsHProp (IsNormalSubgroup N).H: Funext
G: Group
N: Subgroup G
IsHProp (IsNormalSubgroup N)
Proof.H: Funext
G: Group
N: Subgroup G
IsHProp (IsNormalSubgroup N) 
  unfold IsNormalSubgroup; exact _.
Defined.

(** Our definition of normal subgroup and the usual definition are therefore equivalent. *)
Definition equiv_isnormal_conjugate `{Funext} {G : Group} (N : Subgroup G)
  : IsNormalSubgroup N <~> (forall x y, N x -> N (y * x * y^)).H: Funext
G: Group
N: Subgroup G
IsNormalSubgroup N <~>
(forall x y : G, N x -> N (y * x * y^))
Proof.H: Funext
G: Group
N: Subgroup G
IsNormalSubgroup N <~>
(forall x y : G, N x -> N (y * x * y^))
  rapply equiv_iff_hprop.H: Funext
G: Group
N: Subgroup G
IsNormalSubgroup N ->
forall x y : G, N x -> N (y * x * y^)
H: Funext
G: Group
N: Subgroup G
(forall x y : G, N x -> N (y * x * y^)) ->
IsNormalSubgroup N
  -H: Funext
G: Group
N: Subgroup G
IsNormalSubgroup N ->
forall x y : G, N x -> N (y * x * y^) intros is_normal x y.H: Funext
G: Group
N: Subgroup G
is_normal: IsNormalSubgroup N
x, y: G
N x -> N (y * x * y^)
    rapply isnormal_conj.
  -H: Funext
G: Group
N: Subgroup G
(forall x y : G, N x -> N (y * x * y^)) ->
IsNormalSubgroup N intros is_normal'.H: Funext
G: Group
N: Subgroup G
is_normal': forall x y : G, N x -> N (y * x * y^)
IsNormalSubgroup N
    by snapply Build_IsNormalSubgroup'.
Defined.

(** Inner automorphisms of a group [G] restrict to automorphisms of normal subgroups. *)
Definition grp_iso_normal_conj {G : Group} (N : Subgroup G)
  `{!IsNormalSubgroup N} (x : G)
  : subgroup_group N $<~> subgroup_group N.G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x: G
N $<~> N
Proof.G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x: G
N $<~> N
  snapply grp_iso_subgroup_group.G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x: G
G $<~> G
G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x: G
forall x0 : G, N x0 <-> N (?e x0)
  -G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x: G
G $<~> G exact (grp_iso_conj x).
  -G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x: G
forall x0 : G, N x0 <-> N (grp_iso_conj x x0) intros y.G: Group
N: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup N
x, y: G
N y <-> N (grp_iso_conj x y)
    rapply isnormal_conj.
Defined.

(** Left and right cosets are equivalent in normal subgroups. *)
Definition equiv_in_cosetL_in_cosetR_normalsubgroup {G : Group}
  (N : NormalSubgroup G) (x y : G)
  : in_cosetL N x y <~> in_cosetR N x y
  := equiv_in_cosetR_symm _ _ oE equiv_symmetric_in_normalsubgroup _ _ _.

(** Inverses are then respected *)
Definition in_cosetL_inverse {G : Group} {N : NormalSubgroup G} (x y : G)
  : in_cosetL N x^ y^ <~> in_cosetL N x y.G: Group
N: NormalSubgroup G
x, y: G
in_cosetL N x^ y^ <~> in_cosetL N x y
Proof.G: Group
N: NormalSubgroup G
x, y: G
in_cosetL N x^ y^ <~> in_cosetL N x y
  refine (_ oE equiv_in_cosetL_in_cosetR_normalsubgroup _ _ _); cbn.G: Group
N: NormalSubgroup G
x, y: G
N (x^ * (y^)^) <~> N (x^ * y)
  by rewrite inverse_involutive.
Defined.

Definition in_cosetR_inverse {G : Group} {N : NormalSubgroup G} (x y : G)
  : in_cosetR N x^ y^ <~> in_cosetR N x y.G: Group
N: NormalSubgroup G
x, y: G
in_cosetR N x^ y^ <~> in_cosetR N x y
Proof.G: Group
N: NormalSubgroup G
x, y: G
in_cosetR N x^ y^ <~> in_cosetR N x y
  refine (_ oE equiv_in_cosetL_in_cosetR_normalsubgroup _ _ _); cbn.G: Group
N: NormalSubgroup G
x, y: G
N (x * ((y^)^)^) <~> N (x * y^)
  by rewrite grp_inv_inv.
Defined.

(** This lets us prove that left and right coset relations are congruences. *)
Definition in_cosetL_cong {G : Group} {N : NormalSubgroup G}
  (x x' y y' : G)
  : in_cosetL N x y -> in_cosetL N x' y' -> in_cosetL N (x * x') (y * y').G: Group
N: NormalSubgroup G
x, x', y, y': G
in_cosetL N x y ->
in_cosetL N x' y' -> in_cosetL N (x * x') (y * y')
Proof.G: Group
N: NormalSubgroup G
x, x', y, y': G
in_cosetL N x y ->
in_cosetL N x' y' -> in_cosetL N (x * x') (y * y')
  cbn; intros p q.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x^ * y)
q: N (x'^ * y')
N ((x * x')^ * (y * y'))
  (** rewrite goal before applying subgroup_op *)
  rewrite inverse_sg_op, <- simple_associativity.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x^ * y)
q: N (x'^ * y')
N (x'^ * (x^ * (y * y')))
  apply isnormal.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x^ * y)
q: N (x'^ * y')
N (x^ * (y * y') * x'^)
  rewrite simple_associativity, <- simple_associativity.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x^ * y)
q: N (x'^ * y')
N (x^ * y * (y' * x'^))
  apply subgroup_in_op.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x^ * y)
q: N (x'^ * y')
N (x^ * y)
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x^ * y)
q: N (x'^ * y')
N (y' * x'^)
  1: exact p.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x^ * y)
q: N (x'^ * y')
N (y' * x'^)
  apply isnormal.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x^ * y)
q: N (x'^ * y')
N (x'^ * y')
  exact q.
Defined.

Definition in_cosetR_cong  {G : Group} {N : NormalSubgroup G}
  (x x' y y' : G)
  : in_cosetR N x y -> in_cosetR N x' y' -> in_cosetR N (x * x') (y * y').G: Group
N: NormalSubgroup G
x, x', y, y': G
in_cosetR N x y ->
in_cosetR N x' y' -> in_cosetR N (x * x') (y * y')
Proof.G: Group
N: NormalSubgroup G
x, x', y, y': G
in_cosetR N x y ->
in_cosetR N x' y' -> in_cosetR N (x * x') (y * y')
  cbn; intros p q.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * y^)
q: N (x' * y'^)
N (x * x' * (y * y')^)
  (** rewrite goal before applying subgroup_op *)
  rewrite inverse_sg_op, simple_associativity.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * y^)
q: N (x' * y'^)
N (x * x' * y'^ * y^)
  apply isnormal.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * y^)
q: N (x' * y'^)
N (y^ * (x * x' * y'^))
  rewrite <- simple_associativity, simple_associativity.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * y^)
q: N (x' * y'^)
N (y^ * x * (x' * y'^))
  apply subgroup_in_op.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * y^)
q: N (x' * y'^)
N (y^ * x)
G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * y^)
q: N (x' * y'^)
N (x' * y'^)
  2: exact q.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * y^)
q: N (x' * y'^)
N (y^ * x)
  apply isnormal.G: Group
N: NormalSubgroup G
x, x', y, y': G
p: N (x * y^)
q: N (x' * y'^)
N (x * y^)
  exact p.
Defined.

(** ** Trivial subgroup *)

(** The trivial subgroup of a group [G]. *)
Definition trivial_subgroup G : Subgroup G.G: Group
Subgroup G
Proof.G: Group
Subgroup G
  rapply (Build_Subgroup' (fun x => x = 1)).G: Group
1 = 1
G: Group
forall x y : G, x = 1 -> y = 1 -> x * y^ = 1
  1: reflexivity.G: Group
forall x y : G, x = 1 -> y = 1 -> x * y^ = 1
  intros x y p q.G: Group
x, y: G
p: x = 1
q: y = 1
x * y^ = 1
  rewrite p, q.G: Group
x, y: G
p: x = 1
q: y = 1
1 * 1^ = 1
  rewrite left_identity.G: Group
x, y: G
p: x = 1
q: y = 1
1^ = 1
  apply grp_inv_unit.
Defined.

(** The trivial subgroup is always included in any subgroup. *)
Definition trivial_subgroup_rec {G : Group} (H : Subgroup G)
  : forall x, trivial_subgroup G x -> H x.G: Group
H: Subgroup G
forall x : G, trivial_subgroup G x -> H x
Proof.G: Group
H: Subgroup G
forall x : G, trivial_subgroup G x -> H x
  napply paths_ind_r; cbn beta.G: Group
H: Subgroup G
H 1
  exact issubgroup_in_unit.
Defined.

(** The trivial subgroup is a normal subgroup. *)
Instance isnormal_trivial_subgroup {G : Group}
  : IsNormalSubgroup (trivial_subgroup G).G: Group
IsNormalSubgroup (trivial_subgroup G)
Proof.G: Group
IsNormalSubgroup (trivial_subgroup G)
  intros x y p; cbn in p |- *.G: Group
x, y: G
p: x * y = 1
y * x = 1
  apply grp_moveL_1V in p.G: Group
x, y: G
p: x = y^
y * x = 1
  by apply grp_moveL_V1.
Defined.

(** The property of being the trivial subgroup. Note that any group can be automatically coerced to its maximal subgroup, so it makes sense for this predicate to be applied to groups in general. *)
Class IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) :=
  istrivialgroup : forall x, H x -> trivial_subgroup G x.

Instance ishprop_istrivialgroup `{F : Funext} {G : Group} (H : Subgroup G)
  : IsHProp (IsTrivialGroup H)
  := istrunc_forall.

Instance istrivial_trivial_subgroup {G : Group}
  : IsTrivialGroup (trivial_subgroup G)
  := fun x => idmap.

(** Trivial groups are isomorphic to the trivial group. *)
Definition istrivial_iff_grp_iso_trivial {G : Group} (H : Subgroup G)
  : IsTrivialGroup H <-> (subgroup_group H $<~> grp_trivial).G: Group
H: Subgroup G
IsTrivialGroup H <-> H $<~> grp_trivial
Proof.G: Group
H: Subgroup G
IsTrivialGroup H <-> H $<~> grp_trivial
  split.G: Group
H: Subgroup G
IsTrivialGroup H -> H $<~> grp_trivial
G: Group
H: Subgroup G
H $<~> grp_trivial -> IsTrivialGroup H
  -G: Group
H: Subgroup G
IsTrivialGroup H -> H $<~> grp_trivial intros triv.G: Group
H: Subgroup G
triv: IsTrivialGroup H
H $<~> grp_trivial
    snapply cate_adjointify.G: Group
H: Subgroup G
triv: IsTrivialGroup H
H $-> grp_trivial
G: Group
H: Subgroup G
triv: IsTrivialGroup H
grp_trivial $-> H
G: Group
H: Subgroup G
triv: IsTrivialGroup H
?f $o ?g $== Id grp_trivial
G: Group
H: Subgroup G
triv: IsTrivialGroup H
?g $o ?f $== Id H
    1,2: exact grp_homo_const.G: Group
H: Subgroup G
triv: IsTrivialGroup H
grp_homo_const $o grp_homo_const $== Id grp_trivial
G: Group
H: Subgroup G
triv: IsTrivialGroup H
grp_homo_const $o grp_homo_const $== Id H
    +G: Group
H: Subgroup G
triv: IsTrivialGroup H
grp_homo_const $o grp_homo_const $== Id grp_trivial by intros [].
    +G: Group
H: Subgroup G
triv: IsTrivialGroup H
grp_homo_const $o grp_homo_const $== Id H intros [x Hx]; simpl.G: Group
H: Subgroup G
triv: IsTrivialGroup H
x: G
Hx: H x
(1; issubgroup_in_unit) = (x; Hx)
      apply path_sigma_hprop.G: Group
H: Subgroup G
triv: IsTrivialGroup H
x: G
Hx: H x
(1; issubgroup_in_unit).1 = (x; Hx).1
      symmetry.G: Group
H: Subgroup G
triv: IsTrivialGroup H
x: G
Hx: H x
(x; Hx).1 = (1; issubgroup_in_unit).1
      by apply triv.
  -G: Group
H: Subgroup G
H $<~> grp_trivial -> IsTrivialGroup H intros e x Hx.G: Group
H: Subgroup G
e: H $<~> grp_trivial
x: G
Hx: H x
trivial_subgroup G x
    change ((x; Hx).1 = (1; idpath).1).G: Group
H: Subgroup G
e: H $<~> grp_trivial
x: G
Hx: H x
(x; Hx).1 = (1; 1%path).1
    snapply (pr1_path (u:=(_;_)) (v:=(_;_))).G: Group
H: Subgroup G
e: H $<~> grp_trivial
x: G
Hx: H x
H 1
G: Group
H: Subgroup G
e: H $<~> grp_trivial
x: G
Hx: H x
(x; Hx) = (1; ?proj2)
    1: apply subgroup_in_unit.G: Group
H: Subgroup G
e: H $<~> grp_trivial
x: G
Hx: H x
(x; Hx) = (1; subgroup_in_unit H)
    rhs_V exact (grp_homo_unit e^-1$).G: Group
H: Subgroup G
e: H $<~> grp_trivial
x: G
Hx: H x
(x; Hx) = e^-1$ 1
    apply moveL_equiv_V.G: Group
H: Subgroup G
e: H $<~> grp_trivial
x: G
Hx: H x
e (x; Hx) = 1
    apply path_contr.
Defined.

(** All trivial subgroups are isomorphic as groups. *)
Definition grp_iso_trivial_subgroup (G H : Group)
  : subgroup_group (trivial_subgroup G)
    $<~> subgroup_group (trivial_subgroup H).G, H: Group
trivial_subgroup G $<~> trivial_subgroup H
Proof.G, H: Group
trivial_subgroup G $<~> trivial_subgroup H
  snrefine (_^-1$ $oE _).G, H: Group
Group
G, H: Group
trivial_subgroup H $<~> ?b
G, H: Group
trivial_subgroup G $<~> ?b
  1: exact grp_trivial.G, H: Group
trivial_subgroup H $<~> grp_trivial
G, H: Group
trivial_subgroup G $<~> grp_trivial
  1,2: apply istrivial_iff_grp_iso_trivial; exact _.
Defined.

Definition istrivial_grp_iso {G H : Group} (J : Subgroup G) (K : Subgroup H)
  (e : subgroup_group J $<~> subgroup_group K)
  : IsTrivialGroup J -> IsTrivialGroup K.G, H: Group
J: Subgroup G
K: Subgroup H
e: J $<~> K
IsTrivialGroup J -> IsTrivialGroup K
Proof.G, H: Group
J: Subgroup G
K: Subgroup H
e: J $<~> K
IsTrivialGroup J -> IsTrivialGroup K
  intros triv.G, H: Group
J: Subgroup G
K: Subgroup H
e: J $<~> K
triv: IsTrivialGroup J
IsTrivialGroup K
  apply istrivial_iff_grp_iso_trivial in triv.G, H: Group
J: Subgroup G
K: Subgroup H
e: J $<~> K
triv: J $<~> grp_trivial
IsTrivialGroup K
  apply istrivial_iff_grp_iso_trivial.G, H: Group
J: Subgroup G
K: Subgroup H
e: J $<~> K
triv: J $<~> grp_trivial
K $<~> grp_trivial
  exact (triv $oE e^-1$).
Defined.

(** ** Maximal Subgroups *)

(** Every group is a (maximal) subgroup of itself. *)
Definition maximal_subgroup G : Subgroup G.G: Group
Subgroup G
Proof.G: Group
Subgroup G
  rapply (Build_Subgroup G (fun x => Unit)).G: Group
IsSubgroup (fun _ : G => Unit)
  split; auto; exact _.
Defined.

(** We wish to coerce a group to its maximal subgroup. However, if we don't explicitly print [maximal_subgroup] things can get confusing, so we mark it as a coercion to be printed. *)
Coercion maximal_subgroup : Group >-> Subgroup.
Add Printing Coercion maximal_subgroup.

(** The group associated to the maximal subgroup is the original group. Note that this equivalence does not characterize the maximal subgroup, as a proper subgroup can be isomorphic to the whole group. For example, the even integers are isomorphic to the integers. *)
Definition grp_iso_subgroup_group_maximal (G : Group)
  : subgroup_group (maximal_subgroup G) $<~> G.G: Group
maximal_subgroup G $<~> G
Proof.G: Group
maximal_subgroup G $<~> G
  snapply Build_GroupIsomorphism'.G: Group
maximal_subgroup G <~> G
G: Group
IsSemiGroupPreserving ?f
  -G: Group
maximal_subgroup G <~> G rapply equiv_sigma_contr.
  -G: Group
IsSemiGroupPreserving
  (equiv_sigma_contr (maximal_subgroup G)) hnf; reflexivity.
Defined.

(** The maximal subgroup (the group itself) is a normal subgroup. *)
Instance isnormal_maximal_subgroup {G : Group}
  : IsNormalSubgroup (maximal_subgroup G).G: Group
IsNormalSubgroup (maximal_subgroup G)
Proof.G: Group
IsNormalSubgroup (maximal_subgroup G)
  intros x y p; exact tt.
Defined.

(** The property of being a maximal subgroup of a group [G]. *)
Class IsMaximalSubgroup {G : Group} (H : Subgroup G) :=
  ismaximalsubgroup : forall (x : G), H x.

Instance ishprop_ismaximalsubgroup `{Funext}
  {G : Group} (H : Subgroup G)
  : IsHProp (IsMaximalSubgroup H)
  := istrunc_forall.

Instance ismaximalsubgroup_maximalsubgroup {G : Group}
  : IsMaximalSubgroup (maximal_subgroup G)
  := fun g => tt.

(** ** Subgroups in opposite group *)

Instance issubgroup_grp_op {G : Group} (H : G -> Type)
  : IsSubgroup H -> IsSubgroup (G:=grp_op G) H.G: Group
H: G -> Type
IsSubgroup H -> IsSubgroup H
Proof.G: Group
H: G -> Type
IsSubgroup H -> IsSubgroup H
  intros H1.G: Group
H: G -> Type
H1: IsSubgroup H
IsSubgroup H
  snapply Build_IsSubgroup'.G: Group
H: G -> Type
H1: IsSubgroup H
forall x : grp_op G, IsHProp (H x)
G: Group
H: G -> Type
H1: IsSubgroup H
H 1
G: Group
H: G -> Type
H1: IsSubgroup H
forall x y : grp_op G, H x -> H y -> H (x * y^)
  -G: Group
H: G -> Type
H1: IsSubgroup H
forall x : grp_op G, IsHProp (H x) exact _.
  -G: Group
H: G -> Type
H1: IsSubgroup H
H 1 cbn; exact issubgroup_in_unit.
  -G: Group
H: G -> Type
H1: IsSubgroup H
forall x y : grp_op G, H x -> H y -> H (x * y^) intros x y Hx Hy; cbn.G: Group
H: G -> Type
H1: IsSubgroup H
x, y: grp_op G
Hx: H x
Hy: H y
H (y^ * x)
    by apply issubgroup_in_inv_op.
Defined.

(** Note that [grp_op] is definitionally involutive, so the next result also gives us a map [Subgroup (grp_op G) -> Subgroup G]. *)
Definition subgroup_grp_op {G : Group} (H : Subgroup G)
  : Subgroup (grp_op G)
  := Build_Subgroup (grp_op G) H _.

Instance isnormal_subgroup_grp_op {G : Group} (H : Subgroup G)
  : IsNormalSubgroup H -> IsNormalSubgroup (subgroup_grp_op H).G: Group
H: Subgroup G
IsNormalSubgroup H ->
IsNormalSubgroup (subgroup_grp_op H)
Proof.G: Group
H: Subgroup G
IsNormalSubgroup H ->
IsNormalSubgroup (subgroup_grp_op H)
  intros n x y; cbn.G: Group
H: Subgroup G
n: IsNormalSubgroup H
x, y: grp_op G
H (y * x) -> H (x * y)
  exact isnormal.
Defined.

Definition normalsubgroup_grp_op {G : Group}
  : NormalSubgroup G -> NormalSubgroup (grp_op G)
  := fun N => Build_NormalSubgroup (grp_op G) (subgroup_grp_op N) _.

(** ** Preimage subgroup *)

(** The preimage of a subgroup under a group homomorphism is a subgroup. *)
Instance issubgroup_preimage {G H : Group} (f : G $-> H) (S : H -> Type)
  : IsSubgroup S -> IsSubgroup (S o f).G, H: Group
f: G $-> H
S: H -> Type
IsSubgroup S -> IsSubgroup (S o f)
Proof.G, H: Group
f: G $-> H
S: H -> Type
IsSubgroup S -> IsSubgroup (S o f)
  intros H1.G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
IsSubgroup (S o f)
  snapply Build_IsSubgroup'.G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
forall x : G, IsHProp ((fun x0 : G => S (f x0)) x)
G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
(fun x : G => S (f x)) 1
G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
forall x y : G,
(fun x0 : G => S (f x0)) x ->
(fun x0 : G => S (f x0)) y ->
(fun x0 : G => S (f x0)) (x * y^)
  -G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
forall x : G, IsHProp ((fun x0 : G => S (f x0)) x) hnf; exact _.
  -G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
(fun x : G => S (f x)) 1 nrefine (transport S (grp_homo_unit f)^ _).G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
S 1
    exact issubgroup_in_unit.
  -G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
forall x y : G,
(fun x0 : G => S (f x0)) x ->
(fun x0 : G => S (f x0)) y ->
(fun x0 : G => S (f x0)) (x * y^) hnf; intros x y Sfx Sfy.G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
x, y: G
Sfx: S (f x)
Sfy: S (f y)
S (f (x * y^))
    nrefine (transport S (grp_homo_op f _ _)^ _).G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
x, y: G
Sfx: S (f x)
Sfy: S (f y)
S (f x * f y^)
    rapply issubgroup_in_op; only 1: assumption.G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
x, y: G
Sfx: S (f x)
Sfy: S (f y)
S (f y^)
    nrefine (transport S (grp_homo_inv f _)^ _).G, H: Group
f: G $-> H
S: H -> Type
H1: IsSubgroup S
x, y: G
Sfx: S (f x)
Sfy: S (f y)
S (f y)^
    by apply issubgroup_in_inv.
Defined.

Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H)
  : Subgroup G
  := Build_Subgroup G (S o f) _.

(** The preimage of a normal subgroup is again normal. *)
Instance isnormal_subgroup_preimage {G H : Group} (f : G $-> H)
  (N : Subgroup H) `{!IsNormalSubgroup N}
  : IsNormalSubgroup (subgroup_preimage f N).G, H: Group
f: G $-> H
N: Subgroup H
IsNormalSubgroup0: IsNormalSubgroup N
IsNormalSubgroup (subgroup_preimage f N)
Proof.G, H: Group
f: G $-> H
N: Subgroup H
IsNormalSubgroup0: IsNormalSubgroup N
IsNormalSubgroup (subgroup_preimage f N)
  intros x y Nfxy; simpl.G, H: Group
f: G $-> H
N: Subgroup H
IsNormalSubgroup0: IsNormalSubgroup N
x, y: G
Nfxy: subgroup_preimage f N (x * y)
N (f (y * x))
  nrefine (transport N (grp_homo_op _ _ _)^ _).G, H: Group
f: G $-> H
N: Subgroup H
IsNormalSubgroup0: IsNormalSubgroup N
x, y: G
Nfxy: subgroup_preimage f N (x * y)
N (f y * f x)
  apply isnormal.G, H: Group
f: G $-> H
N: Subgroup H
IsNormalSubgroup0: IsNormalSubgroup N
x, y: G
Nfxy: subgroup_preimage f N (x * y)
N (f x * f y)
  exact (transport N (grp_homo_op _ _ _) Nfxy).
Defined.

(** ** Subgroup intersection *)

(** Intersection of two subgroups *)
Definition subgroup_intersection {G : Group} (H K : Subgroup G) : Subgroup G.G: Group
H, K: Subgroup G
Subgroup G
Proof.G: Group
H, K: Subgroup G
Subgroup G
  snapply Build_Subgroup'.G: Group
H, K: Subgroup G
G -> Type
G: Group
H, K: Subgroup G
forall x : G, IsHProp (?H x)
G: Group
H, K: Subgroup G
?H 1
G: Group
H, K: Subgroup G
forall x y : G, ?H x -> ?H y -> ?H (x * y^)
  1: exact (fun g => H g /\ K g).G: Group
H, K: Subgroup G
forall x : G,
IsHProp ((fun g : G => (H g * K g)%type) x)
G: Group
H, K: Subgroup G
(fun g : G => (H g * K g)%type) 1
G: Group
H, K: Subgroup G
forall x y : G,
(fun g : G => (H g * K g)%type) x ->
(fun g : G => (H g * K g)%type) y ->
(fun g : G => (H g * K g)%type) (x * y^)
  1: exact _.G: Group
H, K: Subgroup G
(fun g : G => (H g * K g)%type) 1
G: Group
H, K: Subgroup G
forall x y : G,
(fun g : G => (H g * K g)%type) x ->
(fun g : G => (H g * K g)%type) y ->
(fun g : G => (H g * K g)%type) (x * y^)
  1: split; apply subgroup_in_unit.G: Group
H, K: Subgroup G
forall x y : G,
(fun g : G => (H g * K g)%type) x ->
(fun g : G => (H g * K g)%type) y ->
(fun g : G => (H g * K g)%type) (x * y^)
  intros x y [] [].G: Group
H, K: Subgroup G
x, y: G
fst: H x
snd: K x
fst0: H y
snd0: K y
(H (sg_op x y^) * K (sg_op x y^))%type
  split; by apply subgroup_in_op_inv.
Defined.

(** ** Simple groups *)

Class IsSimpleGroup (G : Group)
  := is_simple_group : forall (N : Subgroup G) `{IsNormalSubgroup G N},
    IsTrivialGroup N + IsMaximalSubgroup N.

(** ** The subgroup generated by a subset *)

(** Underlying type family of a subgroup generated by subset *)
Inductive subgroup_generated_type {G : Group} (X : G -> Type) : G -> Type :=
(** The subgroup should contain all elements of the original family. *)
| sgt_in (g : G) : X g -> subgroup_generated_type X g
(** It should contain the unit. *)
| sgt_unit : subgroup_generated_type X mon_unit
(** Finally, it should be closed under inverses and operation. *)
| sgt_op (g h : G)
  : subgroup_generated_type X g
  -> subgroup_generated_type X h
  -> subgroup_generated_type X (g * h^)
.

Arguments sgt_in {G X g}.
Arguments sgt_unit {G X}.
Arguments sgt_op {G X g h}.

(** Note that [subgroup_generated_type] will not automatically land in [HProp]. For example, if [X] already "contains" the unit of the group, then there are at least two different inhabitants of this family at the unit (given by [sgt_unit] and [sgt_in group_unit _]). Therefore, we propositionally truncate in [subgroup_generated] below. *)

(** Subgroups are closed under inverses. *)
Definition sgt_inv {G : Group} {X} {g : G}
  : subgroup_generated_type X g -> subgroup_generated_type X g^.G: Group
X: G -> Type
g: G
subgroup_generated_type X g ->
subgroup_generated_type X g^
Proof.G: Group
X: G -> Type
g: G
subgroup_generated_type X g ->
subgroup_generated_type X g^
  intros p.G: Group
X: G -> Type
g: G
p: subgroup_generated_type X g
subgroup_generated_type X g^
  rewrite <- left_identity.G: Group
X: G -> Type
g: G
p: subgroup_generated_type X g
subgroup_generated_type X (1 * g^)
  exact (sgt_op sgt_unit p).
Defined.

Definition sgt_inv' {G : Group} {X} {g : G}
  : subgroup_generated_type X g^ -> subgroup_generated_type X g.G: Group
X: G -> Type
g: G
subgroup_generated_type X g^ ->
subgroup_generated_type X g
Proof.G: Group
X: G -> Type
g: G
subgroup_generated_type X g^ ->
subgroup_generated_type X g
  intros p.G: Group
X: G -> Type
g: G
p: subgroup_generated_type X g^
subgroup_generated_type X g
  rewrite <- grp_inv_inv.G: Group
X: G -> Type
g: G
p: subgroup_generated_type X g^
subgroup_generated_type X (g^)^
  by apply sgt_inv.
Defined.

Definition sgt_op' {G : Group} {X} {g h : G}
  : subgroup_generated_type X g
    -> subgroup_generated_type X h
    -> subgroup_generated_type X (g * h).G: Group
X: G -> Type
g, h: G
subgroup_generated_type X g ->
subgroup_generated_type X h ->
subgroup_generated_type X (g * h)
Proof.G: Group
X: G -> Type
g, h: G
subgroup_generated_type X g ->
subgroup_generated_type X h ->
subgroup_generated_type X (g * h)
  intros p q.G: Group
X: G -> Type
g, h: G
p: subgroup_generated_type X g
q: subgroup_generated_type X h
subgroup_generated_type X (g * h)
  rewrite <- (inverse_involutive h).G: Group
X: G -> Type
g, h: G
p: subgroup_generated_type X g
q: subgroup_generated_type X h
subgroup_generated_type X (g * (h^)^)
  exact (sgt_op p (sgt_inv q)).
Defined.

(** The subgroup generated by a subset *)
Definition subgroup_generated {G : Group} (X : G -> Type) : Subgroup G.G: Group
X: G -> Type
Subgroup G
Proof.G: Group
X: G -> Type
Subgroup G
  refine (Build_Subgroup' (merely o subgroup_generated_type X)
            (tr sgt_unit) _).G: Group
X: G -> Type
forall x y : G,
merely (subgroup_generated_type X x) ->
merely (subgroup_generated_type X y) ->
merely (subgroup_generated_type X (x * y^))
  intros x y p q; strip_truncations.G: Group
X: G -> Type
x, y: G
q: subgroup_generated_type X y
p: subgroup_generated_type X x
merely (subgroup_generated_type X (x * y^))
  exact (tr (sgt_op p q)).
Defined.

(** The inclusion of generators into the generated subgroup. *)
Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H : X g)
  : subgroup_generated X
  := (g; tr (sgt_in H)).

(** The generated subgroup is the smallest subgroup containing the generating set. *)
Definition subgroup_generated_rec {G : Group} (X : G -> Type) (S : Subgroup G)
  (i : forall g, X g -> S g)
  : forall g, subgroup_generated X g -> S g.G: Group
X: G -> Type
S: Subgroup G
i: forall g : G, X g -> S g
forall g : G, subgroup_generated X g -> S g
Proof.G: Group
X: G -> Type
S: Subgroup G
i: forall g : G, X g -> S g
forall g : G, subgroup_generated X g -> S g
  intros g; rapply Trunc_rec; intros p.G: Group
X: G -> Type
S: Subgroup G
i: forall g : G, X g -> S g
g: G
p: subgroup_generated_type X g
S g
  induction p as [g Xg | | g h p1 IHp1 p2 IHp2].G: Group
X: G -> Type
S: Subgroup G
i: forall g : G, X g -> S g
g: G
Xg: X g
S g
G: Group
X: G -> Type
S: Subgroup G
i: forall g : G, X g -> S g
S 1
G: Group
X: G -> Type
S: Subgroup G
i: forall g : G, X g -> S g
g, h: G
p1: subgroup_generated_type X g
p2: subgroup_generated_type X h
IHp1: S g
IHp2: S h
S (g * h^)
  -G: Group
X: G -> Type
S: Subgroup G
i: forall g : G, X g -> S g
g: G
Xg: X g
S g by apply i.
  -G: Group
X: G -> Type
S: Subgroup G
i: forall g : G, X g -> S g
S 1 apply subgroup_in_unit.
  -G: Group
X: G -> Type
S: Subgroup G
i: forall g : G, X g -> S g
g, h: G
p1: subgroup_generated_type X g
p2: subgroup_generated_type X h
IHp1: S g
IHp2: S h
S (g * h^) by apply subgroup_in_op_inv.
Defined.

(** If [f : G $-> H] is a group homomorphism and [X] and [Y] are subsets of [G] and [H] such that [f] maps [X] into [Y], then [f] sends the subgroup generated by [X] into the subgroup generated by [Y]. *)
Definition functor_subgroup_generated {G H : Group} (X : G -> Type) (Y : H -> Type)
  (f : G $-> H) (preserves : forall g, X g -> Y (f g))
  : forall g, subgroup_generated X g -> subgroup_generated Y (f g).G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
forall g : G,
subgroup_generated X g -> subgroup_generated Y (f g)
Proof.G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
forall g : G,
subgroup_generated X g -> subgroup_generated Y (f g)
  change (subgroup_generated Y (f ?g))
    with (subgroup_preimage f (subgroup_generated Y) g).G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
forall g : G,
subgroup_generated X g ->
subgroup_preimage f (subgroup_generated Y) g
  apply subgroup_generated_rec.G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
forall g : G,
X g -> subgroup_preimage f (subgroup_generated Y) g
  intros g p.G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
g: G
p: X g
subgroup_preimage f (subgroup_generated Y) g
  apply tr, sgt_in.G, H: Group
X: G -> Type
Y: H -> Type
f: G $-> H
preserves: forall g : G, X g -> Y (f g)
g: G
p: X g
Y (f g)
  by apply preserves.
Defined.

Definition subgroup_eq_functor_subgroup_generated {G H : Group}
  (X : G -> Type) (Y : H -> Type) (f : G $<~> H) (preserves : forall g, X g <-> Y (f g))
  : forall g, subgroup_generated X g <-> subgroup_generated Y (f g).G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
forall g : G,
subgroup_generated X g <-> subgroup_generated Y (f g)
Proof.G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
forall g : G,
subgroup_generated X g <-> subgroup_generated Y (f g)
  intros x; split; revert x.G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
forall x : G,
subgroup_generated X x -> subgroup_generated Y (f x)
G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
forall x : G,
subgroup_generated Y (f x) -> subgroup_generated X x
  -G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
forall x : G,
subgroup_generated X x -> subgroup_generated Y (f x) apply functor_subgroup_generated.G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
forall g : G, X g -> Y (f g)
    apply preserves.
  -G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
forall x : G,
subgroup_generated Y (f x) -> subgroup_generated X x equiv_intro f^-1$ x.G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
x: H
subgroup_generated Y (f (f^-1$ x)) ->
subgroup_generated X (f^-1$ x)
    rewrite eisretr.G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
x: H
subgroup_generated Y x ->
subgroup_generated X (f^-1$ x)
    apply functor_subgroup_generated; clear x.G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
forall g : H, Y g -> X (f^-1$ g)
    equiv_intro f x; intros y.G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
x: G
y: Y (f x)
X (f^-1$ (f x))
    simpl; rewrite (eissect f).G, H: Group
X: G -> Type
Y: H -> Type
f: G $<~> H
preserves: forall g : G, X g <-> Y (f g)
x: G
y: Y (f x)
X x
    by apply preserves.
Defined.

(** A similar result is true if we replace one group by its opposite, i.e. if [f] is an anti-homomorphism.  For simplicity, we state this only for the case in which [f] is the identity isomorphism.  It's also useful in the special case where [X] and [Y] are the same. *)
Definition subgroup_eq_subgroup_generated_op {G : Group}
  (X : G -> Type) (Y : G -> Type) (preserves : forall g, X g <-> Y g)
  : forall g, subgroup_generated X g <-> subgroup_generated (G:=grp_op G) Y g.G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
forall g : G,
subgroup_generated X g <-> subgroup_generated Y g
Proof.G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
forall g : G,
subgroup_generated X g <-> subgroup_generated Y g
  intro g; split.G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g: G
subgroup_generated X g -> subgroup_generated Y g
G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g: G
subgroup_generated Y g -> subgroup_generated X g
  1: change (subgroup_generated X g -> subgroup_grp_op (subgroup_generated (G:=grp_op G) Y) g).G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g: G
subgroup_generated X g ->
subgroup_grp_op (subgroup_generated Y) g
G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g: G
subgroup_generated Y g -> subgroup_generated X g
  2: change (subgroup_generated (G:=grp_op G) Y g -> subgroup_grp_op (subgroup_generated X) g).G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g: G
subgroup_generated X g ->
subgroup_grp_op (subgroup_generated Y) g
G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g: G
subgroup_generated Y g ->
subgroup_grp_op (subgroup_generated X) g
  all: apply subgroup_generated_rec.G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g: G
forall g : G,
X g -> subgroup_grp_op (subgroup_generated Y) g
G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g: G
forall g : grp_op G,
Y g -> subgroup_grp_op (subgroup_generated X) g
  all: intros x Xx.G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g, x: G
Xx: X x
subgroup_grp_op (subgroup_generated Y) x
G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g: G
x: grp_op G
Xx: Y x
subgroup_grp_op (subgroup_generated X) x
  all: apply (tr o sgt_in).G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g, x: G
Xx: X x
Y x
G: Group
X, Y: G -> Type
preserves: forall g : G, X g <-> Y g
g: G
x: grp_op G
Xx: Y x
X x
  all: by apply (preserves x).
Defined.

(** ** Product of subgroups *)

(** The product of two subgroups. *)
Definition subgroup_product {G : Group} (H K : Subgroup G) : Subgroup G
  := subgroup_generated (fun x => (H x + K x)%type).

(** The induction principle for the product. *)
Definition subgroup_product_ind {G : Group} (H K : Subgroup G)
  (P : forall x, subgroup_product H K x -> Type)
  (P_H_in : forall x y, P x (tr (sgt_in (inl y))))
  (P_K_in : forall x y, P x (tr (sgt_in (inr y))))
  (P_unit : P mon_unit (tr sgt_unit))
  (P_op : forall x y h k, P x (tr h) -> P y (tr k) -> P (x * - y) (tr (sgt_op h k)))
  `{forall x y, IsHProp (P x y)}
  : forall x (p : subgroup_product H K x), P x p.G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
forall (x : G) (p : subgroup_product H K x), P x p
Proof.G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
forall (x : G) (p : subgroup_product H K x), P x p
  intros x p.G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
p: subgroup_product H K x
P x p
  strip_truncations.G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
p: subgroup_generated_type
  (fun x : G => (H x + K x)%type) x
P x (tr p)
  induction p as [x s | | x y h IHh k IHk].G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: (H x + K x)%type
P x (tr (sgt_in s))
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
P 1 (tr sgt_unit)
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x, y: G
h: subgroup_generated_type
  (fun x : G => (H x + K x)%type) x
k: subgroup_generated_type
  (fun x : G => (H x + K x)%type) y
IHh: P x (tr h)
IHk: P y (tr k)
P (x * y^) (tr (sgt_op h k))
  +G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: (H x + K x)%type
P x (tr (sgt_in s)) destruct s.G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: H x
P x (tr (sgt_in (inl s)))
G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: K x
P x (tr (sgt_in (inr s)))
    -G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: H x
P x (tr (sgt_in (inl s))) apply P_H_in.
    -G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x: G
s: K x
P x (tr (sgt_in (inr s))) apply P_K_in.
  +G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
P 1 (tr sgt_unit) exact P_unit.
  +G: Group
H, K: Subgroup G
P: forall x : G, subgroup_product H K x -> Type
P_H_in: forall (x : G) (y : H x),
P x (tr (sgt_in (inl y)))
P_K_in: forall (x : G) (y : K x),
P x (tr (sgt_in (inr y)))
P_unit: P 1 (tr sgt_unit)
P_op: forall (x y : G)
(h : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) x)
(k : subgroup_generated_type
       (fun x0 : G => (H x0 + K x0)%type) y),
P x (tr h) ->
P y (tr k) -> P (x * - y) (tr (sgt_op h k))
H0: forall (x : G) (y : subgroup_product H K x),
IsHProp (P x y)
x, y: G
h: subgroup_generated_type
  (fun x : G => (H x + K x)%type) x
k: subgroup_generated_type
  (fun x : G => (H x + K x)%type) y
IHh: P x (tr h)
IHk: P y (tr k)
P (x * y^) (tr (sgt_op h k)) by apply P_op.
Defined.

Definition subgroup_product_incl_l {G : Group} (H K : Subgroup G)
  : forall x, H x -> subgroup_product H K x
  := fun x => tr o sgt_in o inl.

Definition subgroup_product_incl_r {G : Group} (H K : Subgroup G)
  : forall x, K x -> subgroup_product H K x
  := fun x => tr o sgt_in o inr.

(** A product of normal subgroups is normal. *)
Instance isnormal_subgroup_product {G : Group} (H K : Subgroup G)
  `{!IsNormalSubgroup H, !IsNormalSubgroup K}
  : IsNormalSubgroup (subgroup_product H K).G: Group
H, K: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup K
IsNormalSubgroup (subgroup_product H K)
Proof.G: Group
H, K: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup K
IsNormalSubgroup (subgroup_product H K)
  snapply Build_IsNormalSubgroup'.G: Group
H, K: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup K
forall x y : G,
subgroup_product H K x ->
subgroup_product H K (y * x * y^)
  intros x y; revert x.G: Group
H, K: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup K
y: G
forall x : G,
subgroup_product H K x ->
subgroup_product H K (y * x * y^)
  napply (functor_subgroup_generated _ _ (grp_conj y)).G: Group
H, K: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup K
y: G
forall g : G,
H g + K g -> H (grp_conj y g) + K (grp_conj y g)
  intros x.G: Group
H, K: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup H
IsNormalSubgroup1: IsNormalSubgroup K
y, x: G
H x + K x -> H (grp_conj y x) + K (grp_conj y x)
  apply functor_sum; rapply isnormal_conj.
Defined.

Definition normalsubgroup_product {G : Group} (H K : NormalSubgroup G)
  : NormalSubgroup G
  := Build_NormalSubgroup G (subgroup_product H K) _.

Definition functor_subgroup_product {G H : Group}
  {J K : Subgroup G} {L M : Subgroup H}
  (f : G $-> H) (l : forall x, J x -> L (f x)) (r : forall x, K x -> M (f x))
  : forall x, subgroup_product J K x -> subgroup_product L M (f x).G, H: Group
J, K: Subgroup G
L, M: Subgroup H
f: G $-> H
l: forall x : G, J x -> L (f x)
r: forall x : G, K x -> M (f x)
forall x : G,
subgroup_product J K x -> subgroup_product L M (f x)
Proof.G, H: Group
J, K: Subgroup G
L, M: Subgroup H
f: G $-> H
l: forall x : G, J x -> L (f x)
r: forall x : G, K x -> M (f x)
forall x : G,
subgroup_product J K x -> subgroup_product L M (f x)
  snapply functor_subgroup_generated.G, H: Group
J, K: Subgroup G
L, M: Subgroup H
f: G $-> H
l: forall x : G, J x -> L (f x)
r: forall x : G, K x -> M (f x)
forall g : G,
(fun x : G => (J x + K x)%type) g ->
(fun x : H => (L x + M x)%type) (f g)
  exact (fun x => functor_sum (l x) (r x)).
Defined.

Definition subgroup_eq_functor_subgroup_product {G H : Group}
  {J K : Subgroup G} {L M : Subgroup H}
  (f : G $<~> H) (l : forall x, J x <-> L (f x)) (r : forall x, K x <-> M (f x))
  : forall x, subgroup_product J K x <-> subgroup_product L M (f x).G, H: Group
J, K: Subgroup G
L, M: Subgroup H
f: G $<~> H
l: forall x : G, J x <-> L (f x)
r: forall x : G, K x <-> M (f x)
forall x : G,
subgroup_product J K x <-> subgroup_product L M (f x)
Proof.G, H: Group
J, K: Subgroup G
L, M: Subgroup H
f: G $<~> H
l: forall x : G, J x <-> L (f x)
r: forall x : G, K x <-> M (f x)
forall x : G,
subgroup_product J K x <-> subgroup_product L M (f x)
  snapply subgroup_eq_functor_subgroup_generated.G, H: Group
J, K: Subgroup G
L, M: Subgroup H
f: G $<~> H
l: forall x : G, J x <-> L (f x)
r: forall x : G, K x <-> M (f x)
forall g : G,
(fun x : G => (J x + K x)%type) g <->
(fun x : H => (L x + M x)%type) (f g)
  exact (fun x => iff_functor_sum (l x) (r x)).
Defined.

Definition subgroup_eq_product_grp_op {G : Group} (H K : Subgroup G)
  : forall x, subgroup_grp_op (subgroup_product H K) x
    <-> subgroup_product (subgroup_grp_op H) (subgroup_grp_op K) x.G: Group
H, K: Subgroup G
forall x : grp_op G,
subgroup_grp_op (subgroup_product H K) x <->
subgroup_product (subgroup_grp_op H)
  (subgroup_grp_op K) x
Proof.G: Group
H, K: Subgroup G
forall x : grp_op G,
subgroup_grp_op (subgroup_product H K) x <->
subgroup_product (subgroup_grp_op H)
  (subgroup_grp_op K) x
  intro x.G: Group
H, K: Subgroup G
x: grp_op G
subgroup_grp_op (subgroup_product H K) x <->
subgroup_product (subgroup_grp_op H)
  (subgroup_grp_op K) x
  apply subgroup_eq_subgroup_generated_op.G: Group
H, K: Subgroup G
x: grp_op G
forall g : G,
H g + K g <->
subgroup_grp_op H g + subgroup_grp_op K g
  reflexivity.
Defined.

(** *** Paths between generated subgroups *)

(** This gets used twice in [path_subgroup_generated], so we factor it out here. *)
Local Lemma path_subgroup_generated_helper {G : Group}
  (X Y : G -> Type) (K : forall g, merely (X g) -> merely (Y g))
  : forall g, Trunc (-1) (subgroup_generated_type X g)
         -> Trunc (-1) (subgroup_generated_type Y g).G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
forall g : G,
Trunc (-1) (subgroup_generated_type X g) ->
Trunc (-1) (subgroup_generated_type Y g)
Proof.G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
forall g : G,
Trunc (-1) (subgroup_generated_type X g) ->
Trunc (-1) (subgroup_generated_type Y g)
  intro g; apply Trunc_rec; intro ing.G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g: G
ing: subgroup_generated_type X g
Trunc (-1) (subgroup_generated_type Y g)
  induction ing as [g x| |g h Xg IHYg Xh IHYh].G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g: G
x: X g
Trunc (-1) (subgroup_generated_type Y g)
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
Trunc (-1) (subgroup_generated_type Y 1)
G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g, h: G
Xg: subgroup_generated_type X g
Xh: subgroup_generated_type X h
IHYg: Trunc (-1) (subgroup_generated_type Y g)
IHYh: Trunc (-1) (subgroup_generated_type Y h)
Trunc (-1) (subgroup_generated_type Y (g * h^))
  -G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g: G
x: X g
Trunc (-1) (subgroup_generated_type Y g) exact (Trunc_functor (-1) sgt_in (K g (tr x))).
  -G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
Trunc (-1) (subgroup_generated_type Y 1) exact (tr sgt_unit).
  -G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g, h: G
Xg: subgroup_generated_type X g
Xh: subgroup_generated_type X h
IHYg: Trunc (-1) (subgroup_generated_type Y g)
IHYh: Trunc (-1) (subgroup_generated_type Y h)
Trunc (-1) (subgroup_generated_type Y (g * h^)) strip_truncations.G: Group
X, Y: G -> Type
K: forall g : G, merely (X g) -> merely (Y g)
g, h: G
Xg: subgroup_generated_type X g
Xh: subgroup_generated_type X h
IHYh: subgroup_generated_type Y h
IHYg: subgroup_generated_type Y g
Trunc (-1) (subgroup_generated_type Y (g * h^))
    by apply tr, sgt_op.
Defined.

(** If the predicates selecting the generators are merely equivalent, then the generated subgroups are equal. (One could probably prove that the generated subgroup are isomorphic without using univalence.) *)
Definition path_subgroup_generated `{Univalence} {G : Group}
  (X Y : G -> Type) (K : forall g, Trunc (-1) (X g) <-> Trunc (-1) (Y g))
  : subgroup_generated X = subgroup_generated Y.H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
subgroup_generated X = subgroup_generated Y
Proof.H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
subgroup_generated X = subgroup_generated Y
  rapply equiv_path_subgroup'. (* Uses Univalence. *)H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
forall g : G,
subgroup_generated X g <-> subgroup_generated Y g
  intro g; split.H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
g: G
subgroup_generated X g -> subgroup_generated Y g
H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
g: G
subgroup_generated Y g -> subgroup_generated X g
  -H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
g: G
subgroup_generated X g -> subgroup_generated Y g apply path_subgroup_generated_helper, (fun x => fst (K x)).
  -H: Univalence
G: Group
X, Y: G -> Type
K: forall g : G,
Trunc (-1) (X g) <-> Trunc (-1) (Y g)
g: G
subgroup_generated Y g -> subgroup_generated X g apply path_subgroup_generated_helper, (fun x => snd (K x)).
Defined.

(** Equal subgroups have isomorphic underlying groups. *)
Definition equiv_subgroup_group {G : Group} (H1 H2 : Subgroup G)
  : H1 = H2 -> GroupIsomorphism H1 H2
  := ltac:(intros []; exact grp_iso_id).

(** ** Image of a group homomorphism *)

(** The image of a group homomorphism between groups is a subgroup. *)
Definition grp_image {G H : Group} (f : G $-> H) : Subgroup H.G, H: Group
f: G $-> H
Subgroup H
Proof.G, H: Group
f: G $-> H
Subgroup H
  srapply (Build_Subgroup' (fun y => hexists (fun x => f x = y))); cbn beta.G, H: Group
f: G $-> H
hexists (fun x : G => f x = 1)
G, H: Group
f: G $-> H
forall x y : H,
hexists (fun x0 : G => f x0 = x) ->
hexists (fun x0 : G => f x0 = y) ->
hexists (fun x0 : G => f x0 = x * y^)
  -G, H: Group
f: G $-> H
hexists (fun x : G => f x = 1) apply tr.G, H: Group
f: G $-> H
{x : G & f x = 1}
    exists 1.G, H: Group
f: G $-> H
f 1 = 1
    apply grp_homo_unit.
  -G, H: Group
f: G $-> H
forall x y : H,
hexists (fun x0 : G => f x0 = x) ->
hexists (fun x0 : G => f x0 = y) ->
hexists (fun x0 : G => f x0 = x * y^) intros x y p q; strip_truncations; apply tr.G, H: Group
f: G $-> H
x, y: H
q: {x : G & f x = y}
p: {x0 : G & f x0 = x}
{x0 : G & f x0 = x * y^}
    destruct p as [a p], q as [b q].G, H: Group
f: G $-> H
x, y: H
b: G
q: f b = y
a: G
p: f a = x
{x0 : G & f x0 = x * y^}
    exists (a * b^).G, H: Group
f: G $-> H
x, y: H
b: G
q: f b = y
a: G
p: f a = x
f (a * b^) = x * y^
    lhs napply grp_homo_op; f_ap.G, H: Group
f: G $-> H
x, y: H
b: G
q: f b = y
a: G
p: f a = x
f b^ = y^
    lhs napply grp_homo_inv; f_ap.
Defined.

Definition grp_image_in {G H : Group} (f : G $-> H)
  : forall x, grp_image f (f x)
  := fun x => tr (x; idpath).

Definition grp_homo_image_in {G H : Group} (f : G $-> H)
  : G $-> grp_image f
  := subgroup_corec f (grp_image_in f).

(** ** Image of a group embedding *)

(** When the homomorphism is an embedding, we don't need to truncate. *)
Definition grp_image_embedding {G H : Group} (f : G $-> H) `{IsEmbedding f}
  : Subgroup H.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
Subgroup H
Proof.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
Subgroup H
  snapply (Build_Subgroup _ (hfiber f)).G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
IsSubgroup (hfiber f)
  repeat split.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
forall x : H, IsHProp (hfiber f x)
G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
hfiber f 1
G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
forall x y : H,
hfiber f x -> hfiber f y -> hfiber f (x * y)
G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
forall x : H, hfiber f x -> hfiber f x^
  -G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
forall x : H, IsHProp (hfiber f x) exact _.
  -G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
hfiber f 1 exact (mon_unit; grp_homo_unit f).
  -G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
forall x y : H,
hfiber f x -> hfiber f y -> hfiber f (x * y) intros x y [a []] [b []].G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
x, y: H
a, b: G
hfiber f (f a * f b)
    exists (a * b).G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
x, y: H
a, b: G
f (a * b) = f a * f b
    apply grp_homo_op.
  -G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
forall x : H, hfiber f x -> hfiber f x^ intros b [a []].G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
b: H
a: G
hfiber f (f a)^
    exists a^.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
b: H
a: G
f a^ = (f a)^
    apply grp_homo_inv.
Defined.

Definition grp_image_in_embedding {G H : Group} (f : G $-> H) `{IsEmbedding f}
  : GroupIsomorphism G (grp_image_embedding f).G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
GroupIsomorphism G (grp_image_embedding f)
Proof.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
GroupIsomorphism G (grp_image_embedding f)
  snapply Build_GroupIsomorphism.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
GroupHomomorphism G (grp_image_embedding f)
G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
IsEquiv ?grp_iso_homo
  -G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
GroupHomomorphism G (grp_image_embedding f) snapply (subgroup_corec f).G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
forall x : G, grp_image_embedding f (f x)
    exact (fun x => (x; idpath)).
  -G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
IsEquiv (subgroup_corec f (fun x : G => (x; 1%path))) apply isequiv_surj_emb.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
IsConnMap (Tr (-1))
  (subgroup_corec f (fun x : G => (x; 1%path)))
G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
IsEmbedding
  (subgroup_corec f (fun x : G => (x; 1%path)))
    2: exact (cancelL_isembedding (g:=pr1)).G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
IsConnMap (Tr (-1))
  (subgroup_corec f (fun x : G => (x; 1%path)))
    intros [b [a p]]; cbn.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
b: H
a: G
p: f a = b
IsConnected (Tr (-1))
  (hfiber (fun x : G => (f x; x; 1%path)) (b; a; p))
    rapply contr_inhabited_hprop.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
b: H
a: G
p: f a = b
Tr (-1)
  (hfiber (fun x : G => (f x; x; 1%path)) (b; a; p))
    refine (tr (a; _)).G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
b: H
a: G
p: f a = b
(f a; a; 1%path) = (b; a; p)
    srapply path_sigma'.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
b: H
a: G
p: f a = b
f a = b
G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
b: H
a: G
p: f a = b
transport (hfiber f) ?p (a; 1%path) = (a; p)
    1: exact p.G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
b: H
a: G
p: f a = b
transport (hfiber f) p (a; 1%path) = (a; p)
    refine (transport_sigma' _ _ @ _).G, H: Group
f: G $-> H
IsEmbedding0: IsEmbedding f
b: H
a: G
p: f a = b
((a; 1%path).1;
transport (fun x : H => f (a; 1%path).1 = x) p
  (a; 1%path).2) = (a; p)
    by apply path_sigma_hprop.
Defined.

(** The image of a surjective group homomorphism is the maximal subgroup. *)
Instance ismaximal_image_issurj {G H : Group}
  (f : G $-> H) `{IsSurjection f}
  : IsMaximalSubgroup (grp_image f).G, H: Group
f: G $-> H
IsSurjection0: IsConnMap (Tr (-1)) f
IsMaximalSubgroup (grp_image f)
Proof.G, H: Group
f: G $-> H
IsSurjection0: IsConnMap (Tr (-1)) f
IsMaximalSubgroup (grp_image f)
  rapply conn_map_elim.G, H: Group
f: G $-> H
IsSurjection0: IsConnMap (Tr (-1)) f
forall a : G, grp_image f (f a)
  apply grp_image_in.
Defined.

(** ** Image of a subgroup under a group homomorphism *)

(** The image of a subgroup under group homomorphism. *) 
Definition subgroup_image {G H : Group} (f : G $-> H)
  : Subgroup G -> Subgroup H
  := fun K => grp_image (grp_homo_restr f K).

(** By definition, values of [f x] where [x] is in a subgroup [J] are in the image of [J] under [f]. *)
Definition subgroup_image_in {G H : Group} (f : G $-> H) (J : Subgroup G)
  : forall x, J x -> subgroup_image f J (f x)
  := fun x Jx => tr ((x; Jx); idpath).

(** Converting the subgroups to groups, we get the expected surjective (epi) restriction homomorphism. *)
Definition grp_homo_subgroup_image_in {G H : Group}
  (f : G $-> H) (J : Subgroup G)
  : subgroup_group J $-> subgroup_group (subgroup_image f J)
  := functor_subgroup_group f (subgroup_image_in _ _).

(** The restriction map from the subgroup to the image is surjective as expected, by [conn_map_factor1_image]. *)
Definition issurj_grp_homo_subgroup_image_in {G H : Group}
  (f : G $-> H) (J : Subgroup G)
  : IsSurjection (grp_homo_subgroup_image_in f J)
  := _.

(** An image of a subgroup [J] is included in a subgroup [K] if (and only if) [J] is included in the preimage of the subgroup [K]. *)
Definition subgroup_image_rec {G H : Group}
  (f : G $-> H) {J : Subgroup G} {K : Subgroup H}
  (g : forall x, J x -> K (f x))
  : forall x, subgroup_image f J x -> K x.G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
g: forall x : G, J x -> K (f x)
forall x : H, subgroup_image f J x -> K x
Proof.G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
g: forall x : G, J x -> K (f x)
forall x : H, subgroup_image f J x -> K x
  intros x; apply Trunc_rec; intros [[j Jj] p].G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
g: forall x : G, J x -> K (f x)
x: H
j: G
Jj: J j
p: grp_homo_restr f J (j; Jj) = x
K x
  destruct p.G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
g: forall x : G, J x -> K (f x)
j: G
Jj: J j
K (grp_homo_restr f J (j; Jj))
  exact (g j Jj).
Defined.

(** The image functor is adjoint to the preimage functor. *) 
Definition iff_subgroup_image_rec {G H : Group}
  (f : G $-> H) {J : Subgroup G} {K : Subgroup H}
  : (forall x, subgroup_image f J x -> K x)
    <-> (forall x, J x -> subgroup_preimage f K x).G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
(forall x : H, subgroup_image f J x -> K x) <->
(forall x : G, J x -> subgroup_preimage f K x)
Proof.G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
(forall x : H, subgroup_image f J x -> K x) <->
(forall x : G, J x -> subgroup_preimage f K x)
  split.G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
(forall x : H, subgroup_image f J x -> K x) ->
forall x : G, J x -> subgroup_preimage f K x
G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
(forall x : G, J x -> subgroup_preimage f K x) ->
forall x : H, subgroup_image f J x -> K x
  -G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
(forall x : H, subgroup_image f J x -> K x) ->
forall x : G, J x -> subgroup_preimage f K x intros rec x Jx.G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
rec: forall x : H, subgroup_image f J x -> K x
x: G
Jx: J x
subgroup_preimage f K x
    apply rec, tr.G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
rec: forall x : H, subgroup_image f J x -> K x
x: G
Jx: J x
{x0 : J & grp_homo_restr f J x0 = f x}
    by exists (x; Jx).
  -G, H: Group
f: G $-> H
J: Subgroup G
K: Subgroup H
(forall x : G, J x -> subgroup_preimage f K x) ->
forall x : H, subgroup_image f J x -> K x snapply subgroup_image_rec.
Defined.

(** [subgroup_image] preserves normal subgroups when the group homomorphism is surjective. *)
Instance isnormal_subgroup_image {G H : Group} (f : G $-> H)
  (J : Subgroup G) `{!IsNormalSubgroup J} `{!IsSurjection f}
  : IsNormalSubgroup (subgroup_image f J).G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
IsNormalSubgroup (subgroup_image f J)
Proof.G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
IsNormalSubgroup (subgroup_image f J)
  snapply Build_IsNormalSubgroup'.G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
forall x y : H,
subgroup_image f J x ->
subgroup_image f J (y * x * y^)
  intros x y; revert x.G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
y: H
forall x : H,
subgroup_image f J x ->
subgroup_image f J (y * x * y^)
  change (subgroup_image f J (y * ?x * y^))
    with (subgroup_preimage (grp_conj y) (subgroup_image f J) x).G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
y: H
forall x : H,
subgroup_image f J x ->
subgroup_preimage (grp_conj y) (subgroup_image f J) x
  snapply subgroup_image_rec.G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
y: H
forall x : G,
J x ->
subgroup_preimage 
  (grp_conj y) (subgroup_image f J) 
  (f x)
  intros x Jx.G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
y: H
x: G
Jx: J x
subgroup_preimage 
  (grp_conj y) (subgroup_image f J) 
  (f x)
  change (subgroup_image f J ((grp_conj y $o f) x)).G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
y: H
x: G
Jx: J x
subgroup_image f J ((grp_conj y $o f) x)
  revert y; rapply (conn_map_elim (Tr (-1)) f); intros y.G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
x: G
Jx: J x
y: G
subgroup_image f J ((grp_conj (f y) $o f) x)
  rewrite <- grp_homo_conj.G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
x: G
Jx: J x
y: G
subgroup_image f J ((f $o grp_conj y) x)
  napply subgroup_image_in.G, H: Group
f: G $-> H
J: Subgroup G
IsNormalSubgroup0: IsNormalSubgroup J
IsSurjection0: IsConnMap (Tr (-1)) f
x: G
Jx: J x
y: G
J (grp_conj y x)
  by rapply isnormal_conj.
Defined.

(** ** Kernels of group homomorphisms *)

Definition grp_kernel {G H : Group} (f : G $-> H)
  : NormalSubgroup G
  := Build_NormalSubgroup G (subgroup_preimage f (trivial_subgroup _)) _.

(** Corecursion principle for group kernels *)
Definition grp_kernel_corec {A B G : Group} {f : A $-> B}
  (g : G $-> A) (h : f $o g == grp_homo_const)
  : G $-> grp_kernel f.A, B, G: Group
f: A $-> B
g: G $-> A
h: f $o g == grp_homo_const
G $-> grp_kernel f
Proof.A, B, G: Group
f: A $-> B
g: G $-> A
h: f $o g == grp_homo_const
G $-> grp_kernel f
  snapply (subgroup_corec g); exact h.
Defined.

Definition equiv_grp_kernel_corec `{Funext} {A B G : Group} {f : A $-> B}
  : {g : G $-> A & f $o g == grp_homo_const} <~> (G $-> grp_kernel f)
  := equiv_subgroup_corec G (grp_kernel f).

(** The underlying map of a group homomorphism with a trivial kernel is an embedding. *)
Instance isembedding_istrivial_kernel {G H : Group} (f : G $-> H)
  (triv : IsTrivialGroup (grp_kernel f))
  : IsEmbedding f.G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
IsEmbedding f
Proof.G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
IsEmbedding f
  intros h.G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
h: H
IsHProp (hfiber f h)
  apply hprop_allpath.G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
h: H
forall x y : hfiber f h, x = y
  intros [x p] [y q].G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
h: H
x: G
p: f x = h
y: G
q: f y = h
(x; p) = (y; q)
  srapply path_sigma_hprop; unfold pr1.G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
h: H
x: G
p: f x = h
y: G
q: f y = h
x = y
  apply grp_moveL_1M.G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
h: H
x: G
p: f x = h
y: G
q: f y = h
x * y^ = 1
  apply triv; simpl.G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
h: H
x: G
p: f x = h
y: G
q: f y = h
f (x * y^) = 1
  rhs_V exact (grp_inv_r h).G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
h: H
x: G
p: f x = h
y: G
q: f y = h
f (x * y^) = h * h^
  lhs napply grp_homo_op.G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
h: H
x: G
p: f x = h
y: G
q: f y = h
f x * f y^ = h * h^
  napply (ap011 (.*.) p).G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
h: H
x: G
p: f x = h
y: G
q: f y = h
f y^ = h^
  lhs napply grp_homo_inv.G, H: Group
f: G $-> H
triv: IsTrivialGroup (grp_kernel f)
h: H
x: G
p: f x = h
y: G
q: f y = h
(f y)^ = h^
  exact (ap (^) q).
Defined.

(** If the underlying map of a group homomorphism is an embedding then the kernel is trivial. *)
Definition istrivial_kernel_isembedding {G H : Group} (f : G $-> H)
  (emb : IsEmbedding f)
  : IsTrivialGroup (grp_kernel f).G, H: Group
f: G $-> H
emb: IsEmbedding f
IsTrivialGroup (grp_kernel f)
Proof.G, H: Group
f: G $-> H
emb: IsEmbedding f
IsTrivialGroup (grp_kernel f)
  intros g p.G, H: Group
f: G $-> H
emb: IsEmbedding f
g: G
p: grp_kernel f g
trivial_subgroup G g
  rapply (isinj_embedding f).G, H: Group
f: G $-> H
emb: IsEmbedding f
g: G
p: grp_kernel f g
f g = f 1
  exact (p @ (grp_homo_unit f)^).
Defined.
Global Hint Immediate istrivial_kernel_isembedding : typeclass_instances.

(** Characterisation of group embeddings *)
Proposition equiv_istrivial_kernel_isembedding `{F : Funext}
  {G H : Group} (f : G $-> H)
  : IsTrivialGroup (grp_kernel f) <~> IsEmbedding f.F: Funext
G, H: Group
f: G $-> H
IsTrivialGroup (grp_kernel f) <~> IsEmbedding f
Proof.F: Funext
G, H: Group
f: G $-> H
IsTrivialGroup (grp_kernel f) <~> IsEmbedding f
  apply equiv_iff_hprop_uncurried.F: Funext
G, H: Group
f: G $-> H
IsTrivialGroup (grp_kernel f) <-> IsEmbedding f
  split; exact _.
Defined.