(Joint Center)Library PFsection5

(* (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.
Require Import matrix mxalgebra mxrepresentation vector ssrint.
Require Import ssrnum algC classfun character inertia vcharacter.
Require Import PFsection1 PFsection2 PFsection3 PFsection4.

This file covers Peterfalvi, Section 5: Coherence. Defined here: coherent_with S A tau tau1 <-> tau1 is a Z-linear isometry from 'Z[S] to 'Z[irr G] that coincides with tau on 'Z[S, A]. coherent S A tau <-> (S, A, tau) is coherent, i.e., there is a Z-linear isometry tau1 s.t. coherent_with S A tau tau1. subcoherent S tau R <-> S : seq 'cfun(L) is non empty, pairwise orthogonal and closed under complex conjugation, tau is an isometry from 'Z[S, L^# ] to virtual characters in G that maps the difference chi - chi^*, for each chi \in S, to the sum of an orthonormal family R chi of virtual characters of G; also, R chi and R phi are orthogonal unless phi \in chi :: chi^*. dual_iso nu == the Z-linear (additive) mapping phi |-> - nu phi^* for nu : {additive 'CF(L) -> 'CF(G)}. If nu is an isometry extending a subcoherent tau on 'Z[S] with size S = 2, then so is dual_iso nu. We provide a set of definitions that cover the various \cal S notations introduces in Peterfalvi sections 5, 6, 7, and 9 to 14. Iirr_ker K A == the set of all i : Iirr K such that the kernel of 'chi_i contains A. Iirr_kerD K B A == the set of all i : Iirr K such that the kernel of 'chi_i contains A but not B. seqInd L calX == the duplicate-free sequence of characters of L induced from K by the 'chi_i for i in calX. seqIndT K L == the duplicate-free sequence of all characters of L induced by irreducible characters of K. seqIndD K L H M == the duplicate-free sequence of characters of L induced by irreducible characters of K that have M in their kernel, but not H.

Set Implicit Arguments.

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

Results about the set of induced irreducible characters
Section InducedIrrs.

Variables (gT : finGroupType) (K L : {group gT}).
Implicit Types (A B : {set gT}) (H M : {group gT}).
Implicit Type u : {rmorphism algCalgC}.

Section KerIirr.

Definition Iirr_ker A := [set i | A \subset cfker 'chi[K]_i].

Lemma Iirr_kerS A B : B \subset AIirr_ker A \subset Iirr_ker B.

Lemma sum_Iirr_ker_square H :
  H <| K\sum_(i in Iirr_ker H) 'chi_i 1%g ^+ 2 = #|K : H|%:R.

Definition Iirr_kerD B A := Iirr_ker A :\: Iirr_ker B.

Lemma sum_Iirr_kerD_square H M :
    H <| KM <| KM \subset H
  \sum_(i in Iirr_kerD H M) 'chi_i 1%g ^+ 2 = #|K : H|%:R × (#|H : M|%:R - 1).

Lemma Iirr_ker_aut u A i : (aut_Iirr u i \in Iirr_ker A) = (i \in Iirr_ker A).

Lemma Iirr_ker_conjg A i x :
  x \in 'N(A)(conjg_Iirr i x \in Iirr_ker A) = (i \in Iirr_ker A).

Lemma Iirr_kerDS A1 A2 B1 B2 :
  A2 \subset A1B1 \subset B2Iirr_kerD B1 A1 \subset Iirr_kerD B2 A2.

Lemma Iirr_kerDY B A : Iirr_kerD (A <*> B) A = Iirr_kerD B A.

Lemma mem_Iirr_ker1 i : (i \in Iirr_kerD K 1%g) = (i != 0).

End KerIirr.

Hypothesis nsKL : K <| L.
Let sKL := normal_sub nsKL.
Let nKL := normal_norm nsKL.
Let e := #|L : K|%:R : algC.
Let nze : e != 0 := neq0CiG _ _.

Section SeqInd.

Variable calX : {set (Iirr K)}.

The set of characters induced from the irreducibles in calX.
Definition seqInd := undup [seq 'Ind[L] 'chi_i | i in calX].
Local Notation S := seqInd.

Lemma seqInd_uniq : uniq S.

Lemma seqIndP phi :
  reflect (exists2 i, i \in calX & phi = 'Ind[L] 'chi_i) (phi \in S).

Lemma seqInd_on : {subset S 'CF(L, K)}.

Lemma seqInd_char : {subset S character}.

Lemma Cnat_seqInd1 phi : phi \in Sphi 1%g \in Cnat.

Lemma Cint_seqInd1 phi : phi \in Sphi 1%g \in Cint.

Lemma seqInd_neq0 psi : psi \in Spsi != 0.

Lemma seqInd1_neq0 psi : psi \in Spsi 1%g != 0.

Lemma cfnorm_seqInd_neq0 psi : psi \in S'[psi] != 0.

Lemma seqInd_ortho : {in S &, phi psi, phi != psi'[phi, psi] = 0}.

Lemma seqInd_orthogonal : pairwise_orthogonal S.

Lemma seqInd_free : free S.

Lemma seqInd_zcharW : {subset S 'Z[S]}.

Lemma seqInd_zchar : {subset S 'Z[S, K]}.

Lemma seqInd_vcharW : {subset S 'Z[irr L]}.

Lemma seqInd_vchar : {subset S 'Z[irr L, K]}.

Lemma zcharD1_seqInd : 'Z[S, L^#] =i 'Z[S, K^#].

Lemma zcharD1_seqInd_Dade A :
  1%g \notin A{subset S 'CF(L, 1%g |: A)}'Z[S, L^#] =i 'Z[S, A].

Lemma dvd_index_seqInd1 phi : phi \in Sphi 1%g / e \in Cnat.

Lemma sub_seqInd_zchar phi psi :
  phi \in Spsi \in Spsi 1%g *: phi - phi 1%g *: psi \in 'Z[S, K^#].

Lemma sub_seqInd_on phi psi :
  phi \in Spsi \in Spsi 1%g *: phi - phi 1%g *: psi \in 'CF(L, K^#).

Lemma size_irr_subseq_seqInd S1 :
    subseq S1 S{subset S1 irr L}
  (#|L : K| × size S1 = #|[set i | 'Ind 'chi[K]_i \in S1]|)%N.

Section Beta.

Variable xi : 'CF(L).
Hypotheses (Sxi : xi \in S) (xi1 : xi 1%g = e).

Lemma cfInd1_sub_lin_vchar : 'Ind[L, K] 1 - xi \in 'Z[irr L, K^#].

Lemma cfInd1_sub_lin_on : 'Ind[L, K] 1 - xi \in 'CF(L, K^#).

Lemma seqInd_sub_lin_vchar :
  {in S, phi : 'CF(L), phi - (phi 1%g / e) *: xi \in 'Z[S, K^#]}.

Lemma seqInd_sub_lin_on :
  {in S, phi : 'CF(L), phi - (phi 1%g / e) *: xi \in 'CF(L, K^#)}.

End Beta.

End SeqInd.

Implicit Arguments seqIndP [calX phi].

Lemma seqIndS (calX calY : {set Iirr K}) :
 calX \subset calY{subset seqInd calX seqInd calY}.

Definition seqIndT := seqInd setT.

Lemma seqInd_subT calX : {subset seqInd calX seqIndT}.

Lemma mem_seqIndT i : 'Ind[L, K] 'chi_i \in seqIndT.

Lemma seqIndT_Ind1 : 'Ind[L, K] 1 \in seqIndT.

Lemma cfAut_seqIndT u : cfAut_closed u seqIndT.

Definition seqIndD H M := seqInd (Iirr_kerD H M).

Lemma seqIndDY H M : seqIndD (M <*> H) M = seqIndD H M.

Lemma mem_seqInd H M i :
  H <| LM <| L('Ind 'chi_i \in seqIndD H M) = (i \in Iirr_kerD H M).

Lemma seqIndC1P phi :
  reflect (exists2 i, i != 0 & phi = 'Ind 'chi[K]_i) (phi \in seqIndD K 1).

Lemma seqIndC1_filter : seqIndD K 1 = filter (predC1 ('Ind[L, K] 1)) seqIndT.

Lemma seqIndC1_rem : seqIndD K 1 = rem ('Ind[L, K] 1) seqIndT.

Section SeqIndD.

Variables H0 H M : {group gT}.

Local Notation S := (seqIndD H M).

Lemma cfAut_seqInd u : cfAut_closed u S.

Lemma seqInd_conjC_subset1 : H \subset H0cfConjC_subset S (seqIndD H0 1).

Lemma seqInd_sub_aut_zchar u :
  {in S, phi, phi - cfAut u phi \in 'Z[S, K^#]}.

Hypothesis sHK : H \subset K.

Lemma seqInd_sub : {subset S seqIndD K 1}.

Lemma seqInd_ortho_Ind1 : {in S, phi, '[phi, 'Ind[L, K] 1] = 0}.

Lemma seqInd_ortho_cfuni : {in S, phi, '[phi, '1_K] = 0}.

Lemma seqInd_ortho_1 : {in S, phi, '[phi, 1] = 0}.

Lemma sum_seqIndD_square :
    H <| LM <| LM \subset H
  \sum_(phi <- S) phi 1%g ^+ 2 / '[phi] = #|L : H|%:R × (#|H : M|%:R - 1).

Section Odd.

Hypothesis oddL : odd #|L|.

Lemma seqInd_conjC_ortho : {in S, phi, '[phi, phi^*] = 0}.

Lemma seqInd_conjC_neq : {in S, phi, phi^* != phi}%CF.

Lemma seqInd_notReal : ~~ has cfReal S.

Variable r : Iirr L.
Local Notation chi := 'chi_r.
Hypothesis Schi : chi \in S.

Lemma seqInd_conjC_ortho2 : orthonormal (chi :: chi^*)%CF.

Lemma seqInd_nontrivial_irr : (count (mem (irr L)) S > 1)%N.

Lemma seqInd_nontrivial : (size S > 1)%N.

End Odd.

End SeqIndD.

Lemma sum_seqIndC1_square :
  \sum_(phi <- seqIndD K 1) phi 1%g ^+ 2 / '[phi] = e × (#|K|%:R - 1).

End InducedIrrs.

Implicit Arguments seqIndP [gT K L calX phi].
Implicit Arguments seqIndC1P [gT K L phi].

Section Five.

Variable gT : finGroupType.

Section Defs.

Variables L G : {group gT}.

This is Peterfalvi, Definition (5.1). We depart from the text in Section 5 by dropping non-triviality condition, which is not used consistently in the rest of the proof; in particular, it is incompatible with the use of "not coherent" in (6.2), and it is only really used in (7.8), where a weaker condition (size S > 1) would suffice.
Definition coherent_with S A tau (tau1 : {additive 'CF(L)'CF(G)}) :=
  {in 'Z[S], isometry tau1, to 'Z[irr G]} {in 'Z[S, A], tau1 =1 tau}.

Definition coherent S A tau := tau1, coherent_with S A tau tau1.

This is Peterfalvi, Hypothesis (5.2). The Z-linearity constraint on tau will be expressed by an additive or linear structure on tau.
Definition subcoherent S tau R :=
  [/\ (*a*) [/\ {subset S character}, ~~ has cfReal S & conjC_closed S],
      (*b*) {in 'Z[S, L^#], isometry tau, to 'Z[@irr gT G, G^#]},
      (*c*) pairwise_orthogonal S,
      (*d*) {in S, xi : 'CF(L : {set gT}),
              [/\ {subset R xi 'Z[irr G]}, orthonormal (R xi)
                & tau (xi - xi^*)%CF = \sum_(alpha <- R xi) alpha]}
    & (*e*) {in S &, xi phi : 'CF(L),
              orthogonal phi (xi :: xi^*%CF) → orthogonal (R phi) (R xi)}].

Definition dual_iso (nu : {additive 'CF(L)'CF(G)}) :=
  [additive of -%R \o nu \o cfAut conjC].

End Defs.

Section SubsetCoherent.

Variables L G : {group gT}.
Implicit Type tau : 'CF(L)'CF(G).

Lemma subgen_coherent S1 S2 A tau:
  {subset S2 'Z[S1]}coherent S1 A taucoherent S2 A tau.

Lemma subset_coherent S1 S2 A tau:
  {subset S2 S1}coherent S1 A taucoherent S2 A tau.

Lemma subset_coherent_with S1 S2 A tau (tau1 : {additive 'CF(L)'CF(G)}) :
    {subset S1 S2}coherent_with S2 A tau tau1
  coherent_with S1 A tau tau1.

Lemma perm_eq_coherent S1 S2 A tau:
  perm_eq S1 S2coherent S1 A taucoherent S2 A tau.

Lemma dual_coherence S tau R nu :
    subcoherent S tau Rcoherent_with S L^# tau nu → (size S 2)%N
  coherent_with S L^# tau (dual_iso nu).

Lemma coherent_seqInd_conjCirr S tau R nu r :
    subcoherent S tau Rcoherent_with S L^# tau nu
    let chi := 'chi_r in let chi2 := (chi :: chi^*)%CF in
    chi \in S
  [/\ {subset map nu chi2 'Z[irr G]}, orthonormal (map nu chi2),
      chi - chi^*%CF \in 'Z[S, L^#] & (nu chi - nu chi^*)%CF 1%g == 0].

End SubsetCoherent.

This is Peterfalvi (5.3)(a).
Lemma irr_subcoherent (L G : {group gT}) S tau :
    cfConjC_subset S (irr L) → ~~ has cfReal S
    {in 'Z[S, L^#], isometry tau, to 'Z[irr G, G^#]}
  {R | subcoherent S tau R}.

This is Peterfalvi (5.3)(b).
Lemma prDade_subcoherent (G L K H W W1 W2 : {group gT}) A A0 S
    (defW : W1 \x W2 = W) (ddA : prime_Dade_hypothesis G L K H A A0 defW)
    (w_ := fun i jcyclicTIirr defW i j) (sigma := cyclicTIiso ddA)
    (mu := primeTIred ddA) (delta := fun jprimeTIsign ddA j)
    (tau := Dade ddA) :
    let dsw j k := [seq delta j *: sigma (w_ i k) | i : Iirr W1] in
    let Rmu j := dsw j j ++ map -%R (dsw j (conjC_Iirr j)) in
    cfConjC_subset S (seqIndD K L H 1) → ~~ has cfReal S
  {R | [/\ subcoherent S tau R,
           {in [predI S & irr L] & irr W,
               phi w, orthogonal (R phi) (sigma w)}
         & j, R (mu j) = Rmu j ]}.

Section SubCoherentProperties.

Variables (L G : {group gT}) (S : seq 'CF(L)) (R : 'CF(L)seq 'CF(G)).
Variable tau : {linear 'CF(L)'CF(G)}.
Hypothesis cohS : subcoherent S tau R.

Lemma nil_coherent A : coherent [::] A tau.

Lemma subset_subcoherent S1 : cfConjC_subset S1 Ssubcoherent S1 tau R.

Lemma subset_ortho_subcoherent S1 chi :
  {subset S1 S}chi \in Schi \notin S1orthogonal S1 chi.

Lemma subcoherent_split chi beta :
    chi \in Sbeta \in 'Z[irr G]
  exists2 X, X \in 'Z[R chi]
        & Y, [/\ beta = X - Y, '[X, Y] = 0 & orthogonal Y (R chi)].

This is Peterfalvi (5.4). The assumption X \in 'Z[R chi] has been weakened to ' [X, Y] = 0; this stronger form of the lemma is needed to strengthen the proof of (5.6.3) so that it can actually be reused in (9.11.8), as the text suggests.
Lemma subcoherent_norm chi psi (tau1 : {additive 'CF(L)'CF(G)}) X Y :
    [/\ chi \in S, psi \in 'Z[irr L] & orthogonal (chi :: chi^*)%CF psi]
    let S0 := chi - psi :: chi - chi^*%CF in
    {in 'Z[S0], isometry tau1, to 'Z[irr G]}
    tau1 (chi - chi^*)%CF = tau (chi - chi^*)%CF
    [/\ tau1 (chi - psi) = X - Y, '[X, Y] = 0 & orthogonal Y (R chi)]
 [/\ (*a*) '[chi] '[X]
   & (*b*) '[psi] '[Y]
           [/\ '[X] = '[chi], '[Y] = '[psi]
             & exists2 E, subseq E (R chi) & X = \sum_(xi <- E) xi]].

This is Peterfalvi (5.5).
Lemma coherent_sum_subseq chi (tau1 : {additive 'CF(L)'CF(G)}) :
    chi \in S
    {in 'Z[chi :: chi^*%CF], isometry tau1, to 'Z[irr G]}
    tau1 (chi - chi^*%CF) = tau (chi - chi^*%CF) →
  exists2 E, subseq E (R chi) & tau1 chi = \sum_(a <- E) a.

A reformulation of (5.5) that is more convenient to use.
Corollary mem_coherent_sum_subseq S1 chi (tau1 : {additive 'CF(L)'CF(G)}) :
    cfConjC_subset S1 Scoherent_with S1 L^# tau tau1chi \in S1
  exists2 E, subseq E (R chi) & tau1 chi = \sum_(a <- E) a.

A frequently used consequence of (5.5).
Corollary coherent_ortho_supp S1 chi (tau1 : {additive 'CF(L)'CF(G)}) :
    cfConjC_subset S1 Scoherent_with S1 L^# tau tau1
    chi \in Schi \notin S1
  orthogonal (map tau1 S1) (R chi).

An even more frequently used corollary of the corollary above.
Corollary coherent_ortho S1 S2 (tau1 tau2 : {additive 'CF(L)'CF(G)}) :
    cfConjC_subset S1 Scoherent_with S1 L^# tau tau1
    cfConjC_subset S2 Scoherent_with S2 L^# tau tau2
    {subset S2 [predC S1]}
  orthogonal (map tau1 S1) (map tau2 S2).

A glueing lemma exploiting the corollary above.
Lemma bridge_coherent S1 S2 (tau1 tau2 : {additive 'CF(L)'CF(G)}) chi phi :
    cfConjC_subset S1 Scoherent_with S1 L^# tau tau1
    cfConjC_subset S2 Scoherent_with S2 L^# tau tau2
    {subset S2 [predC S1]}
    [/\ chi \in S1, phi \in 'Z[S2] & chi - phi \in 'CF(L, L^#)]
    tau (chi - phi) = tau1 chi - tau2 phi
  coherent (S1 ++ S2) L^# tau.

This is essentially Peterfalvi (5.6.3), which gets reused in (9.11.8).
Lemma extend_coherent_with S1 (tau1 : {additive 'CF(L)'CF(G)}) chi phi a X :
    cfConjC_subset S1 Scoherent_with S1 L^# tau tau1
    [/\ phi \in S1, chi \in S & chi \notin S1]
    [/\ a \in Cint, chi 1%g = a × phi 1%g & '[X, a *: tau1 phi] = 0]
    tau (chi - a *: phi) = X - a *: tau1 phi
  coherent (chi :: chi^*%CF :: S1) L^# tau.

This is Peterfalvi (5.6).
Lemma extend_coherent S1 xi1 chi :
    cfConjC_subset S1 S[/\ xi1 \in S1, chi \in S & chi \notin S1]
    [/\ (*a*) coherent S1 L^# tau,
        (*b*) (xi1 1%g %| chi 1%g)%C
      & (*c*) 2%:R × chi 1%g × xi1 1%g < \sum_(xi <- S1) xi 1%g ^+ 2 / '[xi]]
  coherent (chi :: chi^*%CF :: S1) L^# tau.

This is Peterfalvi (5.7). This is almost a superset of (1.4): we could use it to get a coherent isometry, which would necessarily map irreducibles to signed irreducibles. It would then only remain to show that the signs are chosen consistently, by considering the degrees of the differences.
A corollary of Peterfalvi (5.7) used (sometimes implicitly!) in the proof of lemmas (11.9), (12.4) and (12.5).
Lemma pair_degree_coherence L G S (tau : {linear _'CF(gval G)}) R :
    subcoherent S tau R
  {in S &, phi1 phi2 : 'CF(gval L), phi1 1%g == phi2 1%g
    S1 : seq 'CF(L),
     [/\ phi1 \in S1, phi2 \in S1, cfConjC_subset S1 S & coherent S1 L^# tau]}.

This is Peterfalvi (5.8).
Lemma coherent_prDade_TIred (G H L K W W1 W2 : {group gT}) A A0 S
                            k (tau1 : {additive 'CF(L)'CF(G)})
    (defW : W1 \x W2 = W) (ddA : prime_Dade_hypothesis G L K H A A0 defW)
    (sigma := cyclicTIiso ddA) (w_ := fun i jcyclicTIirr defW i j)
    (mu := primeTIred ddA) (dk := primeTIsign ddA k) (tau := Dade ddA) :
  cfConjC_subset S (seqIndD K L H 1) →
  [/\ ~~ has cfReal S, has (mem (irr L)) S & mu k \in S]
  coherent_with S L^# tau tau1
  let j := conjC_Iirr k in
     tau1 (mu k) = dk *: (\sum_i sigma (w_ i k))
   tau1 (mu k) = - dk *: (\sum_i sigma (w_ i j))
   ( ell, mu ell \in Smu ell 1%g = mu k 1%gell = k ell = j).

Section DadeAut.

Variables (L G : {group gT}) (A : {set gT}).
Implicit Types K H M : {group gT}.
Hypothesis ddA : Dade_hypothesis G L A.

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

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

This is Peterfalvi (5.9)(a), slightly reformulated to allow calS to also contain non-irreducible characters; for groups of odd order, the first assumption holds uniformly for all calS of the form seqIndD.
Lemma cfAut_Dade_coherent calS tau1 i (chi := 'chi_i) :
    coherent_with calS A tau tau1'Z[calS, L^#] =i 'Z[calS, A]
    [/\ 1 < count (mem (irr L)) calS, free calS & cfAut_closed u calS]%N
    chi \in calS
  (tau1 chi)^u = tau1 (chi^u).

End DadeAutIrr.

This covers all the uses of (5.9)(a) in the rest of Peterfalvi, except one instance in (
Lemma cfConjC_Dade_coherent K H M (calS := seqIndD K L H M) tau1 i :
    coherent_with calS A (Dade ddA) tau1'Z[calS, L^#] =i 'Z[calS, A]
    [/\ odd #|G|, K <| L & H \subset K]'chi_i \in calS
  (tau1 'chi_i)^*%CF = tau1 ('chi_i)^*%CF.

This is Peterfalvi (5.9)(b).
Lemma Dade_irr_sub_conjC i (chi := 'chi_i) (phi := chi - chi^*%CF):
  chi \in 'CF(L, 1%g |: A) t, phi^\tau = 'chi_t - ('chi_t)^*%CF.

End DadeAut.

End Five.

Implicit Arguments coherent_prDade_TIred
  [gT G H L K W W1 W2 A0 A S0 k tau1 defW].