Library mathcomp.character.vcharacter
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- 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 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].
- -
-
-
--Set Implicit Arguments.
- -
-Import 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%: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 'CF(B)} :=
- [pred f | (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 'CF(B)} :=
- [pred f | (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 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 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.
- -
-