From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
Require Import Algebra.Groups.Group.
Require Import Algebra.Groups.Subgroup.
Require Import Algebra.Groups.QuotientGroup.
Require Import Spaces.Finite.Finite.
Require Import Spaces.Nat.Core Spaces.Nat.Division.
Require Import Truncations.Core.

Local Open Scope nat_scope.
Local Open Scope mc_mult_scope.

Set Universe Minimization ToSet.

(** * Finite Groups *)

(** ** Basic Properties *)

(** The order of a group is strictly positive. *)
Instance lt_zero_fcard_grp (G : Group) (fin_G : Finite G) : 0 < fcard G.
G: Group
fin_G: Finite G
0 < fcard G
Proof.
G: Group
fin_G: Finite G
0 < fcard G
  pose proof (merely_equiv_fin G) as f.
G: Group
fin_G: Finite G
f: merely (G <~> Fin.Fin (fcard G))
0 < fcard G
  strip_truncations.
G: Group
fin_G: Finite G
f: G <~> Fin.Fin (fcard G)
0 < fcard G
  destruct (fcard G).
G: Group
fin_G: Finite G
f: G <~> Fin.Fin 0
0 < 0
G: Group
fin_G: Finite G
n: nat
f: G <~> Fin.Fin n.+1
0 < n.+1
  -
G: Group
fin_G: Finite G
f: G <~> Fin.Fin 0
0 < 0 contradiction (f mon_unit).
  -
G: Group
fin_G: Finite G
n: nat
f: G <~> Fin.Fin n.+1
0 < n.+1 exact _.
Defined.

(** ** Lagrange's theorem *)

(** Lagrange's Theorem - Given a finite group [G] and a finite subgroup [H] of [G], the order of [H] divides the order of [G].

Note that constructively, a subgroup of a finite group cannot be shown to be finite without excluded middle. We therefore have to assume it is. This in turn implies that the subgroup is decidable. *)
Definition divides_fcard_subgroup {U : Univalence}
  (G : Group) (H : Subgroup G) {fin_G : Finite G} {fin_H : Finite H}
  : (fcard H | fcard G).
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
(fcard H | fcard G)
Proof.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
(fcard H | fcard G)
  exists (subgroup_index G H).
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
(subgroup_index G H * fcard H)%nat = fcard G
  symmetry.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
fcard G = (subgroup_index G H * fcard H)%nat
  refine (fcard_quotient (in_cosetL H) @ _).
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
finadd
  (fun z : Quotient (in_cosetL H) =>
   fcard
     {x : G & (fun x0 : G => trunctype_type (in_class (in_cosetL H) z x0)) x}) =
(subgroup_index G H * fcard H)%nat
  refine (_ @ finadd_const _ _).
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
finadd
  (fun z : Quotient (in_cosetL H) =>
   fcard
     {x : G & (fun x0 : G => trunctype_type (in_class (in_cosetL H) z x0)) x}) =
finadd (fun _ : LeftCoset G H => fcard H)
  apply ap, path_forall.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
(fun z : Quotient (in_cosetL H) =>
 fcard
   {x : G & (fun x0 : G => trunctype_type (in_class (in_cosetL H) z x0)) x}) ==
(fun _ : LeftCoset G H => fcard H)
  srapply Quotient_ind_hprop; simpl.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
forall a : G, fcard {x : G & (fun x0 : G => H (a^ * x0)) x} = fcard H
  intros x.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x: G
fcard {x0 : G & (fun x1 : G => H (x^ * x1)) x0} = fcard H
  apply fcard_equiv'.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x: G
{x0 : G & H (x^ * x0)} <~> H
  apply equiv_sigma_in_cosetL_subgroup.
Defined.

(** As a corollary, the index of a subgroup is the order of the group divided by the order of the subgroup. *)
Definition subgroup_index_fcard_div {U : Univalence}
  (G : Group) (H : Subgroup G) (fin_G : Finite G) (fin_H : Finite H)
  : subgroup_index G H = fcard G / fcard H.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
subgroup_index G H = fcard G / fcard H
Proof.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
subgroup_index G H = fcard G / fcard H
  rapply nat_div_moveL_nV.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
(subgroup_index G H * fcard H)%nat = fcard G
  apply divides_fcard_subgroup.
Defined.

(** Therefore we can show that the order of the quotient group [G / H] is the order of [G] divided by the order of [H]. *)
Definition fcard_grp_quotient {U : Univalence}
  (G : Group) (H : NormalSubgroup G)
  (fin_G : Finite G) (fin_H : Finite H)
  : fcard (QuotientGroup G H) = fcard G / fcard H.
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
fcard (QuotientGroup G H) = fcard G / fcard H
Proof.
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
fcard (QuotientGroup G H) = fcard G / fcard H
  rapply subgroup_index_fcard_div.
Defined.