proposition: Lemma vchar_isometry_base m L (Chi : m.-tuple 'CF(H)) (tau : {linear 'CF(H) -> 'CF(G)}) : (1 < m)%N -> {subset Chi <= irr H} -> free Chi -> (forall chi, chi \in Chi -> chi 1%g = Chi`_0 1%g) -> (forall i : 'I_m, (Chi`_i - Chi`_0) \in 'CF(H, L)) -> {in 'Z[Chi, L], isometry tau, to 'Z[irr G, G^#]} -> exists2 mu : m.-tuple (Iirr G), uniq mu & exists epsilon : bool, forall i : 'I_m, tau (Chi`_i - Chi`_0) = (-1) ^+ epsilon *: ('chi_(mu`_i) - 'chi_(mu`_0)).
proof: Proof. case: m Chi => [|[|m]] // Chi _ irrChi Chifree Chi1 ChiCF [iso_tau Ztau]. rewrite -(tnth_nth 0 _ 0); set chi := tnth Chi. have chiE i: chi i = Chi`_i by rewrite -tnth_nth. have inChi i: chi i \in Chi by apply: mem_tnth. have{} irrChi i: chi i \in irr H by apply: irrChi. have eq_chi i j: (chi i == chi j) = (i == j). by rewrite /chi !(tnth_nth 0) nth_uniq ?size_tuple ?free_uniq. have dot_chi i j: '[chi i, chi j] = (i == j)%:R. rewrite -eq_chi; have [/irrP[{}i ->] /irrP[{}j ->]] := (irrChi i,irrChi j). by rewrite cfdot_irr inj_eq //; apply: irr_inj. pose F i j := chi i - chi j. have DF i j : F i j = F i 0 - F j 0 by rewrite /F opprB addrA subrK. have ZF i j: F i j \in 'Z[Chi, L]. by rewrite zchar_split rpredB ?mem_zchar // DF memvB // /F !chiE. have htau2 i j: i != j -> '[tau (F i j)] = 2%:R. rewrite iso_tau // cfnormB -cfdotC !dot_chi !eqxx eq_sym => /negbTE->. by rewrite -!natrD subr0. have htau1 i j: j != 0 -> j != i -> i != 0 -> '[tau (F i 0), tau (F j 0)] = 1. rewrite iso_tau // cfdotBl !cfdotBr opprB !dot_chi !(eq_sym j). by do 3!move/negbTE->; rewrite !subr0 add0r. have [m0 | nz_m] := boolP (m == 0%N). rewrite -2!eqSS eq_sym in m0; move: (htau2 1 0 isT). case/(vchar_norm2 (Ztau _ (ZF 1 0))) => [k1 [k0 neq_k01 eq_mu]]. pose mu := @Tuple _ _ [:: k0; k1] m0. exists mu; first by rewrite /= andbT inE. exists false => i; rewrite scale1r chiE. have: (i : nat) \in iota 0 2 by rewrite mem_iota (eqP m0) (valP i). rewrite !inE; case/pred2P=> ->; first by rewrite !subrr linear0. by rewrite -eq_mu /F !chiE. have m_gt2: (2 < m.+2)%N by rewrite !ltnS lt0n. pose i2 := Ordinal m_gt2. case: (@vchar_isometry_base3 (tau (F 1 0)) (tau (F i2 0))); auto. case=> [[[k1 k0] k2] e] []; set d := (-1) ^+ e => eq10 eq20. rewrite /= !inE => /and3P[/norP[nek10 nek12]]; rewrite eq_sym => nek20 _. have muP i: {k | (i == 0) ==> (k == k0) & tau (F i 0) == d *: ('chi_k0 - 'chi_k)}. - apply: sig2W; have [-> | nei0] := altP (i =P 0). by exists k0; rewrite ?eqxx // /F !subrr !linear0. have /(vchar_norm2 (Ztau _ (ZF i 0)))[k [k' nekk' eqFkk']] := htau2 i 0 nei0. have [-> | neq_i1] := eqVneq i 1; first by exists k1; rewrite // -eq10. have [-> | neq_i2] := eqVneq i i2; first by exists k2; rewrite // -eq20. have:= @vchar_isometry_base4 (~~ e) k0 k1 k2 k k' nek12. have ZdK u v w: '[u, v - w]_G = (-1) ^+ (~~ e) * '[u, d *: (w - v)]. rewrite cfdotZr rmorph_sign mulrA -signr_addb addNb addbb mulN1r. by rewrite -cfdotNr opprB. rewrite -eqFkk' ZdK -eq10 {}ZdK -eq20 !htau1 //; try by rewrite eq_sym. move/(_ (mulr1 _) (mulr1 _)); rewrite /d eqFkk'. by case e => /eqP <-; [exists k | exists k']; rewrite ?scaler_sign ?opprB. pose mu := [tuple of [seq s2val (muP i) | i <- ord_tuple m.+2]]; exists mu. rewrite map_inj_uniq ?enum_uniq // => i j. case: (muP i) (muP j) => /= ki _ /eqP eq_i0 [/= kj _ /eqP eq_j0] eq_kij. apply/eqP; rewrite -eq_chi -subr_eq0 -cfnorm_eq0 -iso_tau ?ZF //. rewrite -[chi i](subrK (chi 0)) -addrA linearD eq_i0 eq_kij -eq_j0. by rewrite -linearD -opprB subrr !raddf0. exists (~~ e) => i; rewrite -addbT signr_addb -/d -scalerA scaleN1r opprB. rewrite -!tnth_nth -/(F i 0) tnth_map tnth_ord_tuple. suffices /= ->: mu`_0 = k0 by case: (muP i) => /= k _ /eqP. rewrite -(tnth_nth 0 _ 0) tnth_map tnth_ord_tuple. by case: (muP 0) => /= k /(k =P k0). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop prime order ssralg finset fingroup morphism) mathcomp(perm automorphism quotient action zmodp finalg center commutator) mathcomp(poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation) mathcomp(vector falgebra fieldext ssrnum algC rat algnum galois) mathcomp(classfun character inertia integral_char vcharacter)