proposition: Lemma cyclicTIiso_basis_exists : exists xi_ : Iirr W1 -> Iirr W2 -> 'CF(G), [/\ xi_ 0 0 = 1, forall i j, xi_ i j \in 'Z[irr G], forall i j, i != 0 -> j != 0 -> 'Ind (alpha_ i j) = 1 - xi_ i 0 - xi_ 0 j + xi_ i j & forall i1 j1 i2 j2, '[xi_ i1 j1, xi_ i2 j2] = ((i1, j1) == (i2, j2))%:R].
proof: Proof. pose beta i j : 'CF(G) := 'Ind[G] (alpha_ i j) - 1. have Zbeta i j: beta i j \in 'Z[irr G]. by rewrite rpredB ?rpred1 ?cfInd_vchar ?cfCycTI_vchar. have o_alphaG_1 i j: i != 0 -> j != 0 -> '['Ind[G] (alpha_ i j), 1] = 1. by move=> nz_i nz_j; rewrite -cfdot_Res_r rmorph1 cfdot_alpha_1. have o_beta_1 i j: i != 0 -> j != 0 -> '[beta i j, 1] = 0. by move=> nzi nzj; rewrite cfdotBl o_alphaG_1 // cfnorm1 subrr. have o_beta i1 j1 i2 j2 : i1 != 0 -> j1 != 0 -> i2 != 0 -> j2 != 0 -> '[beta i1 j1, beta i2 j2] = ((i1 == i2).+1 * (j1 == j2).+1 - 1)%:R. - move=> nzi1 nzj1 nzi2 nzj2; rewrite mulSnr addnS mulnSr /=. rewrite cfdotBr o_beta_1 // subr0 cfdotBl (cfdotC 1) o_alphaG_1 //. rewrite (normedTI_isometry tiV) ?cfCycTI_on // rmorph1 addrC. rewrite (alphaE i2) cfdotDr !cfdotBr cfdot_alpha_1 // -!addrA addKr addrA. rewrite addrC cfdot_alpha_w // subn1 -addnA !natrD mulnb; congr (_ + _). rewrite alphaE -w_00 !(cfdotBl, cfdotDl) !cfdot_w !eqxx !(eq_sym 0). rewrite (negPf nzi1) (negPf nzj1) (negPf nzi2) (negPf nzj2) /= !andbF !andbT. by rewrite !addr0 !subr0 !opprB !subr0. pose beta_fun := [fun ij => beta (inord ij.1.+1) (inord ij.2.+1)]. have beta_modelP: is_Lmodel ((Nirr W1).-1, (Nirr W2).-1) beta_fun. split=> [ | //= | ij1 ij2 /=/andP[lti1 ltj1] /andP[lti2 ltj2]]. by rewrite -!(ltnS 2) -eqSS NirrW1 NirrW2. by rewrite o_beta -?val_eqE /= ?inordK. pose beta_model := Model beta_modelP (nil_RmodelP G). have betaE i j: i != 0 -> j != 0 -> beta i j = beta_fun (i.-1, j.-1). by move=> nzi nzj /=; rewrite !prednK ?lt0n ?inord_val. have /fin_all_exists [dXi0 betaXi0] i0: exists dX, i0 != 0 -> forall i j, i != 0 -> j != 0 -> '[beta i j, dchi dX] = (i == i0)%:R. - have [/= dX DdX] := @column_pivot (tr_model beta_model) i0. by exists dX => nzi0 i j nzi nzj; rewrite betaE ?DdX. have /fin_all_exists [dX0j betaX0j] j0: exists dX, j0 != 0 -> forall i j, i != 0 -> j != 0 -> '[beta i j, dchi dX] = (j == j0)%:R. - have [dX DdX] := @column_pivot beta_model j0. by exists dX => nzj0 i j nzi nzj; rewrite betaE ?DdX. pose Xi0 j := dchi (dXi0 j); pose X0j i := dchi (dX0j i). pose xi_ i j := if i == 0 then if j == 0 then 1 else - X0j j else if j == 0 then - Xi0 i else beta i j - Xi0 i - X0j j. exists xi_; split=> [| i j | i j nzi nzj | i1 j1 i2 j2]. - by rewrite /xi_ !eqxx. - rewrite /xi_; do 2!case: ifP => _; rewrite ?rpred1 ?rpredN ?dchi_vchar //. by rewrite 2?rpredB ?dchi_vchar. - by rewrite /xi_ /= !ifN // addrCA subrK addrACA subrK addrA addrK. have o_dchi i j dk1 dk2 (phi := beta i j): '[phi, dchi dk1] = 1 -> '[phi, dchi dk2] = 0 -> '[dchi dk1, dchi dk2] = 0. - move=> phi1 phi0; have /eqP: 1 != 0 :> algC := oner_neq0 _. rewrite -phi1 cfdot_dchi; do 2!case: eqP => [->|_]; rewrite ?subrr //. by rewrite dchi_ndirrE cfdotNr phi0 oppr0. have [nzi01 nzj01] := (Iirr1_neq0 ntW1, Iirr1_neq0 ntW2). have X0j_1 j: j != 0 -> '[X0j j, 1] = 0. by move=> nzj; rewrite -dchi1 (o_dchi #1 j) ?betaX0j ?eqxx ?dchi1 ?o_beta_1. have Xi0_1 i: i != 0 -> '[Xi0 i, 1] = 0. by move=> nzi; rewrite -dchi1 (o_dchi i #1) ?betaXi0 ?eqxx ?dchi1 ?o_beta_1. have Xi0_X0j i j: i != 0 -> j != 0 -> '[Xi0 i, X0j j] = 0. move=> nzi nzj; pose j' := conjC_Iirr j. apply: (o_dchi i j'); rewrite (betaX0j, betaXi0) ?conjC_Iirr_eq0 ?eqxx //. by rewrite -(inj_eq irr_inj) conjC_IirrE mulrb ifN ?odd_eq_conj_irr1 ?irr_eq1. have X0j_X0j j j0: j != 0 -> j0 != 0 -> '[X0j j, X0j j0] = (j == j0)%:R. move=> nzj nzj0; case: (altP eqP) => [-> | j0'j]; first exact: cfnorm_dchi. by apply: (o_dchi #1 j); rewrite ?betaX0j ?eqxx ?(negPf j0'j). have Xi0_Xi0 i i0: i != 0 -> i0 != 0 -> '[Xi0 i, Xi0 i0] = (i == i0)%:R. move=> nzi nzi0; case: (altP eqP) => [-> | i0'i]; first exact: cfnorm_dchi. by apply: (o_dchi i #1); rewrite ?betaXi0 ?eqxx ?(negPf i0'i). have oxi_00 i j: '[xi_ i j, xi_ 0 0] = ((i == 0) && (j == 0))%:R. rewrite /xi_; case: ifPn => [_ | nzi]. by case: ifPn => [_ | nzj]; rewrite ?cfnorm1 // cfdotNl X0j_1 ?oppr0. case: ifPn => [_ | nzj]; first by rewrite cfdotNl Xi0_1 ?oppr0. by rewrite 2!cfdotBl o_beta_1 ?X0j_1 ?Xi0_1 ?subr0. have oxi_0j i j j0: '[xi_ i j, xi_ 0 j0] = ((i == 0) && (j == j0))%:R. rewrite /xi_; have [-> | nzj0] := altP (j0 =P 0); first exact: oxi_00. rewrite cfdotNr; case: ifPn => [_ | nzi]. have [-> | nzj] := altP eqP; last by rewrite cfdotNl opprK X0j_X0j. by rewrite cfdotC X0j_1 // conjC0 oppr0 mulrb ifN_eqC. have [_ | nzj] := ifPn; first by rewrite cfdotNl Xi0_X0j ?oppr0. by rewrite 2!cfdotBl Xi0_X0j // subr0 betaX0j ?X0j_X0j // subrr oppr0. have{oxi_00} oxi_i0 i j i0: '[xi_ i j, xi_ i0 0] = ((i == i0) && (j == 0))%:R. rewrite /xi_; have [-> | nzi0] := altP (i0 =P 0); first exact: oxi_00. rewrite cfdotNr andbC; have [_ | nzj] := boolP (j == 0). have [-> | nzi] := altP eqP; last by rewrite cfdotNl opprK Xi0_Xi0. by rewrite cfdotC Xi0_1 // conjC0 oppr0 mulrb ifN_eqC. have [_ | nzi] := ifPn; first by rewrite cfdotNl opprK cfdotC Xi0_X0j ?conjC0. rewrite 2!cfdotBl betaXi0 ?Xi0_Xi0 // subrr add0r opprK. by rewrite cfdotC Xi0_X0j // conjC0. have [-> | nzi2] := altP (i2 =P 0); first exact: oxi_0j. have [-> | nzj2] := altP (j2 =P 0); first exact: oxi_i0. rewrite cfdotC eq_sym; apply: canLR (@conjCK _) _; rewrite rmorph_nat. have [-> | nzi1] := altP (i1 =P 0); first exact: oxi_0j. have [-> | nzj1] := altP (j1 =P 0); first exact: oxi_i0. have ->: xi_ i1 j1 = beta i1 j1 + xi_ i1 0 + xi_ 0 j1 by rewrite /xi_ !ifN. rewrite 2!cfdotDr oxi_i0 oxi_0j andbC /xi_ (negPf nzi2) (negPf nzj2) !addr0. rewrite eq_sym xpair_eqE cfdotC 2!cfdotBr o_beta // betaXi0 ?betaX0j //. by rewrite !pmulrn -!mulrzBr rmorph_int; do 2!case: (_ == _). 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)