Require Import Basics.Overture Basics.Tactics Basics.Equivalences Basics.Iff.Require Import Basics.Overture Basics.Tactics Basics.Equivalences Basics.Iff.
Require Import Types.Universe.
Require Import Groups.Group AbGroups.Abelianization AbGroups.AbelianGroup
  Groups.Commutator Groups.QuotientGroup.
Require Import WildCat.Core WildCat.Equiv.

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.
Local Open Scope group_scope.

(** * Perfect Groups *)

(** ** Definition *)

(** A group is perfect if its abelianization is trivial. *)
Class IsPerfect (G : Group) := contr_abel_isperfect :: IsTrivialGroup (abel G).

(** A group is perfect if its commutator subgroup is the maximal subgroup. *)
#[export] Instance isperfect_maximal_commutator (G : Group)
  : IsMaximalSubgroup [G, G] -> IsPerfect G.
G: Group
IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G] -> IsPerfect G
Proof.
G: Group
IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G] -> IsPerfect G
  intros max.
G: Group
max: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
IsPerfect G
  apply istrivial_iff_grp_iso_trivial.
G: Group
max: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
maximal_subgroup (abel G) $<~> grp_trivial
  nrefine (_ $oE grp_iso_subgroup_group_maximal _).
G: Group
max: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
abel G $<~> grp_trivial
  refine (_ $oE emap abgroup_group (@groupiso_isabelianization G _ _ _ _ _
    (isabelianization_derived_quotient _))).
G: Group
max: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
abgroup_derived_quotient G $<~> grp_trivial
  exact (fst (istrivial_iff_grp_iso_trivial (abgroup_derived_quotient G)) _
    $oE (grp_iso_subgroup_group_maximal _)^-1$).
Defined.

(** Conversely, the commutator subgroup of any perfect group is the maximal subgroup. *)
Definition ismaximalsubgroup_commutator_isperfect `{Univalence} (G : Group)
  : IsPerfect G -> IsMaximalSubgroup [G, G].
H: Univalence
G: Group
IsPerfect G -> IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
Proof.
H: Univalence
G: Group
IsPerfect G -> IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
  intros p.
H: Univalence
G: Group
p: IsPerfect G
IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
  napply (ismaximalsubgroup_istrivial_grp_quotient _ (normalsubgroup_derived _)).
H: Univalence
G: Group
p: IsPerfect G
IsTrivialGroup (maximal_subgroup (G / normalsubgroup_derived G))
  srapply (istrivial_grp_iso (abel G)).
H: Univalence
G: Group
p: IsPerfect G
maximal_subgroup (abel G) $<~>
maximal_subgroup (G / normalsubgroup_derived G)
  nrefine (_^-1$ $oE _ $oE _).
H: Univalence
G: Group
p: IsPerfect G
maximal_subgroup (G / normalsubgroup_derived G) $<~> ?Goal0
H: Univalence
G: Group
p: IsPerfect G
?Goal $<~> ?Goal0
H: Univalence
G: Group
p: IsPerfect G
maximal_subgroup (abel G) $<~> ?Goal
  1,3: apply grp_iso_subgroup_group_maximal.
H: Univalence
G: Group
p: IsPerfect G
abel G $<~> G / normalsubgroup_derived G
  exact (emap abgroup_group (@groupiso_isabelianization G _ _ _ _ _
    (isabelianization_derived_quotient _))).
Defined.

(** ** Basic properties *)
  
(** All simple non-abelian groups are perfect. *)
Definition isperfect_simple_nonabelian `{Univalence}
  (G : Group) {s : IsSimpleGroup G}
  (na : ~ Commutative (A:=G) (.*.))
  : IsPerfect G.
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
IsPerfect G
Proof.
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
IsPerfect G
  (* Since [G] is simple, we can assume the commutator [ [G, G] ] is either trivial or maximal. *)
  destruct (s [G, G] _) as [triv | max].
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
triv: IsTrivialGroup [maximal_subgroup G, maximal_subgroup G]
IsPerfect G
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
max: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
IsPerfect G
  2: by apply isperfect_maximal_commutator.
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
triv: IsTrivialGroup [maximal_subgroup G, maximal_subgroup G]
IsPerfect G
  contradiction na.
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
triv: IsTrivialGroup [maximal_subgroup G, maximal_subgroup G]
Commutative sg_op
  intros x y.
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
triv: IsTrivialGroup [maximal_subgroup G, maximal_subgroup G]
x, y: G
x * y = y * x
  lhs napply grp_commutator_swap_op.
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
triv: IsTrivialGroup [maximal_subgroup G, maximal_subgroup G]
x, y: G
grp_commutator x y * y * x = y * x
  lhs_V napply grp_assoc.
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
triv: IsTrivialGroup [maximal_subgroup G, maximal_subgroup G]
x, y: G
grp_commutator x y * (y * x) = y * x
  rhs_V napply grp_unit_l.
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
triv: IsTrivialGroup [maximal_subgroup G, maximal_subgroup G]
x, y: G
grp_commutator x y * (y * x) = 1 * (y * x)
  apply (ap (.* _)).
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
triv: IsTrivialGroup [maximal_subgroup G, maximal_subgroup G]
x, y: G
grp_commutator x y = 1
  apply triv.
H: Univalence
G: Group
s: IsSimpleGroup G
na: ~ Commutative sg_op
triv: IsTrivialGroup [maximal_subgroup G, maximal_subgroup G]
x, y: G
[maximal_subgroup G, maximal_subgroup G] (grp_commutator x y)
  by apply subgroup_commutator_in.
Defined.

(** A quotient of a perfect group is perfect. *)
Definition isperfect_grp_quotient `{Univalence}
  (G : Group) (N : NormalSubgroup G)
  : IsPerfect G -> IsPerfect (G / N).
H: Univalence
G: Group
N: NormalSubgroup G
IsPerfect G -> IsPerfect (G / N)
Proof.
H: Univalence
G: Group
N: NormalSubgroup G
IsPerfect G -> IsPerfect (G / N)
  intros perf.
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsPerfect G
IsPerfect (G / N)
  apply isperfect_maximal_commutator.
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsPerfect G
IsMaximalSubgroup [maximal_subgroup (G / N), maximal_subgroup (G / N)]
  rapply grp_quotient_ind_hprop.
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsPerfect G
forall x : G,
[maximal_subgroup (G / N), maximal_subgroup (G / N)] (grp_quotient_map x)
  intros x.
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsPerfect G
x: G
[maximal_subgroup (G / N), maximal_subgroup (G / N)] (grp_quotient_map x)
  apply ismaximalsubgroup_commutator_isperfect in perf.
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
x: G
[maximal_subgroup (G / N), maximal_subgroup (G / N)] (grp_quotient_map x)
  generalize (perf x); revert x.
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
forall x : G,
[maximal_subgroup G, maximal_subgroup G] x ->
[maximal_subgroup (G / N), maximal_subgroup (G / N)] (grp_quotient_map x)
  change ([G / N, G / N] (grp_quotient_map ?x))
    with (subgroup_preimage grp_quotient_map [G / N, G / N] x).
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
forall x : G,
[maximal_subgroup G, maximal_subgroup G] x ->
subgroup_preimage grp_quotient_map
  [maximal_subgroup (G / N), maximal_subgroup (G / N)] x
  snapply subgroup_commutator_rec.
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
forall x y : G,
maximal_subgroup G x ->
maximal_subgroup G y ->
subgroup_preimage grp_quotient_map
  [maximal_subgroup (G / N), maximal_subgroup (G / N)] 
  (grp_commutator x y)
  intros x y _ _.
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
x, y: G
subgroup_preimage grp_quotient_map
  [maximal_subgroup (G / N), maximal_subgroup (G / N)] 
  (grp_commutator x y)
  change ([G / N, G / N] (grp_quotient_map (grp_commutator x y))).
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
x, y: G
[maximal_subgroup (G / N), maximal_subgroup (G / N)]
  (grp_quotient_map (grp_commutator x y))
  rewrite grp_homo_commutator.
H: Univalence
G: Group
N: NormalSubgroup G
perf: IsMaximalSubgroup [maximal_subgroup G, maximal_subgroup G]
x, y: G
[maximal_subgroup (G / N), maximal_subgroup (G / N)]
  (grp_commutator (grp_quotient_map x) (grp_quotient_map y))
  by apply subgroup_commutator_in.
Defined.