proposition: Lemma eq_signed_sub_cTIiso phi e i j1 j2 : let rho := (-1) ^+ e *: (eta_ i j1 - eta_ i j2) in phi \in 'Z[irr G] -> '[phi] = 2%:R -> j1 != j2 -> {in V, phi =1 rho} -> phi = rho.
proof: Proof. set rho := _ - _; move: phi => phi0 /= Zphi0 n2phi0 neq_j12 eq_phi_rho. pose phi := (-1) ^+ e *: phi0; pose psi := phi - rho. have{eq_phi_rho} psiV0 z: z \in V -> psi z = 0. by move=> Vz; rewrite !cfunE eq_phi_rho // !cfunE signrMK subrr. have{Zphi0} Zphi: phi \in 'Z[irr G] by rewrite rpredZsign. have{n2phi0} n2phi: '[phi] = 2%:R by rewrite cfnorm_sign. have Zrho: rho \in 'Z[irr G] by rewrite rpredB ?cycTIiso_vchar. have n2rho: '[rho] = 2%:R. by rewrite cfnormBd !cfdot_cycTIiso ?eqxx ?(negPf neq_j12) ?andbF. have [oIphi _ Dphi] := dirr_small_norm Zphi n2phi isT. have [oIrho _ Drho] := dirr_small_norm Zrho n2rho isT. set Iphi := dirr_constt _ in oIphi Dphi. set Irho := dirr_constt _ in oIrho Drho. suffices /eqP eqIrho: Irho == Iphi by rewrite Drho eqIrho -Dphi signrZK. have psi_phi'_lt0 di: di \in Irho :\: Iphi -> '[psi, dchi di] < 0. case/setDP=> rho_di phi'di; rewrite cfdotBl subr_lt0. move: rho_di; rewrite dirr_consttE; apply: le_lt_trans. rewrite real_leNgt -?dirr_consttE ?real0 ?Creal_Cint //. by rewrite Cint_cfdot_vchar ?dchi_vchar. have NCpsi: (NC psi < 2 * minn w1 w2)%N. suffices NCpsi4: (NC psi <= 2 + 2)%N. by rewrite (leq_ltn_trans NCpsi4) // !addnn mul2n ltn_double leq_min w1gt2. by rewrite cycTI_NC_sub // cycTI_NC_norm ?n2phi ?n2rho. pose rhoId := dirr_dIirr (fun sk => (-1) ^+ (sk.1 : bool) *: eta_ i sk.2). have rhoIdE s k: dchi (rhoId (s, k)) = (-1) ^+ s *: eta_ i k. by apply: dirr_dIirrE => sk; rewrite rpredZsign cycTIiso_dirr. rewrite eqEcard oIrho oIphi andbT -setD_eq0; apply/set0Pn=> [[dk1 phi'dk1]]. have [[rho_dk1 _] psi_k1_lt0] := (setDP phi'dk1, psi_phi'_lt0 _ phi'dk1). have dot_dk1: '[rho, dchi dk1] = 1. rewrite Drho cfdot_suml (big_setD1 dk1) //= cfnorm_dchi big1 ?addr0 //. move=> dk2 /setD1P[/negPf dk1'2 /dirr_constt_oppl]; rewrite cfdot_dchi dk1'2. by case: eqP => [-> /negP[] | _ _]; rewrite ?subrr ?ndirrK. have dot_dk2: 0 < '[rho, rho - dchi dk1]. by rewrite cfdotBr dot_dk1 n2rho addrK ltr01. have{dot_dk1 dot_dk2} [s [k Dk1 rho_k2]]: exists s, exists2 k, rhoId (s, k.1) = dk1 & rhoId (~~ s, k.2) \in Irho. - move/cfdot_add_dirr_eq1: dot_dk1. rewrite dirr_dchi rpredN !cycTIiso_dirr //. case=> // Dk1; [exists false, (j1, j2) | exists true, (j2, j1)]; try apply: dirr_inj; rewrite ?dirr_consttE rhoIdE scaler_sign //=. + by rewrite addrC Dk1 addKr in dot_dk2. by rewrite Dk1 addrK in dot_dk2. rewrite -Dk1 rhoIdE cfdotZr rmorph_sign in psi_k1_lt0. have psi_k1_neq0: '[psi, eta_ i k.1] != 0. by rewrite -(can_eq (signrMK s)) mulr0 lt_eqF. set dk2 := rhoId _ in rho_k2. have NCk2'_le1 (dI : {set _}): dk2 \in dI -> #|dI| = 2%N -> (NC (\sum_(dk in dI :\ dk2) dchi dk)%R <= 1)%N. - rewrite (cardsD1 dk2) => -> /eqP/cards1P[dk ->]. by rewrite big_set1 cycTI_NC_dirr ?dirr_dchi. suffices /psi_phi'_lt0/lt_geF/idP[]: dk2 \in Irho :\: Iphi. rewrite rhoIdE cfdotZr signrN rmorphN mulNr oppr_ge0 rmorph_sign. have := small_cycTI_NC psiV0 NCpsi psi_k1_neq0. by case=> // ->; rewrite mulrCA nmulr_lle0 ?ler0n. have: (1 + 1 < NC psi)%N. apply (@leq_trans (minn w1 w2)); first by rewrite leq_min w1gt2. apply: cycTI_NC_minn => //; rewrite NCpsi /NC. by rewrite (cardsD1 (i, k.1)) inE /= psi_k1_neq0. rewrite inE rho_k2 andbT ltnNge; apply: contra => phi_k2. rewrite /psi Drho (big_setD1 dk2) //= Dphi (big_setD1 dk2) //=. by rewrite addrAC opprD addNKr addrC cycTI_NC_sub ?NCk2'_le1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)