proposition: Lemma pivot_coherence S (tau : {additive 'CF(L) -> 'CF(G)}) R eta1 zeta1 : subcoherent S tau R -> eta1 \in S -> zeta1 \in 'Z[irr G] -> {in [predD1 S & eta1], forall eta : 'CF(L), exists2 a, a \in Cnat /\ eta 1%g = a * eta1 1%g & '[tau (eta - a *: eta1), zeta1] = - a * '[eta1]} -> '[zeta1] = '[eta1] -> coherent S L^# tau.
proof: Proof. case=> -[N_S _ _] [Itau Ztau] oSS _ _ Seta1 Zzeta1 isoS Izeta1. have freeS := orthogonal_free oSS; have uniqS := free_uniq freeS. have{oSS} [/andP[S'0 _] oSS] := pairwise_orthogonalP oSS. pose d := eta1 1%g; pose a (eta : 'CF(L)) := truncC (eta 1%g / d). have{S'0} nzd: d != 0 by rewrite char1_eq0 ?N_S ?(memPn S'0). pose S1 := eta1 :: [seq eta - eta1 *+ a eta | eta <- rem eta1 S]. have sS_ZS1: {subset S <= 'Z[S1]}; last apply: (subgen_coherent sS_ZS1). have Zeta1: eta1 \in 'Z[S1] by rewrite mem_zchar ?mem_head. apply/allP; rewrite (eq_all_r (perm_mem (perm_to_rem Seta1))) /= Zeta1. apply/allP=> eta Seta; rewrite -(rpredBr eta (rpredMn (a eta) Zeta1)). exact/mem_zchar/mem_behead/map_f. have{sS_ZS1} freeS1: free S1. have Sgt0: (0 < size S)%N by case: (S) Seta1. rewrite /free eqn_leq dim_span /= size_map size_rem ?prednK // -(eqnP freeS). by apply/dimvS/span_subvP => eta /sS_ZS1/zchar_span. pose iso_eta1 zeta := zeta \in 'Z[S, L^#] /\ '[tau zeta, zeta1] = '[zeta, eta1]. have{} isoS: {in behead S1, forall zeta, iso_eta1 zeta}. rewrite /iso_eta1 => _ /mapP[eta Seta ->]; rewrite mem_rem_uniq // in Seta. have{Seta} [/isoS[q [Nq Dq] Itau_eta1] [eta1'eta Seta]] := (Seta, andP Seta). rewrite zcharD1E rpredB ?rpredMn ?mem_zchar //= -scaler_nat /a Dq mulfK //. by rewrite truncCK // !cfunE Dq subrr cfdotBl cfdotZl -mulNr oSS ?add0r. have isoS1: {in S1, isometry [eta tau with eta1 |-> zeta1], to 'Z[irr G]}. split=> [xi eta | eta]; rewrite !in_cons /=; last first. by case: eqP => [-> | _ /isoS[/Ztau/zcharW]]. do 2!case: eqP => [-> _|_ /isoS[? ?]] //; last exact: Itau. by apply/(can_inj (@conjCK _)); rewrite -!cfdotC. have [nu Dnu IZnu] := Zisometry_of_iso freeS1 isoS1. exists nu; split=> // phi; rewrite zcharD1E => /andP[]. case/(zchar_expansion (free_uniq freeS1)) => b Zb {phi}-> phi1_0. have{phi1_0} b_eta1_0: b eta1 = 0. have:= phi1_0; rewrite sum_cfunE big_cons big_seq big1 ?addr0 => [|zeta]. by rewrite !cfunE (mulIr_eq0 _ (mulIf nzd)) => /eqP. by case/isoS; rewrite cfunE zcharD1E => /andP[_ /eqP->] _; rewrite mulr0. rewrite !raddf_sum; apply/eq_big_seq=> xi S1xi/=; rewrite !raddfZ_Cint //=. by rewrite Dnu //=; case: eqP => // ->; rewrite b_eta1_0 !scale0r. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrint) mathcomp(ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4)