proposition: Theorem cyclicTIiso_exists : {sigma : 'Hom(cfun_vectType W, cfun_vectType G) | [/\ {in 'Z[irr W], isometry sigma, to 'Z[irr G]}, sigma 1 = 1 & {in 'CF(W, V), forall phi : 'CF(W), sigma phi = 'Ind[G] phi}]}.
proof: Proof. pose sigmaVP f := ('CF(W, V) <= lker (linfun f - linfun 'Ind[G]))%VS. pose sigmaP f := [&& orthonormal (map f (irr W)), f 1 == 1 & sigmaVP f]. pose sigma_base f := [seq (dchi (f k) : 'CF(G)) | k : Iirr W]. pose sigma_spec f := sigmaP (sval (linear_of_free (irr W) (sigma_base f))). suffices /sigW[f /and3P[]]: exists f : {ffun _}, sigma_spec f. case: linear_of_free => /=sigma Dsigma o1sigma /eqP sigma1 /eqlfun_inP sigmaV. exists (linfun sigma); split=> [|| phi /sigmaV]; try by rewrite !lfunE. do [rewrite size_map !size_tuple => /(_ (irr_free W) (card_ord _))] in Dsigma. have [inj_sigma dot_sigma] := orthonormalP o1sigma. rewrite -(map_tnth_enum (irr W)) -map_comp in Dsigma inj_sigma. move/eq_in_map in Dsigma; move/injectiveP in inj_sigma. split=> [|_ /zchar_tuple_expansion[z Zz ->]]. apply: isometry_in_zchar=> _ _ /irrP[k1 ->] /irrP[k2 ->] /=. by rewrite !lfunE dot_sigma ?map_f ?mem_irr // cfdot_irr (inj_eq inj_sigma). rewrite linear_sum rpred_sum // => k _; rewrite linearZ rpredZ_Cint //=. by rewrite -tnth_nth lfunE [sigma _]Dsigma ?mem_enum ?dchi_vchar. have [xi_ [xi00 Zxi Dxi o1xi]] := cyclicTIiso_basis_exists. pose f := [ffun k => dirr_dIirr (uncurry xi_) (inv_dprod_Iirr defW k)]. exists f; apply/and3P; case: linear_of_free => /= sigma Dsigma. have{f Dsigma} Deta i j: sigma (w_ i j) = xi_ i j. rewrite /w_ -tnth_map /= (tnth_nth 0) /=. rewrite Dsigma ?irr_free //; last by rewrite !size_tuple card_ord. rewrite nth_mktuple ffunE dprod_IirrK dirr_dIirrE // => {i j} [[i j]] /=. by rewrite dirrE Zxi o1xi !eqxx. have sigma1: sigma 1 = 1 by rewrite -w_00 Deta. rewrite sigma1 /sigmaVP -(span_basis cfWVbasis); split=> //. rewrite map_orthonormal ?irr_orthonormal //; apply: isometry_in_zchar. move=> _ _ /cycTIirrP[i1 [j1 ->]] /cycTIirrP[i2 [j2 ->]] /=. by rewrite !Deta o1xi cfdot_w. apply/span_subvP=> _ /imageP[[i j] /setXP[nzi nzj] ->]; rewrite !inE in nzi nzj. rewrite memv_ker !lfun_simp /= subr_eq0 Dxi //. by rewrite alphaE linearD !linearB sigma1 !Deta. 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)