proposition: Lemma general_Dade_reciprocity alpha (phi : 'CF(G)) (psi : 'CF(L)) : alpha \in 'CF(L, A) -> {in A, forall a, psi a = #|H a|%:R ^-1 * (\sum_(x in H a) phi (x * a)%g)} -> '[alpha^\tau, phi] = '[alpha, psi].
proof: Proof. move=> CFalpha psiA; rewrite (cfdotEl _ (Dade_cfunS _)). pose T := [set repr (a ^: L) | a in A]. have sTA: {subset T <= A}. move=> _ /imsetP[a Aa ->]; have [x Lx ->] := repr_class L a. by rewrite memJ_norm ?(subsetP nAL). pose P_G := [set dd1 x | x in T]. have dd1_id: {in A, forall a, dd1 (repr (a ^: L)) = dd1 a}. by move=> a Aa /=; have [x Lx ->] := repr_class L a; apply: Dade_support1_id. have ->: Atau = cover P_G. apply/setP=> u; apply/bigcupP/bigcupP=> [[a Aa Fa_u] | [Fa]]; last first. by case/imsetP=> a /sTA Aa -> Fa_u; exists a. by exists (dd1 a) => //; rewrite -dd1_id //; do 2!apply: imset_f. have [tiP_G inj_dd1]: trivIset P_G /\ {in T &, injective dd1}. apply: trivIimset => [_ _ /imsetP[a Aa ->] /imsetP[b Ab ->] |]; last first. apply/imsetP=> [[a]]; move/sTA=> Aa; move/esym; move/eqP; case/set0Pn. by exists (a ^ 1)%g; apply: imset2_f; rewrite ?group1 ?rcoset_refl. rewrite !dd1_id //; apply: contraR. by case/Dade_support1_TI=> // x Lx ->; rewrite classGidl. rewrite big_trivIset //= big_imset {P_G tiP_G inj_dd1}//=. symmetry; rewrite (cfdotEl _ CFalpha). pose P_A := [set a ^: L | a in T]. have rLid x: repr (x ^: L) ^: L = x ^: L. by have [y Ly ->] := repr_class L x; rewrite classGidl. have {1}<-: cover P_A = A. apply/setP=> a; apply/bigcupP/idP=> [[_ /imsetP[d /sTA Ab ->]] | Aa]. by case/imsetP=> x Lx ->; rewrite memJ_norm ?(subsetP nAL). by exists (a ^: L); rewrite ?class_refl // -rLid; do 2!apply: imset_f. have [tiP_A injFA]: trivIset P_A /\ {in T &, injective (class^~ L)}. apply: trivIimset => [_ _ /imsetP[a Aa ->] /imsetP[b Ab ->] |]; last first. by apply/imsetP=> [[a _ /esym/eqP/set0Pn[]]]; exists a; apply: class_refl. rewrite !rLid; apply: contraR => /pred0Pn[c /andP[/=]]. by do 2!move/class_eqP <-. rewrite big_trivIset //= big_imset {P_A tiP_A injFA}//=. apply: canRL (mulKf (neq0CG G)) _; rewrite mulrA big_distrr /=. apply: eq_bigr => a /sTA=> {T sTA}Aa. have [La def_Ca] := (subsetP sAL a Aa, defCA Aa). rewrite (eq_bigr (fun _ => alpha a * (psi a)^*)) => [|ax]; last first. by case/imsetP=> x Lx ->{ax}; rewrite !cfunJ. rewrite sumr_const -index_cent1 mulrC -mulr_natr -!mulrA. rewrite (eq_bigr (fun xa => alpha a * (phi xa)^*)) => [|xa Fa_xa]; last first. by rewrite (DadeE _ Aa). rewrite -big_distrr /= -rmorph_sum; congr (_ * _). rewrite mulrC mulrA -natrM mulnC -(Lagrange (subsetIl G 'C[a])). rewrite -mulnA mulnCA -(sdprod_card def_Ca) -mulnA Lagrange ?subsetIl //. rewrite mulnA natrM mulfK ?neq0CG // -conjC_nat -rmorphM; congr (_ ^*). have /and3P[_ tiHa _] := Dade_cover_TI Aa. rewrite (set_partition_big _ (partition_class_support _ _)) //=. rewrite (eq_bigr (fun _ => \sum_(x in H a) phi (x * a)%g)); last first. move=> _ /imsetP[x Gx ->]; rewrite -rcosetE. rewrite (big_imset _ (in2W (conjg_inj x))) (big_imset _ (in2W (mulIg a))) /=. by apply: eq_bigr => u Hu; rewrite cfunJ ?groupM ?(subsetP sLG a). rewrite sumr_const card_orbit astab1Js norm_Dade_cover //. by rewrite natrM -mulrA mulr_natl psiA // mulVKf ?neq0CG. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius ssrnum) mathcomp(matrix mxalgebra mxrepresentation vector algC classfun character) mathcomp(inertia vcharacter) odd_order(PFsection1)