Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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.