(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype.
From mathcomp Require Import bigop finset fingroup morphism automorphism.
From mathcomp Require Import quotient gproduct.

(******************************************************************************)
(*   This file provides basic interfaces for the notion of "generic"          *)
(* characteristic subgroups; these amount to subfunctors of the identity      *)
(* functor in some category of groups.                                        *)
(* See "Generic Proof Tools And Finite Group Theory",                         *)
(* Francois Garillot, PhD, 2011, Chapter 3.                                   *)
(* The implementation proposed here is fairly basic, relying on first order   *)
(* function matching and on structure telescopes, both of which are somewhat  *)
(* limited and fragile. It should switch in the future to more general and    *)
(* more robust quotation matching.                                            *)
(*   The definitions in this file (types, properties and structures) are all  *)
(* packaged under the GFunctor submodule, i.e., client code should refer to   *)
(* GFunctor.continuous, GFunctor.map, etc. Notations, Coercions and Lemmas    *)
(* are exported and thus directly available, however.                         *)
(*   We provide the following:                                                *)
(*      object_map == the type of the (polymorphic) object map of a group     *)
(*                    functor; the %gF scope is bound to object_map.          *)
(*                 := forall gT : finGroupType, {set gT} -> {set gT}.         *)
(*  We define two operations on object_map (with notations in the %gF scope): *)
(*        F1 \o F2 == the composite map; (F1 \o F2) G expands to F1 (F2 G).   *)
(*        F1 %% F2 == F1 computed modulo F2; we have                          *)
(*                    (F1 %% F2) G / F2 G = F1 (G / F2 G)                     *)
(* We define the following (type-polymorphic) properties of an object_map F:  *)
(*     group_valued F <-> F G is a group when G is a group                    *)
(*           closed F <-> F G is a subgroup o fG when G is a group            *)
(*       continuous F <-> F is continuous with respect to morphism image:     *)
(*                        for any f : {morphism G >-> ..}, f @* (F G) is a    *)
(*                        a subgroup of F (f @* G); equivalently, F is        *)
(*                        functorial in the category Grp of groups.           *)
(*                        Most common "characteristic subgroup" are produced  *)
(*                        continuous object maps.                             *)
(*   iso_continuous F <-> F is continuous with respect to isomorphism image;  *)
(*                        equivalently, F is functorial in the Grp groupoid.  *)
(*                        The Puig and the Thompson J subgroups are examples  *)
(*                        of iso_continuous maps that are not continuous.     *)
(*      pcontinuous F <-> F is continuous with respect to partial morphism    *)
(*                        image, i.e., functorial in the category of groups   *)
(*                        and partial morphisms. The center and p-core are    *)
(*                        examples of pcontinuous maps.                       *)
(*       hereditary F <-> inclusion in the image of F is hereditary, i.e.,    *)
(*                        for any subgroup H of G, the intersection of H with *)
(*                        F G is included in H. Note that F is pcontinuous    *)
(*                        iff it is continuous and hereditary; indeed proofs  *)
(*                        of pcontinuous F coerce to proofs of hereditary F   *)
(*                        and continuous F.                                   *)
(*        monotonic F <-> F is monotonic with respect to inclusion: for any   *)
(*                        subgroup H of G, F H is a subgroup of F G. The      *)
(*                        derived and lower central series are examples of    *)
(*                        monotonic maps.                                     *)
(* Four structures provide interfaces to these properties:                    *)
(*    GFunctor.iso_map == structure for object maps that are group_valued,    *)
(*                        closed, and iso_continuous.                         *)
(*  [igFun by Fsub & !Fcont] == the iso_map structure for an object map F     *)
(*                        such that F G is canonically a group when G is, and *)
(*                        given Fsub : closed F and Fcont : iso_continuous F. *)
(*  [igFun by Fsub & Fcont] == as above, but expecting Fcont : continuous F.  *)
(*        [igFun of F] == clone an existing GFunctor.iso_map structure for F. *)
(*        GFunctor.map == structure for continuous object maps, inheriting    *)
(*                        from the GFunctor.iso_map structure.                *)
(*     [gFun by Fcont] == the map structure for an F with a canonical iso_map *)
(*                        structure, given Fcont : continuous F.              *)
(*         [gFun of F] == clone an existing GFunctor.map structure for F.     *)
(*       GFunctor.pmap == structure for pcontinuous object maps, inheriting   *)
(*                        from the GFunctor.map structure.                    *)
(*    [pgFun by Fher] == the pmap structure for an F with a canonical map     *)
(*                        structure, given Fher : hereditary F.               *)
(*        [pgFun of F] == clone an existing GFunctor.pmap structure for F.    *)
(*   GFunctor.mono_map == structure for monotonic, continuous object maps     *)
(*                        inheriting from the GFunctor.map structure.         *)
(*     [mgFun by Fmon] == the mono_map structure for an F with a canonical    *)
(*                        map structure, given Fmon : monotonic F.            *)
(*        [mgFun of F] == clone an existing GFunctor.mono_map structure for F *)
(* Lemmas for these group functors use either a 'gF' prefix or an 'F' suffix. *)
(* The (F1 \o F2) and (F1 %% F2) operations have canonical GFunctor.map       *)
(* structures when F1 is monotonic or hereditary, respectively.               *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Declare Scope gFun_scope.

Import GroupScope.

Delimit Scope gFun_scope with gF.

Module GFunctor.

Definition object_map := forall gT : finGroupType, {set gT} -> {set gT}.

Bind Scope gFun_scope with object_map.

Section Definitions.

Implicit Types gT hT : finGroupType.

Variable F : object_map.

(* Group closure. *)
Definition group_valued := forall gT (G : {group gT}), group_set (F G).

(* Subgroup closure. *)
Definition closed := forall gT (G : {group gT}), F G \subset G.

(* General functoriality, i.e., continuity of the object map *)
Definition continuous :=
  forall gT hT (G : {group gT}) (phi : {morphism G >-> hT}),
    phi @* F G \subset F (phi @* G).

(* Functoriality on the Grp groupoid (arrows are restricted to isos). *)
Definition iso_continuous :=
  forall gT hT (G : {group gT}) (phi : {morphism G >-> hT}),
   'injm phi -> phi @* F G \subset F (phi @* G).

Lemma continuous_is_iso_continuous : continuous -> iso_continuous.
Proof. by move=> Fcont gT hT G phi inj_phi; apply: Fcont. Qed.

(* Functoriality on Grp with partial morphisms. *)
Definition pcontinuous :=
  forall gT hT (G D : {group gT}) (phi : {morphism D >-> hT}),
    phi @* F G \subset F (phi @* G).

Lemma pcontinuous_is_continuous : pcontinuous -> continuous.
Proof. by move=> Fcont gT hT G; apply: Fcont. Qed.

(* Heredity with respect to inclusion *)
Definition hereditary :=
  forall gT (H G : {group gT}), H \subset G -> F G :&: H \subset F H.

Lemma pcontinuous_is_hereditary : pcontinuous -> hereditary.
Proof.
move=> Fcont gT H G sHG; rewrite -{2}(setIidPl sHG) setIC.
by do 2!rewrite -(morphim_idm (subsetIl H _)) morphimIdom ?Fcont.
Qed.

(* Monotonicity with respect to inclusion *)
Definition monotonic :=
  forall gT (H G : {group gT}), H \subset G -> F H \subset F G.

(* Self-expanding composition, and modulo *)

Variables (k : unit) (F1 F2 : object_map).

Definition comp : object_map := fun gT A => F1 (F2 A).

Definition modulo : object_map :=
  fun gT A => coset (F2 A) @*^-1 (F1 (A / (F2 A))).

End Definitions.

Section ClassDefinitions.

Structure iso_map := IsoMap {
  apply : object_map;
  _ : group_valued apply;
  _ : closed apply;
  _ : iso_continuous apply
}.
Local Coercion apply : iso_map >-> object_map.

Structure map := Map { iso_of_map : iso_map; _ : continuous iso_of_map }.
Local Coercion iso_of_map : map >-> iso_map.

Structure pmap := Pmap { map_of_pmap : map; _ : hereditary map_of_pmap }.
Local Coercion map_of_pmap : pmap >-> map.

Structure mono_map := MonoMap { map_of_mono : map; _ : monotonic map_of_mono }.
Local Coercion map_of_mono : mono_map >-> map.

Definition pack_iso F Fcont Fgrp Fsub := @IsoMap F Fgrp Fsub Fcont.

Definition clone_iso (F : object_map) :=
  fun Fgrp Fsub Fcont (isoF := @IsoMap F Fgrp Fsub Fcont) =>
  fun isoF0 & phant_id (apply isoF0) F & phant_id isoF isoF0 => isoF.

Definition clone (F : object_map) :=
  fun isoF & phant_id (apply isoF) F =>
  fun (funF0 : map) & phant_id (apply funF0) F =>
  fun Fcont (funF := @Map isoF Fcont) & phant_id funF0 funF => funF.

Definition clone_pmap (F : object_map) :=
  fun (funF : map) & phant_id (apply funF) F =>
  fun (pfunF0 : pmap) & phant_id (apply pfunF0) F =>
  fun Fher (pfunF := @Pmap funF Fher) & phant_id pfunF0 pfunF => pfunF.

Definition clone_mono (F : object_map) :=
  fun (funF : map) & phant_id (apply funF) F =>
  fun (mfunF0 : mono_map) & phant_id (apply mfunF0) F =>
  fun Fmon (mfunF := @MonoMap funF Fmon) & phant_id mfunF0 mfunF => mfunF.

End ClassDefinitions.

Module Exports.

Identity Coercion fun_of_object_map : object_map >-> Funclass.
Coercion apply : iso_map >-> object_map.
Coercion iso_of_map : map >-> iso_map.
Coercion map_of_pmap : pmap >-> map.
Coercion map_of_mono : mono_map >-> map.
Coercion continuous_is_iso_continuous : continuous >-> iso_continuous.
Coercion pcontinuous_is_continuous : pcontinuous >-> continuous.
Coercion pcontinuous_is_hereditary : pcontinuous >-> hereditary.

Notation "[ 'igFun' 'by' Fsub & Fcont ]" :=
    (pack_iso (continuous_is_iso_continuous Fcont) (fun gT G => groupP _) Fsub)
  (at level 0, format "[ 'igFun'  'by'  Fsub  &  Fcont ]") : form_scope.

Notation "[ 'igFun' 'by' Fsub & ! Fcont ]" :=
    (pack_iso Fcont (fun gT G => groupP _) Fsub)
  (at level 0, format "[ 'igFun'  'by'  Fsub  &  ! Fcont ]") : form_scope.

Notation "[ 'igFun' 'of' F ]" := (@clone_iso F _ _ _ _ id id)
  (at level 0, format "[ 'igFun'  'of'  F ]") : form_scope.

Notation "[ 'gFun' 'by' Fcont ]" := (Map Fcont)
  (at level 0, format "[ 'gFun'  'by'  Fcont ]") : form_scope.

Notation "[ 'gFun' 'of' F ]" := (@clone F _ id _ id _ id)
  (at level 0, format "[ 'gFun'  'of'  F ]") : form_scope.

Notation "[ 'pgFun' 'by' Fher ]" := (Pmap Fher)
  (at level 0, format "[ 'pgFun'  'by'  Fher ]") : form_scope.

Notation "[ 'pgFun' 'of' F ]" := (@clone_pmap F _ id _ id _ id)
  (at level 0, format "[ 'pgFun' 'of'  F ]") : form_scope.

Notation "[ 'mgFun' 'by' Fmon ]" := (MonoMap Fmon)
  (at level 0, format "[ 'mgFun'  'by'  Fmon ]") : form_scope.

Notation "[ 'mgFun' 'of' F ]" := (@clone_mono F _ id _ id _ id)
  (at level 0, format "[ 'mgFun' 'of'  F ]") : form_scope.

End Exports.

End GFunctor.
Export GFunctor.Exports.

Bind Scope gFun_scope with GFunctor.object_map.

Arguments GFunctor.comp F1 F2 _ /.
Notation "F1 \o F2" := (GFunctor.comp F1 F2) : gFun_scope.
Notation "F1 %% F2" := (GFunctor.modulo F1 F2) : gFun_scope.

Section FunctorGroup.

Variables (F : GFunctor.iso_map) (gT : finGroupType) (G : {group gT}).
Lemma gFgroupset : group_set (F gT G). Proof. by case: F. Qed.
Canonical gFgroup := Group gFgroupset.

End FunctorGroup.

Canonical gFmod_group
    (F1 : GFunctor.iso_map) (F2 : GFunctor.object_map)
    (gT : finGroupType) (G : {group gT}) :=
  [group of (F1 %% F2)%gF gT G].

Section IsoFunctorTheory.

Implicit Types gT rT : finGroupType.
Variable F : GFunctor.iso_map.

Lemma gFsub gT (G : {group gT}) : F gT G \subset G.
Proof. by case: F gT G. Qed.

Lemma gFsub_trans gT (G : {group gT}) (A : {pred gT}) :
  G \subset A -> F gT G \subset A.
Proof. exact/subset_trans/gFsub. Qed.

Lemma gF1 gT : F gT 1 = 1. Proof. exact/trivgP/gFsub. Qed.

Lemma gFiso_cont : GFunctor.iso_continuous F.
Proof. by case F. Qed.

Lemma gFchar gT (G : {group gT}) : F gT G \char G.
Proof.
apply/andP; split => //; first by apply: gFsub.
apply/forall_inP=> f Af; rewrite -{2}(im_autm Af) -(autmE Af).
by rewrite -morphimEsub ?gFsub ?gFiso_cont ?injm_autm.
Qed.

Lemma gFnorm gT (G : {group gT}) : G \subset 'N(F gT G).
Proof. exact/char_norm/gFchar. Qed.

Lemma gFnorms gT (G : {group gT}) : 'N(G) \subset 'N(F gT G).
Proof. exact/char_norms/gFchar. Qed.

Lemma gFnormal gT (G : {group gT}) : F gT G <| G.
Proof. exact/char_normal/gFchar. Qed.

Lemma gFchar_trans gT (G H : {group gT}) : H \char G -> F gT H \char G.
Proof. exact/char_trans/gFchar. Qed.

Lemma gFnormal_trans gT (G H : {group gT}) : H <| G -> F gT H <| G.
Proof. exact/char_normal_trans/gFchar. Qed.

Lemma gFnorm_trans gT (A : {pred gT}) (G : {group gT}) :
  A \subset 'N(G) -> A \subset 'N(F gT G).
Proof. by move/subset_trans/(_ (gFnorms G)). Qed.

Lemma injmF_sub gT rT (G D : {group gT}) (f : {morphism D >-> rT}) :
  'injm f -> G \subset D -> f @* (F gT G) \subset F rT (f @* G).
Proof.
move=> injf sGD; have:= gFiso_cont (injm_restrm sGD injf).
by rewrite im_restrm morphim_restrm (setIidPr _) ?gFsub.
Qed.

Lemma injmF gT rT (G D : {group gT}) (f : {morphism D >-> rT}) :
  'injm f -> G \subset D -> f @* (F gT G) = F rT (f @* G).
Proof.
move=> injf sGD; have [sfGD injf'] := (morphimS f sGD, injm_invm injf).
apply/esym/eqP; rewrite eqEsubset -(injmSK injf') ?gFsub_trans //.
by rewrite !(subset_trans (injmF_sub _ _)) ?morphim_invm // gFsub_trans.
Qed.

Lemma gFisom gT rT (G D : {group gT}) R (f : {morphism D >-> rT}) :
  G \subset D -> isom G (gval R) f -> isom (F gT G) (F rT R) f.
Proof.
case/(restrmP f)=> g [gf _ _ _]; rewrite -{f}gf => /isomP[injg <-].
by rewrite sub_isom ?gFsub ?injmF.
Qed.

Lemma gFisog gT rT (G : {group gT}) (R : {group rT}) :
  G \isog R -> F gT G \isog F rT R.
Proof. by case/isogP=> f injf <-; rewrite -injmF // sub_isog ?gFsub. Qed.

End IsoFunctorTheory.

Section FunctorTheory.

Implicit Types gT rT : finGroupType.
Variable F : GFunctor.map.

Lemma gFcont : GFunctor.continuous F.
Proof. by case F. Qed.

Lemma morphimF gT rT (G D : {group gT}) (f : {morphism D >-> rT}) :
  G \subset D -> f @* (F gT G) \subset F rT (f @* G).
Proof.
move=> sGD; rewrite -(setIidPr (gFsub F G)).
by rewrite -{3}(setIid G) -!(morphim_restrm sGD) gFcont.
Qed.

End FunctorTheory.

Section PartialFunctorTheory.

Implicit Types gT rT : finGroupType.

Section BasicTheory.

Variable F : GFunctor.pmap.

Lemma gFhereditary : GFunctor.hereditary F.
Proof. by case F. Qed.

Lemma gFunctorI gT (G H : {group gT}) :
  F gT G :&: H = F gT G :&: F gT (G :&: H).
Proof.
rewrite -{1}(setIidPr (gFsub F G)) [G :&: _]setIC -setIA.
rewrite -(setIidPr (gFhereditary (subsetIl G H))).
by rewrite setIC -setIA (setIidPr (gFsub F (G :&: H))).
Qed.

Lemma pmorphimF : GFunctor.pcontinuous F.
Proof.
move=> gT rT G D f; rewrite -morphimIdom -(setIidPl (gFsub F G)) setICA.
apply: (subset_trans (morphimS f (gFhereditary (subsetIr D G)))).
by rewrite (subset_trans (morphimF F _ _ )) ?morphimIdom ?subsetIl.
Qed.

Lemma gFid gT (G : {group gT}) : F gT (F gT G)  = F gT G.
Proof.
apply/eqP; rewrite eqEsubset gFsub.
by move/gFhereditary: (gFsub F G); rewrite setIid /=.
Qed.

End BasicTheory.

Section Modulo.

Variables (F1 : GFunctor.pmap) (F2 : GFunctor.map).

Lemma gFmod_closed : GFunctor.closed (F1 %% F2).
Proof. by move=> gT G; rewrite sub_cosetpre_quo ?gFsub ?gFnormal. Qed.

Lemma gFmod_cont : GFunctor.continuous (F1 %% F2).
Proof.
move=> gT rT G f; have nF2 := gFnorm F2.
have sDF: G \subset 'dom (coset (F2 _ G)) by rewrite nF2.
have sDFf: G \subset 'dom (coset (F2 _ (f @* G)) \o f).
  by rewrite -sub_morphim_pre ?subsetIl // nF2.
pose K := 'ker (restrm sDFf (coset (F2 _ (f @* G)) \o f)).
have sFK: 'ker (restrm sDF (coset (F2 _ G))) \subset K.
  rewrite {}/K !ker_restrm ker_comp /= subsetI subsetIl !ker_coset /=.
  by rewrite -sub_morphim_pre ?subsetIl // morphimIdom ?morphimF.
have sOF := gFsub F1 (G / F2 _ G); have sGG: G \subset G by [].
rewrite -sub_quotient_pre; last first.
  by apply: subset_trans (nF2 _ _); rewrite morphimS ?gFmod_closed.
suffices im_fact H : F2 _ G \subset gval H -> H \subset G ->
  factm sFK sGG @* (H / F2 _ G) = f @* H / F2 _ (f @* G).
- rewrite -2?im_fact ?gFmod_closed ?gFsub //.
    by rewrite cosetpreK morphimF /= ?morphim_restrm ?setIid.
  by rewrite -sub_quotient_pre ?normG //= trivg_quotient sub1G.
move=> sFH sHG; rewrite -(morphimIdom _ (H / _)) /= {2}morphim_restrm setIid.
rewrite -morphimIG ?ker_coset // -(morphim_restrm sDF) morphim_factm.
by rewrite morphim_restrm morphim_comp -quotientE morphimIdom.
Qed.

Canonical gFmod_igFun := [igFun by gFmod_closed & gFmod_cont].
Canonical gFmod_gFun := [gFun by gFmod_cont].

End Modulo.

Variables F1 F2 : GFunctor.pmap.

Lemma gFmod_hereditary : GFunctor.hereditary (F1 %% F2).
Proof.
move=> gT H G sHG; set FGH := _ :&: H; have nF2H := gFnorm F2 H.
rewrite -sub_quotient_pre; last exact: subset_trans (subsetIr _ _) _.
pose rH := restrm nF2H (coset (F2 _ H)); pose rHM := [morphism of rH].
have rnorm_simpl: rHM @* H = H / F2 _ H by rewrite morphim_restrm setIid.
have nF2G := subset_trans sHG (gFnorm F2 G).
pose rG := restrm nF2G (coset (F2 _ G)); pose rGM := [morphism of rG].
have sqKfK: 'ker rGM \subset 'ker rHM.
  rewrite !ker_restrm !ker_coset (setIidPr (gFsub F2 _)) setIC /=.
  exact: gFhereditary.
have sHH := subxx H; rewrite -rnorm_simpl /= -(morphim_factm sqKfK sHH) /=.
apply: subset_trans (gFcont F1 _); rewrite /= {2}morphim_restrm setIid /=.
apply: subset_trans (morphimS _ (gFhereditary _ (quotientS _ sHG))) => /=.
have ->: FGH / _ = restrm nF2H (coset _) @* FGH.
  by rewrite morphim_restrm setICA setIid.
rewrite -(morphim_factm sqKfK sHH) morphimS //= morphim_restrm -quotientE.
by rewrite setICA setIid (subset_trans (quotientI _ _ _)) // cosetpreK.
Qed.

Canonical gFmod_pgFun := [pgFun by gFmod_hereditary].

End PartialFunctorTheory.

Section MonotonicFunctorTheory.

Implicit Types gT rT : finGroupType.

Lemma gFunctorS (F : GFunctor.mono_map) : GFunctor.monotonic F.
Proof. by case: F. Qed.

Section Composition.

Variables (F1 : GFunctor.mono_map) (F2 : GFunctor.map).

Lemma gFcomp_closed : GFunctor.closed (F1 \o F2).
Proof. by move=> gT G; rewrite !gFsub_trans. Qed.

Lemma gFcomp_cont : GFunctor.continuous (F1 \o F2).
Proof.
move=> gT rT G phi; rewrite (subset_trans (morphimF _ _ (gFsub _ _))) //.
by rewrite (subset_trans (gFunctorS F1 (gFcont F2 phi))).
Qed.

Canonical gFcomp_igFun := [igFun by gFcomp_closed & gFcomp_cont].
Canonical gFcomp_gFun :=[gFun by gFcomp_cont].

End Composition.

Variables F1 F2 : GFunctor.mono_map.

Lemma gFcompS : GFunctor.monotonic (F1 \o F2).
Proof. by move=> gT H G sHG; rewrite !gFunctorS. Qed.

Canonical gFcomp_mgFun := [mgFun by gFcompS].

End MonotonicFunctorTheory.

Section GFunctorExamples.

Implicit Types gT : finGroupType.

Definition idGfun gT := @id {set gT}.

Lemma idGfun_closed : GFunctor.closed idGfun. Proof. by []. Qed.
Lemma idGfun_cont : GFunctor.continuous idGfun. Proof. by []. Qed.
Lemma idGfun_monotonic : GFunctor.monotonic idGfun. Proof. by []. Qed.

Canonical bgFunc_id := [igFun by idGfun_closed & idGfun_cont].
Canonical gFunc_id := [gFun by idGfun_cont].
Canonical mgFunc_id := [mgFun by idGfun_monotonic].

Definition trivGfun gT of {set gT} := [1 gT].

Lemma trivGfun_cont : GFunctor.pcontinuous trivGfun.
Proof. by move=> gT rT D G f; rewrite morphim1. Qed.

Canonical trivGfun_igFun := [igFun by sub1G & trivGfun_cont].
Canonical trivGfun_gFun := [gFun by trivGfun_cont].
Canonical trivGfun_pgFun := [pgFun by trivGfun_cont].

End GFunctorExamples.