(Joint Center)Library PFsection13

This file covers Peterfalvi, Section 13: The Subgroups S and T. The following definitions will be used in PFsection14: FTtypeP_bridge StypeP j == a virtual character of S that mixes characters (locally) beta_ j, betaS that do and do not contain P = S`_\F in their kernels, for StypeP : of_typeP S U defW. := 'Ind[S, P <*> W1] 1 - mu2_ 0 j. FTtypeP_bridge_gap StypeP == the difference between the image of beta_ j (locally) Gamma, GammaS under the Dade isometry for S, and its natural value, 1 - eta_ 0 j (this does not actually depend on j != 0). The following definitions are only used locally across sections: irrIndFittinq S chi <=> chi is an irreducible character of S induced from an irreducible character of 'F(S) (which will be linear here, as 'F(S) is abelian). typeP_TIred_coherent StypeP tau1 <=> tau1 maps the reducible induced characters mu_ j of a type P group S, which is the image under the cyclic TI isometry to S of row sums of irreducibles of W = W1 x W2, to the image of that sum under the cyclic TI isometry to G (except maybe for a sign change if p = #|W2| = 3).

Set Implicit Arguments.

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

Section Thirteen.

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

Definition irr_Ind_Fitting S := [predI irr S & seqIndT 'F(S) S].

Local Notation irrIndH := (irr_Ind_Fitting _).
Local Notation "#1" := (inord 1) (at level 0).

Section Thirteen_2_3_5_to_9.

These assumptions correspond to the part of Peterfalvi, Hypothesis (13.1) that is used to prove (13.2-3) and (13.5-9). Because of the shortcomings of Coq's Section and Module features we will need to repeat most of these assumptions twice down this file to exploit the symmetry between S and T. We anticipate the use of the letter 'H' to designate the Fitting group of S, which Peterfalvi does only locally in (13.5-9), in order not to conflict with (13.17-19), where H denotes the F-core of a Frobenius group. This is not a problem for us, since these lemmas will only appear in the last section of this file, and we will have no use for H at that point since we will have shown in (13.12) that H coincides with P = S`_\F.

Variables S U W W1 W2 : {group gT}.
Hypotheses (maxS : S \in 'M) (defW : W1 \x W2 = W).
Hypotheses (StypeP : of_typeP S U defW).

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 "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
Local Notation V := (cyclicTIset defW).

Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
Local Notation P := `S`_\F%G.
Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
Local Notation PU := S^`(1)%G.
Local Notation "` 'PU'" := `S^`(1) (at level 0) : group_scope.
Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
Local Notation C := 'C_U(`P)%G.
Local Notation "` 'C'" := 'C_`U(`P) (at level 0) : group_scope.
Local Notation H := 'F(S)%G.
Local Notation "` 'H'" := 'F(`S) (at level 0) : group_scope.

Let defS : PU ><| W1 = S.
Let defPU : P ><| U = PU.
Let defH : P \x C = H.

Let notStype1 : FTtype S != 1%N.
Let notStype5 : FTtype S != 5%N.

Let pddS := FT_prDade_hypF maxS StypeP.
Let ptiWS : primeTI_hypothesis S PU defW := FT_primeTI_hyp StypeP.
Let ctiWG : cyclicTI_hypothesis G defW := pddS.

Let ntW1 : W1 :!=: 1.
Let ntW2 : W2 :!=: 1.
Let cycW1 : cyclic W1.
Let cycW2 : cyclic W2.

Let p := #|W2|.
Let q := #|W1|.
Let c := #|C|.
Let u := #|U : C|.

Let oU : #|U| = (u × c)%N.

Let pr_p : prime p.
Let pr_q : prime q.

Let qgt2 : q > 2.
Let pgt2 : p > 2.

Let coPUq : coprime #|PU| q.

Let nirrW1 : #|Iirr W1| = q.
Let nirrW2 : #|Iirr W2| = p.
Let NirrW1 : Nirr W1 = q.
Let NirrW2 : Nirr W2 = p.

Local Open Scope ring_scope.

Let sigma := (cyclicTIiso ctiWG).
Let w_ i j := (cyclicTIirr defW i j).
Local Notation eta_ i j := (sigma (w_ i j)).

Local Notation Imu2 := (primeTI_Iirr ptiWS).
Let mu2_ i j := primeTIirr ptiWS i j.
Let mu_ := primeTIred ptiWS.
Local Notation chi_ j := (primeTIres ptiWS j).

Local Notation Idelta := (primeTI_Isign ptiWS).
Local Notation delta_ j := (primeTIsign ptiWS j).

Local Notation tau := (FT_Dade0 maxS).
Local Notation "chi ^\tau" := (tau chi).

Let calS0 := seqIndD PU S S`_\s 1.
Let rmR := FTtypeP_coh_base maxS StypeP.
Let scohS0 : subcoherent calS0 tau rmR.

Let calS := seqIndD PU S P 1.
Let sSS0 : cfConjC_subset calS calS0.

Local Notation type34ker1 := (FTtype34_Fcore_kernel_trivial maxS StypeP).
Local Notation type34facts := (FTtype34_structure maxS StypeP).
Local Notation type2facts := (FTtypeII_prime_facts maxS StypeP).
Local Notation compl2facts := (compl_of_typeII maxS StypeP).
Local Notation compl3facts := (compl_of_typeIII maxS StypeP).

Local Notation H0 := (Ptype_Fcore_kernel StypeP).

Lemma Ptype_factor_prime : pdiv #|P / H0|%g = p.
Local Notation pHbar_p := Ptype_factor_prime.

Lemma Ptype_Fcore_kernel_trivial : H0 :=: 1%g.
Local Notation H0_1 := Ptype_Fcore_kernel_trivial.

Lemma Ptype_Fcompl_kernel_cent : Ptype_Fcompl_kernel StypeP :=: C.
Local Notation CHbar_C := Ptype_Fcompl_kernel_cent.

This is Peterfalvi (13.2).
Lemma FTtypeP_facts :
  [/\ (*a*) [/\ pred2 2 3 (FTtype S), q < pFTtype S == 2,
                [Frobenius U <*> W1 = U ><| W1] & abelian U],
      (*b*) p.-abelem P #|P| = p ^ q,
      (*c*) u (p ^ q).-1 %/ p.-1,
      (*d*) coherent calS S^# tau
    & (*e*) normedTI 'A0(S) G S {in 'CF(S, 'A0(S)), tau =1 'Ind}]%N.

This should perhaps move to PFsection9.
Lemma FTseqInd_TIred j : j != 0 → mu_ j \in calS.

Lemma FTtypeP_Fitting_abelian : abelian H.
Hint Resolve FTtypeP_Fitting_abelian.

Local Notation calH := (seqIndT H S).

Lemma FTtypeP_Ind_Fitting_1 lambda : lambda \in calHlambda 1%g = (u × q)%:R.
Local Notation calHuq := FTtypeP_Ind_Fitting_1.

This is Peterfalvi (13.3)(a).
Lemma FTprTIred_Ind_Fitting j : j != 0 → mu_ j \in calH.
Local Notation Hmu := FTprTIred_Ind_Fitting.

Lemma FTprTIred1 j : j != 0 → mu_ j 1%g = (u × q)%:R.
Local Notation mu1uq := FTprTIred1.

This is the first assertion of Peterfalvi (13.3)(c).
Lemma FTprTIsign j : delta_ j = 1.
Local Notation delta1 := FTprTIsign.

This is Peterfalvi (13.3)(b).
Helper function for (13.3)(c).
Let signW2 (b : bool) := iter b (@conjC_Iirr _ W2).

Let signW2K b : involutive (signW2 b).

Let signW2_eq0 b : {mono signW2 b: j / j == 0}.

This is a reformulation of the definition condition part of (13.3)(c) that better fits its actual use in (13.7), (13.8) and (13.9) (note however that the p = 3 part will in fact not be used).
Definition typeP_TIred_coherent tau1 :=
  exists2 b : bool, bp = 3
  & j, j != 0 → tau1 (mu_ j) = (-1) ^+ b *: \sum_i eta_ i (signW2 b j).

This is the main part of Peterfalvi (13.3)(c), using the definition above. Note that the text glosses over the quantifier inversion in the second use of (5.8) in the p = 3 case. We must rule out tau1 (mu_ k) = - tau1 (mu_ j) by using the isometry property of tau1 (alternatively, we could use (4.8) to compute tau1 (mu_ k) = tau (mu_ k - mu_ j) + tau1 (mu_ j) directly).
We skip over (13.4), which requires the use of (13.2) and (13.3) on both groups of a type P pair.

Let calS1 := seqIndD H S P 1.

Some facts about calS1 used implicitly throughout (13.5-8).
Let S1mu j : j != 0 → mu_ j \in calS1.

Let calSirr := [seq phi <- calS | phi \in irr S].
Let S1cases zeta :
  zeta \in calS1{j | j != 0 & zeta = mu_ j} + (zeta \in 'Z[calSirr]).

Let sS1S : {subset calS1 'Z[calS]}.

This is Peterfalvi (13.5). We have adapted the statement to its actual use by replacing the Dade (partial) isometry by a (total) coherent isometry, and strengthening the orthogonality condition. This simplifies the assumptions as zeta0 is no longer needed. Note that this lemma is only used to establish various inequalities (13.6-8) that contribute to (13.10), so it does not need to be exported from this section.
Let calS1_split1 (tau1 : {additive _}) zeta1 chi :
   coherent_with calS S^# tau tau1zeta1 \in calS1chi \in 'Z[irr G]
   {in calS1, zeta, zeta != zeta1'[tau1 zeta, chi] = 0}
  let a := '[tau1 zeta1, chi] in
  exists2 alpha,
     alpha \in 'Z[irr H] {subset irr_constt alpha Iirr_ker H P} &
  [/\ (*a*) {in H^#, x, chi x = a / '[zeta1] × zeta1 x + alpha x},
      (*b*)
         \sum_(x in H^#) `|chi x| ^+ 2 =
             a ^+ 2 / '[zeta1] × (#|S|%:R - zeta1 1%g ^+ 2 / '[zeta1])
             - 2%:R × a × (zeta1 1%g × alpha 1%g / '[zeta1])
             + (\sum_(x in H^#) `|alpha x| ^+ 2)
    & (*c*)
         \sum_(x in H^#) `|alpha x| ^+ 2 #|P|.-1%:R × alpha 1%g ^+ 2].

Local Notation eta10 := (eta_ #1 0).
Local Notation eta01 := (eta_ 0 #1).

Let o_tau1_eta (tau1 : {additive _}) i j:
    coherent_with calS S^# tau tau1
  {in 'Z[calSirr], zeta, '[tau1 zeta, eta_ i j] = 0}.

Let P1_int2_lb b : b \in Cint → 2%:R × u%:R × b #|P|.-1%:R × b ^+ 2.

This is Peterfalvi (13.6).
Lemma FTtypeP_sum_Ind_Fitting_lb (tau1 : {additive _}) lambda :
    coherent_with calS S^# tau tau1lambda \in irrIndHlambda \in calS
  \sum_(x in H^#) `|tau1 lambda x| ^+ 2 #|S|%:R - lambda 1%g ^+ 2.

This is Peterfalvi (13.7).
This is Peterfalvi (13.8). We have filled a logical gap in the textbook, which quotes (13.3.c) to get a j such that eta_01 is a component of mu_j^tau1, then asserts that the (orthogonality) assumptions of (13.5) have been checked, apparently implying that because for zeta in calS1 \ mu_j, zeta^tau1 is orthogonal to mu_j^tau1, as per the proof of (13.6), zeta^tau1 must be orthogonal to eta_01. This is wrong, because zeta^tau1, mu_j^tau1 and eta_01 are not characters, but virtual characters. We need to use a more careful line of reasoning, using the more precise characterization of calS1 in the lemma S1cases above (which does use the orthogonal-constituent argument, but for chi_j and Res_H zeta), and the decomposition given in (13.3.c) for all the mu_k.
These are the assumptions for (13.9); K will be set to 'F(T) in the only application of this lemma, on the proof of (13.10).

Variable K : {group gT}.
Let G0 := ~: (class_support H G :|: class_support K G).

Variables (tau1 : {additive 'CF(S)'CF(G)}) (lambda : 'CF(S)).

Hypothesis cohS : coherent_with calS S^# tau tau1.
Hypothesis cohSmu : typeP_TIred_coherent tau1.

Hypotheses (Slam : lambda \in calS) (irrHlam : irrIndH lambda).

This is Peterfalvi (13.9)(a). As this part is only used to establish (13.9.b) it can be Section-local.
Let cover_G0 : {in G0, x, tau1 lambda x != 0 eta_ #1 0 x != 0}.

This is Peterfalvi (13.9)(b).
These assumptions correspond to Peterfalvi, Hypothesis (13.1), most of which gets used to prove (13.4) and (13.9-13).

Variables S U W W1 W2 : {group gT}.
Hypotheses (maxS : S \in 'M) (defW : W1 \x W2 = W).
Hypotheses (StypeP : of_typeP S U defW).

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 "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
Local Notation V := (cyclicTIset defW).

Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
Local Notation P := `S`_\F%G.
Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
Local Notation PU := S^`(1)%G.
Local Notation "` 'PU'" := `S^`(1) (at level 0) : group_scope.
Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
Local Notation C := 'C_U(`P)%G.
Local Notation "` 'C'" := 'C_`U(`P) (at level 0) : group_scope.
Local Notation H := 'F(S)%G.
Local Notation "` 'H'" := 'F(`S) (at level 0) : group_scope.

Let defS : PU ><| W1 = S.
Let defPU : P ><| U = PU.
Let defH : P \x C = H.

Let notStype1 : FTtype S != 1%N.
Let notStype5 : FTtype S != 5%N.

Let pddS := FT_prDade_hypF maxS StypeP.
Let ptiWS : primeTI_hypothesis S PU defW := FT_primeTI_hyp StypeP.
Let ctiWG : cyclicTI_hypothesis G defW := pddS.
Local Notation Sfacts := (FTtypeP_facts maxS StypeP).

Let ntW1 : W1 :!=: 1.
Let ntW2 : W2 :!=: 1.
Let cycW1 : cyclic W1.
Let cycW2 : cyclic W2.

Let p := #|W2|.
Let q := #|W1|.

Let pr_p : prime p.
Let pr_q : prime q.

Let qgt2 : q > 2.
Let pgt2 : p > 2.

Let coPUq : coprime #|PU| q.

Let sW2P: W2 \subset P.

Let p'q : q != p.

Let nirrW1 : #|Iirr W1| = q.
Let nirrW2 : #|Iirr W2| = p.
Let NirrW1 : Nirr W1 = q.
Let NirrW2 : Nirr W2 = p.

Local Open Scope ring_scope.

Let sigma := (cyclicTIiso ctiWG).
Let w_ i j := (cyclicTIirr defW i j).
Local Notation eta_ i j := (sigma (w_ i j)).

Let mu_ := primeTIred ptiWS.
Local Notation tau := (FT_Dade0 maxS).

Let calS0 := seqIndD PU S S`_\s 1.
Let rmR := FTtypeP_coh_base maxS StypeP.
Let scohS0 : subcoherent calS0 tau rmR.

Let calS := seqIndD PU S P 1.
Let sSS0 : cfConjC_subset calS calS0.

Local Notation calH := (seqIndT H S).
Local Notation calHuq := (FTtypeP_Ind_Fitting_1 maxS StypeP).

Section Thirteen_10_to_13_15.

This section factors the assumption that S contains an irreducible induced from a linear character of H. It does not actually export (13.4) and and (4.11) but instead uses them to carry out the bulk of the proofs of (4.12), (4.13) and (4.15). The combinatorial bound m is also local to this Section, but (4.10) has to be exported from an inner Section that factors facts about T, the typeP pair associate of S. Note that u and c are bound locally to this section; we will set u = #|U| after this section.

Variable lambda : 'CF(S).
Hypotheses (Slam : lambda \in calS) (irrHlam : irrIndH lambda).
Let Hlam : lambda \in calH.
Let Ilam : lambda \in irr S.

Let c := #|C|.
Let u := #|U : C|.
Let oU : #|U| = (u × c)%N.

Let m : algC := 1 - q.-1%:R^-1 - q.-1%:R / (q ^ p)%:R + (q.-1 × q ^ p)%:R^-1.

Section Thirteen_4_10.

This Section factors assumptions and facts about T, including Lemma (13.4) is local to this Section.

Variables T V : {group gT}.
Hypotheses (maxT : T \in 'M) (defW21 : W2 \x W1 = W).
Hypothesis TtypeP : of_typeP T V defW21.

Local Notation Q := (gval T)`_\F.
Local Notation D := 'C_(gval V)(Q).
Local Notation K := 'F(gval T).
Let v := #|V : D|.

Local Notation calT := (seqIndD T^`(1) T (gval T)`_\F 1).

This part of the proof of (13.4) is reused in (13.10).
This is Peterfalvi (13.4).
This is Peterfalvi (13.10).
This is (13.10) without the dependency on T.
Let gen_lb_uc : m × (p ^ q.-1)%:R / q%:R < u%:R / c%:R.

Import ssrint.
This is Peterfalvi (13.11).
Let lb_m_cases :
 [/\ (*a*) (q 7)%Nm > 8%:R / 10%:R,
     (*b*) (q 5)%Nm > 7%:R / 10%:R
   & (*c*) q = 3 →
           m > 49%:R / 100 %:R u%:R / c%:R > (p ^ 2).-1%:R / 6 %:R :> algC].

This corollary of (13.11) is used in both (13.12) and (13.15).
Let small_m_q3 : m < (q × p)%:R / (q.*2.+1 × p.-1)%:Rq = 3 (p 5)%N.

A more usable form for (13.10).
This is the bulk of the proof of Peterfalvi (13.12).
This is the main part of the proof of Peterfalvi (13.13).
This is the bulk of the proof of Peterfalvi (13.15). We improve slightly on the end of the argument by maing better use of the bound on u to get p = 5 directly.
This is Peterfalvi (13.12).
Since C is trivial, from here on u will denote #|U|.
Let u := #|U|.
Let ustar := (p ^ q).-1 %/ p.-1.

This is Peterfalvi (13.13).
Lemma FTtypeP_nonGalois_facts :
  ~~ typeP_Galois StypePq = 3 u = (p.-1./2 ^ 2)%N.

Import FinRing.Theory.

This is Peterfalvi (13.14).
Lemma FTtypeP_primes_mod_cases :
  [/\ odd ustar,
      p == 1 %[mod q]q %| ustar
    & p != 1 %[mod q]
      [/\ coprime ustar p.-1, ustar == 1 %[mod q]
        & b, b %| ustarb == 1 %[mod q]]].

This is Peterfalvi (13.15).
This is Peterfalvi (13.16). We have transposed T and Q here so that the lemma does not require assumptions on the associate group.
These assumptions repeat the part of Peterfalvi, Hypothesis (13.1) used to prove (13.17-19).

Variables S U W W1 W2 : {group gT}.
Hypotheses (maxS : S \in 'M) (defW : W1 \x W2 = W).
Hypotheses (StypeP : of_typeP S U defW).

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 "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
Local Notation V := (cyclicTIset defW).

Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
Local Notation P := `S`_\F%G.
Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
Local Notation PU := S^`(1)%G.
Local Notation "` 'PU'" := `S^`(1) (at level 0) : group_scope.
Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.

Let defS : PU ><| W1 = S.
Let defPU : P ><| U = PU.

Let notStype1 : FTtype S != 1%N.
Let notStype5 : FTtype S != 5%N.

Let pddS := FT_prDade_hypF maxS StypeP.
Let ptiWS : primeTI_hypothesis S PU defW := FT_primeTI_hyp StypeP.
Let ctiWG : cyclicTI_hypothesis G defW := pddS.
Local Notation Sfacts := (FTtypeP_facts maxS StypeP).

Let ntW1 : W1 :!=: 1.
Let ntW2 : W2 :!=: 1.
Let cycW1 : cyclic W1.
Let cycW2 : cyclic W2.

Let p := #|W2|.
Let q := #|W1|.

Let pr_p : prime p.
Let pr_q : prime q.

Let qgt2 : q > 2.
Let pgt2 : p > 2.

Let coPUq : coprime #|PU| q.

Let sW2P: W2 \subset P.

Let p'q : q != p.

Let nirrW1 : #|Iirr W1| = q.
Let nirrW2 : #|Iirr W2| = p.
Let NirrW1 : Nirr W1 = q.
Let NirrW2 : Nirr W2 = p.

Local Open Scope ring_scope.

Let sigma := (cyclicTIiso ctiWG).
Let w_ i j := (cyclicTIirr defW i j).
Local Notation eta_ i j := (sigma (w_ i j)).

Let mu_ := primeTIred ptiWS.
Local Notation tau := (FT_Dade0 maxS).

Let calS0 := seqIndD PU S S`_\s 1.
Let rmR := FTtypeP_coh_base maxS StypeP.
Let scohS0 : subcoherent calS0 tau rmR.

Let calS := seqIndD PU S P 1.
Let sSS0 : cfConjC_subset calS calS0.

This is Peterfalvi (13.17).
Lemma FTtypeII_support_facts T L (Q := T`_\F) (H := L`_\F) :
    FTtype S == 2 → typeP_pair S T defWL \in 'M('N(U))
  [/\ (*a*) [Frobenius L with kernel H],
      (*b*) U \subset H
    & (*c*) H ><| W1 = L
          (exists2 y, y \in Q & H ><| (W1 <*> W2 :^ y) = L)].

Local Notation Imu2 := (primeTI_Iirr ptiWS).
Local Notation mu2_ i j := (primeTIirr ptiWS i j).

Definition FTtypeP_bridge j := 'Ind[S, P <*> W1] 1 - mu2_ 0 j.
Local Notation beta_ := FTtypeP_bridge.
Definition FTtypeP_bridge_gap := tau (beta_ #1) - 1 + eta_ 0 #1.
Local Notation Gamma := FTtypeP_bridge_gap.

Let u := #|U|.

This is Peterfalvi (13.18). Part (d) is stated with a slightly weaker hypothesis that fits better with the usage pattern in (13.19) and (14.9).
Lemma FTtypeP_bridge_facts (V_S := class_support (cyclicTIset defW) S) :
  [/\ (*a*) [/\ j, j != 0 → beta_ j \in 'CF(S, 'A0(S))
              & j, j != 0 → beta_ j \in 'CF(S, P^# :|: V_S)],
      (*b*) j, j != 0 → '[beta_ j] = (u.-1 %/ q + 2)%:R,
      (*c*) [/\ j, j != 0 → tau (beta_ j) - 1 + eta_ 0 j = Gamma,
                '[Gamma, 1] = 0 & cfReal Gamma],
      (*d*) X Y : 'CF(G),
              Gamma = X + Y'[X, Y] = 0 →
              orthogonal Y (map sigma (irr W)) →
            '[Y] (u.-1 %/ q)%:R
          & q %| u.-1].

The assumptions of Peterfalvi (13.19). We do not need to put these in a subsection as this is the last Lemma.
Variable L : {group gT}.
Hypotheses (maxL : L \in 'M) (Ltype1 : FTtype L == 1%N).

Local Notation "` 'L'" := (gval L) (at level 0, only parsing) : group_scope.
Local Notation H := `L`_\F%G.
Local Notation "` 'H'" := `L`_\F (at level 0) : group_scope.

Let e := #|L : H|.
Let tauL := FT_Dade maxL.
Let calL := seqIndD H L H 1.

Let frobL : [Frobenius L with kernel H].

The coherence part of the preamble of (13.19).
We re-quantify over the witnesses so that the main part of the lemma can be used for Section variables in the very last part of Section 14.
Variables (tau1 : {additive 'CF(L)'CF(G)}) (phi : 'CF(L)).
Hypothesis cohL : coherent_with calL L^# tauL tau1.
Hypotheses (Lphi : phi \in calL) (phi1e : phi 1%g = e%:R).

Let betaL := 'Ind[L, H] 1 - phi.
Let betaS := beta_ #1.
Let eta01 := eta_ 0 #1.

This is Peterfalvi (13.19).
Lemma FTtypeI_bridge_facts :
  [/\ (*a*) 'A~(L) :&: (class_support P G :|: class_support W G) = set0,
      (*b*) orthogonal (map tau1 calL) (map sigma (irr W)),
      (*c*) j, j != 0 → '[tauL betaL, eta_ 0 j] = '[tauL betaL, eta01]
       & (*c1*) ('[tau betaS, tau1 phi] == 1 %[mod 2])%C
                 #|H|.-1%:R / e%:R (u.-1 %/ q)%:R :> algC
       (*c2*) ('[tauL betaL, eta01] == 1 %[mod 2])%C (p e)%N].

End Thirteen_17_to_19.

End Thirteen.