proposition: Theorem primeTIirr_spec : [/\ injective Imu2, forall i j, 'Ind (ew_ i j) = delta_ j *: (mu2_ i j - mu2_ 0 j), forall i j, sigma (w_ i j) = delta_ j *: mu2_ i j, forall i j, {in W :\: W2, mu2_ i j =1 delta_ j *: w_ i j} & forall k, k \notin codom Imu2 -> {in W :\: W2, 'chi_k =1 \0}].
proof: Proof. have isoV2 := normedTI_isometry normedTI_prTIset (setDSS sWL (sub1G W2)). have /fin_all_exists2[dmu injl_mu Ddmu] j: exists2 dmu : bool * {ffun Iirr W1 -> Iirr L}, injective dmu.2 & forall i, 'Ind (ew_ i j) = dchi (dmu.1, dmu.2 i) - dchi (dmu.1, dmu.2 0). - pose Sj := [tuple w_ i j | i < Nirr W1]. have Sj0: Sj`_0 = w_ 0 j by rewrite (nth_mktuple _ 0 0). have irrSj: {subset Sj <= irr W} by move=> ? /mapP[i _ ->]; apply: mem_irr. have: {in 'Z[Sj, W :\: W2], isometry 'Ind, to 'Z[irr L, L^#]}. split=> [|phi]; first by apply: sub_in2 isoV2; apply: zchar_on. move/(zchar_subset irrSj)/(zchar_onS (setDS W (sub1G W2))). by rewrite !zcharD1E cfInd1 // mulf_eq0 orbC => /andP[/cfInd_vchar-> // ->]. case/vchar_isometry_base=> // [|||i|mu Umu [d Ddmu]]; first by rewrite NirrW1. + rewrite orthonormal_free // (sub_orthonormal irrSj) ?irr_orthonormal //. by apply/injectiveP=> i1 i2 /irr_inj/dprod_Iirr_inj[]. + by move=> _ /mapP[i _ ->]; rewrite Sj0 !lin_char1. + by rewrite nth_mktuple Sj0 V2ew. exists (d, [ffun i => tnth mu i]) => [|i]. apply/injectiveP; congr (uniq _): Umu; rewrite -[LHS]map_tnth_enum. by apply/eq_map=> i; rewrite ffunE. by rewrite -scalerBr /= !ffunE !(tnth_nth 0 mu) -Ddmu nth_mktuple Sj0. pose Imu ij := (dmu ij.2).2 ij.1; pose mu i j := 'chi_(Imu (i, j)). pose d j : algC := (-1) ^+ (dmu j).1. have{} Ddmu i j: 'Ind (ew_ i j) = d j *: (mu i j - mu 0 j). by rewrite Ddmu scalerBr. have{injl_mu} inj_Imu: injective Imu. move=> [i1 j1] [i2 j2]; rewrite /Imu /=; pose S i j k := mu i j :: mu k j. have [-> /injl_mu-> // | j2'1 /eqP/negPf[] /=] := eqVneq j1 j2. apply/(can_inj oddb)/eqP; rewrite -eqC_nat -cfdot_irr -!/(mu _ _) mulr0n. have oIew_j12 i k: '['Ind[L] (ew_ i j1), 'Ind[L] (ew_ k j2)] = 0. by rewrite isoV2 // cfdotBl !cfdotBr !cfdot_w (negPf j2'1) !andbF !subr0. have defSd i j k: mu i j - mu k j = d j *: ('Ind (ew_ i j) - 'Ind (ew_ k j)). by rewrite !Ddmu -scalerBr signrZK opprB addrA subrK. have Sd1 i j k: (mu i j - mu k j) 1%g == 0. by rewrite defSd !(cfunE, cfInd1) ?lin_char1 // !subrr mulr0. have exS i j: {k | {subset S i j k <= 'Z[irr L]} & orthonormal (S i j k)}. have:= w1gt1; rewrite -nirrW1 (cardD1 i) => /card_gt0P/sigW[k /andP[i'k _]]. exists k; first by apply/allP; rewrite /= !irr_vchar. apply/andP; rewrite /= !cfdot_irr !eqxx !andbT /=. by rewrite (inj_eq (injl_mu j)) mulrb ifN_eqC. have [[k1 ZS1 o1S1] [k2 ZS2 o1S2]] := (exS i1 j1, exS i2 j2). rewrite (orthonormal_vchar_diff_ortho (conj ZS1 ZS2)) ?o1S1 ?Sd1 ?andbT //. by rewrite !defSd cfdotZl cfdotZr cfdotBl !cfdotBr !oIew_j12 !subrr !mulr0. pose V2base := [tuple of [seq ew_ ij.1 ij.2 | ij in predX (predC1 0) predT]]. have V2basis: basis_of 'CF(W, W :\: W2) V2base. suffices V2free: free V2base. rewrite basisEfree V2free size_image /= cardX cardC1 nirrW1 nirrW2 -subn1. rewrite mulnBl mul1n dim_cfun_on_abelian ?subsetDl //. rewrite cardsD (setIidPr _) // (dprod_card defW) leqnn andbT. by apply/span_subvP=> _ /mapP[ij _ ->]. apply/freeP=> /= z zV2e0 k. move Dk: (enum_val k) (enum_valP k) => [i j] /andP[/= nz_i _]. rewrite -(cfdot0l (w_ i j)) -{}zV2e0 cfdot_suml (bigD1 k) //= cfdotZl. rewrite nth_image Dk cfdotBl !cfdot_w !eqxx eq_sym (negPf nz_i) subr0 mulr1. rewrite big1 ?addr0 // => k1; rewrite -(inj_eq enum_val_inj) {}Dk nth_image. case: (enum_val k1) => /= i1 j1 ij'ij1. rewrite cfdotZl cfdotBl !cfdot_dprod_irr [_ && _](negPf ij'ij1). by rewrite eq_sym (negPf nz_i) subr0 mulr0. have nsV2W: W :\: W2 <| W by rewrite -sub_abelian_normal ?subsetDl. pose muW k := let: ij := inv_dprod_Iirr defW k in d ij.2 *: mu ij.1 ij.2. have inW := codomP (dprod_Iirr_onto defW _). have ImuW k1 k2: '[muW k1, muW k2] = (k1 == k2)%:R. have [[[i1 j1] -> {k1}] [[i2 j2] -> {k2}]] := (inW k1, inW k2). rewrite cfdotZl cfdotZr !dprod_IirrK (can_eq (dprod_IirrK _)) /= rmorph_sign. rewrite cfdot_irr (inj_eq inj_Imu (_, _) (_, _)) -/(d _). by case: eqP => [[_ ->] | _]; rewrite ?signrMK ?mulr0. have [k|muV2 mu'V2] := equiv_restrict_compl_ortho sWL nsV2W V2basis ImuW. rewrite nth_image; case: (enum_val k) (enum_valP k) => /= i j /andP[/= nzi _]. pose inWj i1 := dprod_Iirr defW (i1, j); rewrite (bigD1 (inWj 0)) //=. rewrite (bigD1 (inWj i)) ?(can_eq (dprod_IirrK _)) ?xpair_eqE ?(negPf nzi) //. rewrite /= big1 ?addr0 => [|k1 /andP[]]; last first. rewrite !(eq_sym k1); have [[i1 j1] -> {k1}] := inW k1. rewrite !(can_eq (dprod_IirrK _)) => ij1'i ij1'0. by rewrite cfdotBl !cfdot_w !mulrb !ifN // subrr scale0r. rewrite /muW !dprod_IirrK /= addrC !cfdotBl !cfdot_w !eqxx /= !andbT. by rewrite eq_sym (negPf nzi) subr0 add0r scaleNr !scale1r -scalerBr. have Dsigma i j: sigma (w_ i j) = d j *: mu i j. apply/esym/eq_in_cycTIiso=> [|x Vx]; first exact: (dirr_dchi (_, _)). by rewrite -muV2 ?(subsetP sV_V2) // /muW dprod_IirrK. have /all_and2[Dd Dmu] j: d j = delta_ j /\ forall i, Imu (i, j) = Imu2 (i, j). suffices DprTI i: primeTIdIirr (i, j) = ((dmu j).1, (dmu j).2 i). by split=> [|i]; rewrite /primeTI_Isign /Imu2 DprTI. apply: dirr_inj; rewrite /primeTIdIirr unlock_with dirr_dIirrE /= ?Dsigma //. by case=> i1 j1; apply: cycTIiso_dirr. split=> [[i1 j1] [i2 j2] | i j | i j | i j x V2x | k mu2p'k]. - by rewrite -!Dmu => /inj_Imu. - by rewrite -!Dmu -Dd -Ddmu. - by rewrite -Dmu -Dd -Dsigma. - by rewrite cfunE -muV2 // /muW dprod_IirrK Dd cfunE signrMK -Dmu. apply: mu'V2 => k1; have [[i j] ->{k1}] := inW k1. apply: contraNeq mu2p'k; rewrite cfdotZr rmorph_sign mulf_eq0 signr_eq0 /=. rewrite /mu Dmu dprod_IirrK -irr_consttE constt_irr inE /= => /eqP <-. exact: codom_f. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset fingroup) mathcomp(morphism perm automorphism quotient action gfunctor gproduct) mathcomp(center commutator zmodp cyclic pgroup nilpotent hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC classfun) mathcomp(character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3)