path: root/mathcomp/odd_order/PFsection4.v

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool ssrfun eqtype ssrnat seq path div choice.
From mathcomp
Require Import fintype tuple finfun bigop prime ssralg poly finset fingroup.
From mathcomp
Require Import morphism perm automorphism quotient action gfunctor gproduct.
From mathcomp
Require Import center commutator zmodp cyclic pgroup nilpotent hall frobenius.
From mathcomp
Require Import matrix mxalgebra mxrepresentation vector ssrnum algC classfun.
From mathcomp
Require Import character inertia vcharacter PFsection1 PFsection2 PFsection3.

(******************************************************************************)
(* This file covers Peterfalvi, Section 4: The Dade isometry of a certain     *)
(* type of subgroup.                                                          *)
(*   Given defW : W1 \x W2 = W, we define here:                               *)
(*  primeTI_hypothesis L K defW <->                                           *)
(*                   L = K ><| W1, where W1 acts in a prime manner on K (see  *)
(*                   semiprime in frobenius.v), and both W1 and W2 = 'C_K(W1) *)
(*                   are nontrivial and cyclic of odd order; these conditions *)
(*                   imply that cyclicTI_hypothesis L defW holds.             *)
(*  -> This is Peterfalvi, Hypothesis (4.2), or Feit-Thompson (13.2).         *)
(*  prime_Dade_definition L K H A A0 defW <->                                 *)
(*                   A0 = A :|: class_support (cyclicTIset defW) L where A is *)
(*                   an L-invariant subset of K^# containing all the elements *)
(*                   of K that do not act freely on H <| L; in addition       *)
(*                   W2 \subset H \subset K.                                  *)
(*  prime_Dade_hypothesis G L K H A A0 defW <->                               *)
(*                   The four assumptions primeTI_hypothesis L K defW,        *)
(*                   cyclicTI_hypothesis G defW, Dade_hypothesis G L A0 and   *)
(*                   prime_Dade_definition L K H A A0 defW hold jointly.      *)
(*  -> This is Peterfalvi, Hypothesis (4.6), or Feit-Thompson (13.3) (except  *)
(*     that H is not required to be nilpotent, and the "supporting groups"    *)
(*     assumptions have been replaced by Dade hypothesis).                    *)
(*  -> This hypothesis is one of the alternatives under which Sibley's        *)
(*     coherence theorem holds (see PFsection6.v), and is verified by all     *)
(*     maximal subgroups of type P in a minimal simple odd group.             *)
(*  -> prime_Dade_hypothesis coerces to Dade_hypothesis, cyclicTI_hypothesis, *)
(*     primeTI_hypothesis and prime_Dade_definition.                          *)
(* For ptiW : primeTI_hypothesis L K defW we also define:                     *)
(*  prime_cycTIhyp ptiW :: cyclicTI_hypothesis L defW (though NOT a coercion) *)
(*  primeTIirr ptiW i j == the (unique) irreducible constituent of the image  *)
(*   (locally) mu2_ i j    in 'CF(L) of w_ i j = cyclicTIirr defW i j under   *)
(*                         the sigma = cyclicTIiso (prime_cycTIhyp ptiW).     *)
(* primeTI_Iirr ptiW ij == the index of mu2_ ij.1 ij.2; indeed mu2_ i j is    *)
(*                         just notation for 'chi_(primeTI_Iirr ptiW (i, j)). *)
(*   primeTIsign ptiW j == the sign of mu2_ i j in sigma (w_ i j), which does *)
(*   (locally) delta_ j    not depend on i.                                   *)
(* primeTI_Isign ptiW j == the boolean b such that delta_ j := (-1) ^+ b.     *)
(*    primeTIres ptiW j == the restriction to K of mu2_ i j, which is an      *)
(*     (locally) chi_ j    irreducible character that does not depend on i.   *)
(*  primeTI_Ires ptiW j == the index of chi_ j := 'chi_(primeTI_Ires ptiW j). *)
(*    primeTIred ptiW j == the (reducible) character equal to the sum of all  *)
(*      (locally) mu_ j    the mu2_ i j, and also to 'Ind (chi_ j).           *)
(* uniform_prTIred_seq ptiW k == the sequence of all the mu_ j, j != 0, with  *)
(*                         the same degree as mu_ k (s.t. mu_ j 1 = mu_ k 1). *)
(******************************************************************************)

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

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

Section Four_1_to_2.

(* This is Peterfalvi (4.1). *)

Variable gT : finGroupType.

Lemma vchar_pairs_orthonormal (X : {group gT}) (a b c d : 'CF(X)) u v :
    {subset (a :: b) <= 'Z[irr X]} /\ {subset (c :: d) <= 'Z[irr X]} ->
    orthonormal (a :: b) && orthonormal (c :: d) ->
    [&& u \is Creal, v \is Creal, u != 0 & v != 0] ->
    [&& '[a - b, u *: c - v *: d] == 0,
         (a - b) 1%g == 0 & (u *: c - v *: d) 1%g == 0] ->
    orthonormal [:: a; b; c; d].
Proof.
have osym2 (e f : 'CF(X)) : orthonormal (e :: f) -> orthonormal (f :: e).
  by rewrite !(orthonormal_cat [::_] [::_]) orthogonal_sym andbCA.
have def_o f S: orthonormal (f :: S) -> '[f : 'CF(X)] = 1.
  by case/andP=> /andP[/eqP].
case=> /allP/and3P[Za Zb _] /allP/and3P[Zc Zd _] /andP[o_ab o_cd].
rewrite (orthonormal_cat (a :: b)) o_ab o_cd /=.
case/and4P=> r_u r_v nz_u nz_v /and3P[o_abcd ab1 cd1].
wlog suff: a b c d u v Za Zb Zc Zd o_ab o_cd r_u r_v nz_u nz_v o_abcd ab1 cd1 /
  '[a, c]_X == 0.
- move=> IH; rewrite /orthogonal /= !andbT (IH a b c d u v) //=.
  have vc_sym (e f : 'CF(X)) : ((e - f) 1%g == 0) = ((f - e) 1%g == 0).
    by rewrite -opprB cfunE oppr_eq0.
  have ab_sym e: ('[b - a, e] == 0) = ('[a - b, e] == 0).
    by rewrite -opprB cfdotNl oppr_eq0.
  rewrite (IH b a c d u v) // 1?osym2 1?vc_sym ?ab_sym //=.
  rewrite -oppr_eq0 -cfdotNr opprB in o_abcd.
  by rewrite (IH a b d c v u) ?(IH b a d c v u) // 1?osym2 1?vc_sym ?ab_sym.
apply: contraLR cd1 => nz_ac.
have [/orthonormal2P[ab0 a1 b1] /orthonormal2P[cd0 c1 d1]] := (o_ab, o_cd).
have [ea [ia def_a]] := vchar_norm1P Za a1.
have{nz_ac} [e defc]: exists e : bool, c = (-1) ^+ e *: a.
  have [ec [ic def_c]] := vchar_norm1P Zc c1; exists (ec (+) ea).
  move: nz_ac; rewrite def_a def_c scalerA; rewrite -signr_addb addbK.
  rewrite cfdotZl cfdotZr cfdot_irr mulrA mulrC mulf_eq0.
  by have [-> // | _]:= ia =P ic; rewrite eqxx.
have def_vbd: v * '[b, d]_X = - ((-1) ^+ e * u).
  apply/eqP; have:= o_abcd; rewrite cfdotDl cfdotNl !raddfB /=.
  rewrite defc !cfdotZr a1 (cfdotC b) ab0 rmorph0 mulr1.
  rewrite -[a]scale1r -{2}[1]/((-1) ^+ false) -(addbb e) signr_addb -scalerA.
  rewrite -defc cfdotZl cd0 !mulr0 opprK addrA !subr0 mulrC addrC addr_eq0.
  by rewrite rmorph_sign !conj_Creal.
have nz_bd: '[b, d] != 0.
  move/esym/eqP: def_vbd; apply: contraTneq => ->.
  by rewrite mulr0 oppr_eq0 mulf_eq0 signr_eq0.
have{nz_bd} defd: d = '[b, d] *: b.
  move: nz_bd; have [eb [ib ->]] := vchar_norm1P Zb b1.
  have [ed [id ->]] := vchar_norm1P Zd d1.
  rewrite scalerA cfdotZl cfdotZr rmorph_sign mulrA cfdot_irr.
  have [-> _ | _] := ib =P id; last by rewrite !mulr0 eqxx.
  by rewrite mulr1 mulrAC -!signr_addb addbb.
rewrite defd scalerA def_vbd scaleNr opprK defc scalerA mulrC -raddfD cfunE.
rewrite !mulf_neq0 ?signr_eq0 // -(subrK a b) -opprB addrCA 2!cfunE.
rewrite (eqP ab1) oppr0 add0r cfunE -mulr2n -mulr_natl mulf_eq0 pnatr_eq0.
by rewrite /= def_a cfunE mulf_eq0 signr_eq0 /= irr1_neq0.
Qed.

Corollary orthonormal_vchar_diff_ortho (X : {group gT}) (a b c d : 'CF(X)) :
    {subset a :: b <= 'Z[irr X]} /\ {subset c :: d <= 'Z[irr X]} ->
    orthonormal (a :: b) && orthonormal (c :: d) ->
    [&& '[a - b, c - d] == 0, (a - b) 1%g == 0 & (c - d) 1%g == 0] ->
  '[a, c] = 0.
Proof.
move=> Zabcd Oabcd; rewrite -[c - d]scale1r scalerBr.
move/(vchar_pairs_orthonormal Zabcd Oabcd) => /implyP.
rewrite rpred1 oner_eq0 (orthonormal_cat (a :: b)) /=.
by case/and3P=> _ _ /andP[] /andP[] /eqP.
Qed.

(* This is Peterfalvi, Hypothesis (4.2), with explicit parameters. *)
Definition primeTI_hypothesis (L K W W1 W2 : {set gT}) of W1 \x W2 = W :=
  [/\ (*a*) [/\ K ><| W1 = L, W1 != 1, Hall L W1 & cyclic W1],
      (*b*) [/\ W2 != 1, W2 \subset K & cyclic W2],
            {in W1^#, forall x, 'C_K[x] = W2}
   &  (*c*) odd #|W|]%g.

End Four_1_to_2.

Arguments Scope primeTI_hypothesis
  [_ group_scope group_scope group_scope _ group_scope group_scope].

Section Four_3_to_5.

Variables (gT : finGroupType) (L K W W1 W2 : {group gT}) (defW : W1 \x W2 = W).
Hypothesis ptiWL : primeTI_hypothesis L K defW.

Let V := cyclicTIset defW.
Let w1 := #|W1|.
Let w2 := #|W2|.

Let defL : K ><| W1 = L. Proof. by have [[]] := ptiWL. Qed.
Let ntW1 : W1 :!=: 1%g. Proof. by have [[]] := ptiWL. Qed.
Let cycW1 : cyclic W1. Proof. by have [[]] := ptiWL. Qed.
Let hallW1 : Hall L W1. Proof. by have [[]] := ptiWL. Qed.

Let ntW2 : W2 :!=: 1%g. Proof. by have [_ []] := ptiWL. Qed.
Let sW2K : W2 \subset K. Proof. by have [_ []] := ptiWL. Qed.
Let cycW2 : cyclic W2. Proof. by have [_ []] := ptiWL. Qed.
Let prKW1 : {in W1^#, forall x, 'C_K[x] = W2}. Proof. by have [] := ptiWL. Qed.

Let oddW : odd #|W|. Proof. by have [] := ptiWL. Qed.

Let nsKL : K <| L. Proof. by case/sdprod_context: defL. Qed.
Let sKL : K \subset L. Proof. by case/andP: nsKL. Qed.
Let sW1L : W1 \subset L. Proof. by case/sdprod_context: defL. Qed.
Let sWL : W \subset L.
Proof. by rewrite -(dprodWC defW) -(sdprodW defL) mulgSS. Qed.
Let sW1W : W1 \subset W. Proof. by have /mulG_sub[] := dprodW defW. Qed.
Let sW2W : W2 \subset W. Proof. by have /mulG_sub[] := dprodW defW. Qed.

Let coKW1 : coprime #|K| #|W1|.
Proof. by rewrite (coprime_sdprod_Hall_r defL). Qed.
Let coW12 : coprime #|W1| #|W2|.
Proof. by rewrite coprime_sym (coprimeSg sW2K). Qed.

Let cycW : cyclic W. Proof. by rewrite (cyclic_dprod defW). Qed.
Let cWW : abelian W. Proof. exact: cyclic_abelian. Qed.
Let oddW1 : odd w1. Proof. exact: oddSg oddW. Qed.
Let oddW2 : odd w2. Proof. exact: oddSg oddW. Qed.

Let ntV : V != set0.
Proof.
by rewrite -card_gt0 card_cycTIset muln_gt0 -!subn1 !subn_gt0 !cardG_gt1 ntW1.
Qed.

Let sV_V2 : V \subset W :\: W2. Proof. by rewrite setDS ?subsetUr. Qed.

Lemma primeTIhyp_quotient (M : {group gT}) :
    (W2 / M != 1)%g -> M \subset K -> M <| L ->
  {defWbar : (W1 / M) \x (W2 / M) = W / M
           & primeTI_hypothesis (L / M) (K / M) defWbar}%g.
Proof.
move=> ntW2bar sMK /andP[_ nML].
have coMW1: coprime #|M| #|W1| by rewrite (coprimeSg sMK).
have [nMW1 nMW] := (subset_trans sW1L nML, subset_trans sWL nML).
have defWbar: (W1 / M) \x (W2 / M) = (W / M)%g.
  by rewrite (quotient_coprime_dprod nMW) ?quotient_odd.
exists defWbar; split; rewrite ?quotient_odd ?quotient_cyclic ?quotientS //.
  have isoW1: W1 \isog W1 / M by rewrite quotient_isog ?coprime_TIg.
  by rewrite -(isog_eq1 isoW1) ?morphim_Hall // (quotient_coprime_sdprod nML).
move=> Kx /setD1P[ntKx /morphimP[x nKx W1x defKx]] /=.
rewrite -cent_cycle -cycle_eq1 {Kx}defKx -quotient_cycle // in ntKx *.
rewrite -strongest_coprime_quotient_cent ?cycle_subG //; first 1 last.
- by rewrite subIset ?sMK.
- by rewrite (coprimeSg (subsetIl M _)) // (coprimegS _ coMW1) ?cycle_subG.
- by rewrite orbC abelian_sol ?cycle_abelian.
rewrite cent_cycle prKW1 // !inE W1x (contraNneq _ ntKx) // => ->.
by rewrite cycle1 quotient1.
Qed.

(* This is the first part of PeterFalvi, Theorem (4.3)(a). *)
Theorem normedTI_prTIset : normedTI (W :\: W2) L W.
Proof.
have [[_ _ cW12 _] [_ _ nKW1 tiKW1]] := (dprodP defW, sdprodP defL).
have nV2W: W \subset 'N(W :\: W2) by rewrite sub_abelian_norm ?subsetDl.
have piW1_W: {in W1 & W2, forall x y, (x * y).`_\pi(W1) = x}.
  move=> x y W1x W2y /=; rewrite consttM /commute ?(centsP cW12 y) //.
  rewrite constt_p_elt ?(mem_p_elt _ W1x) ?pgroup_pi // (constt1P _) ?mulg1 //.
  by rewrite /p_elt -coprime_pi' // (coprimegS _ coW12) ?cycle_subG.
have nzV2W: W :\: W2 != set0 by apply: contraNneq ntV; rewrite -subset0 => <-.
apply/normedTI_memJ_P; split=> // xy g V2xy Lg.
apply/idP/idP=> [| /(subsetP nV2W)/memJ_norm->//].
have{xy V2xy} [/(mem_dprod defW)[x [y [W1x W2y -> _]]] W2'xy] := setDP V2xy.
have{W2'xy} ntx: x != 1%g by have:= W2'xy; rewrite groupMr // => /group1_contra.
have{g Lg} [k [w [Kk /(subsetP sW1W)Ww -> _]]] := mem_sdprod defL Lg.
rewrite conjgM memJ_norm ?(subsetP nV2W) ?(groupMr k) // => /setDP[Wxyk _].
have{Wxyk piW1_W} W1xk: x ^ k \in W1.
  have [xk [yk [W1xk W2yk Dxyk _]]] := mem_dprod defW Wxyk.
  by rewrite -(piW1_W x y) // -consttJ Dxyk piW1_W.
rewrite (subsetP sW2W) // -(@prKW1 x) ?in_setD1 ?ntx // inE Kk /=.
rewrite cent1C (sameP cent1P commgP) -in_set1 -set1gE -tiKW1 inE.
by rewrite (subsetP _ _ (mem_commg W1x Kk)) ?commg_subr // groupM ?groupV.
Qed.

(* Second part of PeterFalvi, Theorem (4.3)(a). *)
Theorem prime_cycTIhyp : cyclicTI_hypothesis L defW.
Proof.
have nVW: W \subset 'N(V) by rewrite sub_abelian_norm ?subsetDl.
by split=> //; apply: normedTI_S normedTI_prTIset.
Qed.
Local Notation ctiW := prime_cycTIhyp.
Let sigma := cyclicTIiso ctiW.
Let w_ i j := cyclicTIirr defW i j.

Let Wlin k : 'chi[W]_k \is a linear_char. Proof. exact/irr_cyclic_lin. Qed.
Let W1lin i : 'chi[W1]_i \is a linear_char. Proof. exact/irr_cyclic_lin. Qed.
Let W2lin i : 'chi[W2]_i \is a linear_char. Proof. exact/irr_cyclic_lin. Qed.
Let w_lin i j : w_ i j \is a linear_char. Proof. exact: Wlin. Qed.

Let nirrW1 : #|Iirr W1| = w1. Proof. exact: card_Iirr_cyclic. Qed.
Let nirrW2 : #|Iirr W2| = w2. Proof. exact: card_Iirr_cyclic. Qed.
Let NirrW1 : Nirr W1 = w1. Proof. by rewrite -nirrW1 card_ord. Qed.
Let NirrW2 : Nirr W2 = w2. Proof. by rewrite -nirrW2 card_ord. Qed.
Let w1gt1 : (1 < w1)%N. Proof. by rewrite cardG_gt1. Qed.

Let cfdot_w i1 j1 i2 j2 : '[w_ i1 j1, w_ i2 j2] = ((i1 == i2) && (j1 == j2))%:R.
Proof. exact: cfdot_dprod_irr. Qed.

(* Witnesses for Theorem (4.3)(b). *)
Fact primeTIdIirr_key : unit. Proof. by []. Qed.
Definition primeTIdIirr_def := dirr_dIirr (sigma \o prod_curry w_).
Definition primeTIdIirr := locked_with primeTIdIirr_key primeTIdIirr_def.
Definition primeTI_Iirr ij := (primeTIdIirr ij).2.
Definition primeTI_Isign j := (primeTIdIirr (0, j)).1.
Local Notation Imu2 := primeTI_Iirr.
Local Notation mu2_ i j := 'chi_(primeTI_Iirr (i, j)).
Local Notation delta_ j := (GRing.sign algCring (primeTI_Isign j)).

Let ew_ i j := w_ i j - w_ 0 j.
Let V2ew i j : ew_ i j \in 'CF(W, W :\: W2).
Proof.
apply/cfun_onP=> x; rewrite !inE negb_and negbK => /orP[W2x | /cfun0->//].
by rewrite -[x]mul1g !cfunE /w_ !dprod_IirrE !cfDprodE ?lin_char1 ?subrr.
Qed.

(* This is Peterfalvi, Theorem (4.3)(b, c). *)
Theorem primeTIirr_spec :
 [/\ (*b*) injective Imu2,
           forall i j, 'Ind (ew_ i j) = delta_ j *: (mu2_ i j - mu2_ 0 j),
           forall i j, sigma (w_ i j) = delta_ j *: mu2_ i j,
     (*c*) forall i j, {in W :\: W2, mu2_ i j =1 delta_ j *: w_ i j}
         & forall k, k \notin codom Imu2 -> {in W :\: W2, 'chi_k =1 \0}].
Proof.
have isoV2 := normedTI_isometry normedTI_prTIset (setDSS sWL (sub1G W2)).
have /fin_all_exists2[dmu injl_mu Ddmu] j:
  exists2 dmu : bool * {ffun Iirr W1 -> Iirr L}, injective dmu.2
    & forall i, 'Ind (ew_ i j) = dchi (dmu.1, dmu.2 i) - dchi (dmu.1, dmu.2 0).
- pose Sj := [tuple w_ i j | i < Nirr W1].
  have Sj0: Sj`_0 = w_ 0 j by rewrite (nth_mktuple _ 0 0).
  have irrSj: {subset Sj <= irr W} by move=> ? /mapP[i _ ->]; apply: mem_irr.
  have: {in 'Z[Sj, W :\: W2], isometry 'Ind, to 'Z[irr L, L^#]}.
    split=> [|phi]; first by apply: sub_in2 isoV2; apply: zchar_on.
    move/(zchar_subset irrSj)/(zchar_onS (setDS W (sub1G W2))).
    by rewrite !zcharD1E cfInd1 // mulf_eq0 orbC => /andP[/cfInd_vchar-> // ->].
  case/vchar_isometry_base=> // [|||i|mu Umu [d Ddmu]]; first by rewrite NirrW1.
  + rewrite orthonormal_free // (sub_orthonormal irrSj) ?irr_orthonormal //.
    by apply/injectiveP=> i1 i2 /irr_inj/dprod_Iirr_inj[].
  + by move=> _ /mapP[i _ ->]; rewrite Sj0 !lin_char1.
  + by rewrite nth_mktuple Sj0 V2ew.
  exists (d, [ffun i => tnth mu i]) => [|i].
    apply/injectiveP; congr (uniq _): Umu.
    by rewrite (eq_map (ffunE _)) map_tnth_enum.
  by rewrite -scalerBr /= !ffunE !(tnth_nth 0 mu) -Ddmu nth_mktuple Sj0.
pose Imu ij := (dmu ij.2).2 ij.1; pose mu i j := 'chi_(Imu (i, j)).
pose d j : algC := (-1) ^+ (dmu j).1.
have{Ddmu} Ddmu i j: 'Ind (ew_ i j) = d j *: (mu i j - mu 0 j).
  by rewrite Ddmu scalerBr.
have{injl_mu} inj_Imu: injective Imu.
  move=> [i1 j1] [i2 j2]; rewrite /Imu /=; pose S i j k := mu i j :: mu k j.
  have [-> /injl_mu-> // | j2'1 /eqP/negPf[] /=] := eqVneq j1 j2.
  apply/(can_inj oddb)/eqP; rewrite -eqC_nat -cfdot_irr -!/(mu _ _) mulr0n.
  have oIew_j12 i k: '['Ind[L] (ew_ i j1), 'Ind[L] (ew_ k j2)] = 0.
    by rewrite isoV2 // cfdotBl !cfdotBr !cfdot_w (negPf j2'1) !andbF !subr0.
  have defSd i j k: mu i j - mu k j = d j *: ('Ind (ew_ i j) - 'Ind (ew_ k j)).
    by rewrite !Ddmu -scalerBr signrZK opprB addrA subrK.
  have Sd1 i j k: (mu i j - mu k j) 1%g == 0.
    by rewrite defSd !(cfunE, cfInd1) ?lin_char1 // !subrr mulr0.
  have exS i j: {k | {subset S i j k <= 'Z[irr L]} & orthonormal (S i j k)}.
    have:= w1gt1; rewrite -nirrW1 (cardD1 i) => /card_gt0P/sigW[k /andP[i'k _]].
    exists k; first by apply/allP; rewrite /= !irr_vchar.
    apply/andP; rewrite /= !cfdot_irr !eqxx !andbT /=.
    by rewrite (inj_eq (injl_mu j)) mulrb ifN_eqC.
  have [[k1 ZS1 o1S1] [k2 ZS2 o1S2]] := (exS i1 j1, exS i2 j2).
  rewrite (orthonormal_vchar_diff_ortho (conj ZS1 ZS2)) ?o1S1 ?Sd1 ?andbT //.
  by rewrite !defSd cfdotZl cfdotZr cfdotBl !cfdotBr !oIew_j12 !subrr !mulr0.
pose V2base := [tuple of [seq ew_ ij.1 ij.2 | ij in predX (predC1 0) predT]].
have V2basis: basis_of 'CF(W, W :\: W2) V2base.
  suffices V2free: free V2base.
    rewrite basisEfree V2free size_image /= cardX cardC1 nirrW1 nirrW2 -subn1.
    rewrite mulnBl mul1n dim_cfun_on_abelian ?subsetDl //.
    rewrite cardsD (setIidPr _) //  (dprod_card defW) leqnn andbT.
    by apply/span_subvP=> _ /mapP[ij _ ->].
  apply/freeP=> /= z zV2e0 k.
  move Dk: (enum_val k) (enum_valP k) => [i j] /andP[/= nz_i _].
  rewrite -(cfdot0l (w_ i j)) -{}zV2e0 cfdot_suml (bigD1 k) //= cfdotZl.
  rewrite nth_image Dk cfdotBl !cfdot_w !eqxx eq_sym (negPf nz_i) subr0 mulr1.
  rewrite big1 ?addr0 // => k1; rewrite -(inj_eq enum_val_inj) {}Dk nth_image.
  case: (enum_val k1) => /= i1 j1 ij'ij1.
  rewrite cfdotZl cfdotBl !cfdot_dprod_irr [_ && _](negPf ij'ij1).
  by rewrite eq_sym (negPf nz_i) subr0 mulr0.
have nsV2W: W :\: W2 <| W by rewrite -sub_abelian_normal ?subsetDl.
pose muW k := let: ij := inv_dprod_Iirr defW k in d ij.2 *: mu ij.1 ij.2.
have inW := codomP (dprod_Iirr_onto defW _).
have ImuW k1 k2: '[muW k1, muW k2] = (k1 == k2)%:R.
  have [[[i1 j1] -> {k1}] [[i2 j2] -> {k2}]] := (inW k1, inW k2).
  rewrite cfdotZl cfdotZr !dprod_IirrK (can_eq (dprod_IirrK _)) /= rmorph_sign.
  rewrite cfdot_irr (inj_eq inj_Imu (_, _) (_, _)) -/(d _).
  by case: eqP => [[_ ->] | _]; rewrite ?signrMK ?mulr0.
have [k|muV2 mu'V2] := equiv_restrict_compl_ortho sWL nsV2W V2basis ImuW.
  rewrite nth_image; case: (enum_val k) (enum_valP k) => /= i j /andP[/= nzi _].
  pose inWj i1 := dprod_Iirr defW (i1, j); rewrite (bigD1 (inWj 0)) //=.
  rewrite (bigD1 (inWj i)) ?(can_eq (dprod_IirrK _)) ?xpair_eqE ?(negPf nzi) //.
  rewrite /= big1 ?addr0 => [|k1 /andP[]]; last first.
    rewrite !(eq_sym k1); have [[i1 j1] -> {k1}] := inW k1.
    rewrite !(can_eq (dprod_IirrK _)) => ij1'i ij1'0.
    by rewrite cfdotBl !cfdot_w !mulrb !ifN // subrr scale0r.
  rewrite /muW !dprod_IirrK /= addrC !cfdotBl !cfdot_w !eqxx /= !andbT.
  by rewrite eq_sym (negPf nzi) subr0 add0r scaleNr !scale1r -scalerBr.
have Dsigma i j: sigma (w_ i j) = d j *: mu i j.
  apply/esym/eq_in_cycTIiso=> [|x Vx]; first exact: (dirr_dchi (_, _)).
  by rewrite -muV2 ?(subsetP sV_V2) // /muW dprod_IirrK.
have /all_and2[Dd Dmu] j: d j = delta_ j /\ forall i, Imu (i, j) = Imu2 (i, j).
  suffices DprTI i: primeTIdIirr (i, j) = ((dmu j).1, (dmu j).2 i).
    by split=> [|i]; rewrite /primeTI_Isign /Imu2 DprTI.
  apply: dirr_inj; rewrite /primeTIdIirr unlock_with dirr_dIirrE /= ?Dsigma //.
  by case=> i1 j1; apply: cycTIiso_dirr.
split=> [[i1 j1] [i2 j2] | i j | i j | i j x V2x | k mu2p'k].
- by rewrite -!Dmu => /inj_Imu.
- by rewrite -!Dmu -Dd -Ddmu.
- by rewrite -Dmu -Dd -Dsigma.
- by rewrite cfunE -muV2 // /muW dprod_IirrK Dd cfunE signrMK -Dmu.
apply: mu'V2 => k1; have [[i j] ->{k1}] := inW k1.
apply: contraNeq mu2p'k; rewrite cfdotZr rmorph_sign mulf_eq0 signr_eq0 /=.
rewrite /mu Dmu dprod_IirrK -irr_consttE constt_irr inE /= => /eqP <-.
exact: codom_f.
Qed.

(* These lemmas restate the various parts of Theorem (4.3)(b, c) separately. *)
Lemma prTIirr_inj : injective Imu2. Proof. by case: primeTIirr_spec. Qed.

Corollary cfdot_prTIirr i1 j1 i2 j2 :
  '[mu2_ i1 j1, mu2_ i2 j2] = ((i1 == i2) && (j1 == j2))%:R.
Proof. by rewrite cfdot_irr (inj_eq prTIirr_inj). Qed.

Lemma cfInd_sub_prTIirr i j :
  'Ind[L] (w_ i j - w_ 0 j) = delta_ j *: (mu2_ i j - mu2_ 0 j).
Proof. by case: primeTIirr_spec i j. Qed.

Lemma cycTIiso_prTIirr i j : sigma (w_ i j) = delta_ j *: mu2_ i j.
Proof. by case: primeTIirr_spec. Qed.

Lemma prTIirr_id i j : {in W :\: W2, mu2_ i j =1 delta_ j *: w_ i j}.
Proof. by case: primeTIirr_spec. Qed.

Lemma not_prTIirr_vanish k : k \notin codom Imu2 -> {in W :\: W2, 'chi_k =1 \0}.
Proof. by case: primeTIirr_spec k. Qed.

(* This is Peterfalvi, Theorem (4.3)(d). *)
Theorem prTIirr1_mod i j : (mu2_ i j 1%g == delta_ j %[mod w1])%C.
Proof.
rewrite -(cfRes1 W1) -['Res _](subrK ('Res (delta_ j *: w_ i j))) cfunE.
set phi := _ - _; pose a := '[phi, 1].
have phi_on_1: phi \in 'CF(W1, 1%g).
  apply/cfun_onP=> g; have [W1g | /cfun0-> //] := boolP (g \in W1).
  rewrite -(coprime_TIg coW12) inE W1g !cfunE !cfResE //= => W2'g.
  by rewrite prTIirr_id ?cfunE ?subrr // inE W2'g (subsetP sW1W).
have{phi_on_1} ->: phi 1%g = a * w1%:R.
  rewrite mulrC /a (cfdotEl _ phi_on_1) mulVKf ?neq0CG //.
  by rewrite big_set1 cfun11 conjC1 mulr1.
rewrite cfResE // cfunE lin_char1 // mulr1 eqCmod_addl_mul //.
by rewrite Cint_cfdot_vchar ?rpred1 ?rpredB ?cfRes_vchar ?rpredZsign ?irr_vchar.
Qed.

Lemma prTIsign_aut u j : delta_ (aut_Iirr u j) = delta_ j.
Proof.
have /eqP := cfAut_cycTIiso ctiW u (w_ 0 j).
rewrite -cycTIirr_aut aut_Iirr0 -/sigma !cycTIiso_prTIirr raddfZsign /=.
by rewrite -aut_IirrE eq_scaled_irr => /andP[/eqP].
Qed.

Lemma prTIirr_aut u i j :
  mu2_ (aut_Iirr u i) (aut_Iirr u j) = cfAut u (mu2_ i j).
Proof.
rewrite -!(canLR (signrZK _) (cycTIiso_prTIirr _ _)) -!/(delta_ _).
by rewrite prTIsign_aut raddfZsign /= cfAut_cycTIiso -cycTIirr_aut.
Qed.

(* The (reducible) column sums of the prime TI irreducibles. *)
Definition primeTIred j : 'CF(L) := \sum_i mu2_ i j.
Local Notation mu_ := primeTIred.

Definition uniform_prTIred_seq j0 :=
  image mu_ [pred j | j != 0 & mu_ j 1%g == mu_ j0 1%g].

Lemma prTIred_aut u j : mu_ (aut_Iirr u j) = cfAut u (mu_ j).
Proof.
rewrite raddf_sum [mu_ _](reindex_inj (aut_Iirr_inj u)).
by apply: eq_bigr => i _; rewrite /= prTIirr_aut.
Qed.

Lemma cfdot_prTIirr_red i j k : '[mu2_ i j, mu_ k] = (j == k)%:R.
Proof.
rewrite cfdot_sumr (bigD1 i) // cfdot_prTIirr eqxx /=.
rewrite big1 ?addr0 // => i1 neq_i1i.
by rewrite cfdot_prTIirr eq_sym (negPf neq_i1i).
Qed.

Lemma cfdot_prTIred j1 j2 : '[mu_ j1, mu_ j2] = ((j1 == j2) * w1)%:R.
Proof.
rewrite cfdot_suml (eq_bigr _ (fun i _ => cfdot_prTIirr_red i _ _)) sumr_const.
by rewrite mulrnA card_Iirr_cyclic.
Qed.

Lemma cfnorm_prTIred j : '[mu_ j] = w1%:R.
Proof. by rewrite cfdot_prTIred eqxx mul1n. Qed.

Lemma prTIred_neq0 j : mu_ j != 0.
Proof. by rewrite -cfnorm_eq0 cfnorm_prTIred neq0CG. Qed.

Lemma prTIred_char j : mu_ j \is a character.
Proof. by apply: rpred_sum => i _; apply: irr_char. Qed.

Lemma prTIred_1_gt0 j : 0 < mu_ j 1%g.
Proof. by rewrite char1_gt0 ?prTIred_neq0 ?prTIred_char. Qed.

Lemma prTIred_1_neq0 i : mu_ i 1%g != 0.
Proof. by rewrite char1_eq0 ?prTIred_neq0 ?prTIred_char. Qed.

Lemma prTIred_inj : injective mu_.
Proof.
move=> j1 j2 /(congr1 (cfdot (mu_ j1)))/esym/eqP; rewrite !cfdot_prTIred.
by rewrite eqC_nat eqn_pmul2r ?cardG_gt0 // eqxx; case: (j1 =P j2).
Qed.

Lemma prTIred_not_real j : j != 0 -> ~~ cfReal (mu_ j).
Proof.
apply: contraNneq; rewrite -prTIred_aut -irr_eq1 -odd_eq_conj_irr1 //.
by rewrite -aut_IirrE => /prTIred_inj->.
Qed.

Lemma prTIsign0 : delta_ 0 = 1.
Proof.
have /esym/eqP := cycTIiso_prTIirr 0 0; rewrite -[sigma _]scale1r.
by rewrite /w_ /sigma cycTIirr00 cycTIiso1 -irr0 eq_scaled_irr => /andP[/eqP].
Qed.

Lemma prTIirr00 : mu2_ 0 0 = 1.
Proof.
have:= cycTIiso_prTIirr 0 0; rewrite prTIsign0 scale1r.
by rewrite /w_ /sigma cycTIirr00 cycTIiso1.
Qed.

(* This is PeterFalvi (4.4). *)
Lemma prTIirr0P k :
  reflect (exists i, 'chi_k = mu2_ i 0) (K \subset cfker 'chi_k).
Proof.
suff{k}: [set k | K \subset cfker 'chi_k] == [set Imu2 (i, 0) | i : Iirr W1].
  move/eqP/setP/(_ k); rewrite inE => ->.
  by apply: (iffP imsetP) => [[i _]|[i /irr_inj]] ->; exists i.
have [isoW1 abW1] := (sdprod_isog defL, cyclic_abelian cycW1).
have abLbar: abelian (L / K) by rewrite -(isog_abelian isoW1).
rewrite eqEcard andbC card_imset ?nirrW1 => [| i1 i2 /prTIirr_inj[] //].
rewrite [w1](card_isog isoW1) -card_Iirr_abelian //.
rewrite -(card_image (can_inj (mod_IirrK nsKL))) subset_leq_card; last first.
  by apply/subsetP=> _ /imageP[k1 _ ->]; rewrite inE mod_IirrE ?cfker_mod.
apply/subsetP=> k; rewrite inE => kerKk.
have /irrP[ij DkW]: 'Res 'chi_k \in irr W.
  rewrite lin_char_irr ?cfRes_lin_char // lin_irr_der1.
  by apply: subset_trans kerKk; rewrite der1_min ?normal_norm.
have{ij DkW} [i DkW]: exists i, 'Res 'chi_k = w_ i 0.
  have /codomP[[i j] Dij] := dprod_Iirr_onto defW ij; exists i.
  rewrite DkW Dij; congr (w_ i _); apply/eqP; rewrite -subGcfker.
  rewrite -['chi_j](cfDprodKr_abelian defW i) // -dprod_IirrE -{}Dij -{}DkW.
  by rewrite cfResRes // sub_cfker_Res // (subset_trans sW2K kerKk).
apply/imsetP; exists i => //=; apply/irr_inj.
suffices ->: 'chi_k = delta_ 0 *: mu2_ i 0 by rewrite prTIsign0 scale1r.
rewrite -cycTIiso_prTIirr -(eq_in_cycTIiso _ (irr_dirr k)) // => x /setDP[Wx _].
by rewrite -/(w_ i 0) -DkW cfResE.
Qed.

(* This is the first part of PeterFalvi, Theorem (4.5)(a). *)
Theorem cfRes_prTIirr_eq0 i j : 'Res[K] (mu2_ i j) = 'Res (mu2_ 0 j).
Proof.
apply/eqP; rewrite -subr_eq0 -rmorphB /=; apply/eqP/cfun_inP=> x0 Kx0.
rewrite -(canLR (signrZK _) (cfInd_sub_prTIirr i j)) -/(delta_ j).
rewrite cfResE // !cfunE (cfun_on0 (cfInd_on _ (V2ew i j))) ?mulr0 //.
apply: contraL Kx0 => /imset2P[x y /setDP[Wx W2'x] Ly ->] {x0}.
rewrite memJ_norm ?(subsetP (normal_norm nsKL)) //; apply: contra W2'x => Kx.
by rewrite -(mul1g W2) -(coprime_TIg coKW1) group_modr // inE Kx (dprodW defW).
Qed.

Lemma prTIirr_1 i j : mu2_ i j 1%g = mu2_ 0 j 1%g.
Proof. by rewrite -!(@cfRes1 _ K L) cfRes_prTIirr_eq0. Qed.

Lemma prTIirr0_1 i : mu2_ i 0 1%g = 1.
Proof. by rewrite prTIirr_1 prTIirr00 cfun11. Qed.

Lemma prTIirr0_linear i : mu2_ i 0 \is a linear_char.
Proof. by rewrite qualifE irr_char /= prTIirr0_1. Qed.

Lemma prTIred_1 j : mu_ j 1%g = w1%:R * mu2_ 0 j 1%g.
Proof.
rewrite mulr_natl -nirrW1 sum_cfunE.
by rewrite -sumr_const; apply: eq_bigr => i _; rewrite prTIirr_1.
Qed.

Definition primeTI_Ires j : Iirr K := cfIirr ('Res[K] (mu2_ 0 j)).
Local Notation Ichi := primeTI_Ires.
Local Notation chi_ j := 'chi_(Ichi j).

(* This is the rest of PeterFalvi, Theorem (4.5)(a). *)
Theorem prTIres_spec j : chi_ j = 'Res (mu2_ 0 j) /\ mu_ j = 'Ind (chi_ j).
Proof.
rewrite /Ichi; set chi_j := 'Res _.
have [k chi_j_k]: {k | k \in irr_constt chi_j} := constt_cfRes_irr K _.
have Nchi_j: chi_j \is a character by rewrite cfRes_char ?irr_char.
have lb_mu_1: w1%:R * 'chi_k 1%g <= mu_ j 1%g ?= iff (chi_j == 'chi_k).
  have [chi' Nchi' Dchi_j] := constt_charP _ Nchi_j chi_j_k.
  rewrite prTIred_1 (mono_lerif (ler_pmul2l (gt0CG W1))).
  rewrite -subr_eq0 Dchi_j addrC addKr -(canLR (addrK _) Dchi_j) !cfunE.
  rewrite lerif_subLR addrC -lerif_subLR cfRes1 subrr -char1_eq0 // eq_sym.
  by apply: lerif_eq; rewrite char1_ge0.
pose psi := 'Ind 'chi_k - mu_ j; have Npsi: psi \is a character.
  apply/forallP=> l; rewrite coord_cfdot cfdotBl; set a := '['Ind _, _].
  have Na: a \in Cnat by rewrite Cnat_cfdot_char_irr ?cfInd_char ?irr_char.
  have [[i /eqP Dl] | ] := altP (@existsP _ (fun i => 'chi_l == mu2_ i j)).
    have [n Da] := CnatP a Na; rewrite Da cfdotC Dl cfdot_prTIirr_red.
    rewrite rmorph_nat -natrB ?Cnat_nat // eqxx lt0n -eqC_nat -Da.
    by rewrite -irr_consttE constt_Ind_Res Dl cfRes_prTIirr_eq0.
  rewrite negb_exists => /forallP muj'l.
  rewrite cfdot_suml big1 ?subr0 // => i _.
  rewrite cfdot_irr -(inj_eq irr_inj) mulrb ifN_eqC ?muj'l //.
have ub_mu_1: mu_ j 1%g <= 'Ind[L] 'chi_k 1%g ?= iff ('Ind 'chi_k == mu_ j).
  rewrite -subr_eq0 -/psi (canRL (subrK _) (erefl psi)) cfunE -lerif_subLR.
  by rewrite subrr -char1_eq0 // eq_sym; apply: lerif_eq; rewrite char1_ge0.
have [_ /esym] := lerif_trans lb_mu_1 ub_mu_1; rewrite cfInd1 //.
by rewrite -(index_sdprod defL) eqxx => /andP[/eqP-> /eqP <-]; rewrite irrK.
Qed.

Lemma cfRes_prTIirr i j : 'Res[K] (mu2_ i j) = chi_ j.
Proof. by rewrite cfRes_prTIirr_eq0; case: (prTIres_spec j). Qed.

Lemma cfInd_prTIres j : 'Ind[L] (chi_ j) = mu_ j.
Proof. by have [] := prTIres_spec j. Qed.

Lemma cfRes_prTIred j : 'Res[K] (mu_ j) = w1%:R *: chi_ j.
Proof.
rewrite -nirrW1 scaler_nat -sumr_const linear_sum /=; apply: eq_bigr => i _.
exact: cfRes_prTIirr.
Qed.

Lemma prTIres_aut u j : chi_ (aut_Iirr u j) = cfAut u (chi_ j).
Proof.
by rewrite -(cfRes_prTIirr (aut_Iirr u 0)) prTIirr_aut -cfAutRes cfRes_prTIirr.
Qed.

Lemma prTIres0 : chi_ 0 = 1.
Proof. by rewrite -(cfRes_prTIirr 0) prTIirr00 cfRes_cfun1. Qed.

Lemma prTIred0 : mu_ 0 = w1%:R *: '1_K.
Proof.
by rewrite -cfInd_prTIres prTIres0 cfInd_cfun1 // -(index_sdprod defL).
Qed.

Lemma prTIres_inj : injective Ichi.
Proof. by move=> j1 j2 Dj; apply: prTIred_inj; rewrite -!cfInd_prTIres Dj. Qed.

(* This is the first assertion of Peterfalvi (4.5)(b). *)
Theorem prTIres_irr_cases k (theta := 'chi_k) (phi := 'Ind theta) :
  {j | theta = chi_ j} + {phi \in irr L /\ (forall i j, phi != mu2_ i j)}.
Proof.
pose imIchi := [set Ichi j | j : Iirr W2].
have [/imsetP/sig2_eqW[j _] | imIchi'k] := boolP (k \in imIchi).
  by rewrite /theta => ->; left; exists j.
suffices{phi} theta_inv: 'I_L[theta] = K.
  have irr_phi: phi \in irr L by apply: inertia_Ind_irr; rewrite ?theta_inv.
  right; split=> // i j; apply: contraNneq imIchi'k => Dphi; apply/imsetP.
  exists j => //; apply/eqP; rewrite -[k == _]constt_irr -(cfRes_prTIirr i).
  by rewrite -constt_Ind_Res -/phi Dphi irr_consttE cfnorm_irr oner_eq0.
rewrite -(sdprodW (sdprod_modl defL (sub_inertia _))); apply/mulGidPl.
apply/subsetP=> z /setIP[W1z Itheta_z]; apply: contraR imIchi'k => K'z.
have{K'z} [Lz ntz] := (subsetP sW1L z W1z, group1_contra K'z : z != 1%g).
have [p p_pr p_z]: {p | prime p & p %| #[z]} by apply/pdivP; rewrite order_gt1.
have coKp := coprime_dvdr (dvdn_trans p_z (order_dvdG W1z)) coKW1.
wlog{p_z} p_z: z W1z Lz Itheta_z ntz / p.-elt z.
  move/(_ z.`_p)->; rewrite ?groupX ?p_elt_constt //.
  by rewrite (sameP eqP constt1P) /p_elt p'natE ?negbK.
have JirrP: is_action L (@conjg_Iirr gT K); last pose Jirr := Action JirrP.
  split=> [y k1 k2 eq_k12 | k1 y1 y2 Gy1 Gy2]; apply/irr_inj.
    by apply/(can_inj (cfConjgK y)); rewrite -!conjg_IirrE eq_k12.
  by rewrite !conjg_IirrE (cfConjgM _ nsKL).
have [[_ nKL] [nKz _]] := (andP nsKL, setIdP Itheta_z).
suffices{k theta Itheta_z} /eqP->: imIchi == 'Fix_Jirr[z].
  by apply/afix1P/irr_inj; rewrite conjg_IirrE inertiaJ.
rewrite eqEcard; apply/andP; split.
  apply/subsetP=> _ /imsetP[j _ ->]; apply/afix1P/irr_inj.
  by rewrite conjg_IirrE -(cfRes_prTIirr 0) (cfConjgRes _ _ nsKL) ?cfConjg_id.
have ->: #|imIchi| = w2 by rewrite card_imset //; apply: prTIres_inj.
have actsL_KK: [acts L, on classes K | 'Js \ subsetT L].
  rewrite astabs_ract subsetIidl; apply/subsetP=> y Ly; rewrite !inE /=.
  apply/subsetP=> _ /imsetP[x Kx ->]; rewrite !inE /= -class_rcoset.
  by rewrite norm_rlcoset ?class_lcoset ?mem_classes ?memJ_norm ?(subsetP nKL).
rewrite (card_afix_irr_classes Lz actsL_KK) => [|k x y Kx /=]; last first.
  by case/imsetP=> _ /imsetP[t Kt ->] ->; rewrite conjg_IirrE cfConjgEJ ?cfunJ.
apply: leq_trans (subset_leq_card _) (leq_imset_card (class^~ K) _).
apply/subsetP=> _ /setIP[/imsetP[x Kx ->] /afix1P/normP nxKz].
suffices{Kx} /pred0Pn[t /setIP[xKt czt]]: #|'C_(x ^: K)[z]| != 0%N.
  rewrite -(class_eqP xKt); apply: mem_imset; have [y Ky Dt] := imsetP xKt.
  by rewrite -(@prKW1 z) ?(czt, inE) ?ntz // Dt groupJ.
have{coKp}: ~~ (p %| #|K|) by rewrite -prime_coprime // coprime_sym.
apply: contraNneq => /(congr1 (modn^~ p))/eqP; rewrite mod0n.
rewrite -cent_cycle -afixJ -sylow.pgroup_fix_mod ?astabsJ ?cycle_subG //.
by move/dvdn_trans; apply; rewrite -index_cent1 dvdn_indexg.
Qed.

(* Implicit elementary converse to the above. *)
Lemma prTIred_not_irr j : mu_ j \notin irr L.
Proof. by rewrite irrEchar cfnorm_prTIred pnatr_eq1 gtn_eqF ?andbF. Qed.

(* This is the second assertion of Peterfalvi (4.5)(b). *)
Theorem prTIind_irr_cases ell (phi := 'chi_ell) :
   {i : _ & {j | phi = mu2_ i j}}
     + {k | k \notin codom Ichi & phi = 'Ind 'chi_k}.
Proof.
have [k] := constt_cfRes_irr K ell; rewrite -constt_Ind_Res => kLell.
have [[j Dk] | [/irrP/sig_eqW[l1 DkL] chi'k]] := prTIres_irr_cases k.
  have [i /=/eqP <- | mu2j'l] := pickP (fun i => mu2_ i j == phi).
    by left; exists i, j.
  case/eqP: kLell; rewrite Dk cfInd_prTIres cfdot_suml big1 // => i _.
  by rewrite cfdot_irr -(inj_eq irr_inj) mu2j'l.
right; exists k; last by move: kLell; rewrite DkL constt_irr inE => /eqP <-.
apply/codomP=> [[j Dk]]; have/negP[] := prTIred_not_irr j.
by rewrite -cfInd_prTIres -Dk DkL mem_irr.
Qed.

End Four_3_to_5.

Notation primeTIsign ptiW j :=
  (GRing.sign algCring (primeTI_Isign ptiW j)) (only parsing).
Notation primeTIirr ptiW i j := 'chi_(primeTI_Iirr ptiW (i, j)) (only parsing).
Notation primeTIres ptiW j := 'chi_(primeTI_Ires ptiW j) (only parsing).

Arguments prTIirr_inj [gT L K W W1 W2 defW] ptiWL [x1 x2].
Arguments prTIred_inj [gT L K W W1 W2 defW] ptiWL [x1 x2].
Arguments prTIres_inj [gT L K W W1 W2 defW] ptiWL [x1 x2].
Arguments not_prTIirr_vanish [gT L K W W1 W2 defW] ptiWL [k].

Section Four_6_t0_10.

Variables (gT : finGroupType) (G L K H : {group gT}) (A A0 : {set gT}).
Variables (W W1 W2 : {group gT}) (defW : W1 \x W2 = W).

Local Notation V := (cyclicTIset defW).

(* These correspond to Peterfalvi, Hypothesis (4.6). *)
Definition prime_Dade_definition :=
  [/\ (*c*) [/\ H <| L, W2 \subset H & H \subset K],
      (*d*) [/\ A <| L, \bigcup_(h in H^#) 'C_K[h]^# \subset A & A \subset K^#]
    & (*e*) A0 = A :|: class_support V L].
 
Record prime_Dade_hypothesis : Prop := PrimeDadeHypothesis {
  prDade_cycTI :> cyclicTI_hypothesis G defW;
  prDade_prTI  :> primeTI_hypothesis L K defW;
  prDade_hyp   :> Dade_hypothesis G L A0;
  prDade_def   :> prime_Dade_definition
}.

Hypothesis prDadeHyp : prime_Dade_hypothesis.

Let ctiWG : cyclicTI_hypothesis G defW := prDadeHyp.
Let ptiWL : primeTI_hypothesis L K defW := prDadeHyp.
Let ctiWL : cyclicTI_hypothesis L defW := prime_cycTIhyp ptiWL.
Let ddA0 : Dade_hypothesis G L A0 := prDadeHyp.
Local Notation ddA0def := (prDade_def prDadeHyp).

Local Notation w_ i j := (cyclicTIirr defW i j).
Local Notation sigma := (cyclicTIiso ctiWG).
Local Notation eta_ i j := (sigma (w_ i j)).
Local Notation mu2_ i j := (primeTIirr ptiWL i j).
Local Notation delta_ j := (primeTIsign ptiWL j).
Local Notation chi_ j := (primeTIres ptiWL j).
Local Notation mu_ := (primeTIred ptiWL).
Local Notation tau := (Dade ddA0).

Let defA0 : A0 = A :|: class_support V L. Proof. by have [] := ddA0def. Qed.
Let nsAL : A <| L. Proof. by have [_ []] := ddA0def. Qed.
Let sAA0 : A \subset A0. Proof. by rewrite defA0 subsetUl. Qed.

Let nsHL : H <| L. Proof. by have [[]] := ddA0def. Qed.
Let sHK : H \subset K. Proof. by have [[]] := ddA0def. Qed.
Let defL : K ><| W1 = L. Proof. by have [[]] := ptiWL. Qed.
Let sKL : K \subset L. Proof. by have /mulG_sub[] := sdprodW defL. Qed.
Let coKW1 : coprime #|K| #|W1|.
Proof. by rewrite (coprime_sdprod_Hall_r defL); have [[]] := ptiWL. Qed.

Let sIH_A : \bigcup_(h in H^#) 'C_K[h]^# \subset A.
Proof. by have [_ []] := ddA0def. Qed.

Let sW2H : W2 \subset H. Proof. by have [[]] := ddA0def. Qed.
Let ntW1 : W1 :!=: 1%g. Proof. by have [[]] := ptiWL. Qed.
Let ntW2 : W2 :!=: 1%g. Proof. by have [_ []] := ptiWL. Qed.

Let oddW : odd #|W|. Proof. by have [] := ctiWL. Qed.
Let sW1W : W1 \subset W. Proof. by have /mulG_sub[] := dprodW defW. Qed.
Let sW2W : W2 \subset W. Proof. by have /mulG_sub[] := dprodW defW. Qed.
Let tiW12 : W1 :&: W2 = 1%g. Proof. by have [] := dprodP defW. Qed.

Let cycW : cyclic W. Proof. by have [] := ctiWG. Qed.
Let cycW1 : cyclic W1. Proof. by have [[]] := ptiWL. Qed.
Let cycW2 : cyclic W2. Proof. by have [_ []] := ptiWL. Qed.
Let sLG : L \subset G. Proof. by case: ddA0. Qed.
Let sW2K : W2 \subset K. Proof. by have [_ []] := ptiWL. Qed.

Let sWL : W \subset L.
Proof. by rewrite -(dprodWC defW) -(sdprodW defL) mulgSS. Qed.
Let sWG : W \subset G. Proof. exact: subset_trans sWL sLG. Qed.

Let oddW1 : odd #|W1|. Proof. exact: oddSg oddW. Qed.
Let oddW2 : odd #|W2|. Proof. exact: oddSg oddW. Qed.

Let w1gt1 : (2 < #|W1|)%N. Proof. by rewrite odd_gt2 ?cardG_gt1. Qed.
Let w2gt2 : (2 < #|W2|)%N. Proof. by rewrite odd_gt2 ?cardG_gt1. Qed.

Let nirrW1 : #|Iirr W1| = #|W1|. Proof. exact: card_Iirr_cyclic. Qed.
Let nirrW2 : #|Iirr W2| = #|W2|. Proof. exact: card_Iirr_cyclic. Qed.
Let W1lin i : 'chi[W1]_i \is a linear_char. Proof. exact/irr_cyclic_lin. Qed.
Let W2lin i : 'chi[W2]_i \is a linear_char. Proof. exact/irr_cyclic_lin. Qed.
 
(* This is the first part of Peterfalvi (4.7). *) 
Lemma prDade_irr_on k : 
   ~~ (H \subset cfker 'chi[K]_k) -> 'chi_k \in 'CF(K, 1%g |: A).
Proof.
move=> kerH'i; apply/cfun_onP=> g; rewrite !inE => /norP[ntg A'g].
have [Kg | /cfun0-> //] := boolP (g \in K).
apply: irr_reg_off_ker_0 (normalS _ _ nsHL) kerH'i _ => //.
apply/trivgP/subsetP=> h /setIP[Hh cgh]; apply: contraR A'g => nth.
apply/(subsetP sIH_A)/bigcupP; exists h; first exact/setDP.
by rewrite 3!inE ntg Kg cent1C.
Qed.

(* This is the second part of Peterfalvi (4.7). *) 
Lemma prDade_Ind_irr_on k : 
   ~~ (H \subset cfker 'chi[K]_k) -> 'Ind[L] 'chi_k \in 'CF(L, 1%g |: A).
Proof.
move/prDade_irr_on/(cfInd_on sKL); apply: cfun_onS; rewrite class_supportEr.
by apply/bigcupsP=> _ /normsP-> //; rewrite normsU ?norms1 ?normal_norm.
Qed.

(* Third part of Peterfalvi (4.7). *)
Lemma cfker_prTIres j : j != 0 ->  ~~ (H \subset cfker (chi_ j)).
Proof.
rewrite -(cfRes_prTIirr _ 0) cfker_Res ?irr_char // subsetI sHK /=.
apply: contra => kerHmu0j; rewrite -irr_eq1; apply/eqP/cfun_inP=> y W2y.
have [[x W1x ntx] mulW] := (trivgPn _ ntW1, dprodW defW).
rewrite cfun1E W2y -(cfDprodEr defW _ W1x W2y) -dprodr_IirrE -dprod_Iirr0l.
have{ntx} W2'x: x \notin W2 by rewrite -[x \in W2]andTb -W1x -in_setI tiW12 inE.
have V2xy: (x * y)%g \in W :\: W2 by rewrite inE -mulW mem_mulg ?groupMr ?W2'x.
rewrite -[w_ 0 j](signrZK (primeTI_Isign ptiWL j)) cfunE -prTIirr_id //.
have V2x: x \in W :\: W2 by rewrite inE W2'x (subsetP sW1W).
rewrite cfkerMr ?(subsetP (subset_trans sW2H kerHmu0j)) ?prTIirr_id // cfunE.
by rewrite signrMK -[x]mulg1 dprod_Iirr0l dprodr_IirrE cfDprodEr ?lin_char1.
Qed.

(* Fourth part of Peterfalvi (4.7). *)
Lemma prDade_TIres_on j : j != 0 -> chi_ j \in 'CF(K, 1%g |: A).
Proof. by move/cfker_prTIres/prDade_irr_on. Qed.

(* Last part of Peterfalvi (4.7). *)
Lemma prDade_TIred_on j : j != 0 -> mu_ j \in 'CF(L, 1%g |: A).
Proof. by move/cfker_prTIres/prDade_Ind_irr_on; rewrite cfInd_prTIres. Qed.

Import ssrint.

(* Second part of PeterFalvi (4.8). *)
Lemma prDade_TIsign_eq i j k : 
  mu2_ i j 1%g = mu2_ i k 1%g -> delta_ j = delta_ k.
Proof.
move=> eqjk; have{eqjk}: (delta_ j == delta_ k %[mod #|W1|])%C.
  apply: eqCmod_trans (prTIirr1_mod ptiWL i k).
  by rewrite eqCmod_sym -eqjk (prTIirr1_mod ptiWL).
have /negP: ~~ (#|W1| %| 2) by rewrite gtnNdvd.
rewrite /eqCmod -![delta_ _]intr_sign -rmorphB dvdC_int ?Cint_int //= intCK.
by do 2!case: (primeTI_Isign _ _).
Qed.

(* First part of PeterFalvi (4.8). *)
Lemma prDade_sub_TIirr_on i j k :
    j != 0 -> k != 0 -> mu2_ i j 1%g = mu2_ i k 1%g ->
  mu2_ i j - mu2_ i k \in 'CF(L, A0).
Proof.
move=> nzj nzk eq_mu1.
apply/cfun_onP=> g; rewrite defA0 !inE negb_or !cfunE => /andP[A'g V'g].
have [Lg | L'g] := boolP (g \in L); last by rewrite !cfun0 ?subrr.
have{Lg} /bigcupP[_ /rcosetsP[x W1x ->] Kx_g]: g \in cover (rcosets K W1).
  by rewrite (cover_partition (rcosets_partition_mul W1 K)) (sdprodW defL).
have [x1 | ntx] := eqVneq x 1%g.
  have [-> | ntg] := eqVneq g 1%g; first by rewrite eq_mu1 subrr.
  have{A'g} A1'g: g \notin 1%g |: A by rewrite !inE negb_or ntg.
  rewrite x1 mulg1 in Kx_g; rewrite -!(cfResE (mu2_ i _) sKL) ?cfRes_prTIirr //.
  by rewrite !(cfun_onP (prDade_TIres_on _)) ?subrr.
have coKx: coprime #|K| #[x] by rewrite (coprime_dvdr (order_dvdG W1x)).
have nKx: x \in 'N(K) by have [_ _ /subsetP->] := sdprodP defL.
have [/cover_partition defKx _] := partition_cent_rcoset nKx coKx.
have def_cKx: 'C_K[x] = W2 by have [_ _ -> //] := ptiWL; rewrite !inE ntx.
move: Kx_g; rewrite -defKx def_cKx cover_imset => /bigcupP[z /(subsetP sKL)Lz].
case/imsetP=> _ /rcosetP[y W2y ->] Dg; rewrite Dg !cfunJ //.
have V2yx: (y * x)%g \in W :\: W2.
  rewrite inE -(dprodWC defW) mem_mulg // andbT groupMl //.
  by rewrite -[x \in W2]andTb -W1x -in_setI tiW12 inE.
rewrite 2?{1}prTIirr_id //.
have /set1P->: y \in [1].
  rewrite -tiW12 inE W2y andbT; apply: contraR V'g => W1'y.
  by rewrite Dg mem_imset2 // !inE negb_or -andbA -in_setD groupMr ?W1'y.
rewrite -commute1 (prDade_TIsign_eq eq_mu1) !cfunE -mulrBr.
by rewrite !dprod_IirrE !cfDprodE // !lin_char1 // subrr mulr0.
Qed.

(* This is last part of PeterFalvi (4.8). *)
Lemma prDade_sub_TIirr i j k :
    j != 0 -> k != 0 -> mu2_ i j 1%g = mu2_ i k 1%g -> 
  tau (mu2_ i j - mu2_ i k) = delta_ j *: (eta_ i j - eta_ i k).
Proof.
move=> nz_j nz_k eq_mu2jk_1.
have [-> | k'j] := eqVneq j k; first by rewrite !subrr !raddf0.
have [[Itau Ztau] [_ Zsigma]] := (Dade_Zisometry ddA0, cycTI_Zisometry ctiWL).
set dmu2 := _ - _; set dsw := _ - _; have Dmu2 := prTIirr_id ptiWL.
have Zmu2: dmu2 \in 'Z[irr L, A0].
  by rewrite zchar_split rpredB ?irr_vchar ?prDade_sub_TIirr_on.
apply: eq_signed_sub_cTIiso => // [||x Vx].
- exact: zcharW (Ztau _ Zmu2).
- rewrite Itau // cfnormBd ?cfnorm_irr // (cfdot_prTIirr ptiWL).
  by rewrite (negPf k'j) andbF.
have V2x: x \in W :\: W2 by rewrite (subsetP _ x Vx) // setDS ?subsetUr.
rewrite !(cfunE, Dade_id) ?(cycTIiso_restrict _ _ Vx) //; last first.
  by rewrite defA0 inE orbC mem_class_support.
by rewrite !Dmu2 // (prDade_TIsign_eq eq_mu2jk_1) !cfunE -mulrBr.
Qed.

Lemma prDade_supp_disjoint : V \subset ~: K.
Proof.
rewrite subDset setUC -subDset setDE setCK setIC -(dprod_modr defW sW2K).
by rewrite coprime_TIg // dprod1g subsetUr.
Qed.

(* This is Peterfalvi (4.9).                                                  *)
(* We have added the "obvious" fact that calT is pairwise orthogonal, since   *)
(* we require this to prove membership in 'Z[calT], we encapsulate the        *)
(* construction of tau1, and state its conformance to tau on the "larger"     *)
(* domain 'Z[calT, L^#], so that clients can avoid using the domain equation  *)
(* in part (a).                                                               *)
Theorem uniform_prTIred_coherent k (calT := uniform_prTIred_seq ptiWL k) :
    k != 0 ->
  (*a*) [/\ pairwise_orthogonal calT, ~~ has cfReal calT, cfConjC_closed calT,
            'Z[calT, L^#] =i 'Z[calT, A]
          & exists2 psi, psi != 0 & psi \in 'Z[calT, A]]
  (*b*) /\ (exists2 tau1 : {linear 'CF(L) -> 'CF(G)},
           forall j, tau1 (mu_ j) = delta_ k *: (\sum_i sigma (w_ i j))
         & {in 'Z[calT], isometry tau1, to 'Z[irr G]}
        /\ {in 'Z[calT, L^#], tau1 =1 tau}).
Proof.
have uniqT: uniq calT by apply/dinjectiveP; apply: in2W; apply: prTIred_inj.
have sTmu: {subset calT <= codom mu_} by apply: image_codom.
have oo_mu: pairwise_orthogonal (codom mu_).
  apply/pairwise_orthogonalP; split=> [|_ _ /codomP[j1 ->] /codomP[j2 ->]].
    apply/andP; split; last by apply/injectiveP; apply: prTIred_inj.
    by apply/codomP=> [[i /esym/eqP/idPn[]]]; apply: prTIred_neq0.
  by rewrite cfdot_prTIred; case: (j1 =P j2) => // -> /eqP.
have real'T: ~~ has cfReal calT.
  by apply/hasPn=> _ /imageP[j /andP[nzj _] ->]; apply: prTIred_not_real.
have ccT: cfConjC_closed calT.
  move=> _ /imageP[j Tj ->]; rewrite -prTIred_aut image_f // inE aut_Iirr_eq0.
  by rewrite prTIred_aut cfunE conj_Cnat ?Cnat_char1 ?prTIred_char.
have TonA: 'Z[calT, L^#] =i 'Z[calT, A].
  have A'1: 1%g \notin A by apply: contra (subsetP sAA0 _) _; have [] := ddA0.
  move=> psi; rewrite zcharD1E -(setU1K A'1) zcharD1; congr (_ && _).
  apply/idP/idP; [apply: zchar_trans_on psi => psi Tpsi | exact: zcharW].
  have [j /andP[nz_j _] Dpsi] := imageP Tpsi.
  by rewrite zchar_split mem_zchar // Dpsi prDade_TIred_on.
move=> nzk; split.
  split=> //; first exact: sub_pairwise_orthogonal oo_mu.
  have Tmuk: mu_ k \in calT by rewrite image_f // inE nzk /=.
  exists ((mu_ k)^*%CF - mu_ k); first by rewrite subr_eq0 (hasPn real'T).
  rewrite -TonA -rpredN opprB sub_aut_zchar ?zchar_onG ?mem_zchar ?ccT //.
  by move=> _ /mapP[j _ ->]; rewrite char_vchar ?prTIred_char.
pose f0 j := delta_ k *: (\sum_i eta_ i j); have in_mu := codom_f mu_.
pose f1 psi := f0 (iinv (valP (insigd (in_mu k) psi))).
have f1mu j: f1 (mu_ j) = f0 j.
  have in_muj := in_mu j.
  rewrite /f1 /insigd /insubd /= insubT /=; [idtac].
  by rewrite iinv_f //; apply: prTIred_inj.
have iso_f1: {in codom mu_, isometry f1, to 'Z[irr G]}.
  split=> [_ _ /codomP[j1 ->] /codomP[j2 ->] | _ /codomP[j ->]]; last first.
    by rewrite f1mu rpredZsign rpred_sum // => i _; apply: cycTIiso_vchar.
  rewrite !f1mu cfdotZl cfdotZr rmorph_sign signrMK !cfdot_suml.
  apply: eq_bigr => i1 _; rewrite !cfdot_sumr; apply: eq_bigr => i2 _.
  by rewrite cfdot_cycTIiso cfdot_prTIirr.
have [tau1 Dtau1 Itau1] := Zisometry_of_iso (orthogonal_free oo_mu) iso_f1.
exists tau1 => [j|]; first by rewrite Dtau1 ?codom_f ?f1mu.
split=> [|psi]; first by apply: sub_iso_to Itau1 => //; apply: zchar_subset.
rewrite zcharD1E => /andP[/zchar_expansion[//|z _ Dpsi] /eqP psi1_0].
rewrite -[psi]subr0 -(scale0r (mu_ k)) -(mul0r (mu_ k 1%g)^-1) -{}psi1_0.
rewrite {psi}Dpsi sum_cfunE mulr_suml scaler_suml -sumrB !raddf_sum /=.
apply: eq_big_seq => _ /imageP[j /andP[nzj /eqP eq_mujk_1] ->].
rewrite cfunE eq_mujk_1 mulfK ?prTIred_1_neq0 // -scalerBr !linearZ /=.
congr (_ *: _); rewrite {z}linearB !Dtau1 ?codom_f // !f1mu -scalerBr -!sumrB.
rewrite !linear_sum; apply: eq_bigr => i _ /=.
have{eq_mujk_1} eq_mu2ijk_1: mu2_ i j 1%g = mu2_ i k 1%g.
  by apply: (mulfI (neq0CG W1)); rewrite !prTIirr_1 -!prTIred_1.
by rewrite -(prDade_TIsign_eq eq_mu2ijk_1) prDade_sub_TIirr.
Qed.

(* This is Peterfalvi (4.10). *)
Lemma prDade_sub2_TIirr i j :
  tau (delta_ j *: mu2_ i j - delta_ j *: mu2_ 0 j - mu2_ i 0 + mu2_ 0 0)
    = eta_ i j - eta_ 0 j - eta_ i 0 + eta_ 0 0.
Proof.
pose V0 := class_support V L; have sVV0: V \subset V0 := sub_class_support L V.
have sV0A0: V0 \subset A0 by rewrite defA0 subsetUr.
have nV0L: L \subset 'N(V0) := class_support_norm V L.
have [_ _ /normedTI_memJ_P[ntV _ tiV]] := ctiWG.
have [/andP[sA0L _] _ A0'1 _ _] := ddA0.
have{sA0L A0'1} sV0G: V0 \subset G^#.
  by rewrite (subset_trans sV0A0) // subsetD1 A0'1 (subset_trans sA0L).
have{sVV0} ntV0: V0 != set0 by apply: contraNneq ntV; rewrite -subset0 => <-.
have{ntV} tiV0: normedTI V0 G L.
  apply/normedTI_memJ_P; split=> // _ z /imset2P[u y Vu Ly ->] Gz.
  apply/idP/idP=> [/imset2P[u1 y1 Vu1 Ly1 Duyz] | Lz]; last first.
    by rewrite -conjgM mem_imset2 ?groupM.
  rewrite -[z](mulgKV y1) groupMr // -(groupMl _ Ly) (subsetP sWL) //.
  by rewrite -(tiV u) ?groupM ?groupV // ?(subsetP sLG) // !conjgM Duyz conjgK.
have{ntV0 sV0A0 nV0L tiV0} DtauV0: {in 'CF(L, V0), tau =1 'Ind}.
  by move=> beta V0beta; rewrite /= -(restr_DadeE _ sV0A0) //; apply: Dade_Ind.
pose alpha := cfCyclicTIset defW i j; set beta := _ *: mu2_ i j - _ - _ + _.
have Valpha: alpha \in 'CF(W, V) := cfCycTI_on ctiWL i j.
have Dalpha: alpha = w_ i j - w_ 0 j - w_ i 0 + w_ 0 0.
  by rewrite addrC {1}cycTIirr00 addrA addrAC addrA addrAC -cfCycTI_E.
rewrite -!(linearB sigma) -linearD -Dalpha cycTIiso_Ind //.
suffices ->: beta = 'Ind[L] alpha by rewrite DtauV0 ?cfInd_on ?cfIndInd.
rewrite Dalpha -addrA -[w_ 0 0]opprK -opprD linearB /= /beta -scalerBr.
by rewrite !(cfInd_sub_prTIirr ptiWL) prTIsign0 scale1r opprD opprK addrA.
Qed.
 
End Four_6_t0_10.