(Joint Center)Library PFsection7

(* (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 commutator nilpotent frobenius.
Require Import matrix mxalgebra mxrepresentation BGsection3 vector.
Require Import ssrnum algC classfun character inertia vcharacter.
Require Import PFsection1 PFsection2 PFsection4 PFsection5 PFsection6.

This file covers Peterfalvi, Section 7: Non-existence of a Certain Type of Group of Odd Order Defined here: inDade ddA == the right inverse to the Dade isometry with respect to G, L, A, given ddA : Dade_hypothesis G L A. phi^\rho == locally-bindable Notation for invDade ddA phi.

Set Implicit Arguments.

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

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

Section Seven.

Variables (gT : finGroupType) (G : {group gT}).
Implicit Types (L H P : {group gT}) (DH : gT{group gT}).

Properties of the inverse to the Dade isometry (Peterfalvi (7.1) to (7.3).
Section InverseDade.

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

Local Notation "alpha ^\tau" := (Dade ddA alpha).
Local Notation Atau := (Dade_support ddA).
Local Notation H := (Dade_signalizer ddA).

Let nsAL : A <| L.
Let sAL : A \subset L.
Let nAL : L \subset 'N(A).
Let sLG : L \subset G.

This is the Definition embedded in Peterfalvi, Hypothesis (7.1).
Fact invDade_subproof (chi : 'CF(G)) :
  is_class_fun <<L>>
    [ffun a #|H a|%:R^-1 × (\sum_(x in H a) chi (x × a)%g) *+ (a \in A)].
Definition invDade alpha := Cfun 1 (invDade_subproof alpha).

Local Notation "alpha ^\rho" := (invDade alpha).

Fact invDade_is_linear : linear invDade.
Canonical invDade_linear := Linear invDade_is_linear.
Canonical invDade_additive := Additive invDade_is_linear.

Lemma invDade_on chi : chi^\rho \in 'CF(L, A).

Lemma invDade_cfun1 : 1^\rho = '1_A.

This is Peterfalvi (2.7), restated using invDade.
This is Peterfalvi (7.2)(a).
Lemma DadeK alpha : alpha \in 'CF(L, A)(alpha^\tau)^\rho = alpha.

This is Peterfalvi (7.2)(b); note that by (7.2)(a) chi is in the image of tau iff chi = (chi^\rho)^\tau, and this condition is easier to write.
This is Peterfalvi (7.3).
Lemma leC_cfnorm_invDade_support chi :
  '[chi^\rho] #|G|%:R^-1 × (\sum_(g in Atau) `|chi g| ^+ 2)
     ?= iff [ a in A, u in H a, chi (u × a)%g == chi a].

This is the norm expansion embedded in Peterfalvi (7.3).
Hypothesis (7.4) and Lemma (7.5).
These declarations correspond to Peterfalvi, Hypothesis (7.4); as it is only instantiated twice after this section we leave it unbundled.
Variables (I : finType) (L : I{group gT}) (A : I{set gT}).
Hypothesis ddA : i : I, Dade_hypothesis G (L i) (A i).

Local Notation Atau i := (Dade_support (ddA i)).
Local Notation "alpha ^\rho" := (invDade (ddA _) alpha).
Hypothesis disjointA : i j, i != j[disjoint Atau i & Atau j].

This is Peterfalvi (7.5).
Hypothesis (7.6), and Lemmas (7.7) and (7.8)
Section Dade_seqIndC1.

In this section, A = H^# with H <| L.
Variables L H : {group gT}.
Let A := H^#.
Hypothesis ddA : Dade_hypothesis G L A.

Local Notation Atau := (Dade_support ddA).
Local Notation "alpha ^\tau" := (Dade ddA alpha).
Local Notation "alpha ^\rho" := (invDade ddA alpha).

Let calT := seqIndT H L.
Local Notation calS := (seqIndD H L H 1).
Local Notation Ind1H := ('Ind[gval L, gval H] 1).
Let uniqS : uniq calS := seqInd_uniq _ _.

Let h := #|H|%:R : algC.
Let e := #|L : H|%:R : algC.

Let nsAL : A <| L.
Let sLG : L \subset G.
Let nsHL : H <| L.
Let sHL := normal_sub nsHL.
Let nHL := normal_norm nsHL.

Let nzh : h != 0 := neq0CG H.
Let nze : e != 0 := neq0CiG L H.
Let nzL : #|L|%:R != 0 := neq0CG L.

Let eh : e × h = #|L|%:R.

Section InvDadeSeqInd.

Variables (xi0 : 'CF(L)) (S : seq 'CF(L)) (chi : 'CF(G)).
Implicit Types xi mu : 'CF(L).

Let d xi := xi 1%g / xi0 1%g.
Let psi xi := xi - d xi *: xi0.
Let c xi := '[(psi xi)^\tau, chi].

Let uc c xi mu := (c xi)^* × c mu / ('[xi] × '[mu]).
Let u c xi mu := uc c xi mu × ('[xi, mu] - xi 1%g × mu 1%g / (e × h)).

This is Peterfalvi (7.7); it is stated using a bespoke concrete Prop so as to encapsulate the coefficient definitions given above.
CoInductive is_invDade_seqInd_sum : Prop :=
  InvDadeSeqIndSum (c := c) (u := u c) of
   (*a*) {in A, x, (chi^\rho) x = \sum_(xi <- S) (c xi)^* / '[xi] × xi x}
 & (*b*) '[chi^\rho] = \sum_(xi <- S) \sum_(mu <- S) u xi mu.

Lemma invDade_seqInd_sum : perm_eq calT (xi0 :: S) → is_invDade_seqInd_sum.

End InvDadeSeqInd.

This is Peterfalvi (7.8). Our version is slightly stronger because we state the nontriviality of S directly than through the coherence premise (see the discussion of (6.2)).
Lemma Dade_Ind1_sub_lin (nu : {additive 'CF(L)'CF(G)}) r (zeta := 'chi_r) :
    coherent_with calS A (Dade ddA) nu → (1 < size calS)%N
    zeta \in calSzeta 1%g = e
  let beta := (Ind1H - zeta)^\tau in let calSnu := map nu calS in
  let sumSnu := \sum_(xi <- calS) xi 1%g / e / '[xi] *: nu xi in
  [/\ (*a1*) [/\ orthogonal calSnu [:: 1], '[beta, 1] = 1 & beta \in 'Z[irr G]],
      exists2 Gamma,
      (*a2*) [/\ orthogonal calSnu [:: Gamma], '[Gamma, 1] = 0
             & exists2 a, a \in Cint & beta = 1 - nu zeta + a *: sumSnu + Gamma]
    & (*b*) e (h - 1) / 2%:R
            '[(nu zeta)^\rho] 1 - e / h '[Gamma] e - 1
    & (*c*) {in irr G, chi, orthogonal calSnu [:: chi]
        [/\ {in A, chi^\rho =1 (fun _'[beta, chi])}
          & '[chi^\rho] = #|A|%:R / #|L|%:R × '[beta, chi] ^+ 2]}].

End Dade_seqIndC1.

The other results of the section are specific to groups of odd order.
Hypothesis oddG : odd #|G|.

We explicitly factor out several intermediate results from the proof of (7.9) that are reused throughout the proof (including in (7.10) below).

Import ssrint.
Lemma cfdot_real_vchar_even phi psi :
    phi \in 'Z[irr G] cfReal phipsi \in 'Z[irr G] cfReal psi
  (2 %| '[phi, psi])%C = (2 %| '[phi, 1])%C || (2 %| '[psi, 1])%C.

Section DisjointDadeOrtho.

Variables (L1 L2 H1 H2 : {group gT}).
Let A1 := H1^#.
Let A2 := H2^#.

Hypothesis ddA1 : Dade_hypothesis G L1 A1.
Hypothesis ddA2 : Dade_hypothesis G L2 A2.
Let Atau1 := Dade_support ddA1.
Let tau1 := Dade ddA1.
Let Atau2 := Dade_support ddA2.
Let tau2 := Dade ddA2.

Hypothesis disjointA : [disjoint Atau1 & Atau2].

Lemma disjoint_Dade_ortho phi psi : '[tau1 phi, tau2 psi] = 0.

Let odd_Dade_context L H : Dade_hypothesis G L H^#H <| L odd #|L|.

This lemma encapsulates most uses of lemma (4.1) in the rest of the proof.
Lemma disjoint_coherent_ortho P1 P2 nu1 nu2 i1 i2 :
    let S1 := seqIndD H1 L1 P1 1 in let S2 := seqIndD H2 L2 P2 1 in
    let chi1 := 'chi_i1 in let chi2 := 'chi_i2 in
    coherent_with S1 A1 tau1 nu1coherent_with S2 A2 tau2 nu2
    P1 \subset H1P2 \subset H2chi1 \in S1chi2 \in S2
  '[nu1 chi1, nu2 chi2] = 0.

This is Peterfalvi (7.9). We have inlined Hypothesis (7.4) because although it is readily available for the proof of (7.10), it would be inconvenient to establish in (14.4). Note that our Delta corresponds to Delta - 1 in the Peterfalvi proof.
Let beta L H ddA zeta := @Dade _ G L H^# ddA ('Ind[L, H] 1 - zeta).
Lemma Dade_sub_lin_nonorthogonal nu1 nu2 i1 i2 :
    let S1 := seqIndD H1 L1 H1 1 in let S2 := seqIndD H2 L2 H2 1 in
    coherent_with S1 A1 tau1 nu1coherent_with S2 A2 tau2 nu2
    let zeta1 := 'chi_i1 in let zeta2 := 'chi_i2 in
    zeta1 \in S1zeta1 1%g = #|L1 : H1|%:R
    zeta2 \in S2zeta2 1%g = #|L2 : H2|%:R
  '[beta ddA1 zeta1, nu2 zeta2] != 0 '[beta ddA2 zeta2, nu1 zeta1] != 0.

End DisjointDadeOrtho.

This final section factors the assumptions common to (7.10) and (7.11). We add solvability of the Frobenius groups, so as not to rely on the theorem of Thompson asserting the nilpotence of Frobenius kernels.

Section CoherentFrobeniusPartition.

Variables (k : nat) (L H E : 'I_k{group gT}).

Local Notation A i := (gval (H i))^#.
Let h_ i : algC := #|H i|%:R.
Let e_ i : algC := #|L i : H i|%:R.
Let G0 := G :\: \bigcup_(i < k) class_support (H i)^# G.

Hypothesis k_ge2: (k 2)%N.

a
Hypothesis frobeniusL_G :
   i, [/\ L i \subset G, solvable (L i) & [Frobenius L i = H i ><| E i]].

b
Hypothesis normedTI_A : i, normedTI (A i) G (L i).

c
Hypothesis card_coprime : i j, i != jcoprime #|H i| #|H j|.

A numerical fact that is used in both (7.10) and (7.11)
Let e_bounds i : 1 < e_ i e_ i (h_ i - 1) / 2%:R.

This is Peterfalvi (7.10).
Lemma coherent_Frobenius_bound : i, let e := e_ i in let h := h_ i in
  (e - 1) × ((h - 2%:R × e - 1) / (e × h) + 2%:R / (h × (h + 2%:R)))
      (#|G0|%:R - 1) / #|G|%:R.

This is Peterfalvi (7.11).