(Joint Center)Library PFsection2

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
Require Import fintype tuple finfun bigop prime ssralg poly finset center.
Require Import fingroup morphism perm automorphism quotient action zmodp.
Require Import gfunctor gproduct cyclic pgroup frobenius ssrnum.
Require Import matrix mxalgebra mxrepresentation vector algC classfun character.
Require Import inertia vcharacter PFsection1.

This file covers Peterfalvi, Section 2: the Dade isometry Defined here: Dade_hypothesis G L A <-> G, L, and A satisfy the hypotheses under which which the Dade isometry relative to G, L and A is well-defined. For ddA : Dade_hypothesis G L A, we also define Dade ddA == the Dade isometry relative to G, L and A. Dade_signalizer ddA a == the normal complement to 'C_L[a] in 'C_G[a] for a in A (this is usually denoted by H a). Dade_support1 ddA a == the set of elements identified with a by the Dade isometry. Dade_support ddA == the natural support of the Dade isometry. The following are used locally in expansion of the Dade isometry as a sum of induced characters: Dade_transversal ddA == a transversal of the L-conjugacy classes of non empty subsets of A. Dade_set_signalizer ddA B == the generalization of H to B \subset A, denoted 'H(B) below. Dade_set_normalizer ddA B == the generalization of 'C_G[a] to B. denoted 'M(B) = 'H(B) ><| 'N_L(B) below. Dade_cfun_restriction ddA B aa == the composition of aa \in 'CF(L, A) with the projection of 'M(B) onto 'N_L(B), parallel to 'H(B). In addition, if sA1A : A1 \subset A and nA1L : L \subset 'N(A1), we have restr_Dade_hyp ddA sA1A nA1L : Dade_hypothesis G L A1 H restr_Dade ddA sA1A nA1L == the restriction of the Dade isometry to 'CF(L, A1).

Set Implicit Arguments.

Import GroupScope GRing.Theory Num.Theory.
Local Open Scope ring_scope.

Reserved Notation "alpha ^\tau" (at level 2, format "alpha ^\tau").

Section Two.

Variable gT : finGroupType.

This is Peterfalvi (2.1).
Lemma partition_cent_rcoset (H : {group gT}) g (C := 'C_H[g]) (Cg := C :* g) :
    g \in 'N(H)coprime #|H| #[g]
  partition (Cg :^: H) (H :* g) #|Cg :^: H| = #|H : C|.

Definition is_Dade_signalizer (G L A : {set gT}) (H : gT{group gT}) :=
  {in A, a, H a ><| 'C_L[a] = 'C_G[a]}.

This is Peterfalvi Definition (2.2).
Definition Dade_hypothesis (G L A : {set gT}) :=
  [/\ A <| L, L \subset G, 1%g \notin A,
   (*a*) {in A &, x, {subset x ^: G x ^: L}}
 & (*b*) exists2 H, is_Dade_signalizer G L A H
 & (*c*) {in A &, a b, coprime #|H a| #|'C_L[b]| }].

Variables (G L : {group gT}) (A : {set gT}).

Let pi := [pred p | [ a in A, p \in \pi('C_L[a])]].

Let piCL a : a \in Api.-group 'C_L[a].

Fact Dade_signalizer_key : unit.
Definition Dade_signalizer_def a := 'O_pi^'('C_G[a])%G.
Definition Dade_signalizer of Dade_hypothesis G L A :=
  locked_with Dade_signalizer_key Dade_signalizer_def.

Hypothesis ddA : Dade_hypothesis G L A.
Notation H := (Dade_signalizer ddA).
Canonical Dade_signalizer_unlockable := [unlockable fun H].

Let pi'H a : pi^'.-group (H a).
Let nsHC a : H a <| 'C_G[a].

Lemma Dade_signalizer_sub a : H a \subset G.

Lemma Dade_signalizer_cent a : H a \subset 'C[a].

Let nsAL : A <| L.
Let sAL : A \subset L.
Let nAL : L \subset 'N(A).
Let sLG : L \subset G.
Let notA1 : 1%g \notin A.
Let conjAG : {in A &, x, {subset x ^: G x ^: L}}.
Let sHG := Dade_signalizer_sub.
Let cHA := Dade_signalizer_cent.
Let notHa0 a : H a :* a :!=: set0.

Let HallCL a : a \in Api.-Hall('C_G[a]) 'C_L[a].

Lemma def_Dade_signalizer H1 : is_Dade_signalizer G L A H1{in A, H =1 H1}.

Lemma Dade_sdprod : is_Dade_signalizer G L A H.
Let defCA := Dade_sdprod.

Lemma Dade_coprime : {in A &, a b, coprime #|H a| #|'C_L[b]| }.
Let coHL := Dade_coprime.

Definition Dade_support1 a := class_support (H a :* a) G.
Local Notation dd1 := Dade_support1.

Lemma mem_Dade_support1 a x : a \in Ax \in H a → (x × a)%g \in dd1 a.

This is Peterfalvi (2.3), except for the existence part, which is covered below in the NormedTI section.
Lemma Dade_normedTI_P :
  reflect (A != set0 {in A, a, H a = 1%G}) (normedTI A G L).

This is Peterfalvi (2.4)(a) (extended to all a thanks to our choice of H).
Lemma DadeJ a x : x \in LH (a ^ x) :=: H a :^ x.

Lemma Dade_support1_id a x : x \in Ldd1 (a ^ x) = dd1 a.

Let piHA a u : a \in Au \in H a :* au.`_pi = a.

This is Peterfalvi (2.4)(b).
Lemma Dade_support1_TI : {in A &, a b,
  ~~ [disjoint dd1 a & dd1 b]exists2 x, x \in L & b = a ^ x}.

This is an essential strengthening of Peterfalvi (2.4)(c).
Lemma Dade_cover_TI : {in A, a, normedTI (H a :* a) G 'C_G[a]}.

This is Peterfalvi (2.4)(c).
This is Peterfalvi Definition (2.5).
Fact Dade_subproof (alpha : 'CF(L)) :
  is_class_fun <<G>> [ffun x oapp alpha 0 [pick a in A | x \in dd1 a]].
Definition Dade alpha := Cfun 1 (Dade_subproof alpha).

Lemma Dade_is_linear : linear Dade.
Canonical Dade_additive := Additive Dade_is_linear.
Canonical Dade_linear := Linear Dade_is_linear.

Local Notation "alpha ^\tau" := (Dade alpha).

This is the validity of Peterfalvi, Definition (2.5)
Lemma DadeE alpha a u : a \in Au \in dd1 aalpha^\tau u = alpha a.

Lemma Dade_id alpha : {in A, a, alpha^\tau a = alpha a}.

Lemma Dade_cfunS alpha : alpha^\tau \in 'CF(G, Atau).

Lemma Dade_cfun alpha : alpha^\tau \in 'CF(G, G^#).

Lemma Dade1 alpha : alpha^\tau 1%g = 0.

Lemma Dade_id1 :
  {in 'CF(L, A) & 1%g |: A, alpha a, alpha^\tau a = alpha a}.

Section AutomorphismCFun.

Variable u : {rmorphism algCalgC}.
Local Notation "alpha ^u" := (cfAut u alpha).

Lemma Dade_aut alpha : (alpha^u)^\tau = (alpha^\tau)^u.

End AutomorphismCFun.

Lemma Dade_conjC alpha : (alpha^*)^\tau = ((alpha^\tau)^*)%CF.

This is Peterfalvi (2.7), main part
Lemma general_Dade_reciprocity alpha (phi : 'CF(G)) (psi : 'CF(L)) :
    alpha \in 'CF(L, A)
  {in A, a, psi a = #|H a|%:R ^-1 × (\sum_(x in H a) phi (x × a)%g)}
  '[alpha^\tau, phi] = '[alpha, psi].

This is Peterfalvi (2.7), second part.
Lemma Dade_reciprocity alpha (phi : 'CF(G)) :
    alpha \in 'CF(L, A)
    {in A, a, {in H a, u, phi (u × a)%g = phi a}}
  '[alpha^\tau, phi] = '[alpha, 'Res[L] phi].

This is Peterfalvi (2.6)(a).
Supplement to Peterfalvi (2.3)/(2.6)(a); implies Isaacs Lemma 7.7.
Lemma Dade_Ind : normedTI A G L{in 'CF(L, A), Dade =1 'Ind}.

Definition Dade_set_signalizer (B : {set gT}) := \bigcap_(a in B) H a.
Local Notation "''H' ( B )" := (Dade_set_signalizer B)
  (at level 8, format "''H' ( B )") : group_scope.
Canonical Dade_set_signalizer_group B := [group of 'H(B)].
Definition Dade_set_normalizer B := 'H(B) <*> 'N_L(B).
Local Notation "''M' ( B )" := (Dade_set_normalizer B)
  (at level 8, format "''M' ( B )") : group_scope.
Canonical Dade_set_normalizer_group B := [group of 'M(B)].

Let calP := [set B : {set gT} | B \subset A & B != set0].

This is Peterfalvi (2.8).
Lemma Dade_set_sdprod : {in calP, B, 'H(B) ><| 'N_L(B) = 'M(B)}.

Section DadeExpansion.

Variable aa : 'CF(L).
Hypothesis CFaa : aa \in 'CF(L, A).

Definition Dade_restrm B :=
  if B \in calP then remgr 'H(B) 'N_L(B) else trivm 'M(B).
Fact Dade_restrM B : {in 'M(B) &, {morph Dade_restrm B : x y / x × y}%g}.
Canonical Dade_restr_morphism B := Morphism (@Dade_restrM B).
Definition Dade_cfun_restriction B :=
  cfMorph ('Res[Dade_restrm B @* 'M(B)] aa).

Local Notation "''aa_' B" := (Dade_cfun_restriction B)
  (at level 3, B at level 2, format "''aa_' B") : ring_scope.

Definition Dade_transversal := [set repr (B :^: L) | B in calP].
Local Notation calB := Dade_transversal.

Lemma Dade_restrictionE B x :
  B \in calP'aa_B x = aa (remgr 'H(B) 'N_L(B) x) *+ (x \in 'M(B)).
Local Notation rDadeE := Dade_restrictionE.

Lemma Dade_restriction_vchar B : aa \in 'Z[irr L]'aa_B \in 'Z[irr 'M(B)].

Let sMG B : B \in calP'M(B) \subset G.

This is Peterfalvi (2.10.1)
Lemma Dade_Ind_restr_J :
  {in L & calP, x B, 'Ind[G] 'aa_(B :^ x) = 'Ind[G] 'aa_B}.

This is Peterfalvi (2.10.2)
Lemma Dade_setU1 : {in calP & A, B a, 'H(a |: B) = 'C_('H(B))[a]}.

Let calA g (X : {set gT}) := [set x in G | g ^ x \in X]%g.

This is Peterfalvi (2.10.3)
Lemma Dade_Ind_expansion B g :
    B \in calP
  [/\ g \notin Atau → ('Ind[G, 'M(B)] 'aa_B) g = 0
    & {in A, a, g \in dd1 a
       ('Ind[G, 'M(B)] 'aa_B) g =
          (aa a / #|'M(B)|%:R) ×
               \sum_(b in 'N_L(B) :&: a ^: L) #|calA g ('H(B) :* b)|%:R}].

This is Peterfalvi (2.10)
This is Peterfalvi (2.6)(b)
Lemma Dade_vchar alpha : alpha \in 'Z[irr L, A]alpha^\tau \in 'Z[irr G].

This summarizes Peterfalvi (2.6).
Lemma Dade_Zisometry : {in 'Z[irr L, A], isometry Dade, to 'Z[irr G, G^#]}.

End Two.

Section RestrDade.

Variables (gT : finGroupType) (G L : {group gT}) (A A1 : {set gT}).
Hypothesis ddA : Dade_hypothesis G L A.
Hypotheses (sA1A : A1 \subset A) (nA1L : L \subset 'N(A1)).
Let ssA1A := subsetP sA1A.

This is Peterfalvi (2.11), first part.
This is Peterfalvi (2.11), second part.
Lemma restr_DadeE : {in 'CF(L, A1), restr_Dade =1 Dade ddA}.

End RestrDade.

Section NormedTI.

Variables (gT : finGroupType) (G L : {group gT}) (A : {set gT}).
Hypotheses (tiAG : normedTI A G L) (sAG1 : A \subset G^#).

This is the existence part of Peterfalvi (2.3).
This is the identity part of Isaacs, Lemma 7.7.
Lemma normedTI_Ind_id1 :
  {in 'CF(L, A) & 1%g |: A, alpha, 'Ind[G] alpha =1 alpha}.

A more restricted, but more useful form.
Lemma normedTI_Ind_id :
  {in 'CF(L, A) & A, alpha, 'Ind[G] alpha =1 alpha}.

This is the isometry part of Isaacs, Lemma 7.7. The statement in Isaacs is slightly more general in that it allows for beta \in 'CF(L, 1%g |: A); this appears to be more cumbersome than useful.