Library mathcomp.character.vcharacter
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime order.
From mathcomp Require Import ssralg poly finset fingroup morphism perm.
From mathcomp Require Import automorphism quotient finalg action gproduct.
From mathcomp Require Import zmodp commutator cyclic center pgroup sylow.
From mathcomp Require Import frobenius vector ssrnum ssrint intdiv algC.
From mathcomp Require Import algnum classfun character integral_char.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime order.
From mathcomp Require Import ssralg poly finset fingroup morphism perm.
From mathcomp Require Import automorphism quotient finalg action gproduct.
From mathcomp Require Import zmodp commutator cyclic center pgroup sylow.
From mathcomp Require Import frobenius vector ssrnum ssrint intdiv algC.
From mathcomp Require Import algnum classfun character integral_char.
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.
Set Implicit Arguments.
Import Order.TTheory GroupScope GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Section Basics.
Variables (gT : finGroupType) (B : {set gT}) (S : seq 'CF(B)) (A : {set gT}).
Definition Zchar : {pred 'CF(B)} :=
[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 →
∃ 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 'CF(B)} :=
[pred f | (f \in irr B) || (- f \in irr B)].
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 →
∃ 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 'CF(B)} :=
[pred f | (f \in irr B) || (- f \in irr B)].
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 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.
Arguments of_irrK {gT G phi} [i] phi_i : rename.
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 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.
Arguments of_irrK {gT G phi} [i] phi_i : rename.