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.

(** ** Lagrange's theorem *)

Local Open Scope mc_scope.
Local Open Scope nat_scope.

Definition subgroup_index {U : Univalence} (G : Group) (H : Subgroup G)
  (fin_G : Finite G) (fin_H : Finite H)
  : nat.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
nat
Proof.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
nat
  refine (fcard (Quotient (in_cosetL H))).
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
Finite (Quotient (in_cosetL H))
  nrapply finite_quotient.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
Finite G
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
is_mere_relation G (in_cosetL H)
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
Reflexive (in_cosetL H)
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
Transitive (in_cosetL H)
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
Symmetric (in_cosetL H)
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
forall x y : G, Decidable (in_cosetL H x y)
  1-5: exact _.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
forall x y : G, Decidable (in_cosetL H x y)
  intros x y.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x, y: G
Decidable (in_cosetL H x y)
  pose (dec_H := detachable_finite_subset H).
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x, y: G
dec_H:= detachable_finite_subset H: forall x : G, Decidable (H x)
Decidable (in_cosetL H x y)
  apply dec_H.
Defined.

(** 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 exlcluded middle. We therefore have to assume it is. This in turn implies that the subgroup is decidable. *)
Theorem lagrange {U : Univalence} (G : Group) (H : Subgroup G)
  (fin_G : Finite G) (fin_H : Finite H)
  : exists d, d * (fcard H) = fcard G.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
{d : nat & d * fcard H = fcard G}
Proof.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
{d : nat & d * 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 fin_G fin_H * fcard H = fcard G
  symmetry.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
fcard G = subgroup_index G H fin_G fin_H * fcard H
  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 fin_G fin_H * fcard H
  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 _ : Quotient (in_cosetL 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 _ : Quotient (in_cosetL H) => fcard H)
  srapply Quotient_ind_hprop.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
forall x : G,
(fun q : Quotient (in_cosetL H) =>
 (fun z : Quotient (in_cosetL H) =>
  fcard
    {x0 : G &
    (fun x1 : G =>
     trunctype_type (in_class (in_cosetL H) z x1)) x0})
   q = (fun _ : Quotient (in_cosetL H) => fcard H) q)
  (class_of (in_cosetL H) x)
  simpl. (** simpl is better than cbn here *)
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
forall x : G,
fcard {x0 : G & (fun x1 : G => H (sg_op (- x) x1)) x0} =
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 (sg_op (- 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 (sg_op (- x) x0)} <~> H
  (** Now we must show that cosets are all equivalent as types. *)
  simpl.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x: G
{x0 : G & H (sg_op (- x) x0)} <~> {x : _ & H x}
  snrapply equiv_functor_sigma.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x: G
G -> G
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x: G
IsEquiv ?f
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x: G
forall a : G,
(fun x0 : G => H (sg_op (- x) x0)) a -> H (?f a)
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x: G
forall a : G, IsEquiv (?g a)
  2: apply (isequiv_group_left_op (-x)).
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x: G
forall a : G,
(fun x0 : G => H (sg_op (- x) x0)) a ->
H (sg_op (- x) a)
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x: G
forall a : G, IsEquiv (?g a)
  1: hnf; trivial.
U: Univalence
G: Group
H: Subgroup G
fin_G: Finite G
fin_H: Finite H
x: G
forall a : G,
IsEquiv
  (((fun a0 : G => idmap)
    :
    forall a0 : G,
    (fun x0 : G => H (sg_op (- x) x0)) a0 ->
    H (sg_op (- x) a0)) a)
  exact _.
Defined.

Corollary lagrange_normal {U : Univalence} (G : Group) (H : NormalSubgroup G)
  (fin_G : Finite G) (fin_H : Finite H)
  : fcard (QuotientGroup G H) * fcard H = fcard G.
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
fcard (QuotientGroup G H) * fcard H = fcard G
Proof.
U: Univalence
G: Group
H: NormalSubgroup G
fin_G: Finite G
fin_H: Finite H
fcard (QuotientGroup G H) * fcard H = fcard G
  apply lagrange.
Defined.