Library mathcomp.character.vcharacter
(* (c) Copyright 2006-2015 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].
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)].
Implicit Arguments dirr [[gT]].
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)].
Implicit Arguments dirr [[gT]].
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.