Library mathcomp.character.vcharacter
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+Set Implicit Arguments.
+ +
+Import GroupScope GRing.Theory Num.Theory.
+Local Open Scope ring_scope.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+Set Implicit Arguments.
+ +
+Import GroupScope GRing.Theory Num.Theory.
+Local Open Scope ring_scope.
+ +
+
+ This file provides basic notions of virtual character theory:
+ 'Z[S, A] == collective predicate for the phi that are Z-linear
+ combinations of elements of S : seq 'CF(G) and have
+ support in A : {set gT}.
+ 'Z[S] == collective predicate for the Z-linear combinations of
+ elements of S.
+ 'Z[irr G] == the collective predicate for virtual characters.
+ dirr G == the collective predicate for normal virtual characters,
+ i.e., virtual characters of norm 1:
+ mu \in dirr G <=> m \in 'Z[irr G] and ' [mu] = 1
+ <=> mu or - mu \in irr G.
+> othonormal subsets of 'Z[irr G] are contained in dirr G.
+ dIirr G == an index type for normal virtual characters.
+ dchi i == the normal virtual character of index i.
+ of_irr i == the (unique) irreducible constituent of dchi i:
+ dchi i = 'chi(of_irr i) or - 'chi(of_irr i).
+ ndirr i == the index of - dchi i.
+ dirr1 G == the normal virtual character index of 1 : 'CF(G), the
+ principal character.
+ dirr_dIirr j f == the index i (or dirr1 G if it does not exist) such that
+ dchi i = f j.
+ dirr_constt phi == the normal virtual character constituents of phi:
+ i \in dirr_constt phi <=> [dchi i, phi] > 0.
+ to_dirr phi i == the normal virtual character constituent of phi with an
+ irreducible constituent i, when i \in irr_constt phi.
+
+
+
+
+Section Basics.
+ +
+Variables (gT : finGroupType) (B : {set gT}) (S : seq 'CF(B)) (A : {set gT}).
+ +
+Definition Zchar : pred_class :=
+ [pred phi in 'CF(B, A) | dec_Cint_span (in_tuple S) phi].
+Fact Zchar_key : pred_key Zchar.
+Canonical Zchar_keyed := KeyedPred Zchar_key.
+ +
+Lemma cfun0_zchar : 0 \in Zchar.
+ +
+Fact Zchar_zmod : zmod_closed Zchar.
+Canonical Zchar_opprPred := OpprPred Zchar_zmod.
+Canonical Zchar_addrPred := AddrPred Zchar_zmod.
+Canonical Zchar_zmodPred := ZmodPred Zchar_zmod.
+ +
+Lemma scale_zchar a phi : a \in Cint → phi \in Zchar → a *: phi \in Zchar.
+ +
+End Basics.
+ +
+Notation "''Z[' S , A ]" := (Zchar S A)
+ (at level 8, format "''Z[' S , A ]") : group_scope.
+Notation "''Z[' S ]" := 'Z[S, setT]
+ (at level 8, format "''Z[' S ]") : group_scope.
+ +
+Section Zchar.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+Implicit Types (A B : {set gT}) (S : seq 'CF(G)).
+ +
+Lemma zchar_split S A phi :
+ phi \in 'Z[S, A] = (phi \in 'Z[S]) && (phi \in 'CF(G, A)).
+ +
+Lemma zcharD1E phi S : (phi \in 'Z[S, G^#]) = (phi \in 'Z[S]) && (phi 1%g == 0).
+ +
+Lemma zcharD1 phi S A :
+ (phi \in 'Z[S, A^#]) = (phi \in 'Z[S, A]) && (phi 1%g == 0).
+ +
+Lemma zcharW S A : {subset 'Z[S, A] ≤ 'Z[S]}.
+ +
+Lemma zchar_on S A : {subset 'Z[S, A] ≤ 'CF(G, A)}.
+ +
+Lemma zchar_onS A B S : A \subset B → {subset 'Z[S, A] ≤ 'Z[S, B]}.
+ +
+Lemma zchar_onG S : 'Z[S, G] =i 'Z[S].
+ +
+Lemma irr_vchar_on A : {subset 'Z[irr G, A] ≤ 'CF(G, A)}.
+ +
+Lemma support_zchar S A phi : phi \in 'Z[S, A] → support phi \subset A.
+ +
+Lemma mem_zchar_on S A phi :
+ phi \in 'CF(G, A) → phi \in S → phi \in 'Z[S, A].
+ +
+
+
++Section Basics.
+ +
+Variables (gT : finGroupType) (B : {set gT}) (S : seq 'CF(B)) (A : {set gT}).
+ +
+Definition Zchar : pred_class :=
+ [pred phi in 'CF(B, A) | dec_Cint_span (in_tuple S) phi].
+Fact Zchar_key : pred_key Zchar.
+Canonical Zchar_keyed := KeyedPred Zchar_key.
+ +
+Lemma cfun0_zchar : 0 \in Zchar.
+ +
+Fact Zchar_zmod : zmod_closed Zchar.
+Canonical Zchar_opprPred := OpprPred Zchar_zmod.
+Canonical Zchar_addrPred := AddrPred Zchar_zmod.
+Canonical Zchar_zmodPred := ZmodPred Zchar_zmod.
+ +
+Lemma scale_zchar a phi : a \in Cint → phi \in Zchar → a *: phi \in Zchar.
+ +
+End Basics.
+ +
+Notation "''Z[' S , A ]" := (Zchar S A)
+ (at level 8, format "''Z[' S , A ]") : group_scope.
+Notation "''Z[' S ]" := 'Z[S, setT]
+ (at level 8, format "''Z[' S ]") : group_scope.
+ +
+Section Zchar.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+Implicit Types (A B : {set gT}) (S : seq 'CF(G)).
+ +
+Lemma zchar_split S A phi :
+ phi \in 'Z[S, A] = (phi \in 'Z[S]) && (phi \in 'CF(G, A)).
+ +
+Lemma zcharD1E phi S : (phi \in 'Z[S, G^#]) = (phi \in 'Z[S]) && (phi 1%g == 0).
+ +
+Lemma zcharD1 phi S A :
+ (phi \in 'Z[S, A^#]) = (phi \in 'Z[S, A]) && (phi 1%g == 0).
+ +
+Lemma zcharW S A : {subset 'Z[S, A] ≤ 'Z[S]}.
+ +
+Lemma zchar_on S A : {subset 'Z[S, A] ≤ 'CF(G, A)}.
+ +
+Lemma zchar_onS A B S : A \subset B → {subset 'Z[S, A] ≤ 'Z[S, B]}.
+ +
+Lemma zchar_onG S : 'Z[S, G] =i 'Z[S].
+ +
+Lemma irr_vchar_on A : {subset 'Z[irr G, A] ≤ 'CF(G, A)}.
+ +
+Lemma support_zchar S A phi : phi \in 'Z[S, A] → support phi \subset A.
+ +
+Lemma mem_zchar_on S A phi :
+ phi \in 'CF(G, A) → phi \in S → phi \in 'Z[S, A].
+ +
+
+ A special lemma is needed because trivial fails to use the cfun_onT Hint.
+
+
+Lemma mem_zchar S phi : phi \in S → phi \in 'Z[S].
+ +
+Lemma zchar_nth_expansion S A phi :
+ phi \in 'Z[S, A] →
+ {z | ∀ i, z i \in Cint & phi = \sum_(i < size S) z i *: S`_i}.
+ +
+Lemma zchar_tuple_expansion n (S : n.-tuple 'CF(G)) A phi :
+ phi \in 'Z[S, A] →
+ {z | ∀ i, z i \in Cint & phi = \sum_(i < n) z i *: S`_i}.
+ +
+
+
++ +
+Lemma zchar_nth_expansion S A phi :
+ phi \in 'Z[S, A] →
+ {z | ∀ i, z i \in Cint & phi = \sum_(i < size S) z i *: S`_i}.
+ +
+Lemma zchar_tuple_expansion n (S : n.-tuple 'CF(G)) A phi :
+ phi \in 'Z[S, A] →
+ {z | ∀ i, z i \in Cint & phi = \sum_(i < n) z i *: S`_i}.
+ +
+
+ A pure seq version with the extra hypothesis of S's unicity.
+
+
+Lemma zchar_expansion S A phi : uniq S →
+ phi \in 'Z[S, A] →
+ {z | ∀ xi, z xi \in Cint & phi = \sum_(xi <- S) z xi *: xi}.
+ +
+Lemma zchar_span S A : {subset 'Z[S, A] ≤ <<S>>%VS}.
+ +
+Lemma zchar_trans S1 S2 A B :
+ {subset S1 ≤ 'Z[S2, B]} → {subset 'Z[S1, A] ≤ 'Z[S2, A]}.
+ +
+Lemma zchar_trans_on S1 S2 A :
+ {subset S1 ≤ 'Z[S2, A]} → {subset 'Z[S1] ≤ 'Z[S2, A]}.
+ +
+Lemma zchar_sub_irr S A :
+ {subset S ≤ 'Z[irr G]} → {subset 'Z[S, A] ≤ 'Z[irr G, A]}.
+ +
+Lemma zchar_subset S1 S2 A :
+ {subset S1 ≤ S2} → {subset 'Z[S1, A] ≤ 'Z[S2, A]}.
+ +
+Lemma zchar_subseq S1 S2 A :
+ subseq S1 S2 → {subset 'Z[S1, A] ≤ 'Z[S2, A]}.
+ +
+Lemma zchar_filter S A (p : pred 'CF(G)) :
+ {subset 'Z[filter p S, A] ≤ 'Z[S, A]}.
+ +
+End Zchar.
+ +
+Section VChar.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+Implicit Types (A B : {set gT}) (phi chi : 'CF(G)) (S : seq 'CF(G)).
+ +
+Lemma char_vchar chi : chi \is a character → chi \in 'Z[irr G].
+ +
+Lemma irr_vchar i : 'chi[G]_i \in 'Z[irr G].
+ +
+Lemma cfun1_vchar : 1 \in 'Z[irr G].
+ +
+Lemma vcharP phi :
+ reflect (exists2 chi1, chi1 \is a character
+ & exists2 chi2, chi2 \is a character & phi = chi1 - chi2)
+ (phi \in 'Z[irr G]).
+ +
+Lemma Aint_vchar phi x : phi \in 'Z[irr G] → phi x \in Aint.
+ +
+Lemma Cint_vchar1 phi : phi \in 'Z[irr G] → phi 1%g \in Cint.
+ +
+Lemma Cint_cfdot_vchar_irr i phi : phi \in 'Z[irr G] → '[phi, 'chi_i] \in Cint.
+ +
+Lemma cfdot_vchar_r phi psi :
+ psi \in 'Z[irr G] → '[phi, psi] = \sum_i '[phi, 'chi_i] × '[psi, 'chi_i].
+ +
+Lemma Cint_cfdot_vchar : {in 'Z[irr G] &, ∀ phi psi, '[phi, psi] \in Cint}.
+ +
+Lemma Cnat_cfnorm_vchar : {in 'Z[irr G], ∀ phi, '[phi] \in Cnat}.
+ +
+Fact vchar_mulr_closed : mulr_closed 'Z[irr G].
+Canonical vchar_mulrPred := MulrPred vchar_mulr_closed.
+Canonical vchar_smulrPred := SmulrPred vchar_mulr_closed.
+Canonical vchar_semiringPred := SemiringPred vchar_mulr_closed.
+Canonical vchar_subringPred := SubringPred vchar_mulr_closed.
+ +
+Lemma mul_vchar A :
+ {in 'Z[irr G, A] &, ∀ phi psi, phi × psi \in 'Z[irr G, A]}.
+ +
+Section CfdotPairwiseOrthogonal.
+ +
+Variables (M : {group gT}) (S : seq 'CF(G)) (nu : 'CF(G) → 'CF(M)).
+Hypotheses (Inu : {in 'Z[S] &, isometry nu}) (oSS : pairwise_orthogonal S).
+ +
+Let freeS := orthogonal_free oSS.
+Let uniqS : uniq S := free_uniq freeS.
+Let Z_S : {subset S ≤ 'Z[S]}.
+Let notS0 : 0 \notin S.
+Let dotSS := proj2 (pairwise_orthogonalP oSS).
+ +
+Lemma map_pairwise_orthogonal : pairwise_orthogonal (map nu S).
+ +
+Lemma cfproj_sum_orthogonal P z phi :
+ phi \in S →
+ '[\sum_(xi <- S | P xi) z xi *: nu xi, nu phi]
+ = if P phi then z phi × '[phi] else 0.
+ +
+Lemma cfdot_sum_orthogonal z1 z2 :
+ '[\sum_(xi <- S) z1 xi *: nu xi, \sum_(xi <- S) z2 xi *: nu xi]
+ = \sum_(xi <- S) z1 xi × (z2 xi)^* × '[xi].
+ +
+Lemma cfnorm_sum_orthogonal z :
+ '[\sum_(xi <- S) z xi *: nu xi] = \sum_(xi <- S) `|z xi| ^+ 2 × '[xi].
+ +
+Lemma cfnorm_orthogonal : '[\sum_(xi <- S) nu xi] = \sum_(xi <- S) '[xi].
+ +
+End CfdotPairwiseOrthogonal.
+ +
+Lemma orthogonal_span S phi :
+ pairwise_orthogonal S → phi \in <<S>>%VS →
+ {z | z = fun xi ⇒ '[phi, xi] / '[xi] & phi = \sum_(xi <- S) z xi *: xi}.
+ +
+Section CfDotOrthonormal.
+ +
+Variables (M : {group gT}) (S : seq 'CF(G)) (nu : 'CF(G) → 'CF(M)).
+Hypotheses (Inu : {in 'Z[S] &, isometry nu}) (onS : orthonormal S).
+Let oSS := orthonormal_orthogonal onS.
+Let freeS := orthogonal_free oSS.
+Let nS1 : {in S, ∀ phi, '[phi] = 1}.
+ +
+Lemma map_orthonormal : orthonormal (map nu S).
+ +
+Lemma cfproj_sum_orthonormal z phi :
+ phi \in S → '[\sum_(xi <- S) z xi *: nu xi, nu phi] = z phi.
+ +
+Lemma cfdot_sum_orthonormal z1 z2 :
+ '[\sum_(xi <- S) z1 xi *: xi, \sum_(xi <- S) z2 xi *: xi]
+ = \sum_(xi <- S) z1 xi × (z2 xi)^*.
+ +
+Lemma cfnorm_sum_orthonormal z :
+ '[\sum_(xi <- S) z xi *: nu xi] = \sum_(xi <- S) `|z xi| ^+ 2.
+ +
+Lemma cfnorm_map_orthonormal : '[\sum_(xi <- S) nu xi] = (size S)%:R.
+ +
+Lemma orthonormal_span phi :
+ phi \in <<S>>%VS →
+ {z | z = fun xi ⇒ '[phi, xi] & phi = \sum_(xi <- S) z xi *: xi}.
+ +
+End CfDotOrthonormal.
+ +
+Lemma cfnorm_orthonormal S :
+ orthonormal S → '[\sum_(xi <- S) xi] = (size S)%:R.
+ +
+Lemma vchar_orthonormalP S :
+ {subset S ≤ 'Z[irr G]} →
+ reflect (∃ I : {set Iirr G}, ∃ b : Iirr G → bool,
+ perm_eq S [seq (-1) ^+ b i *: 'chi_i | i in I])
+ (orthonormal S).
+ +
+Lemma vchar_norm1P phi :
+ phi \in 'Z[irr G] → '[phi] = 1 →
+ ∃ b : bool, ∃ i : Iirr G, phi = (-1) ^+ b *: 'chi_i.
+ +
+Lemma zchar_small_norm phi n :
+ phi \in 'Z[irr G] → '[phi] = n%:R → (n < 4)%N →
+ {S : n.-tuple 'CF(G) |
+ [/\ orthonormal S, {subset S ≤ 'Z[irr G]} & phi = \sum_(xi <- S) xi]}.
+ +
+Lemma vchar_norm2 phi :
+ phi \in 'Z[irr G, G^#] → '[phi] = 2%:R →
+ ∃ i, exists2 j, j != i & phi = 'chi_i - 'chi_j.
+ +
+End VChar.
+ +
+Section Isometries.
+ +
+Variables (gT : finGroupType) (L G : {group gT}) (S : seq 'CF(L)).
+Implicit Type nu : {additive 'CF(L) → 'CF(G)}.
+ +
+Lemma Zisometry_of_cfnorm (tauS : seq 'CF(G)) :
+ pairwise_orthogonal S → pairwise_orthogonal tauS →
+ map cfnorm tauS = map cfnorm S → {subset tauS ≤ 'Z[irr G]} →
+ {tau : {linear 'CF(L) → 'CF(G)} | map tau S = tauS
+ & {in 'Z[S], isometry tau, to 'Z[irr G]}}.
+ +
+Lemma Zisometry_of_iso f :
+ free S → {in S, isometry f, to 'Z[irr G]} →
+ {tau : {linear 'CF(L) → 'CF(G)} | {in S, tau =1 f}
+ & {in 'Z[S], isometry tau, to 'Z[irr G]}}.
+ +
+Lemma Zisometry_inj A nu :
+ {in 'Z[S, A] &, isometry nu} → {in 'Z[S, A] &, injective nu}.
+ +
+Lemma isometry_in_zchar nu : {in S &, isometry nu} → {in 'Z[S] &, isometry nu}.
+ +
+End Isometries.
+ +
+Section AutVchar.
+ +
+Variables (u : {rmorphism algC → algC}) (gT : finGroupType) (G : {group gT}).
+Implicit Type (S : seq 'CF(G)) (phi chi : 'CF(G)).
+ +
+Lemma cfAut_zchar S A psi :
+ cfAut_closed u S → psi \in 'Z[S, A] → psi^u \in 'Z[S, A].
+ +
+Lemma cfAut_vchar A psi : psi \in 'Z[irr G, A] → psi^u \in 'Z[irr G, A].
+ +
+Lemma sub_aut_zchar S A psi :
+ {subset S ≤ 'Z[irr G]} → psi \in 'Z[S, A] → psi^u \in 'Z[S, A] →
+ psi - psi^u \in 'Z[S, A^#].
+ +
+Lemma conjC_vcharAut chi x : chi \in 'Z[irr G] → (u (chi x))^* = u (chi x)^*.
+ +
+Lemma cfdot_aut_vchar phi chi :
+ chi \in 'Z[irr G] → '[phi^u , chi^u] = u '[phi, chi].
+ +
+Lemma vchar_aut A chi : (chi^u \in 'Z[irr G, A]) = (chi \in 'Z[irr G, A]).
+ +
+End AutVchar.
+ +
+Definition cfConjC_vchar := cfAut_vchar conjC.
+ +
+Section MoreVchar.
+ +
+Variables (gT : finGroupType) (G H : {group gT}).
+ +
+Lemma cfRes_vchar phi : phi \in 'Z[irr G] → 'Res[H] phi \in 'Z[irr H].
+ +
+Lemma cfRes_vchar_on A phi :
+ H \subset G → phi \in 'Z[irr G, A] → 'Res[H] phi \in 'Z[irr H, A].
+ +
+Lemma cfInd_vchar phi : phi \in 'Z[irr H] → 'Ind[G] phi \in 'Z[irr G].
+ +
+Lemma sub_conjC_vchar A phi :
+ phi \in 'Z[irr G, A] → phi - (phi^*)%CF \in 'Z[irr G, A^#].
+ +
+Lemma Frobenius_kernel_exists :
+ [Frobenius G with complement H] → {K : {group gT} | [Frobenius G = K ><| H]}.
+ +
+End MoreVchar.
+ +
+Definition dirr (gT : finGroupType) (B : {set gT}) : pred_class :=
+ [pred f : 'CF(B) | (f \in irr B) || (- f \in irr B)].
+ +
+Section Norm1vchar.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+Fact dirr_key : pred_key (dirr G).
+Canonical dirr_keyed := KeyedPred dirr_key.
+ +
+Fact dirr_oppr_closed : oppr_closed (dirr G).
+ Canonical dirr_opprPred := OpprPred dirr_oppr_closed.
+ +
+Lemma dirr_opp v : (- v \in dirr G) = (v \in dirr G).
+Lemma dirr_sign n v : ((-1)^+ n *: v \in dirr G) = (v \in dirr G).
+ +
+Lemma irr_dirr i : 'chi_i \in dirr G.
+ +
+Lemma dirrP f :
+ reflect (∃ b : bool, ∃ i, f = (-1) ^+ b *: 'chi_i) (f \in dirr G).
+ +
+
+
++ phi \in 'Z[S, A] →
+ {z | ∀ xi, z xi \in Cint & phi = \sum_(xi <- S) z xi *: xi}.
+ +
+Lemma zchar_span S A : {subset 'Z[S, A] ≤ <<S>>%VS}.
+ +
+Lemma zchar_trans S1 S2 A B :
+ {subset S1 ≤ 'Z[S2, B]} → {subset 'Z[S1, A] ≤ 'Z[S2, A]}.
+ +
+Lemma zchar_trans_on S1 S2 A :
+ {subset S1 ≤ 'Z[S2, A]} → {subset 'Z[S1] ≤ 'Z[S2, A]}.
+ +
+Lemma zchar_sub_irr S A :
+ {subset S ≤ 'Z[irr G]} → {subset 'Z[S, A] ≤ 'Z[irr G, A]}.
+ +
+Lemma zchar_subset S1 S2 A :
+ {subset S1 ≤ S2} → {subset 'Z[S1, A] ≤ 'Z[S2, A]}.
+ +
+Lemma zchar_subseq S1 S2 A :
+ subseq S1 S2 → {subset 'Z[S1, A] ≤ 'Z[S2, A]}.
+ +
+Lemma zchar_filter S A (p : pred 'CF(G)) :
+ {subset 'Z[filter p S, A] ≤ 'Z[S, A]}.
+ +
+End Zchar.
+ +
+Section VChar.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+Implicit Types (A B : {set gT}) (phi chi : 'CF(G)) (S : seq 'CF(G)).
+ +
+Lemma char_vchar chi : chi \is a character → chi \in 'Z[irr G].
+ +
+Lemma irr_vchar i : 'chi[G]_i \in 'Z[irr G].
+ +
+Lemma cfun1_vchar : 1 \in 'Z[irr G].
+ +
+Lemma vcharP phi :
+ reflect (exists2 chi1, chi1 \is a character
+ & exists2 chi2, chi2 \is a character & phi = chi1 - chi2)
+ (phi \in 'Z[irr G]).
+ +
+Lemma Aint_vchar phi x : phi \in 'Z[irr G] → phi x \in Aint.
+ +
+Lemma Cint_vchar1 phi : phi \in 'Z[irr G] → phi 1%g \in Cint.
+ +
+Lemma Cint_cfdot_vchar_irr i phi : phi \in 'Z[irr G] → '[phi, 'chi_i] \in Cint.
+ +
+Lemma cfdot_vchar_r phi psi :
+ psi \in 'Z[irr G] → '[phi, psi] = \sum_i '[phi, 'chi_i] × '[psi, 'chi_i].
+ +
+Lemma Cint_cfdot_vchar : {in 'Z[irr G] &, ∀ phi psi, '[phi, psi] \in Cint}.
+ +
+Lemma Cnat_cfnorm_vchar : {in 'Z[irr G], ∀ phi, '[phi] \in Cnat}.
+ +
+Fact vchar_mulr_closed : mulr_closed 'Z[irr G].
+Canonical vchar_mulrPred := MulrPred vchar_mulr_closed.
+Canonical vchar_smulrPred := SmulrPred vchar_mulr_closed.
+Canonical vchar_semiringPred := SemiringPred vchar_mulr_closed.
+Canonical vchar_subringPred := SubringPred vchar_mulr_closed.
+ +
+Lemma mul_vchar A :
+ {in 'Z[irr G, A] &, ∀ phi psi, phi × psi \in 'Z[irr G, A]}.
+ +
+Section CfdotPairwiseOrthogonal.
+ +
+Variables (M : {group gT}) (S : seq 'CF(G)) (nu : 'CF(G) → 'CF(M)).
+Hypotheses (Inu : {in 'Z[S] &, isometry nu}) (oSS : pairwise_orthogonal S).
+ +
+Let freeS := orthogonal_free oSS.
+Let uniqS : uniq S := free_uniq freeS.
+Let Z_S : {subset S ≤ 'Z[S]}.
+Let notS0 : 0 \notin S.
+Let dotSS := proj2 (pairwise_orthogonalP oSS).
+ +
+Lemma map_pairwise_orthogonal : pairwise_orthogonal (map nu S).
+ +
+Lemma cfproj_sum_orthogonal P z phi :
+ phi \in S →
+ '[\sum_(xi <- S | P xi) z xi *: nu xi, nu phi]
+ = if P phi then z phi × '[phi] else 0.
+ +
+Lemma cfdot_sum_orthogonal z1 z2 :
+ '[\sum_(xi <- S) z1 xi *: nu xi, \sum_(xi <- S) z2 xi *: nu xi]
+ = \sum_(xi <- S) z1 xi × (z2 xi)^* × '[xi].
+ +
+Lemma cfnorm_sum_orthogonal z :
+ '[\sum_(xi <- S) z xi *: nu xi] = \sum_(xi <- S) `|z xi| ^+ 2 × '[xi].
+ +
+Lemma cfnorm_orthogonal : '[\sum_(xi <- S) nu xi] = \sum_(xi <- S) '[xi].
+ +
+End CfdotPairwiseOrthogonal.
+ +
+Lemma orthogonal_span S phi :
+ pairwise_orthogonal S → phi \in <<S>>%VS →
+ {z | z = fun xi ⇒ '[phi, xi] / '[xi] & phi = \sum_(xi <- S) z xi *: xi}.
+ +
+Section CfDotOrthonormal.
+ +
+Variables (M : {group gT}) (S : seq 'CF(G)) (nu : 'CF(G) → 'CF(M)).
+Hypotheses (Inu : {in 'Z[S] &, isometry nu}) (onS : orthonormal S).
+Let oSS := orthonormal_orthogonal onS.
+Let freeS := orthogonal_free oSS.
+Let nS1 : {in S, ∀ phi, '[phi] = 1}.
+ +
+Lemma map_orthonormal : orthonormal (map nu S).
+ +
+Lemma cfproj_sum_orthonormal z phi :
+ phi \in S → '[\sum_(xi <- S) z xi *: nu xi, nu phi] = z phi.
+ +
+Lemma cfdot_sum_orthonormal z1 z2 :
+ '[\sum_(xi <- S) z1 xi *: xi, \sum_(xi <- S) z2 xi *: xi]
+ = \sum_(xi <- S) z1 xi × (z2 xi)^*.
+ +
+Lemma cfnorm_sum_orthonormal z :
+ '[\sum_(xi <- S) z xi *: nu xi] = \sum_(xi <- S) `|z xi| ^+ 2.
+ +
+Lemma cfnorm_map_orthonormal : '[\sum_(xi <- S) nu xi] = (size S)%:R.
+ +
+Lemma orthonormal_span phi :
+ phi \in <<S>>%VS →
+ {z | z = fun xi ⇒ '[phi, xi] & phi = \sum_(xi <- S) z xi *: xi}.
+ +
+End CfDotOrthonormal.
+ +
+Lemma cfnorm_orthonormal S :
+ orthonormal S → '[\sum_(xi <- S) xi] = (size S)%:R.
+ +
+Lemma vchar_orthonormalP S :
+ {subset S ≤ 'Z[irr G]} →
+ reflect (∃ I : {set Iirr G}, ∃ b : Iirr G → bool,
+ perm_eq S [seq (-1) ^+ b i *: 'chi_i | i in I])
+ (orthonormal S).
+ +
+Lemma vchar_norm1P phi :
+ phi \in 'Z[irr G] → '[phi] = 1 →
+ ∃ b : bool, ∃ i : Iirr G, phi = (-1) ^+ b *: 'chi_i.
+ +
+Lemma zchar_small_norm phi n :
+ phi \in 'Z[irr G] → '[phi] = n%:R → (n < 4)%N →
+ {S : n.-tuple 'CF(G) |
+ [/\ orthonormal S, {subset S ≤ 'Z[irr G]} & phi = \sum_(xi <- S) xi]}.
+ +
+Lemma vchar_norm2 phi :
+ phi \in 'Z[irr G, G^#] → '[phi] = 2%:R →
+ ∃ i, exists2 j, j != i & phi = 'chi_i - 'chi_j.
+ +
+End VChar.
+ +
+Section Isometries.
+ +
+Variables (gT : finGroupType) (L G : {group gT}) (S : seq 'CF(L)).
+Implicit Type nu : {additive 'CF(L) → 'CF(G)}.
+ +
+Lemma Zisometry_of_cfnorm (tauS : seq 'CF(G)) :
+ pairwise_orthogonal S → pairwise_orthogonal tauS →
+ map cfnorm tauS = map cfnorm S → {subset tauS ≤ 'Z[irr G]} →
+ {tau : {linear 'CF(L) → 'CF(G)} | map tau S = tauS
+ & {in 'Z[S], isometry tau, to 'Z[irr G]}}.
+ +
+Lemma Zisometry_of_iso f :
+ free S → {in S, isometry f, to 'Z[irr G]} →
+ {tau : {linear 'CF(L) → 'CF(G)} | {in S, tau =1 f}
+ & {in 'Z[S], isometry tau, to 'Z[irr G]}}.
+ +
+Lemma Zisometry_inj A nu :
+ {in 'Z[S, A] &, isometry nu} → {in 'Z[S, A] &, injective nu}.
+ +
+Lemma isometry_in_zchar nu : {in S &, isometry nu} → {in 'Z[S] &, isometry nu}.
+ +
+End Isometries.
+ +
+Section AutVchar.
+ +
+Variables (u : {rmorphism algC → algC}) (gT : finGroupType) (G : {group gT}).
+Implicit Type (S : seq 'CF(G)) (phi chi : 'CF(G)).
+ +
+Lemma cfAut_zchar S A psi :
+ cfAut_closed u S → psi \in 'Z[S, A] → psi^u \in 'Z[S, A].
+ +
+Lemma cfAut_vchar A psi : psi \in 'Z[irr G, A] → psi^u \in 'Z[irr G, A].
+ +
+Lemma sub_aut_zchar S A psi :
+ {subset S ≤ 'Z[irr G]} → psi \in 'Z[S, A] → psi^u \in 'Z[S, A] →
+ psi - psi^u \in 'Z[S, A^#].
+ +
+Lemma conjC_vcharAut chi x : chi \in 'Z[irr G] → (u (chi x))^* = u (chi x)^*.
+ +
+Lemma cfdot_aut_vchar phi chi :
+ chi \in 'Z[irr G] → '[phi^u , chi^u] = u '[phi, chi].
+ +
+Lemma vchar_aut A chi : (chi^u \in 'Z[irr G, A]) = (chi \in 'Z[irr G, A]).
+ +
+End AutVchar.
+ +
+Definition cfConjC_vchar := cfAut_vchar conjC.
+ +
+Section MoreVchar.
+ +
+Variables (gT : finGroupType) (G H : {group gT}).
+ +
+Lemma cfRes_vchar phi : phi \in 'Z[irr G] → 'Res[H] phi \in 'Z[irr H].
+ +
+Lemma cfRes_vchar_on A phi :
+ H \subset G → phi \in 'Z[irr G, A] → 'Res[H] phi \in 'Z[irr H, A].
+ +
+Lemma cfInd_vchar phi : phi \in 'Z[irr H] → 'Ind[G] phi \in 'Z[irr G].
+ +
+Lemma sub_conjC_vchar A phi :
+ phi \in 'Z[irr G, A] → phi - (phi^*)%CF \in 'Z[irr G, A^#].
+ +
+Lemma Frobenius_kernel_exists :
+ [Frobenius G with complement H] → {K : {group gT} | [Frobenius G = K ><| H]}.
+ +
+End MoreVchar.
+ +
+Definition dirr (gT : finGroupType) (B : {set gT}) : pred_class :=
+ [pred f : 'CF(B) | (f \in irr B) || (- f \in irr B)].
+ +
+Section Norm1vchar.
+ +
+Variables (gT : finGroupType) (G : {group gT}).
+ +
+Fact dirr_key : pred_key (dirr G).
+Canonical dirr_keyed := KeyedPred dirr_key.
+ +
+Fact dirr_oppr_closed : oppr_closed (dirr G).
+ Canonical dirr_opprPred := OpprPred dirr_oppr_closed.
+ +
+Lemma dirr_opp v : (- v \in dirr G) = (v \in dirr G).
+Lemma dirr_sign n v : ((-1)^+ n *: v \in dirr G) = (v \in dirr G).
+ +
+Lemma irr_dirr i : 'chi_i \in dirr G.
+ +
+Lemma dirrP f :
+ reflect (∃ b : bool, ∃ i, f = (-1) ^+ b *: 'chi_i) (f \in dirr G).
+ +
+
+ This should perhaps be the definition of dirr.
+
+
+Lemma dirrE phi : phi \in dirr G = (phi \in 'Z[irr G]) && ('[phi] == 1).
+ +
+Lemma cfdot_dirr f g : f \in dirr G → g \in dirr G →
+ '[f, g] = (if f == - g then -1 else (f == g)%:R).
+ +
+Lemma dirr_norm1 phi : phi \in 'Z[irr G] → '[phi] = 1 → phi \in dirr G.
+ +
+Lemma dirr_aut u phi : (cfAut u phi \in dirr G) = (phi \in dirr G).
+ +
+Definition dIirr (B : {set gT}) := (bool × (Iirr B))%type.
+ +
+Definition dirr1 (B : {set gT}) : dIirr B := (false, 0).
+ +
+Definition ndirr (B : {set gT}) (i : dIirr B) : dIirr B :=
+ (~~ i.1, i.2).
+ +
+Lemma ndirr_diff (i : dIirr G) : ndirr i != i.
+ +
+Lemma ndirrK : involutive (@ndirr G).
+ +
+Lemma ndirr_inj : injective (@ndirr G).
+ +
+Definition dchi (B : {set gT}) (i : dIirr B) : 'CF(B) :=
+ (-1)^+ i.1 *: 'chi_i.2.
+ +
+Lemma dchi1 : dchi (dirr1 G) = 1.
+ +
+Lemma dirr_dchi i : dchi i \in dirr G.
+ +
+Lemma dIrrP phi : reflect (∃ i, phi = dchi i) (phi \in dirr G).
+ +
+Lemma dchi_ndirrE (i : dIirr G) : dchi (ndirr i) = - dchi i.
+ +
+Lemma cfdot_dchi (i j : dIirr G) :
+ '[dchi i, dchi j] = (i == j)%:R - (i == ndirr j)%:R.
+ +
+Lemma dchi_vchar i : dchi i \in 'Z[irr G].
+ +
+Lemma cfnorm_dchi (i : dIirr G) : '[dchi i] = 1.
+ +
+Lemma dirr_inj : injective (@dchi G).
+ +
+Definition dirr_dIirr (B : {set gT}) J (f : J → 'CF(B)) j : dIirr B :=
+ odflt (dirr1 B) [pick i | dchi i == f j].
+ +
+Lemma dirr_dIirrPE J (f : J → 'CF(G)) (P : pred J) :
+ (∀ j, P j → f j \in dirr G) →
+ ∀ j, P j → dchi (dirr_dIirr f j) = f j.
+ +
+Lemma dirr_dIirrE J (f : J → 'CF(G)) :
+ (∀ j, f j \in dirr G) → ∀ j, dchi (dirr_dIirr f j) = f j.
+ +
+Definition dirr_constt (B : {set gT}) (phi: 'CF(B)) : {set (dIirr B)} :=
+ [set i | 0 < '[phi, dchi i]].
+ +
+Lemma dirr_consttE (phi : 'CF(G)) (i : dIirr G) :
+ (i \in dirr_constt phi) = (0 < '[phi, dchi i]).
+ +
+Lemma Cnat_dirr (phi : 'CF(G)) i :
+ phi \in 'Z[irr G] → i \in dirr_constt phi → '[phi, dchi i] \in Cnat.
+ +
+Lemma dirr_constt_oppr (i : dIirr G) (phi : 'CF(G)) :
+ (i \in dirr_constt (-phi)) = (ndirr i \in dirr_constt phi).
+ +
+Lemma dirr_constt_oppI (phi: 'CF(G)) :
+ dirr_constt phi :&: dirr_constt (-phi) = set0.
+ +
+Lemma dirr_constt_oppl (phi: 'CF(G)) i :
+ i \in dirr_constt phi → (ndirr i) \notin dirr_constt phi.
+ +
+Definition to_dirr (B : {set gT}) (phi : 'CF(B)) (i : Iirr B) : dIirr B :=
+ ('[phi, 'chi_i] < 0, i).
+ +
+Definition of_irr (B : {set gT}) (i : dIirr B) : Iirr B := i.2.
+ +
+Lemma irr_constt_to_dirr (phi: 'CF(G)) i : phi \in 'Z[irr G] →
+ (i \in irr_constt phi) = (to_dirr phi i \in dirr_constt phi).
+ +
+Lemma to_dirrK (phi: 'CF(G)) : cancel (to_dirr phi) (@of_irr G).
+ +
+Lemma of_irrK (phi: 'CF(G)) :
+ {in dirr_constt phi, cancel (@of_irr G) (to_dirr phi)}.
+ +
+Lemma cfdot_todirrE (phi: 'CF(G)) i (phi_i := dchi (to_dirr phi i)) :
+ '[phi, phi_i] *: phi_i = '[phi, 'chi_i] *: 'chi_i.
+ +
+Lemma cfun_sum_dconstt (phi : 'CF(G)) :
+ phi \in 'Z[irr G] →
+ phi = \sum_(i in dirr_constt phi) '[phi, dchi i] *: dchi i.
+
+
++ +
+Lemma cfdot_dirr f g : f \in dirr G → g \in dirr G →
+ '[f, g] = (if f == - g then -1 else (f == g)%:R).
+ +
+Lemma dirr_norm1 phi : phi \in 'Z[irr G] → '[phi] = 1 → phi \in dirr G.
+ +
+Lemma dirr_aut u phi : (cfAut u phi \in dirr G) = (phi \in dirr G).
+ +
+Definition dIirr (B : {set gT}) := (bool × (Iirr B))%type.
+ +
+Definition dirr1 (B : {set gT}) : dIirr B := (false, 0).
+ +
+Definition ndirr (B : {set gT}) (i : dIirr B) : dIirr B :=
+ (~~ i.1, i.2).
+ +
+Lemma ndirr_diff (i : dIirr G) : ndirr i != i.
+ +
+Lemma ndirrK : involutive (@ndirr G).
+ +
+Lemma ndirr_inj : injective (@ndirr G).
+ +
+Definition dchi (B : {set gT}) (i : dIirr B) : 'CF(B) :=
+ (-1)^+ i.1 *: 'chi_i.2.
+ +
+Lemma dchi1 : dchi (dirr1 G) = 1.
+ +
+Lemma dirr_dchi i : dchi i \in dirr G.
+ +
+Lemma dIrrP phi : reflect (∃ i, phi = dchi i) (phi \in dirr G).
+ +
+Lemma dchi_ndirrE (i : dIirr G) : dchi (ndirr i) = - dchi i.
+ +
+Lemma cfdot_dchi (i j : dIirr G) :
+ '[dchi i, dchi j] = (i == j)%:R - (i == ndirr j)%:R.
+ +
+Lemma dchi_vchar i : dchi i \in 'Z[irr G].
+ +
+Lemma cfnorm_dchi (i : dIirr G) : '[dchi i] = 1.
+ +
+Lemma dirr_inj : injective (@dchi G).
+ +
+Definition dirr_dIirr (B : {set gT}) J (f : J → 'CF(B)) j : dIirr B :=
+ odflt (dirr1 B) [pick i | dchi i == f j].
+ +
+Lemma dirr_dIirrPE J (f : J → 'CF(G)) (P : pred J) :
+ (∀ j, P j → f j \in dirr G) →
+ ∀ j, P j → dchi (dirr_dIirr f j) = f j.
+ +
+Lemma dirr_dIirrE J (f : J → 'CF(G)) :
+ (∀ j, f j \in dirr G) → ∀ j, dchi (dirr_dIirr f j) = f j.
+ +
+Definition dirr_constt (B : {set gT}) (phi: 'CF(B)) : {set (dIirr B)} :=
+ [set i | 0 < '[phi, dchi i]].
+ +
+Lemma dirr_consttE (phi : 'CF(G)) (i : dIirr G) :
+ (i \in dirr_constt phi) = (0 < '[phi, dchi i]).
+ +
+Lemma Cnat_dirr (phi : 'CF(G)) i :
+ phi \in 'Z[irr G] → i \in dirr_constt phi → '[phi, dchi i] \in Cnat.
+ +
+Lemma dirr_constt_oppr (i : dIirr G) (phi : 'CF(G)) :
+ (i \in dirr_constt (-phi)) = (ndirr i \in dirr_constt phi).
+ +
+Lemma dirr_constt_oppI (phi: 'CF(G)) :
+ dirr_constt phi :&: dirr_constt (-phi) = set0.
+ +
+Lemma dirr_constt_oppl (phi: 'CF(G)) i :
+ i \in dirr_constt phi → (ndirr i) \notin dirr_constt phi.
+ +
+Definition to_dirr (B : {set gT}) (phi : 'CF(B)) (i : Iirr B) : dIirr B :=
+ ('[phi, 'chi_i] < 0, i).
+ +
+Definition of_irr (B : {set gT}) (i : dIirr B) : Iirr B := i.2.
+ +
+Lemma irr_constt_to_dirr (phi: 'CF(G)) i : phi \in 'Z[irr G] →
+ (i \in irr_constt phi) = (to_dirr phi i \in dirr_constt phi).
+ +
+Lemma to_dirrK (phi: 'CF(G)) : cancel (to_dirr phi) (@of_irr G).
+ +
+Lemma of_irrK (phi: 'CF(G)) :
+ {in dirr_constt phi, cancel (@of_irr G) (to_dirr phi)}.
+ +
+Lemma cfdot_todirrE (phi: 'CF(G)) i (phi_i := dchi (to_dirr phi i)) :
+ '[phi, phi_i] *: phi_i = '[phi, 'chi_i] *: 'chi_i.
+ +
+Lemma cfun_sum_dconstt (phi : 'CF(G)) :
+ phi \in 'Z[irr G] →
+ phi = \sum_(i in dirr_constt phi) '[phi, dchi i] *: dchi i.
+
+ GG -- rewrite pattern fails in trunk
+ move=> PiZ; rewrite [X in X = _ ]cfun_sum_constt.
+
+
+
+
+Lemma cnorm_dconstt (phi : 'CF(G)) :
+ phi \in 'Z[irr G] →
+ '[phi] = \sum_(i in dirr_constt phi) '[phi, dchi i] ^+ 2.
+ +
+Lemma dirr_small_norm (phi : 'CF(G)) n :
+ phi \in 'Z[irr G] → '[phi] = n%:R → (n < 4)%N →
+ [/\ #|dirr_constt phi| = n, dirr_constt phi :&: dirr_constt (- phi) = set0 &
+ phi = \sum_(i in dirr_constt phi) dchi i].
+ +
+Lemma cfdot_sum_dchi (phi1 phi2 : 'CF(G)) :
+ '[\sum_(i in dirr_constt phi1) dchi i,
+ \sum_(i in dirr_constt phi2) dchi i] =
+ #|dirr_constt phi1 :&: dirr_constt phi2|%:R -
+ #|dirr_constt phi1 :&: dirr_constt (- phi2)|%:R.
+ +
+Lemma cfdot_dirr_eq1 :
+ {in dirr G &, ∀ phi psi, ('[phi, psi] == 1) = (phi == psi)}.
+ +
+Lemma cfdot_add_dirr_eq1 :
+ {in dirr G & &, ∀ phi1 phi2 psi,
+ '[phi1 + phi2, psi] = 1 → psi = phi1 ∨ psi = phi2}.
+ +
+End Norm1vchar.
+
++Lemma cnorm_dconstt (phi : 'CF(G)) :
+ phi \in 'Z[irr G] →
+ '[phi] = \sum_(i in dirr_constt phi) '[phi, dchi i] ^+ 2.
+ +
+Lemma dirr_small_norm (phi : 'CF(G)) n :
+ phi \in 'Z[irr G] → '[phi] = n%:R → (n < 4)%N →
+ [/\ #|dirr_constt phi| = n, dirr_constt phi :&: dirr_constt (- phi) = set0 &
+ phi = \sum_(i in dirr_constt phi) dchi i].
+ +
+Lemma cfdot_sum_dchi (phi1 phi2 : 'CF(G)) :
+ '[\sum_(i in dirr_constt phi1) dchi i,
+ \sum_(i in dirr_constt phi2) dchi i] =
+ #|dirr_constt phi1 :&: dirr_constt phi2|%:R -
+ #|dirr_constt phi1 :&: dirr_constt (- phi2)|%:R.
+ +
+Lemma cfdot_dirr_eq1 :
+ {in dirr G &, ∀ phi psi, ('[phi, psi] == 1) = (phi == psi)}.
+ +
+Lemma cfdot_add_dirr_eq1 :
+ {in dirr G & &, ∀ phi1 phi2 psi,
+ '[phi1 + phi2, psi] = 1 → psi = phi1 ∨ psi = phi2}.
+ +
+End Norm1vchar.
+