proposition: Lemma FTtype1_ortho_constant (psi : 'CF(G)) x : {in calS, forall phi, orthogonal psi (R phi)} -> x \in L :\: H -> {in x *: H, forall y, psi y = psi x}%g.
proof: Proof. move=> opsiR /setDP[Lx H'x]; pose Rpsi := 'Res[L] psi. have nsHL: H <| L := gFnormal _ _; have [sHL _] := andP nsHL. have [U [[[_ _ sdHU] [U1 inertU1] _] _]] := FTtypeP 1 maxL Ltype1. have /= [_ _ TIsub]:= FTtypeI_II_facts maxL Ltype1 sdHU. pose ddL := FT_Dade_hyp maxL. have A1Hdef : 'A1(L) = H^# by apply: FTsupp1_type1. have dot_irr xi j : xi \in calS -> j \in S_ xi -> '['chi_j, xi] = 1. move=> xi_calS Sj. have -> : xi = \sum_(i <- enum (S_ xi)) 'chi_i. by rewrite big_filter; have [] := FTtype1_seqInd_facts maxL Ltype1 xi_calS. rewrite (bigD1_seq j) ?mem_enum ?enum_uniq //= cfdotDr cfdot_sumr cfnorm_irr. by rewrite big1 ?addr0 // => k i'k; rewrite cfdot_irr eq_sym (negPf i'k). have {dot_irr} supp12B y xi j1 j2 : xi \in calS -> j1 \in S_ xi -> j2 \in S_ xi -> y \notin ('A(L) :\: H^#) -> ('chi_j1 - 'chi_j2) y = 0. - move=> calS_xi Sj1 Sj2 yADHn. have [xiD xi_cst sup_xi] := FTtype1_seqInd_facts maxL Ltype1 calS_xi. have [Hy | H'y] := boolP (y \in H); last first. suffices /cfun_on0->: y \notin 1%g |: 'A(L) by rewrite ?rpredB ?sup_xi. by rewrite !inE negb_or negb_and (group1_contra H'y) ?H'y in yADHn *. have [s _ xiIndD] := seqIndP calS_xi. pose sum_sL := \sum_(xi_z <- ('chi_s ^: L)%CF) xi_z. suffices Dxi: {in S_ xi, forall i, 'chi_i y = sum_sL y}. by rewrite !cfunE !Dxi ?subrr. move=> k Sk; pose phiH := 'Res[H] 'chi_k. transitivity (phiH y); first by rewrite cfResE ?normal_sub. have phiH_s_1: '[phiH, 'chi_s] = 1 by rewrite cfdot_Res_l -xiIndD dot_irr. have phiH_s: s \in irr_constt phiH by rewrite irr_consttE phiH_s_1 oner_eq0. by rewrite [phiH](Clifford_Res_sum_cfclass _ phiH_s) // phiH_s_1 scale1r. have {supp12B} oResD xi i1 i2 : xi \in calS -> i1 \in S_ xi -> i2 \in S_ xi -> '['Res[L] psi, 'chi_i1 - 'chi_i2] = 0. - move=> calS_xi Si1 Si2; rewrite cfdotC Frobenius_reciprocity -cfdotC. case: (altP (i1 =P i2))=> [-> | d12]; first by rewrite subrr linear0 cfdot0r. have {} supp12B y: y \notin 'A(L) :\: H^# -> ('chi_i1 - 'chi_i2) y = 0. exact: (supp12B _ xi _ _ calS_xi). case: (FTtype1_seqInd_facts maxL Ltype1 calS_xi) => _ cst1 supA. move/(_ _ Si1): (supA) => /cfun_onP s1; case/(constantP 0): (cst1) => [n]. move/all_pred1P /allP => nseqD; move/(_ _ Si2): (supA) => /cfun_onP s2. have nchi11: 'chi_i1 1%g = n by apply/eqP/nseqD/image_f. have{nseqD} nchi12: 'chi_i2 1%g = n by apply/eqP/nseqD/image_f. have i12_1: 'chi_i1 1%g == 'chi_i2 1%g by rewrite nchi11 nchi12. have sH1A: H^# \subset 'A(L) by rewrite Fcore_sub_FTsupp. have nzAH: 'A(L) :\: H^# != set0. apply: contra d12 => /eqP tADH; apply/eqP; apply: irr_inj; apply/cfunP=> w. apply/eqP; rewrite -subr_eq0; have := supp12B w; rewrite !cfunE => -> //. by rewrite tADH in_set0. have{nzAH} tiH: normedTI ('A(L) :\: H^#) G L by rewrite -A1Hdef TIsub ?A1Hdef. have{} supp12B : 'chi_i1 - 'chi_i2 \in 'CF(L, 'A(L) :\: H^#). by apply/cfun_onP; apply: supp12B. have [_ /subsetIP[_ nAHL] _] := normedTI_P tiH. pose tau1 := restr_Dade ddL (subsetDl _ _) nAHL. have tauInd: {in 'CF(L, 'A(L) :\: H^#), tau1 =1 'Ind} := Dade_Ind _ tiH. rewrite -{}tauInd // [tau1 _]restr_DadeE {tau1 nAHL}//. suffices Rtau12: Dade ddL ('chi_i1 - 'chi_i2) \in 'Z[R xi]. by rewrite (span_orthogonal (opsiR xi _)) ?memv_span1 ?(zchar_span Rtau12). case: (Rgen _ _) @R => rR [scohS]; case: (R1gen _ _) => /= R1 scohI ? DrR. rewrite -/calS in scohS; set calI := image _ _ in scohI. have [Ii1 Ii2]: 'chi_i1 \in calI /\ 'chi_i2 \in calI. by split; apply/image_f/FTtype1_irrP; exists xi. have [calI2 [I2i1 I2i2 sI2I] []] := pair_degree_coherence scohI Ii1 Ii2 i12_1. move=> tau2 cohI2; have [_ <-] := cohI2; last first. by rewrite zcharD1E rpredB ?mem_zchar // 2!cfunE subr_eq0. suffices R_I2 j: j \in S_ xi -> 'chi_j \in calI2 -> tau2 'chi_j \in 'Z[rR xi]. by rewrite raddfB rpredB ?R_I2. move=> Sj /(mem_coherent_sum_subseq scohI sI2I cohI2)[e R1e ->]. rewrite DrR big_seq rpred_sum // => phi /(mem_subseq R1e) R1phi. by apply/mem_zchar/flatten_imageP; exists j. suffices ResL: {in x *: H, forall y, Rpsi y = Rpsi x}%g. move=> w xHw; case/lcosetP: xHw (ResL w xHw) => h Hh -> {w}. by rewrite !cfResE ?subsetT ?groupM // ?(subsetP sHL). move=> _ /lcosetP[h Hh ->] /=; rewrite (cfun_sum_cfdot Rpsi). pose calX := Iirr_kerD L H 1%g; rewrite (bigID (mem calX) xpredT) /= !cfunE. set sumX := \sum_(i in _) _; suffices HsumX: sumX \in 'CF(L, H). rewrite !(cfun_on0 HsumX) ?groupMr // !sum_cfunE. rewrite !add0r; apply: eq_bigr => i; rewrite !inE sub1G andbT negbK => kerHi. by rewrite !cfunE cfkerMr ?(subsetP kerHi). rewrite [sumX](set_partition_big _ (FTtype1_irr_partition L)) /=. apply: rpred_sum => A; rewrite inE => /mapP[xi calS_xi defA]. have [-> | [j Achij]] := set_0Vmem A; first by rewrite big_set0 rpred0. suffices ->: \sum_(i in A) '[Rpsi, 'chi_i] *: 'chi_i = '[Rpsi, 'chi_j] *: xi. by rewrite rpredZ // (seqInd_on _ calS_xi). have [-> _ _] := FTtype1_seqInd_facts maxL Ltype1 calS_xi; rewrite -defA. rewrite scaler_sumr; apply: eq_bigr => i Ai; congr (_ *: _); apply/eqP. by rewrite -subr_eq0 -cfdotBr (oResD xi) /S_ -?defA. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop order prime ssralg finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxpoly mxrepresentation mxabelem vector) mathcomp(falgebra fieldext finfield) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC cyclotomic algnum) mathcomp(classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10) odd_order(PFsection11)