path: root/mathcomp/odd_order/PFsection11.v

(* (c) Copyright 2006-2015 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 center.
From mathcomp
Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
From mathcomp
Require Import gfunctor gproduct cyclic commutator gseries nilpotent pgroup.
From mathcomp
Require Import sylow hall abelian maximal frobenius.
From mathcomp
Require Import matrix mxalgebra mxrepresentation mxabelem vector.
From mathcomp
Require Import BGsection1 BGsection3 BGsection7 BGsection15 BGsection16.
From mathcomp
Require Import ssrnum ssrint algC classfun character inertia vcharacter.
From mathcomp
Require Import PFsection1 PFsection2 PFsection3 PFsection4 PFsection5.
From mathcomp
Require Import PFsection6 PFsection7 PFsection8 PFsection9 PFsection10.

(******************************************************************************)
(* This file covers Peterfalvi, Section 11: Maximal subgroups of Types        *)
(* III and IV.                                                                *)
(******************************************************************************)

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

Import GroupScope GRing.Theory FinRing.Theory Num.Theory.

Section Eleven.

(* This is Peterfalvi (11.1). *)
Lemma lbound_expn_odd_prime p q : 
   odd p -> odd q -> prime p -> prime q -> p != q -> 4 * q ^ 2 + 1 < p ^ q.
Proof.
move=> odd_p odd_q pr_p pr_q p_neq_q.
have{pr_p pr_q} [pgt2 qgt2] : 2 < p /\ 2 < q by rewrite !odd_prime_gt2.
have [qlt5 | qge5 {odd_q qgt2 p_neq_q}] := ltnP q 5.
  have /eqP q3: q == 3 by rewrite eqn_leq qgt2 andbT -ltnS -(odd_ltn 5).
  apply: leq_trans (_ : 5 ^ q <= p ^ q); first by rewrite q3.
  by rewrite leq_exp2r // odd_geq // ltn_neqAle pgt2 eq_sym -q3 p_neq_q.
apply: leq_trans (_ : 3 ^ q <= p ^ q); last by rewrite -(subnKC qge5) leq_exp2r.
elim: q qge5 => // q IHq; rewrite ltnS leq_eqVlt => /predU1P[<- // | qge5].
rewrite (expnS 3); apply: leq_trans {IHq}(leq_mul (leqnn 3) (IHq qge5)).
rewrite -!addnS mulnDr leq_add // mulnCA leq_mul // !(mul1n, mulSnr).
by rewrite -addn1 sqrnD muln1 -(subnKC qge5) !leq_add ?leq_mul.
Qed.

Local Open Scope ring_scope.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Types H K L N P Q R S T U V W : {group gT}.

Variables M U W W1 W2 : {group gT}.
Hypotheses (maxM : M \in 'M) (defW : W1 \x W2 = W) (MtypeP : of_typeP M U defW).
Hypothesis notMtype2 : FTtype M != 2.

Let notMtype5 : FTtype M != 5. Proof. exact: FTtype5_exclusion. Qed.
Let notMtype1 : FTtype M != 1%N. Proof. exact: FTtypeP_neq1 MtypeP. Qed.
Let Mtype34 : FTtype M \in pred2 3 4.
Proof.
by have:= FTtype_range M; rewrite -mem_iota !inE !orbA orbC 3?[_ == _](negPf _).
Qed.
Let Mtype_gt2 : (FTtype M > 2)%N. Proof. by case/pred2P: Mtype34 => ->. Qed.

Local Notation H0 := (Ptype_Fcore_kernel MtypeP).
Local Notation "` 'H0'" := (gval H0) (at level 0, only parsing) : group_scope.
Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope.
Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
Local Notation H := `M`_\F%G.
Local Notation "` 'H'" := `M`_\F (at level 0) : group_scope.
Local Notation HU := M^`(1)%G.
Local Notation "` 'HU'" := `M^`(1)%g (at level 0) : group_scope.
Local Notation U' := U^`(1)%G.
Local Notation "` 'U''" := `U^`(1)%g (at level 0) : group_scope.
Local Notation C := 'C_U(`H)%G.
Local Notation "` 'C'" := 'C_`U(`H) (at level 0) : group_scope.
Local Notation HC := (`H <*> `C)%G.
Local Notation "` 'HC'" := (`H <*> `C) (at level 0) : group_scope.
Local Notation H0C := (`H0 <*> `C)%G.
Local Notation "` 'H0C'" := (`H0 <*> `C) (at level 0) : group_scope.
Local Notation Hbar := (`H / `H0)%g.

Local Notation S_ := (seqIndD HU M HU).
Local Notation tau := (FT_Dade0 maxM).
Local Notation R := (FTtypeP_coh_base maxM MtypeP).
Local Notation V := (cyclicTIset defW).

Let Mtype24 := compl_of_typeII_IV maxM MtypeP notMtype5.

Let defMs : M`_\s = HU. Proof. exact: FTcore_type_gt2. Qed.
Let defA1 : 'A1(M) = HU^#. Proof. by rewrite /= -defMs. Qed.
Let defA : 'A(M) = HU^#. Proof. by rewrite FTsupp_eq1. Qed.
Let sHU_A0 : HU^# \subset 'A0(M). Proof. by rewrite -defA FTsupp_sub0. Qed.

Let calS := seqIndD HU M M`_\s 1.
Let scohM : subcoherent calS tau R. Proof. exact: FTtypeP_subcoherent. Qed.
Let scoh1 : subcoherent (S_ 1) tau R.
Proof. by rewrite -{2}(group_inj defMs). Qed.

Let p := #|W2|.
Let pr_p : prime p. Proof. by have [] := FTtypeP_primes maxM MtypeP. Qed.
Let ntW2 : W2 :!=: 1%g. Proof. by rewrite -cardG_gt1 prime_gt1. Qed.
Let cycW2 : cyclic W2. Proof. exact: prime_cyclic. Qed.
Let def_p : pdiv #|Hbar| = p. Proof. exact: typeIII_IV_core_prime. Qed.

Let q := #|W1|.
Let pr_q : prime q. Proof. by have [] := FTtypeP_primes maxM MtypeP. Qed.
Let ntW1 : W1 :!=: 1%g. Proof. by rewrite -cardG_gt1 prime_gt1. Qed.
Let cycW1 : cyclic W1. Proof. exact: prime_cyclic. Qed.

Let defM : HU ><| W1 = M. Proof. by have [[]] := MtypeP. Qed.
Let defHU : H ><| U = HU. Proof. by have [_ []] := MtypeP. Qed.

Let nsHUM : HU <| M. Proof. exact: gFnormal. Qed.
Let sHUM : HU \subset M. Proof. exact: gFsub. Qed.
Let sHHU : H \subset HU. Proof. by have /mulG_sub[] := sdprodW defHU. Qed.
Let sUHU : U \subset HU. Proof. by have /mulG_sub[] := sdprodW defHU. Qed.
Let sUM : U \subset M. Proof. exact: subset_trans sUHU sHUM. Qed.

Let coHUq : coprime #|HU| q.
Proof. by rewrite (coprime_sdprod_Hall_r defM); have [[]] := MtypeP. Qed.
Let coUq : coprime #|U| q. Proof. exact: coprimeSg coHUq. Qed.
	
Let neq_pq : p != q.
Proof.
apply: contraTneq coHUq => <-; rewrite coprime_sym prime_coprime ?cardSg //.
by rewrite -(typeP_cent_compl MtypeP) subsetIl.
Qed.

Let solHU : solvable HU. Proof. exact: solvableS sHUM (mmax_sol maxM). Qed.
Let solH : solvable H. Proof. exact: solvableS sHHU solHU. Qed.

Let ltM''HU :  M^`(2)%g \proper HU.
Proof. by rewrite (sol_der1_proper solHU) // -defMs FTcore_neq1. Qed.

Let frobMtilde : [Frobenius M / M^`(2) = (HU / M^`(2)) ><| (W1 / M^`(2))].
Proof.
have [[_ _ _ _] _ _ [_ _ _ sW2M'' prHUW1 ] _] := MtypeP.
by rewrite Frobenius_coprime_quotient ?gFnormal //; split=> // _ /prHUW1->.
Qed.

Let defHC : H \x C = HC.
Proof. 
by have [defHC _ _ _] := typeP_context MtypeP; rewrite /= (dprodWY defHC).
Qed.

Let nC_UW1 : U <*> W1 \subset 'N(C).
Proof.
have /sdprodP[_ _ nHUW1 _] := Ptype_Fcore_sdprod MtypeP.
by rewrite normsI ?norms_cent // join_subG normG; have [_ []] := MtypeP.
Qed.

Let nsCM : C <| M.
Proof.
rewrite /normal subIset ?sUM //= -{1}(sdprodW (Ptype_Fcore_sdprod MtypeP)).
by rewrite mulG_subG cents_norm // centsC subsetIr.
Qed.

Let nsCU : C <| U. Proof. exact: normalS (subsetIl _ _) sUM nsCM. Qed.
Let nsHC_M : HC <| M. Proof. by rewrite normalY ?gFnormal. Qed.
Let sHC_HU : HC \subset HU. Proof. by rewrite join_subG sHHU subIset ?sUHU. Qed.
Let nsHC_HU : HC <| HU. Proof. exact: normalS nsHC_M. Qed.

Let chiefH0 : chief_factor M H0 H.
Proof. by have [] := Ptype_Fcore_kernel_exists maxM MtypeP notMtype5. Qed.

Let minHbar : minnormal Hbar (M / H0).
Proof. exact: chief_factor_minnormal. Qed.

Let abelHbar : p.-abelem Hbar.
Proof.
have solHbar : solvable (H / H0) by rewrite quotient_sol.
have [_ _] := minnormal_solvable minHbar (subxx _) solHbar.
by rewrite /is_abelem def_Ptype_factor_prime.
Qed.

Let sH0H : H0 \subset H.
Proof. by have/andP[/maxgroupp/andP[/proper_sub]]:= chiefH0. Qed.

Let nH0M: M \subset 'N(H0).
Proof. by have /andP[/maxgroupp/andP[]] := chiefH0. Qed.

Let nsH0H : H0 <| H.
Proof. by rewrite /normal sH0H gFsub_trans. Qed.

Let nsH0C_M : H0C <| M.
Proof. by rewrite normalY // /normal ?(subset_trans sH0H) ?gFsub. Qed.

Let defH0C : H0 \x C = H0C.
Proof.
have /dprodP[_ _ cHC tiHC] := defHC.
by rewrite dprodEY ?(centsS sH0H) //; apply/trivgP; rewrite -tiHC setSI.
Qed.

(* Group-theoretic consequences of the coherence and non-coherence theorems   *)
(* of Sections 5, 9 and 10 for maximal subgroups of type III and IV.          *)

(* This is Peterfalvi (11.3). *)
Lemma FTtype34_noncoherence : ~ coherent (S_ H0C) M^# tau.
Proof.
move=> cohH0C; suff: coherent (S_ 1) M^# tau by apply: FTtype345_noncoherence.
have /mulG_sub[_ sW1M] := sdprodW defM.
have [nsHHU _ _ nHU tiHU] := sdprod_context defHU.
have sHM: H \subset M := gFsub _ _.
have [sCM sH0C_M]: C \subset M /\ H0C \subset M by rewrite !normal_sub.
have nH0_C := subset_trans sCM nH0M.
have sH0C_HC: H0C \subset HC by apply: genS (setSU _ _).
have defF: HC :=: 'F(M) by have [/dprodWY] := typeP_context MtypeP.
have{defF} nilHC: nilpotent (HC / 1) by rewrite defF quotient_nil ?Fitting_nil.
have /bounded_seqIndD_coherence-bounded_coh1 := scoh1.
apply: bounded_coh1 nilHC cohH0C _; rewrite ?sub1G ?normal1 //.
have[_ _ /= oHbar] := Ptype_Fcore_factor_facts maxM MtypeP notMtype5.
rewrite -(index_sdprod defM) -divgS // -(dprod_card defHC) -(dprod_card defH0C).
rewrite divnMr ?cardG_gt0 // divg_normal // oHbar def_p -/q.
by rewrite lbound_expn_odd_prime ?mFT_odd.
Qed.

(* This is Peterfalvi (11.4). *)
Lemma bounded_proper_coherent H1 :
  H1 <| M -> H1 \proper HU -> coherent (S_ H1) M^# tau ->
    (#|HU : H1| <= 2 * q * #|U : C| + 1)%N.
Proof.
move=> nsH1_M psH1_M' cohH1; have [nsHHU _ _ _ _] := sdprod_context defHU.
suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R.
  rewrite  indexgg sqrtC1 mulr1 -leC_nat natrD -ler_subl_addr -mulnA natrM.
  congr (_ <= _ * _%:R); apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 HC)).
  rewrite Lagrange ?normal_sub // mulnCA -(dprod_card defHC) -mulnA mulnC.
  by rewrite Lagrange ?subsetIl // (sdprod_card defHU) (sdprod_card defM).
apply/negP/(coherent_seqIndD_bound _ _ scoh1 _ _ _ FTtype34_noncoherence) => //.
suffices /center_idP->: abelian (HC / H0C) by rewrite genS ?setSU.
suffices /isog_abelian<-: Hbar \isog HC / H0C by apply: abelem_abelian abelHbar.
by rewrite /= [`H0C]joingC quotient_sdprodr_isog ?(dprodWsdC defHC).
Qed.

(* This is Peterfalvi (11.5). *)
Lemma FTtype34_der2 : M^`(2)%g = HC.
Proof.
have [defFM [_ not_cHU] _ _] := typeP_context MtypeP.
have [_ sW1M _ _ tiHU_W1] := sdprod_context defM.
have{defFM} sM''_HC: M^`(2)%g \subset HC.
  by rewrite -defHC defFM; have [_ _ []] := MtypeP.
have scohM'': subcoherent (S_ M^`(2)) tau R.
  exact/(subset_subcoherent scoh1)/seqInd_conjC_subset1.
have cohM'': coherent (S_ M^`(2)) M^# tau.
  apply: uniform_degree_coherence scohM'' _.
  apply: all_pred1_constant #|M : HU|%:R _ _; rewrite all_map.
  apply/allP=> _ /seqIndP[s /setDP[kerM'' _] ->] /=; rewrite inE in kerM''.
  by rewrite cfInd1 ?gFsub // lin_char1 ?mulr1 ?lin_irr_der1.
have ubHC: (#|HC : M^`(2)| < 2 * q + 1)%N.
  rewrite -(ltn_pmul2r (indexg_gt0 U C)) mulnDl mul1n.
  apply: leq_ltn_trans (_ : 2 * q * #|U : C| + 1 < _)%N; last first.
    by rewrite ltn_add2l indexg_gt1 subsetIidl not_cHU //; have [] := Mtype24.
  have {1}->: #|U : C| = #|HU : HC| by apply: index_sdprodr (subsetIl _ _).
  by rewrite mulnC (Lagrange_index sHC_HU) // bounded_proper_coherent ?gFnormal.
have regHC_W1: semiregular (HC / M^`(2)) (W1 / M^`(2)).
  by apply: semiregularS (Frobenius_reg_ker frobMtilde); rewrite quotientS.
suffices /dvdnP[k Dk]: 2 * q %| #|HC : M^`(2)|.-1.
  apply: contraTeq ubHC; rewrite -leqNgt eqEsubset sM''_HC -indexg_gt1 addn1.
  by rewrite -[#|_:_|]prednK // {}Dk !ltnS muln_gt0 => /andP[/leq_pmull->].
rewrite Gauss_dvd; last by rewrite coprime2n mFT_odd.
rewrite dvdn2 -subn1 odd_sub // addbT negbK subn1.
rewrite -card_quotient; last by rewrite (subset_trans sHC_HU) // (der_norm 1).
have Dq: q = #|W1 / M^`(2)|%g.
  apply/card_isog/quotient_isog; first by rewrite (subset_trans sW1M) ?gFnorm.
  by apply/trivgP; rewrite -tiHU_W1 setSI // (der_sub 1).
rewrite quotient_odd ?mFT_odd //= Dq regular_norm_dvd_pred ?quotient_norms //.
by rewrite (subset_trans sW1M) ?normal_norm.
Qed.
Local Notation defM'' := FTtype34_der2.

(* This is Peterfalvi (11.6). *)
Lemma FTtype34_facts (H' := H^`(1)%g):
  [/\ p.-group H, U \subset 'C(H0), H0 :=: H' & C :=: U']. 
Proof.
have nilH: nilpotent H := Fcore_nil M.
have /sdprod_context[/andP[_ nHM] sUW1M _ _ _] := Ptype_Fcore_sdprod MtypeP.
have coH_UW1: coprime #|H| #|U <*> W1| := Ptype_Fcore_coprime MtypeP.
have [[_ mulHU _ tiHU] [nHU isomHU]] := (sdprodP defHU, sdprod_isom defHU).
have{sUW1M} cH0U: U \subset 'C(H0).
  have frobUW1 := Ptype_compl_Frobenius maxM MtypeP notMtype5.
  have nH0_UW1 := subset_trans sUW1M nH0M; have [_ nH0W1] := joing_subP nH0_UW1.
  have [coH0_UW1 solH0] := (coprimeSg sH0H coH_UW1, solvableS sH0H solH).
  have [_ -> //] := Frobenius_Wielandt_fixpoint frobUW1 nH0_UW1 coH0_UW1 solH0.
  have ->: 'C_H0(W1) = H0 :&: 'C_H(W1) by rewrite setIA (setIidPl sH0H).
  have nH0C: 'C_H(W1) \subset 'N(H0) by rewrite subIset // normal_norm.
  rewrite cardMg_TI // -LagrangeMl -card_quotient {nH0C}//.
  rewrite coprime_quotient_cent ?(coprimeSg sHHU) //=.
  have [_ -> _] := Ptype_Fcore_factor_facts maxM MtypeP notMtype5.
  by rewrite (typeP_cent_core_compl MtypeP) def_p.
have{isomHU} defC: C :=: U'.
  have [injHquo defHUb] := isomP isomHU.
  apply: (injm_morphim_inj injHquo); rewrite ?subsetIl ?morphim_der ?der_sub //.
  rewrite defHUb morphim_restrm -quotientE setIA setIid -quotientMidl /=.
  by rewrite (dprodW defHC) -defM'' -quotient_der // -mulHU mul_subG ?normG.
have{coH_UW1} defH0: H0 :=: H'.
  pose Hhat := (H / H')%g; pose Uhat := (U / H')%g; pose HUhat := (HU / H')%g.
  have nH'H: H \subset 'N(H') by apply: gFnorm.
  have nH'U: U \subset 'N(H') by apply: gFnorm_trans.
  apply/eqP; rewrite eqEsubset andbC.
  rewrite der1_min ?(abelem_abelian abelHbar) ?normal_norm //=.
  rewrite -quotient_sub1 /= -/H'; last exact: subset_trans sH0H nH'H.
  suffices <-: 'C_Hhat(Uhat) = 1%g.
    by rewrite subsetI quotientS //= quotient_cents // centsC.
  suffices: ~~ ('C_Hhat(Uhat)^`(1)%g \proper 'C_Hhat(Uhat)).
    exact: contraNeq (sol_der1_proper (quotient_sol _ solH) (subsetIl Hhat _)).
  have {2}<-: HUhat^`(1)%g :&: 'C_Hhat(Uhat) = 'C_Hhat(Uhat).
    rewrite -quotient_der ?[HU^`(1)%g]defM''; last by rewrite -mulHU mul_subG.
    by rewrite (setIidPr _) ?subIset // quotientS ?joing_subl.
  suffices defHUhat: 'C_Hhat(Uhat) \x ([~: Hhat, Uhat] <*> Uhat) = HUhat.
    rewrite -(dprod_modl (der_dprod 1 defHUhat)) ?der_sub //= -/Hhat.
    rewrite [rhs in _ \x rhs](trivgP _) ?dprodg1 ?properxx //= -/Hhat.
    by have [_ _ _ <-] := dprodP defHUhat; rewrite setIC setIS ?der_sub.
  have coHUhat: coprime #|Hhat| #|Uhat|.
    by rewrite coprime_morph ?(coprimegS _ coH_UW1) ?joing_subl.
  have defHhat: 'C_Hhat(Uhat) \x [~: Hhat, Uhat] = Hhat. 
    by rewrite dprodC coprime_abelian_cent_dprod ?der_abelian ?quotient_norms.
  rewrite /HUhat -(sdprodWY defHU) quotientY //= -(dprodWY defHhat).
  have [_ _ cCRhat tiCRhat] := dprodP defHhat.
  rewrite dprodEY ?joingA //; first by rewrite join_subG cCRhat centsC subsetIr.
  apply/trivgP; rewrite /= joingC norm_joinEl ?commg_normr //= -/Hhat -/Uhat.
  rewrite -tiCRhat !(setIAC _ 'C(_)) setSI // subsetI subsetIl /=.
  by rewrite -group_modr ?commg_subl ?quotient_norms //= coprime_TIg ?mul1g.
suffices{defC defH0}: p.-group H by [].
pose R := 'O_p^'(H); have hallR: p^'.-Hall(H) R := nilpotent_pcore_Hall _ nilH.
have defRHp: R \x 'O_p(H) = H by rewrite dprodC nilpotent_pcoreC.
suffices R_1: R :=: 1%g by rewrite -defRHp R_1 dprod1g pcore_pgroup.
have /subsetIP[sRH cUR]: R \subset 'C_H(U).
  have oH: #|H| = (p ^ q * #|'C_H(U)|)%N.
    by have:= typeII_IV_core maxM MtypeP notMtype5 => /=; rewrite ifN => // -[].
  apply/setIidPl/eqP; rewrite eqEcard subsetIl /= (card_Hall hallR) {}oH.
  rewrite (card_Hall (setI_normal_Hall _ hallR _)) ?subsetIl ?gFnormal //.
  rewrite partnM ?expn_gt0 ?cardG_gt0 //= part_p'nat ?mul1n ?pnatNK //.
  by rewrite pnat_exp ?pnat_id.
suffices: ~~ (R^`(1)%g \proper R) by apply: contraNeq (sol_der1_proper solH _). 
have /setIidPr {2}<-: R \subset HU^`(1)%g.
  by rewrite [HU^`(1)%g]defM'' -(dprodWY defHC) sub_gen ?subsetU ?sRH.
suffices defRHpU: R \x ('O_p(H) <*> U) = HU.
  rewrite -(dprod_modl (der_dprod 1 defRHpU)) ?der_sub //= -/R setIC.
  rewrite [rhs in _ \x rhs](trivgP _) ?dprodg1 ?properxx //= -/R.
  by have /dprodP[_ _ _ <-] := defRHpU; rewrite setIS ?der_sub.
rewrite -(sdprodWY defHU) -[in RHS](dprodWY defRHp) -joingA.
have [_ _ cRHp tiRHp] := dprodP defRHp.
rewrite dprodEY //= -/R; first by rewrite join_subG cRHp centsC.
rewrite joingC norm_joinEl 1?gFnorm_trans //.
by rewrite -(setIidPl sRH) -setIA -group_modr ?gFsub // tiHU mul1g.
Qed.

Let frobUW1bar : [Frobenius U <*> W1 / C = (U / C) ><| (W1 / C)].
Proof.
have frobUW1: [Frobenius U <*> W1 = U ><| W1].
  exact: Ptype_compl_Frobenius MtypeP notMtype5.
have [defUW1 ntU _ _ _] := Frobenius_context frobUW1.
have [[_ _ _ defC] regUW1] := (FTtype34_facts, Frobenius_reg_ker frobUW1).
rewrite Frobenius_coprime_quotient // /normal ?subIset ?joing_subl //.
by split=> [|x /regUW1->]; rewrite ?sub1G //= defC (sol_der1_proper solHU).
Qed.

(* This is Peterfalvi (11.7).                                                 *)
(* We have recast the linear algebra arguments in the original text in pure-  *)
(* group-theoretic terms: the overhead of the abelem_rV correspondence is not *)
(* justifiable here, as the Ssreflect linear algebra library lacks specific   *)
(* support for bilinear forms: we use D y z := [~ coset Q y, coset Q z] as    *)
(* our "linear form". D is antisymmetric as D z y = (D y z)^-1, so we only    *)
(* show that D is "linear" in z, that is, that D y is a group morphism with   *)
(* domain H whose kernel contains H0, when y \in H, and we do not bother to   *)
(* factor D to obtain a form over Hbar = H / H0.                              *)
(*   We further rework the argument to support this change in perspective:    *)
(*  - We remove any reference to linear algebra in the "Galois" (9.7b) case,  *)
(*    where U acts irreducibly on Hbar: we revert to the proof of the         *)
(*    original Odd Order paper, using the fact that H / Q is extraspecial.    *)
(*  - In the "non-Galois" (9.7a) case, we use the W1-conjugation class of a   *)
(*    generator of H1 as an explicit basis of Hbar, indexed by W1, and we     *)
(*    use the elements xbar_ w = coset H0 (x_ w) of this basis instead of     *)
(*    arbitrary y in H_i, as the same argument then justifies extending       *)
(*    commutativity to all of Hbar.                                           *)
(*  - We construct phi as the morphism mapping ubar in Ubar to the n such     *)
(*    that the action of ubar on H1 is exponentiation by n. We derive a       *)
(*    morphism phi_ w ubar for the action of Ubar on H1 ^ w, for w in W1, by  *)
(*    composign with the action QV of W1 on Ubar by inverse conjugation.      *)
(*  - We exchange the two alternatives in the (9.7a) case; most of proof is   *)
(*    thus by contradiction with the C_U(Hbar) != u assertion in (9.6),       *)
(*    first establishing case 9.7a (as 9.7b contradicts q odd), then that D   *)
(*    is nontrivial for some x_ w1 and x_ w2 (as (H / Q)' = H0 / Q != 1),     *)
(*    whence (phi_ w1 u)(phi_ w2 u) = 1, whence (phi u)^-1 = phi u and        *)
(*    phi = 1, i.e., Ubar centralises Wbar.                                   *)
(* Note finally that we simply construct U as a maximal subgroup of H0 normal *)
(* in H, as the nilpotence of H / Q implies that H0 / Q lies in its center.   *)
Lemma FTtype34_Fcore_kernel_trivial :
  [/\ p.-abelem H, #|H| = (p ^ q)%N & `H0 = 1%g].
Proof.
have [[_ _ nHU tiHU] [pH cH0U defH' _]] := (sdprodP defHU, FTtype34_facts).
have [/mulG_sub[_ sW1M] nH0H] := (sdprodW defM, normal_norm nsH0H).
have nHW1: W1 \subset 'N(H) := subset_trans sW1M (gFnorm _ M).
have nUW1: W1 \subset 'N(U) by have [_ []] := MtypeP.
pose bar := coset_morphism H0; pose Hbar := (H / H0)%g; pose Ubar := (U / H0)%g.
have [Cbar_neqU _ /= oHbar] := Ptype_Fcore_factor_facts maxM MtypeP notMtype5.
rewrite -/Hbar def_p // -/q in oHbar.
have [nH0U nH0W1] := (subset_trans sUM nH0M, subset_trans sW1M nH0M).
suffices H0_1 : `H0 = 1%g.
  have isoHbar: H \isog H / H0 by rewrite H0_1 quotient1_isog.
  by rewrite (isog_abelem isoHbar) (card_isog isoHbar).
apply: contraNeq Cbar_neqU => ntH0; rewrite [Ptype_Fcompl_kernel _]unlock.
suffices: Hbar \subset 'C(Ubar).
  by rewrite (sameP eqP setIidPl) sub_astabQ nH0U centsC.
have pH0 := pgroupS sH0H pH; have{ntH0} [_ _ [k oH0]] := pgroup_pdiv pH0 ntH0.
have{k oH0} [Q maxQ nsQH]: exists2 Q : {group gT}, maximal Q H0 & Q <| H.
  have [Q [sQH0 nsQH oQ]] := normal_pgroup pH nsH0H (leq_pred _).
  exists Q => //; apply: p_index_maximal => //.
  by rewrite -divgS // oQ oH0 pfactorK //= expnS mulnK ?expn_gt0 ?cardG_gt0.
have nsQH0: Q <| H0 := p_maximal_normal (pgroupS sH0H pH) maxQ.
have [[sQH0 nQH0] nQH] := (andP nsQH0, normal_norm nsQH).
have nQU: U \subset 'N(Q) by rewrite cents_norm ?(centsS sQH0).
pose hat := coset_morphism Q; pose Hhat := (H / Q)%g; pose H0hat := (H0 / Q)%g.
have{maxQ} oH0hat: #|H0hat| = p by rewrite card_quotient ?(p_maximal_index pH0).
have defHhat': Hhat^`(1)%g = H0hat by rewrite -quotient_der -?defH'.
have ntH0hat: H0hat != 1%g by rewrite -cardG_gt1 oH0hat prime_gt1.
have pHhat: p.-group Hhat by apply: quotient_pgroup.
have nsH0Hhat: H0hat <| Hhat by apply: quotient_normal.
have sH0hatZ: H0hat \subset 'Z(Hhat).
  by rewrite prime_meetG ?oH0hat // meet_center_nil ?(pgroup_nil pHhat).
have{pHhat} gal'M: ~~ typeP_Galois MtypeP.
  have sZHhat: 'Z(Hhat) \subset Hhat := center_sub _.
  have nsH0hatZ: H0hat <| 'Z(Hhat) := normalS sH0hatZ sZHhat nsH0Hhat.
  have [f injf im_f] := third_isom sQH0 nsQH nsH0H.
  have fHhat: f @* (Hhat / H0hat) = Hbar by rewrite im_f.
  apply: contra (odd (logn p #|Hhat|)) _ _; last first.
    rewrite -(divnK (cardSg (quotientS Q sH0H))) divg_normal // oH0hat.
    by rewrite -(card_injm injf) // fHhat oHbar -expnSr pfactorK //= mFT_odd.
  rewrite /typeP_Galois acts_irrQ // => /mingroupP[_ minUHbar].
  suffices /(card_extraspecial pHhat)[n _ ->]: extraspecial Hhat.
    by rewrite pfactorK //= odd_double.
  have abelH: p.-abelem (Hhat / H0hat)%g by rewrite -(injm_abelem injf) ?fHhat.
  suffices{abelH} defZHhat: 'Z(Hhat) = H0hat.
    do 2?split; rewrite defZHhat ?oH0hat //.
    apply/eqP; rewrite eqEsubset (Phi_min pHhat) ?normal_norm //=.
    by rewrite (Phi_joing pHhat) defHhat' joing_subl.
  apply: contraNeq ntH0hat; rewrite eqEsubset sH0hatZ andbT => not_esHhat.
  rewrite -defHhat'; apply/eqP/derG1P/center_idP/(quotient_inj nsH0hatZ)=> //.
  apply: (injm_morphim_inj injf); rewrite ?quotientS //= fHhat -/Hhat -/H0hat.
  rewrite minUHbar //= -/Hbar -?fHhat 1?morphim_injm_eq1 ?morphimS // -subG1.
  rewrite quotient_sub1 ?(normal_norm nsH0hatZ) // not_esHhat -['Z(_)]cosetpreK.
  rewrite im_f ?sub_cosetpre_quo // quotient_norms ?norm_quotient_pre //.
  by rewrite gFnorm_trans ?quotient_norms.
have [H1 []] := typeP_Galois_Pn maxM notMtype5 gal'M.
rewrite def_p => oH1 nH1Ubar _ /bigdprodWY-defHbar _.
have /cyclicP[xbar defH1]: cyclic H1 by rewrite prime_cyclic ?oH1.
have H1xbar: xbar \in H1 by rewrite defH1 cycle_id.
have sH1_Hbar: H1 \subset Hbar.
  by rewrite -[Hbar]defHbar (bigD1 1%g) ?group1 ?conjsg1 ?joing_subl.
have{sH1_Hbar} Hxbar: xbar \in Hbar := subsetP sH1_Hbar xbar H1xbar.
have /morphimP[x nH0x Hx /= Dxbar] := Hxbar.
have{oH1} oxbar: #[xbar] = p by rewrite orderE -defH1.
have memH0: {in H &, forall y z, [~ y, z] \in H0}.
  by rewrite defH'; apply: mem_commg.
have [_ /centsP-cHH0hat] := subsetIP sH0hatZ; move/subsetP in nQH.
pose D y z := [~ hat z, hat y].
have D_H0_1 y z: y \in H -> z \in H0 -> D y z = 1%g.
  by move=> Hy H0z; apply/eqP/commgP/cHH0hat; apply: mem_quotient.
have H0_D: {in H &, forall y z, D y z \in H0hat}.
  by move=> y z Hy Hz; rewrite -defHhat' mem_commg ?mem_quotient.
have Dsym y z: (D y z)^-1%g = D z y by rewrite invg_comm.
have Dmul y: y \in H -> {in H &, {morph D y: z t / z * t}}%g.
  move=> Hy z t Hz Ht; rewrite {1}/D morphM ?nQH // commMgR; congr (_ * _)%g.
  by rewrite -{2}morphR ?nQH // -/(D t _) D_H0_1 ?memH0 // mulg1.
pose Dm y Hy : {morphism H >-> coset_of Q} := Morphism (Dmul y Hy).
have{D_H0_1} kerDmH0 y Hy: H0 \subset 'ker (Dm y Hy).
  by rewrite subsetI sH0H; apply/subsetP=> z H0z; rewrite !inE /= D_H0_1.
pose x_ w := (x ^ w)%g; pose xbar_ w := (xbar ^ bar w)%g.
move/subsetP in nHW1; move/subsetP in nHU.
have Hx_ w: w \in W1 -> (x_ w \in H) * {in U, forall u, x_ w ^ u \in H}%g.
  by move/nHW1=> nHw; split=> [|u /nHU-nHu]; rewrite !memJ_norm.
have Dx: {in H &, forall y z, {in W1, forall w, D (x_ w) y = 1} -> D y z = 1}%g.
  move=> y z Hy Hz Dxy1; apply/(kerP (Dm y Hy) Hz); apply: subsetP z Hz.
  rewrite -(quotientSGK nH0H) ?kerDmH0 // -defHbar gen_subG.
  apply/bigcupsP=> _ /morphimP[w nH0w W1w ->] /=.
  rewrite defH1 Dxbar -quotient_cycle -?quotientJ ?quotientS // -cycleJ.
  by rewrite cycle_subG !inE /= Hx_ //= -Dsym eq_invg1 Dxy1.
pose ntrivD := [exists w in [predX W1 & W1], #[D (x_ w.1) (x_ w.2)] == p].
have{ntrivD Dx} /exists_inP[[w1 w2] /andP/=[Ww1 Ww2] /eqP-oDx12]: ntrivD.
  apply: contraR ntH0hat => Dx_1; rewrite -defHhat' -subG1 gen_subG.
  apply/subsetP=> _ /imset2P[_ _ /morphimP[y ? Hy ->] /morphimP[z ? Hz ->] ->].
  apply/set1P/Dx=> // w2 Ww2; rewrite Dx ?Hx_ // => w1 Ww1.
  have abelH0hat: p.-abelem H0hat by apply: prime_abelem.
  apply: contraNeq Dx_1 => /(abelem_order_p abelH0hat)oDx12.
  by apply/exists_inP; exists (w1, w2); rewrite ?inE ?Ww1 // oDx12 ?H0_D ?Hx_.
have /subsetP-nUW1bar: (W1 / H0)%g \subset 'N(Ubar) := quotient_norms H0 nUW1.
move/subsetP in nH0H; move/subsetP in nH0W1.
pose n (phi : {morphism Ubar >-> {unit 'F_p}}) ubar : nat := val (phi ubar).
have [phi Dphi]: {phi | {in Ubar, forall ub, xbar ^ ub =xbar ^+ n phi ub}}%g.
  pose xbar_Autm := invm (injm_Zp_unitm xbar).
  have /restrmP[phi [Dphi _ _ _]]: Ubar \subset 'dom (xbar_Autm \o conj_aut H1).
    by rewrite -sub_morphim_pre //= im_Zp_unitm -defH1 Aut_conj_aut.
  rewrite /n pdiv_id // -oxbar; exists phi => ubar /(subsetP nH1Ubar)Uubar.
  transitivity (Zp_unitm (phi ubar) xbar); last by rewrite autE /= -?defH1.
  by rewrite Dphi invmK ?im_Zp_unitm -?defH1 ?Aut_aut ?norm_conj_autE.
pose QV ubar w := (ubar ^ (bar w)^-1)%g.
have UbarQV: {in Ubar & W1, forall ubar w, QV ubar w \in Ubar}.
  by move=> ub w Uub W1w; rewrite /= memJ_norm ?groupV ?nUW1bar ?mem_quotient.
pose phi_ w ub := phi (QV ub w); pose nphi_ w ub := n phi (QV ub w).
have xbarJ: {in W1 & Ubar, forall w ub, xbar_ w ^ ub = xbar_ w ^+ nphi_ w ub}%g.
  by move=> w ubar * /=; rewrite -conjgM conjgCV conjgM Dphi ?UbarQV // conjXg.
have{oDx12} phi_w12 ubar: ubar \in Ubar -> (phi_ w1 ubar * phi_ w2 ubar = 1)%g.
  pose n_u := nphi_ ^~ ubar => Uubar; have [u nH0u Uu Dubar] := morphimP Uubar.
  suffices: n_u w1 * n_u w2 == 1 %[mod #[D (x_ w1) (x_ w2)]].
    by apply: contraTeq; rewrite oDx12 -!val_Fp_nat // natrM !natr_Zp.
  have DXn: {in H & W1, forall y w, D y (x_ w) ^+ n_u w = D y (x_ w ^ u)}%g.
    move=> y w Hy W1w; set z := x_ w; have [Hz /(_ u Uu) Hzu] := Hx_ w W1w.
    rewrite -(morphX (Dm y Hy)) //; apply/rcoset_kerP; rewrite ?groupX //.
    have /subsetP: H0 :* z ^ u \subset 'ker (Dm y Hy) :* z ^ u by rewrite mulSg.
    apply; apply/rcoset_kercosetP; rewrite ?groupX ?nH0H //.
    by rewrite morphX ?morphJ ?(nH0W1 w) // ?nH0H //= -Dubar -Dxbar xbarJ.
  rewrite -eq_expg_mod_order -{1}Dsym expgM expgVn ?(DXn, Dsym) ?Hx_ //.
  rewrite /D -!morphR ?nQH ?Hx_ // -conjRg (conjg_fixP _) //. 
  by apply/commgP/esym/(centsP cH0U); rewrite ?memH0 ?Hx_.
pose wbar := bar (w1 * w2 ^-1)%g; pose W1bar := (W1 / H0)%g.
have W1wbar: wbar \in W1bar by rewrite mem_quotient ?groupM ?groupV.
have{phi_w12} phiJ: {in Ubar, forall ubar, phi (ubar ^ wbar) = (phi ubar)^-1}%g.
  move=> ubar Uubar; apply/esym/eqP; rewrite eq_invg_mul.
  rewrite [wbar]morphM ?morphV ?nH0W1 ?groupV // -{1}[ubar](conjgK (bar w1)).
  by rewrite conjgM phi_w12 // memJ_norm ?nUW1bar ?mem_quotient.
have coW1bar2: coprime #|W1bar| 2 by rewrite coprimen2 quotient_odd ?mFT_odd.
have coUbar2: coprime #|Ubar| 2 by rewrite coprimen2 quotient_odd ?mFT_odd.
have{wbar phiJ W1wbar} phiV: {in Ubar, forall ubar, phi ubar = (phi ubar)^-1}%g.
  move=> ubar Uubar; rewrite /= -phiJ // -(expgK coW1bar2 W1wbar) -expgM mul2n.
  elim: (expg_invn _ _) => [|k IHk]; first by rewrite conjg1.
  by do 2!rewrite expgSr conjgM phiJ ?memJ_norm ?nUW1bar ?groupX // ?invgK.
rewrite -[Hbar]defHbar gen_subG defH1; apply/bigcupsP=> _ /morphimP[w _ Ww ->].
rewrite -cycleJ cycle_subG -/(xbar_ _); apply/centP=> ubar Uubar; apply/commgP.
apply/conjg_fixP; rewrite xbarJ // /nphi_ -[QV _ w](expgK coUbar2) ?UbarQV //.
by rewrite /n !morphX ?groupX 1?expgS 1?{1}phiV ?UbarQV // mulVg expg1n.
Qed.

Let defU' : C :=: U'. Proof. by have [] := FTtype34_facts. Qed.
Let H0_1 : H0 :=: 1%g. Proof. by have [] := FTtype34_Fcore_kernel_trivial. Qed.

Lemma Ptype_Fcompl_kernel_cent : Ptype_Fcompl_kernel MtypeP :=: C.
Proof.
rewrite [Ptype_Fcompl_kernel MtypeP]unlock /= (group_inj H0_1).
by rewrite astabQ -morphpreIim -injm_cent ?injmK ?ker_coset ?norms1.
Qed.
Local Notation defC := Ptype_Fcompl_kernel_cent.

(* Character theory proper. *)

Let pddM := FT_prDade_hyp maxM MtypeP.
Let ptiWM : primeTI_hypothesis M HU defW := FT_primeTI_hyp MtypeP.
Let ctiWG : cyclicTI_hypothesis G defW := pddM.
Let ctiWM : cyclicTI_hypothesis M defW := prime_cycTIhyp ptiWM.

Local Notation sigma := (cyclicTIiso ctiWG).
Local Notation w_ i j := (cyclicTIirr defW i j).
Local Notation eta_ i j := (sigma (w_ i j)).
Local Notation mu_ := (primeTIred ptiWM).
Local Notation Idelta := (primeTI_Isign ptiWM).
Local Notation delta_ j := (primeTIsign ptiWM j).
Local Notation d := (FTtype345_TIirr_degree MtypeP).
Local Notation n := (FTtype345_ratio MtypeP).
Local Notation delta := (FTtype345_TIsign MtypeP).

Implicit Types zeta xi lambda : 'CF(M).

Let u := #|U / C|%g.
Let mu2_ i j := primeTIirr ptiWM i j.
Let etaW := map sigma (irr W).
Let eq_proj_eta (alpha gamma : 'CF(G)) := orthogonal (alpha - gamma) etaW.
Let eta_col j := \sum_i eta_ i j.
Let bridge0 zeta := mu_ 0 - zeta.

Let proj_col_eta j0 i j : '[eta_col j0, eta_ i j] = (j == j0)%:R.
Proof.
rewrite cfdot_suml (bigD1 i) //= cfdot_cycTIiso eqxx eq_sym.
by rewrite big1 ?addr0 // => k /negPf-i'k; rewrite cfdot_cycTIiso i'k.
Qed.

Let nirrW1 : #|Iirr W1| = q. Proof. by rewrite card_Iirr_cyclic. Qed.
Let NirrW1 : Nirr W1 = q. Proof. by rewrite -nirrW1 card_ord. Qed.

Let nirrW2 : #|Iirr W2| = p. Proof. by rewrite card_Iirr_cyclic. Qed.
Let NirrW2 : Nirr W2 = p. Proof. by rewrite -nirrW2 card_ord. Qed.

Let calT := seqIndT HU M.
Let S1 := S_ HC.
Let S2 := seqIndD HU M HC C.

Let sS10 : cfConjC_subset S1 calS.
Proof. by apply: seqInd_conjC_subset1; rewrite /= ?defMs. Qed.

Let sS20 : cfConjC_subset S2 calS.
Proof. by apply: seqInd_conjC_subset1; rewrite /= ?defMs. Qed.

Let scohS1 : subcoherent S1 tau R. Proof. exact: subset_subcoherent sS10. Qed.
Let scohS2 : subcoherent S2 tau R. Proof. exact: subset_subcoherent sS20. Qed.

Let S1_1 : {in S1, forall zeta, zeta 1%g = q%:R}.
Proof.
move=> _ /seqIndP[s /setDP[kerM'' _] ->]; rewrite !inE -defM'' in kerM''.
by rewrite cfInd1 ?gFsub // -(index_sdprod defM) lin_char1 ?mulr1 ?lin_irr_der1.
Qed.

Let cohS1 : coherent S1 M^# tau.
Proof.
apply: uniform_degree_coherence scohS1 _.
by apply/(@all_pred1_constant _ q%:R)/allP=> _ /=/mapP[zeta /S1_1<- ->].
Qed.

Let irrS1 : {subset S1 <= irr M}.
Proof.
move=> _ /seqIndP[s /setDP[kerHC kerHU] ->]; rewrite !inE in kerHC kerHU.
rewrite -(quo_IirrK _ kerHC) // mod_IirrE // cfIndMod // cfMod_irr //.
have /irr_induced_Frobenius_ker := FrobeniusWker frobMtilde; rewrite defM''.
by apply; rewrite quo_Iirr_eq0 // -subGcfker.
Qed.

Let o1S1 : orthonormal S1.
Proof. exact: sub_orthonormal (seqInd_uniq _ _) (irr_orthonormal _). Qed.

Let cfdotS1 : {in S1 &, forall zeta xi, '[zeta, xi] = (zeta == xi)%:R}.
Proof. by case/orthonormalP: o1S1. Qed.

Let omu2S1 i j : {in S1, forall zeta, '[mu2_ i j, zeta] = 0}.
Proof.
move=> zeta S1zeta; have [s _ Dzeta] := seqIndP S1zeta.
rewrite Dzeta -cfdot_Res_l cfRes_prTIirr cfdot_irr mulrb ifN_eq //.
apply: contraNneq (prTIred_not_irr ptiWM j) => Ds.
by rewrite -cfInd_prTIres Ds -Dzeta irrS1.
Qed.

Let Tmu j : mu_ j \in calT. Proof. by rewrite -cfInd_prTIres mem_seqIndT. Qed.

Let omuS1 j : {in S1, forall zeta,  '[mu_ j, zeta] = 0}.
Proof.
by move=> zeta S1zeta /=; rewrite cfdot_suml big1 // => i _; apply: omu2S1.
Qed.

Let Zbridge0 : {in S1, forall zeta, bridge0 zeta \in 'Z[irr M, HU^#]}.
Proof.
have mu0_1: mu_ 0 1%g = q%:R by rewrite prTIred_1 prTIirr0_1 mulr1.
move=> zeta S1zeta; rewrite /= zcharD1 !cfunE subr_eq0 mu0_1 S1_1 // eqxx. 
by rewrite rpredB ?(seqInd_vchar _ (Tmu 0)) ?(seqInd_vchar _ S1zeta).
Qed.

Let A0bridge0 : {in S1, forall zeta, bridge0 zeta \in 'CF(M, 'A0(M))}.
Proof. by move=> zeta /Zbridge0/zchar_on/cfun_onS->. Qed.

Let sS1S2' : {subset S1 <= [predC S2]}.
Proof.  
by move=> _ /seqIndP[s /setDP[kHCs _] ->]; rewrite !inE mem_seqInd // inE kHCs.
Qed.

Let defS2: S2 = seqIndD HU M H H0C.
Proof. by rewrite /S2 H0_1 -!joinGE join1G joinGC seqIndDY. Qed.

Let cohS2: coherent S2 M^# tau.
Proof.
apply: subset_coherent (Ptype_core_coherence maxM MtypeP notMtype5).
by rewrite defC defS2; apply: seqIndS; rewrite Iirr_kerDS ?genS ?setUS ?der_sub.
Qed.

Let Smu := [seq mu_ j | j in predC1 0].
Let Sred := filter [predC irr M] (seqIndD HU M H H0).

Let memSred : Sred =i Smu.
Proof.
have [szSred _ memSred _] := typeP_reducible_core_Ind maxM MtypeP notMtype5.
have uSred: uniq Sred by apply: filter_uniq (seqInd_uniq _ _).
suffices{uSred}: (size Smu <= size Sred)%N by case/leq_size_perm.
by rewrite szSred def_p size_map -cardE cardC1 nirrW2.
Qed.

Let mu_1 j : j != 0 -> mu_ j 1%g = (q * u)%:R.
Proof.
move=> nzj; have Smuj: mu_ j \in Sred by rewrite memSred image_f.
have [_ _ _ /(_ _ Smuj)[]] := typeP_reducible_core_Ind maxM MtypeP notMtype5.
by rewrite defC.
Qed.

Let memS2red : [predD S2 & irr M] =i Smu.
Proof.
move=> xi; rewrite defS2 -memSred mem_filter; apply: andb_id2l => /= red_xi.
apply/idP/idP=> [|Sxi]; first by apply: seqIndS; rewrite Iirr_kerDS ?joing_subl.
have [_ _ _ /(_ xi)] := typeP_reducible_core_Ind maxM MtypeP notMtype5.
by rewrite defC mem_filter /= red_xi; case.
Qed.

Let i1 : Iirr W1 := inord 1.
Let nz_i1 : i1 != 0. Proof. by rewrite Iirr1_neq0. Qed.
Let j1 : Iirr W2 := inord 1.
Let nz_j1 : j1 != 0. Proof. by rewrite Iirr1_neq0. Qed.

(* This is Peterfalvi (11.8). *)
(* We have rearranged the argument somewhat:                                  *)
(* - Step (11.8.4) was out of sequence as it involves changing the definition *)
(*   of tau2, which requires showing that (11.8.2-3) are preserved by this    *)
(*   change; since (11.8.4) does not use (11.8.2-3) we avoid this by proving  *)
(*   (11.8.4) first.                                                          *)
(* - The first part of step (11.8.3) is the last fact that needs to be proved *)
(*   for an arbitrary j != 0; (11.8.1, 5-6) can all use the same fixed j != 0 *)
(*   (we take j = 1), provided (11.8.3) is proved before (11.8.2), which it   *)
(*   doe not use.                                                             *)
(* - Steps (11.8.2) and (11.8.5) are really as combination, to provide an     *)
(*   expression for tau (alpha i j) for an arbitrary i. We merge their proofs *)
(*   so we can use a fixed i for the whole combined step and hide some        *)
(*   intermediate technical facts.                                            *)
(* - We also reorganise the contents of the superstep, proving most of        *)
(*   (11.8.5) between the first and last two parts of (11.8.2); this          *)
(*   simplifies the latter because a is then known to be even, so we can show *)
(*   directly that a is 0 or 2, and then that X = eta i j - eta i 0.          *)
Lemma FTtype34_not_ortho_cycTIiso zeta :
  zeta \in S1 -> ~~ eq_proj_eta (tau (bridge0 zeta)) (eta_col 0).
Proof.
move=> S1zeta; set psi := tau _; apply/negP=> proj_psi_eta.
have irr_zeta: zeta \in irr M := irrS1 S1zeta.
have Szeta: zeta \in S_ 1 by apply: seqInd_sub S1zeta.
have Zzeta_S1: {in S1, forall xi, zeta - xi \in 'Z[S1, M^#]}.
  by move=> * /=; rewrite zcharD1E rpredB ?mem_zchar //= !cfunE !S1_1 ?subrr.
have n1S1: {in S1, forall xi, '[xi] = 1} by move=> xi /irrS1/irrWnorm.
have Z_S1: {in S1, forall xi, xi \in 'Z[S1]} by apply: mem_zchar.
have [p_gt0 q_gt0 u_gt0]: [/\ p > 0, q > 0 & u > 0]%N by rewrite !cardG_gt0.
have q_gt2: (q > 2)%N by rewrite odd_prime_gt2 ?mFT_odd.
have mu2_1 i j: j != 0 -> mu2_ i j 1%g = d%:R.
  by have [/(_ i j)] := FTtype345_constants maxM MtypeP notMtype2.
(* This is (11.8.1). *)
have [Dd delta1 Dn]: [/\ d = u, delta = 1 & n = (size S1)%:R].
  have size_S1 : (size S1 * q = u - 1)%N.
    rewrite mulnC [q](index_sdprod defM).
      rewrite (size_irr_subseq_seqInd _ (subseq_refl _)) //.
    transitivity #|[set mod_Iirr t | t : Iirr (HU / HC) in predC1 0]|.
      apply/eq_card=> s; rewrite inE mem_seqInd // !inE subGcfker.
      apply/andP/imsetP=> [[nzs kHCs] | [t nzt ->]].
        by exists (quo_Iirr HC s); rewrite ?quo_IirrK // inE quo_Iirr_eq0.
      by rewrite mod_Iirr_eq0 // mod_IirrE // cfker_mod.
    rewrite card_imset; last exact: can_inj (mod_IirrK _).
    have isoUC: U / C \isog HU / HC by apply: quotient_sdprodr_isog.
    rewrite subn1 cardC1 card_Iirr_abelian -?(card_isog isoUC) //.
    by rewrite -(isog_abelian isoUC) defU' der_abelian.
  have Dd: d = u.
    apply/eqP; rewrite -(eqn_pmul2l q_gt0) -eqC_nat -(mu_1 nz_j1).
    by rewrite natrM prTIred_1 mu2_1.
  suffices delta1: delta = 1.
    by rewrite /n Dd delta1 -(@natrB _  _ 1) // -size_S1 natrM mulfK ?neq0CG.
  have: (delta == 1 %[mod q])%C.
    rewrite -(eqCmod_transl _ (prTIirr1_mod ptiWM 0 j1)) mu2_1 // -/q Dd.
    by rewrite /eqCmod -(@natrB _ u 1) // dvdC_nat -size_S1 dvdn_mull.
  rewrite -[1]subr0 [delta]signrE -/ptiWM eqCmodDl eqCmodN opprK.
  by rewrite eqCmod0_nat; case: (Idelta j1); first rewrite gtnNdvd.
have deltaZ gamma: delta *: gamma = gamma by rewrite delta1 scale1r.
have [tau1 coh_tau1] := cohS1; pose zeta1 := tau1 zeta.
(* This is (11.8.4). *)
without loss Dpsi: tau1 coh_tau1 @zeta1 / psi = eta_col 0 - zeta1.
  move=> IHtau1; have [[Itau1 Ztau1] Dtau1] := coh_tau1.
  have tau1_dirr: {in S1, forall xi, tau1 xi \in dirr G}.
    by move=> xi S1xi; rewrite /= dirrE Ztau1 ?Itau1 ?mem_zchar //= n1S1.
  pose chi : 'CF(G) := eta_col 0 - psi.
  have Dpsi: psi = eta_col 0 - chi by rewrite opprD opprK addNKr.
  have chi'zeta1: chi <> zeta1.
    by move=> Dchi; case: (IHtau1 tau1); rewrite -/zeta1 -?Dchi.
  have dirr_chi: chi \in dirr G.
    apply: dirr_norm1.
      rewrite rpredB ?rpred_sum // => [i _|]; first exact: cycTIiso_vchar.
      rewrite Dade_vchar // zchar_split A0bridge0 //.
      by rewrite rpredB ?char_vchar ?prTIred_char ?irrWchar.
    apply: (addrI q%:R); transitivity '[psi]; last first.
      rewrite Dade_isometry ?A0bridge0 // (cfnormBd (omuS1 _ _)) //. 
      by rewrite cfnorm_prTIred n1S1.
    rewrite Dpsi [RHS]cfnormDd; last first.
      rewrite opprB cfdotC cfdot_sumr big1 ?conjC0 // => i _.
      by rewrite (orthoPl proj_psi_eta) ?map_f ?mem_irr.
    rewrite cfnormN -nirrW1 -sumr_const cfdot_sumr.
    by congr (_ + _); apply: eq_bigr => i _; rewrite proj_col_eta.
  have Dchi: {in S1, forall xi, xi != zeta -> chi = - tau1 xi}.
    move=> xi S1xi /negPf-zeta'xi; have irr_xi := irrS1 S1xi.
    suffices: '[zeta1 - tau1 xi, chi] = 1.
      by case/cfdot_add_dirr_eq1; rewrite ?rpredN ?tau1_dirr.
    rewrite /= cfdotBr cfdot_sumr big1 => [|i _]; last first.
      have oS1eta := coherent_ortho_cycTIiso MtypeP sS10 coh_tau1.
      by rewrite cfdotBl !oS1eta ?irrS1 ?subrr.
    rewrite -raddfB Dtau1 ?Zzeta_S1 // Dade_isometry ?A0bridge0 //; last first.
      exact: cfun_onS sHU_A0 (zcharD1_seqInd_on _ (Zzeta_S1 xi S1xi)).
    rewrite cfdotBr cfdotC cfdotBr 2?omuS1 // subrr conjC0 !sub0r opprK.
    by rewrite cfdotBl n1S1 // cfdotS1 // zeta'xi subr0.
  have S1zetaC: zeta^*%CF \in S1 by rewrite cfAut_seqInd.
  have Dchi_zetaC: chi = - tau1 zeta^*%CF.
    by rewrite -Dchi ?(seqInd_conjC_neq _ _ _ S1zeta) ?mFT_odd.
  suffices S1le2: (size S1 <= size [:: zeta; zeta^*%CF])%N.
    case: (IHtau1 (dual_iso tau1)); last by rewrite /= -Dchi_zetaC.
    exact: dual_coherence scohS1 coh_tau1 S1le2.
  rewrite uniq_leq_size ?seqInd_uniq // => xi S1xi.
  rewrite !inE -implyNb; apply/implyP=> zeta'xi; apply/eqP.
  apply: (Zisometry_inj Itau1); rewrite ?mem_zchar ?cfAut_seqInd //.
  by apply: oppr_inj; rewrite -Dchi.
have [[Itau1 Ztau1] Dtau1] := coh_tau1.
have tau1_dirr: {in S1, forall xi, tau1 xi \in dirr G}.
  by move=> xi S1xi; rewrite /= dirrE Ztau1 ?Itau1 ?mem_zchar //= n1S1.
have oS1eta i j: {in S1, forall xi, '[tau1 xi, eta_ i j] = 0}.
  by move=> xi S1xi /=; rewrite (coherent_ortho_cycTIiso _ _ coh_tau1) ?irrS1.
pose alpha_ := FTtype345_bridge MtypeP zeta.
have A0alpha i j : j != 0 -> alpha_ i j \in 'CF(M, 'A0(M)).
  by move/supp_FTtype345_bridge->; rewrite ?S1_1.
have alpha_S1 i j: {in S1, forall xi, '[alpha_ i j, xi] = n *- (xi == zeta)}.
  move=> xi S1xi; rewrite /= !cfdotBl !cfdotZl !omu2S1 // mulr0 subrr add0r.
  by rewrite cfdotS1 // eq_sym mulr_natr.
pose beta_ i j := tau (alpha_ i j) - (eta_ i j - eta_ i 0) + n *: zeta1.
pose beta := beta_ 0 j1.
(* This is the first part of (11.8.3). *)
have betaE i j: j != 0 -> beta_ i j = beta.
  move=> nz_j; transitivity (beta_ i j1); congr (_ + _); apply/eqP.
    rewrite eq_sym -subr_eq0 [rhs in _ + rhs]opprD addrACA -opprD subr_eq0.
    rewrite -linearB /= !opprB !addrA !subrK -!/(mu2_ i _).
    by rewrite [Dade pddM _]prDade_sub_TIirr ?mu2_1 //= deltaZ.
  rewrite -subr_eq0 !opprD addrACA -3!opprD opprK subr_eq0 addrACA addrA.
  rewrite -(prDade_sub2_TIirr pddM) -!/(mu2_ _ _) !deltaZ -linearB /=.
  by rewrite opprB addrA subrK !deltaZ opprD opprK addrACA addrA.
pose j := j1. (* The remainder of the proof only uses j = 1. *)
(* This is the second part of (11.8.3). *)
have Rbeta: cfReal beta.
  rewrite /cfReal eq_sym -subr_eq0 rmorphD !rmorphB /= opprB 2!opprD opprB -/j.
  rewrite 2![(eta_ 0 _)^*%CF]cfAut_cycTIiso -!cycTIirr_aut !aut_Iirr0 -Dade_aut.
  set k := aut_Iirr conjC j; rewrite -(betaE 0 k) ?aut_Iirr_eq0 // addrACA.
  rewrite addrC addr_eq0 addrCA subrK opprD opprK Dn raddfZnat -!raddfB /= -Dn. 
  apply/eqP; rewrite (cfConjC_Dade_coherent coh_tau1) ?mFT_odd // -raddfB.
  rewrite Dtau1 ?Zzeta_S1 ?cfAut_seqInd //= -linearZ scalerBr; congr (tau _).
  rewrite opprD !rmorphB !deltaZ /= -!prTIirr_aut !aut_Iirr0 addrACA subrr.
  by rewrite add0r opprK addrC Dn -raddfZnat.
(* This is the consequence of Peterfalvi (11.8.2) and (11.8.5). *)
have tau_alpha i: tau (alpha_ i j) = eta_ i j - eta_ i 0 - n *: zeta1.
  set phi := tau (alpha_ i j); pose sum_tau1 := \sum_(xi <- S1) tau1 xi.
  have A0alpha_j k: alpha_ k j \in 'CF(M, 'A0(M)) by apply: A0alpha.
  have Zphi: phi \in 'Z[irr G].
    by rewrite Dade_vchar // zchar_split vchar_FTtype345_bridge /=.
  have [Y S1_Y [X [Dphi oYX oXS1]]] := orthogonal_split (map tau1 S1) phi.
  (* This is the first part of 11.8.2 *)
  have [a Za defY]: exists2 a, a \in Cint & Y = a *: sum_tau1 - n *: zeta1.
    have [a_ Da defY] := orthonormal_span (map_orthonormal Itau1 o1S1) S1_Y.
    have{Da} Da: {in S1, forall xi, a_ (tau1 xi) = '[phi, tau1 xi]}.
      by move=> xi Sxi; rewrite Da Dphi cfdotDl (orthoPl oXS1) ?map_f ?addr0.
    exists (a_ (tau1 zeta) + n).
      by rewrite Dn rpredD ?rpred_nat // Da // Cint_cfdot_vchar ?Ztau1 ?Z_S1.
    rewrite defY big_map scaler_sumr !(bigD1_seq _ S1zeta) ?seqInd_uniq //=.
    rewrite addrAC scalerDl addrK !(big_seq_cond (predC1 _)) /=; congr (_ + _).
    apply: eq_bigr => xi /andP[S1xi zeta'xi]; congr (_ *: _); rewrite !Da //.
    apply: canRL (addNKr _) _; rewrite addrC -opprB -!raddfB Dtau1 ?Zzeta_S1//=.
    rewrite Dade_isometry //; last first.
      exact: cfun_onS (zcharD1_seqInd_on _ (Zzeta_S1 _ S1xi)).
    by rewrite cfdotBr !alpha_S1 // !mulrb eqxx ifN_eq // !(addr0, opprK).
  have psi_phi: '[psi, phi] = -1 + n. (* This is part of (11.8.5). *)
    rewrite cfdotC Dade_isometry ?A0bridge0 //.
    rewrite cfdotBr !cfdotBl deltaZ !cfdotZl n1S1 // mulr1.
    rewrite !cfdot_prTIirr_red (negPf nz_j1) eqxx !omu2S1 //= cfdotC omuS1 //.
    by rewrite conjC0 mulr0 opprB !subr0 add0r rmorphD rmorphN Dn !rmorph_nat.
  have{psi_phi} col0_beta: '[eta_col 0, beta] = a. (* Also part of (11.8.5). *)
    apply/(addIr (-1 + n))/(canRL (addNKr _)).
    rewrite addrCA addrA addrACA -{}psi_phi Dpsi cfdotBl; congr (_ + _).
      rewrite -(betaE i j) // cfdotDr !cfdotBr -/phi cfdotZr -!addrA.
      apply/(canLR (addNKr _)); rewrite addNr !cfdot_suml.
      rewrite big1 ?add0r ?opprK => [|k _]; last first.
        by rewrite cfdot_cycTIiso andbC eq_sym (negPf nz_j1).
      rewrite addrCA big1 ?mulr0 ?add0r => [|k _]; last first.
        by rewrite cfdotC oS1eta ?conjC0.
      rewrite addrC (bigD1 i) // cfnorm_cycTIiso /= addKr big1 // => k i'k.
      by rewrite cfdot_cycTIiso (negPf i'k).
    rewrite cfdotC Dphi cfdotDl (orthoPl oXS1) ?map_f // addr0.
    rewrite defY cfdotBl scaler_sumr cfproj_sum_orthonormal //.
    rewrite cfdotZl Itau1 ?mem_zchar ?n1S1 // mulr1 rmorphB opprD opprK.
    by rewrite Dn rmorph_nat conj_Cint.
    have a_even: (2 %| a)%C. (* Third internal part of (11.8.5). *)
    have Zbeta: beta \in 'Z[irr G].
      rewrite -{1}(betaE i j) // rpredD ?rpredB ?Zphi ?cycTIiso_vchar //.
      by rewrite Dn rpredZnat // Ztau1 ?mem_zchar.
    rewrite -col0_beta cfdot_real_vchar_even ?mFT_odd //; first 1 last.
      split; first by apply/rpred_sum=> k _; apply: cycTIiso_vchar.
      apply/eqP; rewrite [RHS](reindex_inj (can_inj (@conjC_IirrK _ _))) /=.
      rewrite rmorph_sum; apply/eq_bigr=> k _ /=.
      by rewrite cfAut_cycTIiso -cycTIirr_aut aut_Iirr0.
    have eta00: eta_ 0 0 = 1 by rewrite cycTIirr00 cycTIiso1.
    rewrite orbC cfdotDl 2!cfdotBl cfdotZl -eta00 oS1eta // mulr0 addr0.
    rewrite opprB addrC 2!{1}cfdot_cycTIiso (negPf nz_j1) subr0 /= eta00.
    rewrite Dade_reciprocity // => [|x _ y _]; last by rewrite !cfun1E !inE.
    rewrite cfRes_cfun1 !cfdotBl deltaZ !cfdotZl -!/(mu2_ 0 _).
    rewrite -(prTIirr00 ptiWM) !cfdot_prTIirr cfdotC omu2S1 // conjC0 mulr0.
    by rewrite (negPf nz_j1) add0r subr0 subrr rpred0.
  have nY: '[Y] = n * a * (a - 2%:R) + n ^+ 2. (* Resuming step (11.8.2). *)
    rewrite defY cfnormD cfnormN !cfnormZ cfdotNr cfdotZr.
    rewrite cfnorm_map_orthonormal // -Dn Itau1 ?mem_zchar ?n1S1 // mulr1.
    rewrite scaler_sumr cfproj_sum_orthonormal // rmorphN addrAC.
    rewrite Dn rmorphM !Cint_normK ?rpred_nat // !rmorph_nat conj_Cint // -Dn.
    by rewrite -mulr2n mulrC mulrA -mulr_natr mulNr -mulrBr.
  have{a_even} Da: (a == 0) || (a == 2%:R). (* Second part of (11.8.2). *)
    suffices (b := a - 1): b ^+ 2 == 1.
      by rewrite -!(can_eq (subrK 1) a) add0r addrK orbC -eqf_sqr expr1n.
    have S1gt0: (0 < size S1)%N by case: (S1) S1zeta.
    have: n * b ^+ 2 <= n *+ 3.
      have: 2%:R + n <= n *+ 3 by rewrite addrC ler_add2l ler_muln2r Dn ler1n.
      apply: ler_trans; rewrite sqrrB1 -mulr_natr -mulrBr mulrDr mulrA mulr1.
      rewrite ler_add2r -(ler_add2r (n ^+ 2 + '[X])) !addrA -nY -cfnormDd //.
      by rewrite -Dphi norm_FTtype345_bridge ?S1_1 // ler_addl cfnorm_ge0.
    have Zb: b \in Cint by rewrite rpredB ?rpred1 ?Za.
    have nz_b: b != 0 by rewrite subr_eq0 (memPn _ a a_even) ?(dvdC_nat 2 1).
    rewrite eqr_le sqr_Cint_ge1 {nz_b}//= andbT -Cint_normK // Dn -mulrnA.
    have /CnatP[m ->] := Cnat_norm_Cint Zb; rewrite -natrX -natrM leC_nat.
    by rewrite leq_pmul2l // lern1 -ltnS (ltn_sqr m 2) (leq_sqr m 1).
  have{nY Da} defX: X = eta_ i j - eta_ i 0. (* Last part of (11.8.2). *)
    have{nY Da} /eqP-nY: '[Y] == n ^+ 2.
      by rewrite -subr_eq0 nY addrK -mulrA !mulf_eq0 !subr_eq0 Da orbT.
    have coh_zeta_phi := FTtype345_bridge_coherence _ _ Szeta _ coh_tau1.
    have:= Dphi; rewrite addrC => /coh_zeta_phi->; rewrite ?S1_1 ?deltaZ //.
    rewrite defY scaler_sumr big_seq rpredB ?rpred_sum // => [xi Sxi|].
      by rewrite rpredZ_Cint ?mem_zchar ?map_f.
    by rewrite Dn rpredZnat ?mem_zchar ?map_f.
  have{col0_beta} a0: a = 0. (* This is the conclusion of (11.8.5). *)
    rewrite cfdot_suml big1 // in col0_beta => k _.
    rewrite -(betaE i j) // /beta_ -/phi Dphi -defX addrK defY subrK.
    rewrite cfdotZr cfdot_sumr big1_seq ?mulr0 // => xi S1xi.
    by rewrite cfdotC oS1eta ?conjC0.
  by rewrite Dphi defY defX a0 ?inE ?eqxx // scale0r sub0r addrC.
(* This is step (11.8.6). *)
pose theta := mu_ j - d%:R *: zeta.
have /andP/=[red_muj S2muj]: mu_ j \in [predD S2 & irr M].
  by rewrite memS2red image_f.
have HUtheta: theta \in 'CF(M, HU^#).
  rewrite cfun_onD1 !cfunE mu_1 ?S1_1 // Dd mulrC natrM subrr eqxx.
  by rewrite rpredB ?rpredZ ?(seqInd_on _ S1zeta) ?(seqInd_on _ S2muj).
have Dtheta: theta = mu_ 0 - zeta + \sum_i alpha_ i j.
  rewrite !sumrB -scaler_sumr delta1 scale1r.
  rewrite [X in _ = X]addrC -!addrA -/(mu_ 0); congr (_ + _).
  rewrite [X in _ = _ + X]addrC !addrA addNr add0r -opprD; congr (- _).
  rewrite sumr_const nirrW1 -scaler_nat scalerA mulrC.
  by rewrite divfK ?neq0CG // delta1 addrC scalerBl scale1r subrK.
have tau_theta: tau theta = eta_col j - d%:R *: zeta1.
  pose psi1 i := eta_ i j1 - eta_ i 0 - n *: zeta1.
  have Dpsi1 i: tau (alpha_ i j) = psi1 i by apply: tau_alpha.
  rewrite Dtheta [tau _]raddfD raddf_sum (eq_bigr psi1) //= {Dpsi1}/psi1 -/psi.
  rewrite Dpsi !sumrB  [X in X = _]addrC -!addrA; congr (_ + _).
  rewrite -opprB -opprD -opprB -/(eta_col 0) addrA addrK; congr (- _).
  rewrite sumr_const nirrW1 -scaler_nat scalerA mulrC.
  by rewrite divfK ?neq0CG // delta1 scalerBl scale1r subrK.
have [tau2 coh_tau2] := cohS2.
without loss tau2muj: tau2 coh_tau2 / tau2 (mu_ j) = eta_col j; last first.
  case: FTtype34_noncoherence; rewrite H0_1 -joinGE join1G.
  have uS12: uniq (S2 ++ S1).
    by rewrite cat_uniq ?seqInd_uniq ?andbT //=; apply/hasPn.
  have /perm_eq_coherent: perm_eq (S2 ++ S1) (S_ C); last apply.
    apply: uniq_perm_eq; rewrite ?seqInd_uniq // => xi; rewrite mem_cat.
    apply/idP/idP=> [/orP | /seqIndP[i /setDP[kCi k'HUi] ->]].
      by case; apply/seqIndS/Iirr_kerDS; rewrite ?joing_subr.
    by rewrite !mem_seqInd // inE orbC inE kCi k'HUi andbT orbN.
  move: tau_theta; rewrite -tau2muj // -raddfZnat.
  apply: (bridge_coherent scohM) sS20 coh_tau2 sS10 coh_tau1 sS1S2' _. 
  by rewrite (cfun_onS _ HUtheta) ?setSD // rpredZnat ?Z_S1.
move=> IHtau2; apply: (IHtau2 tau2 coh_tau2); have [IZtau2 Dtau2] := coh_tau2.
have{IHtau2} /hasP[xi S2xi /=irr_xi]: has [mem irr M] S2.
  apply/hasPn=> redS2 {tau2 coh_tau2 IZtau2 Dtau2}.
  have muS2: {subset S2 <= Smu} by move=> xi S2xi; rewrite -memS2red !inE redS2.
  have [_ [tau2 tau2mu coh_tau2]] := uniform_prTIred_coherent pddM nz_j1.
  have S2uniform: {subset S2 <= uniform_prTIred_seq pddM j}.
    move=> _ /muS2/imageP[k nz_k ->]; apply: image_f.
    by rewrite !inE [_ != 0]nz_k /= !mu_1.
  apply: (IHtau2 tau2); first exact: subset_coherent_with coh_tau2.
  have [_ /(_ _ nz_j1) Ez _ _] := FTtype345_constants maxM MtypeP notMtype2.
  by have:= tau2mu j; rewrite Ez -/delta delta1 scale1r.
suffices: '[tau2 (mu_ j), eta_col j] != 0.
  have:= FTtypeP_coherent_TIred sS20 coh_tau2 irr_xi S2xi S2muj.
  case=> _ -> [[-> ->] | [-> -> _] /eqP[]]; first by rewrite deltaZ.
  rewrite -[cyclicTIiso _]/sigma cfdot_sumr big1 ?mulr0 // => i _.
  rewrite cfdotZl proj_col_eta -(inj_eq irr_inj) conjC_IirrE eq_sym.
  by rewrite odd_eq_conj_irr1 ?mFT_odd // irr_eq1 (negPf nz_j1) mulr0.
pose gamma := xi 1%g *: mu_ j - mu_ j 1%g *: xi.
have: '[tau2 gamma, tau theta] != 0.
  have [Txi Tzeta] := (seqInd_subT S2xi, seqInd_subT S1zeta).
  have S2gamma: gamma \in 'Z[S2, HU^#] by apply: sub_seqInd_zchar.
  rewrite Dtau2 ?zcharD1_seqInd //; move/zchar_on in S2gamma.
  rewrite Dade_isometry ?(cfun_onS sHU_A0) // cfdotBr cfdotZr !cfdotBl !cfdotZl.
  rewrite cfnorm_prTIred omuS1 // (seqInd_ortho _ _ S2muj) ?(memPn red_muj) //.
  rewrite (seqInd_ortho _ Txi) ?(memPn (sS1S2' _)) // !(mulr0, subr0) mulf_eq0.
  by rewrite char1_eq0 ?irrWchar // -cfnorm_eq0 irrWnorm ?oner_eq0 ?neq0CG.
apply: contraNneq => o_muj_etaj; rewrite {}tau_theta !{gamma}raddfB subr_eq0 /=.
have /CnatP[xi1 ->]: xi 1%g \in Cnat by rewrite Cnat_char1 ?irrWchar.
rewrite mu_1 // cfdotZr !cfdotBl !raddfZnat !cfdotZl {}o_muj_etaj cfdot_sumr.
have /orthogonalP oS2_S1: orthogonal (map tau2 S2) (map tau1 S1).
  exact: (coherent_ortho scohM) sS20 coh_tau2 sS10 coh_tau1 sS1S2'.
rewrite !oS2_S1 ?map_f // big1 ?(mulr0, subr0) // => k _.
exact: (coherent_ortho_cycTIiso _ _ coh_tau2).
Qed.

(* This is Peterfalvi (11.9). *)
(* Note that in the proof of part (a), the text improperly suggests using     *)
(* (5.3.b) to show then tau (zeta - zeta^alpha) is orthogonal to the eta i j. *)
(* Since alpha might not be conjugation, this is not obvious. Indeed the best *)
(* way to derive this is to use (5.5) together with the coherence of S(HC).   *)
(* In part (c) we start by reducing the proof to q <= p - 1; we also don't    *)
(* compute [tau (mu0 - zeta), tau2 lambda] = [chi, tau2 lambda] since this    *)
(* is not needed to prove than u = a: one only needs to show that the         *)
(* the left-hand side is an integer, which is in fact required to show that   *)
(* the right-hand is an integer.                                              *)
Lemma FTtype34_structure (eta0row := \sum_j eta_ 0 j) :
  [/\ (*a*) {in S1, forall zeta, eq_proj_eta (tau (bridge0 zeta)) eta0row},
      (*b*) (p < q)%N
    & (*c*) FTtype M == 3 /\ typeP_Galois MtypeP].
Proof.
have sum_etaW F: \sum_(eta <- etaW) F eta = \sum_i \sum_j F (eta_ i j).
  rewrite big_map big_tuple (reindex (dprod_Iirr defW)) /=.
    by rewrite pair_bigA; apply: eq_bigr => -[i j].
  by exists (inv_dprod_Iirr defW) => ij; rewrite ?dprod_IirrK ?inv_dprod_IirrK.
have bridgeS1: {in S1, forall zeta, eq_proj_eta (tau (bridge0 zeta)) eta0row}.
  move=> zeta S1zeta; set phi := bridge0 zeta; have irr_zeta := irrS1 S1zeta.
  have [X etaX [chi [Dchi oXchi o_chi_eta]]] := orthogonal_split etaW (tau phi).
  have [Isigma Zsigma] := cycTI_Zisometry ctiWG.
  have{o_chi_eta} o_chi_eta i j: '[chi, eta_ i j] = 0.
    by rewrite (orthoPl o_chi_eta) ?map_f ?mem_irr.
  have o1etaW: orthonormal etaW by rewrite map_orthonormal ?irr_orthonormal.
  have [a Da defX] := orthonormal_span o1etaW etaX; pose a_ := a (eta_ _ _).
  have{Da} Da i j: a_ i j = '[tau phi, eta_ i j].
    by rewrite Dchi cfdotDl o_chi_eta addr0 /a_ Da.
  have Zphi: phi \in 'Z[irr M, HU^#] by apply: Zbridge0.
  have A0phi: phi \in 'CF(M, 'A0(M)) by apply: A0bridge0.
  have a00_1 : a_ 0 0 = 1.
    rewrite Da cycTIirr00 [sigma 1]cycTIiso1.
    rewrite Dade_reciprocity // => [|x _ y _]; last by rewrite !cfun1E !inE.
    rewrite rmorph1 /= -(prTIirr00 ptiWM) -/(mu2_ 0 0) cfdotC.
    by rewrite cfdotBr cfdot_prTIirr_red omu2S1 // subr0 rmorph1.
  have aut_phi nu: cfAut nu (tau phi) = tau phi + tau (zeta - cfAut nu zeta).
    rewrite -Dade_aut !rmorphB !raddfB /= !addrA subrK.
    by rewrite -prTIred_aut aut_Iirr0.
  have Za i j: a_ i j \in Cint.
    rewrite Da Cint_cfdot_vchar ?cycTIiso_vchar //.
    by rewrite Dade_vchar ?(zchar_onS sHU_A0).
  have [tau1 coh_tau1] := cohS1; have [_ Dtau1] := coh_tau1.
  have o_tau1_eta := coherent_ortho_cycTIiso MtypeP sS10 coh_tau1.
  have a_aut nu i j: a (cfAut nu (eta_ i j)) = a_ i j.
    symmetry; transitivity '[cfAut nu (tau phi), cfAut nu (eta_ i j)].
      by rewrite cfdot_aut_vchar ?cycTIiso_vchar // -Da aut_Cint.
    rewrite aut_phi cfAut_cycTIiso -cycTIirr_aut [a _]Da cfdotDl addrC.
    rewrite -Dtau1 ?zcharD1_seqInd ?seqInd_sub_aut_zchar // raddfB cfdotBl.
    by rewrite !o_tau1_eta ?cfAut_seqInd ?cfAut_irr // subr0 add0r.
  pose a10 := a_ i1 0; pose a01 := a_ 0 j1; pose a11 := a_ i1 j1.
  have Da10 i: i != 0 -> a_ i 0 = a10.
    case/(cfExp_prime_transitive pr_q nz_i1) => k co_k_wi1 Dwi.
    rewrite -(cforder_dprodl defW) -dprod_IirrEl in co_k_wi1.
    have [[nu eta10nu] _] := cycTIiso_aut_exists ctiWG co_k_wi1.
    by rewrite /a_ dprod_IirrEl Dwi rmorphX /= -dprod_IirrEl eta10nu a_aut.
  have Da01 j: j != 0 -> a_ 0 j = a01.
    case/(cfExp_prime_transitive pr_p nz_j1) => k co_k_wj1 Dwj.
    rewrite -(cforder_dprodr defW) -dprod_IirrEr in co_k_wj1.
    have [[nu eta01nu] _] := cycTIiso_aut_exists ctiWG co_k_wj1.
    by rewrite /a_ dprod_IirrEr Dwj rmorphX /= -dprod_IirrEr eta01nu a_aut.
  have DaB1 i j: a_ i j = a_ i 0 + a_ 0 j - a_ 0 0.
    apply: (canRL (addrK _)); rewrite !Da cycTIiso_cfdot_exchange // => x Vx.
    have /setDP[A0x A'x]: x \in 'A0(M) :\: 'A(M).
      by rewrite (FTsupp0_typeP maxM MtypeP) // mem_class_support.
    by rewrite Dade_id // (cfun_on0 (zchar_on Zphi)) // -defA.
  pose p1 : algC := p.-1%:R; pose q1 : algC := q.-1%:R.
  have normX: '[X] = 1 + q1 * a10 ^+ 2 + p1 * a01 ^+ 2 + p1 * q1 * a11 ^+ 2.
    transitivity (\sum_i \sum_j a_ i j ^+ 2).
      rewrite defX cfnorm_sum_orthonormal // sum_etaW.
      by apply/eq_bigr=> i _; apply/eq_bigr=> j _; rewrite Cint_normK ?Za.
    rewrite -addrA addrACA (bigD1 0) //= (bigD1 0) //= a00_1 expr1n.
    rewrite -natrM !mulr_natl mulrnA -mulrnDl.
    rewrite -nirrW1 -nirrW2 -!(cardC1 0) -!sumr_const.
    congr (1 + _ + _); first by apply: eq_bigr => j /Da01->.
    apply: eq_bigr => i /Da10-Dai0; rewrite (bigD1 0) //= Dai0; congr (_ + _).
    by apply: eq_bigr => j /Da01-Da0j; rewrite DaB1 Dai0 Da0j -DaB1.
  have normX_le_q: '[X] <= q%:R.
    rewrite -(ler_add2r '[chi]) -cfnormDd // -Dchi -ler_subl_addl.
    have ->: '[tau phi] - q%:R = 1.
      rewrite Dade_isometry ?A0bridge0 // cfnormBd; last by rewrite omuS1.
      by rewrite cfnorm_prTIred cfdotS1 // eqxx addrC addKr.
    suffices: '[chi] != 0.
      suffices /CnatP[nchi ->]: '[chi] \in Cnat by rewrite ler1n lt0n -eqC_nat.
      rewrite Cnat_cfnorm_vchar // -(canLR (addKr _) Dchi) defX addrC rpredB //.
         by rewrite Dade_vchar // (zchar_onS (FTsupp_sub0 M)) ?defA.
       rewrite big_map big_seq rpred_sum // => _ /(cycTIirrP defW)[i [j ->]].
       by rewrite rpredZ_Cint ?Za ?cycTIiso_vchar.
    pose theta := zeta - zeta^*%CF.
    have Ztheta: theta \in 'Z[S1, HU^#] by apply: seqInd_sub_aut_zchar.
    have: '[tau phi, tau theta] != 0.
      rewrite Dade_isometry //; last by rewrite (cfun_onS _ (zchar_on Ztheta)).
      rewrite cfdotBl !cfdotBr ?omuS1 ?cfAut_seqInd // subr0 add0r oppr_eq0.
      rewrite irrWnorm // (seqInd_conjC_ortho _ _ _ S1zeta) ?mFT_odd //.
      by rewrite subr0 oner_eq0.
    rewrite cfnorm_eq0 Dchi; apply: contraNneq => ->; rewrite addr0 defX.
    rewrite -Dtau1 ?zcharD1_seqInd //.
    rewrite cfdot_suml big_map big1_seq // => _ /(cycTIirrP defW)[i [j ->]].
    apply/eqP; rewrite cfdotC fmorph_eq0 cfdotZr raddfB cfdotBl.
    by rewrite !o_tau1_eta ?cfAut_seqInd ?cfAut_irr // subrr mulr0.
  have a2_ge0 i j: 0 <= a_ i j ^+ 2 by rewrite -realEsqr Creal_Cint.
  have a11_0: a11 = 0.
    have: ('[X] < (2 * q.-1)%:R).
      rewrite (ler_lt_trans normX_le_q) // ltC_nat -subn1 mulnBr ltn_subRL.
      by rewrite !mul2n -!addnn ltn_add2r odd_prime_gt2 ?mFT_odd.
    apply: contraTeq => nz_a11; rewrite ler_gtF // normX ler_paddl //.
      by rewrite !mulr_natl ?addr_ge0 ?ler01 ?mulrn_wge0 ?a2_ge0.
    rewrite -mulr_natl -natrM ?ler_pmul ?natr_ge0 ?sqr_Cint_ge1 ?Za //.
    by rewrite leC_nat leq_mul // -subn1 ltn_subRL odd_prime_gt2 ?mFT_odd.
  rewrite a11_0 expr0n /= mulr0 addr0 in normX.
  have a10_a01: a10 + a01 = 1.
    by apply/eqP; rewrite -subr_eq0 -a00_1 -DaB1 -/a11 a11_0.
  have{o_chi_eta} o_chi_eta: orthogonal chi etaW.
    by apply/orthoPl=> _ /mapP[_ /(cycTIirrP defW)[i [j ->]] ->].
  have a10_0: a10 = 0.
    apply: contraNeq (FTtype34_not_ortho_cycTIiso S1zeta) => nz_a10.
    have a01_0: a01 = 0.
      apply: contraTeq normX_le_q => nz_a01; rewrite normX ltr_geF //.
      rewrite ltr_spaddr 1?mulr_gt0 ?ltr0n -?subn1 ?subn_gt0 ?prime_gt1 //.
        by rewrite ltr_def sqrf_eq0 nz_a01 a2_ge0.
      rewrite -ler_subl_addl -(natrB _ (prime_gt0 pr_q)) subn1 -mulr_natl.
      by rewrite ler_wpmul2l ?ler0n // sqr_Cint_ge1 ?Za.
    suffices <-: X = eta_col 0 by rewrite Dchi /eq_proj_eta addrC addKr.
    rewrite defX sum_etaW exchange_big (bigD1 0) //= addrC.
    rewrite big1 ?add0r => [|j nz_j]; first apply: eq_bigr => i _; last first.
      rewrite (bigD1 0) // [a _]Da01 //= a01_0 scale0r add0r big1 // => i nz_i.
      by rewrite [a _]DaB1 Da10 // Da01 // a10_a01 a00_1 subrr scale0r.
    have [-> | nz_i] := eqVneq i 0; first by rewrite [a _]a00_1 scale1r.
    by rewrite [a _]Da10 // (canRL (addrK _) a10_a01) a01_0 subr0 scale1r.
  suffices <-: X = eta0row by rewrite Dchi /eq_proj_eta addrC addKr.
  rewrite defX sum_etaW (bigD1 0) //= addrC.
  rewrite big1 ?add0r => [|i nz_i]; first apply: eq_bigr => j _; last first.
    rewrite (bigD1 0) // [a _]Da10 //= a10_0 scale0r add0r big1 // => j nz_j.
    by rewrite [a _]DaB1 Da10 // Da01 // a10_a01 a00_1 subrr scale0r.
  have [-> | nz_j] := eqVneq j 0; first by rewrite [a _]a00_1 scale1r.
  by rewrite [a _]Da01 // (canRL (addKr _) a10_a01) a10_0 oppr0 add0r scale1r.
have [zeta [irr_zeta Szeta zeta1]] := FTtypeP_ref_irr maxM MtypeP.
have{zeta1} [S1zeta zeta1]: zeta \in S1 /\ zeta 1%g = q%:R.
  split=> //; have [k nz_k Dzeta] := seqIndC1P Szeta.
  rewrite Dzeta mem_seqInd // !inE subGcfker nz_k -defM'' lin_char_der1 //.
  rewrite -mulr_natl Dzeta cfInd1 //= -(index_sdprod defM) in zeta1.
  by apply/andP; rewrite irr_char -(mulfI _ zeta1) ?neq0CG.
have{Szeta} ltpq: (p < q)%N.
  rewrite ltn_neqAle neq_pq leqNgt /=.
  apply: contra (FTtype34_not_ortho_cycTIiso S1zeta) => ltqp.
  case/(FTtype345_Dade_bridge0 _ MtypeP): Szeta => // chi [-> _ _ o_chi_eta].
  rewrite /eq_proj_eta addrC addKr (orthogonal_oppl chi).
  by apply/orthoPl=> _ /mapP[_ /(cycTIirrP defW)[i [j ->]] ->].
suffices galM: typeP_Galois MtypeP.
  have [_ [_ _ _ [/= cycUbar _ _]]] := typeP_Galois_P maxM notMtype5 galM.
  have{cycUbar} cycUbar: cyclic (U / U') by rewrite -defU' -defC.
  have nilU: nilpotent U by have [_ []] := MtypeP.
  case/orP: Mtype34 => // /(compl_of_typeIV maxM MtypeP)[_ /negP[]].
  exact/cyclic_abelian/cyclic_nilpotent_quo_der1_cyclic.
apply: contraLR ltpq => gal'M; rewrite -leqNgt (leq_trans _ (leq_pred _)) //.
have [_ _ _] := typeP_nonGalois_characters maxM notMtype5 gal'M.
case: (_ gal'M) => H1 /= [_ _ nH1U _ []]; set a := #|U : _| => a_gt1.
rewrite def_p -/q -defU' -defS2 => a_dv_p1 cycUhat _.
set irr_qa := [pred lambda in irr M | lambda 1%g == (q * a)%:R] => S2_qa.
have{S2_qa}/hasP[lambda S2lambda /andP[irr_lambda /eqP-lambda1]]: has irr_qa S2.
  have [a2_dv_pu] := S2_qa; rewrite has_count; apply: leq_trans.
  rewrite -(@ltn_pmul2r (a ^ 2 * #|C|)); last first.
    by rewrite !muln_gt0 (ltnW a_gt1) cardG_gt0.
  by rewrite mul0n divnK // muln_gt0 cardG_gt0 -subn1 subn_gt0 prime_gt1.
have{nH1U cycUhat} a_dv_u: a %| u.
  rewrite /u card_quotient ?normal_norm // indexgS // defU'.
  rewrite der1_min ?cyclic_abelian // normsI ?normG //.
  by rewrite (subset_trans nH1U) // astab_norm.
pose j := j1; pose psi := mu_ j - (u %/ a)%:R *: lambda.
have /andP/=[red_muj S2muj]: mu_ j \in [predD S2 & irr M].
  by rewrite memS2red image_f.
have S2psi: psi \in 'Z[S2, M^#].
  rewrite zcharD1E rpredB ?rpredZnat ?mem_zchar //=.
  by rewrite !cfunE mu_1 // lambda1 -natrM mulnCA divnK ?subrr.
pose phi := tau (mu_ 0 - zeta).
have o_phi_psi: '[phi, tau psi] = 0.
  have Apsi: psi \in 'CF(M, 'A(M)) by rewrite defA (zcharD1_seqInd_on _ S2psi).
  have [Tzeta Tlambda] := (seqInd_subT  S1zeta, seqInd_subT S2lambda).
  rewrite Dade_isometry ?A0bridge0 ?(cfun_onS (FTsupp_sub0 M)) //.
  rewrite cfdotBl !cfdotBr !cfdotZr cfdot_prTIred eq_sym (negPf nz_j1) add0r.
  rewrite !(seqInd_ortho _ Tzeta) ?Tmu ?(memPnC (sS1S2' S1zeta)) // add0r.
  rewrite (seqInd_ortho _ (Tmu 0)) ?(memPnC (prTIred_not_irr _ _)) // !mulr0.
  by rewrite subrr.
have [tau2 coh_tau2] := cohS2; have [[_ Ztau2] Dtau2] := coh_tau2.
have ua_1: (u %/ a)%:R * `|'[phi, tau2 lambda]| == 1.
  rewrite -normr_nat -normrM mulr_natl -!raddfMn -[_ *+ _](subrK (mu_ j)) /=.
  rewrite -opprB addrC raddfB cfdotBr -scaler_nat (Dtau2 _ S2psi) o_phi_psi.
  case: (FTtypeP_coherent_TIred _ coh_tau2 _ S2lambda S2muj) => // -[b k] -> _.
  rewrite -/(eta_col k) cfdotZr rmorph_sign subr0 normrMsign.
  rewrite -[phi](subrK eta0row) cfdotDl cfdot_sumr big1 => [|j' _]; last first.
    by rewrite (orthoPl (bridgeS1 _ _)) ?map_f ?mem_irr.
  rewrite add0r cfdotC norm_conjC cfdot_sumr (bigD1 k) //= proj_col_eta eqxx.
  by rewrite big1 ?addr0 ?normr1 // => i k'i; rewrite proj_col_eta (negPf k'i).
have Du: u = a.
  apply/eqP; rewrite -[a]mul1n eqn_mul ?(ltnW a_gt1) // -eqC_nat.
  move: ua_1; rewrite Cnat_mul_eq1 ?rpred_nat //; first by case/andP.
  rewrite Cnat_norm_Cint ?Cint_cfdot_vchar //; last by rewrite Ztau2 ?mem_zchar.
  rewrite Dade_vchar // zchar_split A0bridge0 //.
  by rewrite rpredB ?char_vchar ?prTIred_char ?irrWchar.
have lequ: (q <= u)%N.
  have u1_gt0: (0 < u.-1)%N by rewrite -subn1 subn_gt0 Du.
  rewrite (leq_trans _ (leq_pred u)) // dvdn_leq //.
  suffices ->: q = #|W1 / C|%g by apply: Frobenius_dvd_ker1 frobUW1bar.
  apply/card_isog/quotient_isog; first by have [] := joing_subP nC_UW1.
  by rewrite setIAC (coprime_TIg coUq) setI1g.
by rewrite (leq_trans lequ) // Du dvdn_leq // -subn1 subn_gt0 prime_gt1.
Qed.

End Eleven.