From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.character.vcharacter.html | 412 ++++++++++++------------
1 file changed, 203 insertions(+), 209 deletions(-)
(limited to 'docs/htmldoc/mathcomp.character.vcharacter.html')
diff --git a/docs/htmldoc/mathcomp.character.vcharacter.html b/docs/htmldoc/mathcomp.character.vcharacter.html
index 4b01b7a..d4710a2 100644
--- a/docs/htmldoc/mathcomp.character.vcharacter.html
+++ b/docs/htmldoc/mathcomp.character.vcharacter.html
@@ -21,14 +21,6 @@
-
Require Import mathcomp.ssreflect.ssreflect.
-
-
-
Set Implicit Arguments.
-
-
-
Import GroupScope GRing.Theory Num.Theory.
-
Local Open Scope ring_scope.
@@ -62,20 +54,27 @@
+
+
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}).
+
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.
+
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.
+
Lemma cfun0_zchar : 0
\in Zchar.
Fact Zchar_zmod :
zmod_closed Zchar.
@@ -84,56 +83,56 @@
Canonical Zchar_zmodPred :=
ZmodPred Zchar_zmod.
-
Lemma scale_zchar a phi :
a \in Cint → phi \in Zchar → a *: phi \in Zchar.
+
Lemma scale_zchar a phi :
a \in Cint → phi \in Zchar → a *: phi \in Zchar.
End Basics.
-
Notation "''Z[' S , A ]" := (
Zchar S A)
+
Notation "''Z[' S , A ]" := (
Zchar S A)
(
at level 8,
format "''Z[' S , A ]") :
group_scope.
-
Notation "''Z[' S ]" :=
'Z[S, setT]
+
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)).
+
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)).
+
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 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
).
+
(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 zcharW S A :
{subset 'Z[S, A] ≤ 'Z[S]}.
-
Lemma zchar_on S A :
{subset 'Z[S, A] ≤ 'CF(G, A)}.
+
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_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 zchar_onG S :
'Z[S, G] =i 'Z[S].
-
Lemma irr_vchar_on A :
{subset 'Z[irr G, A] ≤ 'CF(G, A)}.
+
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 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].
+
phi \in 'CF(G, A) → phi \in S → phi \in 'Z[S, A].
-
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_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_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]}.
+
{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]}.
+
{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]}.
+
{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]}.
+
{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]}.
+
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]}.
+
Lemma zchar_filter S A (
p :
pred 'CF(G)) :
+
{subset 'Z[filter p S, A] ≤ 'Z[S, A]}.
End Zchar.
@@ -199,45 +198,45 @@
Section VChar.
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
-
Implicit Types (
A B :
{set gT}) (
phi chi :
'CF(G)) (
S :
seq 'CF(G)).
+
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 char_vchar chi :
chi \is a character → chi \in 'Z[irr G].
-
Lemma irr_vchar i :
'chi[G]_i \in 'Z[irr G].
+
Lemma irr_vchar i :
'chi[G]_i \in 'Z[irr G].
-
Lemma cfun1_vchar : 1
\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]).
+
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 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_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 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].
+
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 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}.
+
Lemma Cnat_cfnorm_vchar :
{in 'Z[irr G], ∀ phi,
'[phi] \in Cnat}.
-
Fact vchar_mulr_closed :
mulr_closed 'Z[irr G].
+
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.
@@ -245,114 +244,114 @@
Lemma mul_vchar A :
-
{in 'Z[irr G, A] &, ∀ phi psi,
phi × psi \in 'Z[irr G, 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).
+
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).
+
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.
+
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].
+
'[\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].
+
'[\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].
+
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}.
+
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).
+
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
}.
+
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.
+
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)^*.
+
'[\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.
+
'[\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 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}.
+
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.
+
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])
+
{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.
+
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]}.
+
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.
+
phi \in 'Z[irr G, G^#] → '[phi] = 2
%:R →
+
∃ i, exists2 j, j != i & phi = 'chi_i - 'chi_j.
End VChar.
@@ -361,28 +360,28 @@
Section Isometries.
-
Variables (
gT :
finGroupType) (
L G :
{group gT}) (
S :
seq 'CF(L)).
-
Implicit Type nu :
{additive 'CF(L) → 'CF(G)}.
+
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_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]}}.
+
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}.
+
{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}.
+
Lemma isometry_in_zchar nu :
{in S &, isometry nu} → {in 'Z[S] &, isometry nu}.
End Isometries.
@@ -391,30 +390,30 @@
Section AutVchar.
-
Variables (
u :
{rmorphism algC → algC}) (
gT :
finGroupType) (
G :
{group gT}).
-
Implicit Type (
S :
seq 'CF(G)) (
phi chi :
'CF(G)).
+
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].
+
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 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^#].
+
{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 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].
+
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]).
+
Lemma vchar_aut A chi :
(chi^u \in 'Z[irr G, A]) = (chi \in 'Z[irr G, A]).
End AutVchar.
@@ -426,57 +425,57 @@
Section MoreVchar.
-
Variables (
gT :
finGroupType) (
G H :
{group gT}).
+
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 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].
+
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 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^#].
+
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]}.
+
[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)].
+
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}).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
-
Fact dirr_key :
pred_key (
dirr G).
-
Canonical dirr_keyed :=
KeyedPred dirr_key.
+
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 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 irr_dirr i :
'chi_i \in dirr G.
Lemma dirrP f :
-
reflect (
∃ b :
bool, ∃ i, f = (-1
) ^+ b *: 'chi_i) (
f \in dirr G).
+
reflect (
∃ b :
bool, ∃ i, f = (-1
) ^+ b *: 'chi_i) (
f \in dirr G).
-
Lemma dirrE phi :
phi \in dirr G = (phi \in 'Z[irr G]) && ('[phi] == 1
).
+
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 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_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).
+
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 dIirr (
B :
{set gT}) := (
bool × (Iirr B))%
type.
-
Definition dirr1 (
B :
{set gT}) :
dIirr B :=
(false, 0
).
+
Definition dirr1 (
B :
{set gT}) :
dIirr B :=
(false, 0
).
-
Definition ndirr (
B :
{set gT}) (
i :
dIirr B) :
dIirr B :=
-
(~~ i.1, i.2).
+
Definition ndirr (
B :
{set gT}) (
i :
dIirr B) :
dIirr B :=
+
(~~ i.1, i.2).
-
Lemma ndirr_diff (
i :
dIirr G) :
ndirr i != i.
+
Lemma ndirr_diff (
i :
dIirr G) :
ndirr i != i.
-
Lemma ndirrK :
involutive (@
ndirr G).
+
Lemma ndirrK :
involutive (@
ndirr G).
-
Lemma ndirr_inj :
injective (@
ndirr G).
+
Lemma ndirr_inj :
injective (@
ndirr G).
-
Definition dchi (
B :
{set gT}) (
i :
dIirr B) :
'CF(B) :=
-
(-1
)^+ i.1 *: 'chi_i.2.
+
Definition dchi (
B :
{set gT}) (
i :
dIirr B) :
'CF(B) :=
+
(-1
)^+ i.1 *: 'chi_i.2.
-
Lemma dchi1 :
dchi (
dirr1 G)
= 1.
+
Lemma dchi1 :
dchi (
dirr1 G)
= 1.
-
Lemma dirr_dchi i :
dchi i \in dirr G.
+
Lemma dirr_dchi i :
dchi i \in dirr G.
-
Lemma dIrrP phi :
reflect (
∃ i, phi = dchi i) (
phi \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 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.
+
'[dchi i, dchi j] = (i == j)%:R - (i == ndirr j)%:R.
-
Lemma dchi_vchar i :
dchi i \in 'Z[irr G].
+
Lemma dchi_vchar i :
dchi i \in 'Z[irr G].
-
Lemma cfnorm_dchi (
i :
dIirr G) :
'[dchi i] = 1.
+
Lemma cfnorm_dchi (
i :
dIirr G) :
'[dchi i] = 1.
-
Lemma dirr_inj :
injective (@
dchi G).
+
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].
+
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_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.
+
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]].
+
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 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 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_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_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.
+
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 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.
+
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 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 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 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 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 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 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 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_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)}.
+
{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}.
+
{in dirr G & &, ∀ phi1 phi2 psi,
+
'[phi1 + phi2, psi] = 1
→ psi = phi1 ∨ psi = phi2}.
End Norm1vchar.
+
+