From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
.../mathcomp.character.mxrepresentation.html | 1850 ++++++++++----------
1 file changed, 941 insertions(+), 909 deletions(-)
(limited to 'docs/htmldoc/mathcomp.character.mxrepresentation.html')
diff --git a/docs/htmldoc/mathcomp.character.mxrepresentation.html b/docs/htmldoc/mathcomp.character.mxrepresentation.html
index 3105471..e0acbeb 100644
--- a/docs/htmldoc/mathcomp.character.mxrepresentation.html
+++ b/docs/htmldoc/mathcomp.character.mxrepresentation.html
@@ -21,7 +21,6 @@
@@ -129,7 +128,7 @@
classically; the socleType structure encapsulates this
use of classical logic.
DecSocleType rG == a socleType rG structure, for a representation over a
- decidable field type.
+ decidable field type. DecSocleType rG is opaque.
socle_base W == for W : (sG : socleType), a simple module whose
component is W; socle_simple W and socle_module W are
proofs that socle_base W is a simple module.
@@ -235,48 +234,66 @@
H, with nsGH : H <| G, given by Clifford's theorem. More
precisely this is a total action of G on socle_sort sH,
where sH : socleType (subg_repr rG (normal_sub sGH)).
+ We build on the MatrixFormula toolkit to define decision procedures for
+ the reducibility property:
+ mxmodule_form rG U == a formula asserting that the interpretation of U is
+ a module of the representation rG.
+ mxnonsimple_form rG U == a formula asserting that the interpretation of U
+ contains a proper nontrivial rG-module.
+ mxnonsimple_sat rG U <=> mxnonsimple_form rG U is satisfied.
More involved constructions are encapsulated in two Coq submodules:
MatrixGenField == a module that encapsulates the lengthy details of the
construction of appropriate extension fields. We assume we
- have an irreducible representation r of a group G, and a
- non-scalar matrix A that centralises an r(G), as this data
+ have an irreducible representation rG of a group G, and a
+ non-scalar matrix A that centralises rG(G), as this data
is readily extracted from the Jacobson density theorem. It
then follows from Schur's lemma that the ring generated by
A is a field on which the extension of the representation
- r of G is reducible. Note that this is equivalent to the
+ rG of G is reducible. Note that this is equivalent to the
more traditional quotient of the polynomial ring by an
irreducible polynomial (the minimal polynomial of A), but
much better suited to our needs.
Here are the main definitions of MatrixGenField; they all have three
- proofs as arguments: rG : mx_repr r G, irrG : mx_irreducible rG, and
- cGA : centgmx rG A, which ensure the validity of the construction and
- allow us to define Canonical instances (the ~~ is_scalar_mx A assumption
- is only needed to prove reducibility).
+ proofs as arguments: (implicit) rG : mx_repr n G, irrG : mx_irreducible rG
+ and cGA : centgmx rG A. These ensure the validity of the construction and
+ allow us to define Canonical instances; we assume degree_mxminpoly A > 1
+ (which is equivalent to ~~ is_scalar_mx A) only to prove reducibility.
+ gen_of irrG cGA == the carrier type of the field generated by A. It is
at least equipped with a fieldType structure; we also
propagate any decFieldType/finFieldType structures on the
original field.
- + gen irrG cGA == the morphism injecting into gen_of rG irrG cGA.
- + groot irrG cGA == the root of mxminpoly A in the gen_of field.
+ + gen irrG cGA == the morphism injecting into gen_of irrG cGA.
+ + groot irrG cGA == the root of mxminpoly A in the gen_of irrG cGA field.
+ + pval x, rVval x, mxval x == the interpretation of x : gen_of irrG cGA
+ as a polynomial, a row vector, and a matrix, respectively.
+ Both irrG and cGA are implicit arguments here.
+ gen_repr irrG cGA == an alternative to the field extension
representation, which consists in reconsidering the
original module as a module over the new gen_of field,
thereby DIVIDING the original dimension n by the degree of
the minimal polynomial of A. This can be simpler than the
- extension method, and is actually required by the proof
- that odd groups are p-stable (B & G 6.1-2, and Appendix A)
- but is only applicable if G is the LARGEST group
- represented by rG (e.g., NOT for B & G 2.6).
- + val_gen/in_gen rG irrG cGA : the bijections from/to the module
- corresponding to gen_repr.
- + rowval_gen rG irrG cGA : the projection of row spaces in the module
- corresponding to gen_repr to row spaces in 'rV_n.
- We build on the MatrixFormula toolkit to define decision procedures for
- the reducibility property:
- + mxmodule_form rG U == a formula asserting that the interpretation of U
- is a module of the representation rG of G via r.
- + mxnonsimple_form rG U == a formula asserting that the interpretation
- of U contains a proper nontrivial rG-module.
+ extension method, is actually required by the proof that
+ odd groups are p-stable (B & G 6.1-2, and Appendix A), but
+ is only applicable if G is the LARGEST group represented
+ by rG (e.g., NOT for B & G 2.6).
+ + gen_dim A == the dimension of gen_repr irrG cGA (only depends on A).
+ + in_gen irrG cGA W == the ROWWISE image of a matrix W : 'M[F](m, n),
+ i.e., interpreting W as a sequence of m tow vectors,
+ under the bijection from rG to gen_repr irrG cGA.
+ The sequence length m is a maximal implicit argument
+ passed between the explicit argument cGA and W.
+ + val_gen W == the ROWWISE image of an 'M[gen_of irrG cGA](m, gen_dim A)
+ matrix W under the bijection from gen_repr irrG cGA to rG.
+ + rowval_gen W == the ROWSPACE image of W under the bijection from
+ gen_repr irrG cGA to rG, i.e., a 'M[F]_n matrix whose row
+ space is the image of the row space of W.
+ This is the A-ideal generated by val_gen W.
+ + gen_sat e f <=> f : GRing.formula (gen_of irrG cGA) is satisfied in
+ environment e : seq (gen_of irrG cGA), provided F has a
+ decFieldType structure.
+ + gen_env e, gen_term t, gen_form f == interpretations of environments,
+ terms, and RING formulas over gen_of irrG cGA as row
+ vector formulae, used to construct gen_sat.
@@ -346,19 +363,19 @@
developped the theory of matrix subalgebras for F-algebras.
-
Definition enveloping_algebra_mx :=
\matrix_(i < #|G|) mxvec (
rG (
enum_val i)).
+
Definition enveloping_algebra_mx :=
\matrix_(i < #|G|) mxvec (
rG (
enum_val i)).
Section Stabiliser.
-
Variables (
m :
nat) (
U :
'M[R]_(m, n)).
+
Variables (
m :
nat) (
U :
'M[R]_(m, n)).
-
Definition rstab :=
[set x in G | U ×m rG x == U].
+
Definition rstab :=
[set x in G | U ×m rG x == U].
-
Lemma rstab_sub :
rstab \subset G.
+
Lemma rstab_sub :
rstab \subset G.
Lemma rstab_group_set :
group_set rstab.
@@ -377,23 +394,23 @@
Section CentHom.
-
Variable f :
'M[R]_n.
+
Variable f :
'M[R]_n.
-
Definition rcent :=
[set x in G | f ×m rG x == rG x ×m f].
+
Definition rcent :=
[set x in G | f ×m rG x == rG x ×m f].
-
Lemma rcent_sub :
rcent \subset G.
+
Lemma rcent_sub :
rcent \subset G.
Lemma rcent_group_set :
group_set rcent.
Canonical rcent_group :=
Group rcent_group_set.
-
Definition centgmx :=
G \subset rcent.
+
Definition centgmx :=
G \subset rcent.
-
Lemma centgmxP :
reflect (
∀ x,
x \in G → f ×m rG x = rG x ×m f)
centgmx.
+
Lemma centgmxP :
reflect (
∀ x,
x \in G → f ×m rG x = rG x ×m f)
centgmx.
End CentHom.
@@ -407,26 +424,26 @@
@@ -437,14 +454,14 @@
-
Definition rcenter :=
[set g in G | is_scalar_mx (
rG g)
].
+
Definition rcenter :=
[set g in G | is_scalar_mx (
rG g)
].
Fact rcenter_group_set :
group_set rcenter.
Canonical rcenter_group :=
Group rcenter_group_set.
-
Lemma rcenter_normal :
rcenter <| G.
+
Lemma rcenter_normal :
rcenter <| G.
End OneRepresentation.
@@ -455,20 +472,20 @@
Section Proper.
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n' :
nat).
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n' :
nat).
Variable rG :
mx_representation G n.
-
Lemma repr_mxMr :
{in G &, {morph rG : x y / (
x × y)%
g >-> x × y}}.
+
Lemma repr_mxMr :
{in G &, {morph rG : x y / (
x × y)%
g >-> x × y}}.
-
Lemma repr_mxVr :
{in G, {morph rG : x / (
x^-1)%
g >-> x^-1}}.
+
Lemma repr_mxVr :
{in G, {morph rG : x / (
x^-1)%
g >-> x^-1}}.
-
Lemma repr_mx_unitr x :
x \in G → rG x \is a GRing.unit.
+
Lemma repr_mx_unitr x :
x \in G → rG x \is a GRing.unit.
-
Lemma repr_mxX m :
{in G, {morph rG : x / (
x ^+ m)%
g >-> x ^+ m}}.
+
Lemma repr_mxX m :
{in G, {morph rG : x / (
x ^+ m)%
g >-> x ^+ m}}.
End Proper.
@@ -477,39 +494,39 @@
Section ChangeGroup.
-
Variables (
gT :
finGroupType) (
G H :
{group gT}) (
n :
nat).
+
Variables (
gT :
finGroupType) (
G H :
{group gT}) (
n :
nat).
Variables (
rG :
mx_representation G n).
Section SubGroup.
-
Hypothesis sHG :
H \subset G.
+
Hypothesis sHG :
H \subset G.
Lemma subg_mx_repr :
mx_repr H rG.
Definition subg_repr :=
MxRepresentation subg_mx_repr.
-
Lemma rcent_subg U :
rcent rH U = H :&: rcent rG U.
+
Lemma rcent_subg U :
rcent rH U = H :&: rcent rG U.
Section Stabiliser.
-
Variables (
m :
nat) (
U :
'M[R]_(m, n)).
+
Variables (
m :
nat) (
U :
'M[R]_(m, n)).
-
Lemma rstab_subg :
rstab rH U = H :&: rstab rG U.
+
Lemma rstab_subg :
rstab rH U = H :&: rstab rG U.
End Stabiliser.
-
Lemma rker_subg :
rker rH = H :&: rker rG.
+
Lemma rker_subg :
rker rH = H :&: rker rG.
-
Lemma subg_mx_faithful :
mx_faithful rG → mx_faithful rH.
+
Lemma subg_mx_faithful :
mx_faithful rG → mx_faithful rH.
End SubGroup.
@@ -518,34 +535,34 @@
Section SameGroup.
-
Hypothesis eqGH :
G :==: H.
+
Hypothesis eqGH :
G :==: H.
-
Lemma eqg_repr_proof :
H \subset G.
+
Lemma eqg_repr_proof :
H \subset G.
Definition eqg_repr :=
subg_repr eqg_repr_proof.
-
Lemma rcent_eqg U :
rcent rH U = rcent rG U.
+
Lemma rcent_eqg U :
rcent rH U = rcent rG U.
Section Stabiliser.
-
Variables (
m :
nat) (
U :
'M[R]_(m, n)).
+
Variables (
m :
nat) (
U :
'M[R]_(m, n)).
-
Lemma rstab_eqg :
rstab rH U = rstab rG U.
+
Lemma rstab_eqg :
rstab rH U = rstab rG U.
End Stabiliser.
-
Lemma rker_eqg :
rker rH = rker rG.
+
Lemma rker_eqg :
rker rH = rker rG.
-
Lemma eqg_mx_faithful :
mx_faithful rH = mx_faithful rG.
+
Lemma eqg_mx_faithful :
mx_faithful rH = mx_faithful rG.
End SameGroup.
@@ -557,27 +574,27 @@
Section Morphpre.
-
Variables (
aT rT :
finGroupType) (
D :
{group aT}) (
f :
{morphism D >-> rT}).
-
Variables (
G :
{group rT}) (
n :
nat) (
rG :
mx_representation G n).
+
Variables (
aT rT :
finGroupType) (
D :
{group aT}) (
f :
{morphism D >-> rT}).
+
Variables (
G :
{group rT}) (
n :
nat) (
rG :
mx_representation G n).
-
Lemma morphpre_mx_repr :
mx_repr (
f @*^-1 G) (
rG \o f).
+
Lemma morphpre_mx_repr :
mx_repr (
f @*^-1 G) (
rG \o f).
Canonical morphpre_repr :=
MxRepresentation morphpre_mx_repr.
Section Stabiliser.
-
Variables (
m :
nat) (
U :
'M[R]_(m, n)).
+
Variables (
m :
nat) (
U :
'M[R]_(m, n)).
-
Lemma rstab_morphpre :
rstab rGf U = f @*^-1 (rstab rG U).
+
Lemma rstab_morphpre :
rstab rGf U = f @*^-1 (rstab rG U).
End Stabiliser.
-
Lemma rker_morphpre :
rker rGf = f @*^-1 (rker rG).
+
Lemma rker_morphpre :
rker rGf = f @*^-1 (rker rG).
End Morphpre.
@@ -586,20 +603,20 @@
Section Morphim.
-
Variables (
aT rT :
finGroupType) (
G D :
{group aT}) (
f :
{morphism D >-> rT}).
-
Variables (
n :
nat) (
rGf :
mx_representation (
f @* G)
n).
+
Variables (
aT rT :
finGroupType) (
G D :
{group aT}) (
f :
{morphism D >-> rT}).
+
Variables (
n :
nat) (
rGf :
mx_representation (
f @* G)
n).
-
Definition morphim_mx of G \subset D :=
fun x ⇒
rGf (
f x).
+
Definition morphim_mx of G \subset D :=
fun x ⇒
rGf (
f x).
-
Hypothesis sGD :
G \subset D.
+
Hypothesis sGD :
G \subset D.
-
Lemma morphim_mxE x :
morphim_mx sGD x = rGf (
f x).
+
Lemma morphim_mxE x :
morphim_mx sGD x = rGf (
f x).
-
Let sG_f'fG :
G \subset f @*^-1 (f @* G).
+
Let sG_f'fG :
G \subset f @*^-1 (f @* G).
Lemma morphim_mx_repr :
mx_repr G (
morphim_mx sGD).
@@ -607,16 +624,16 @@
Section Stabiliser.
-
Variables (
m :
nat) (
U :
'M[R]_(m, n)).
+
Variables (
m :
nat) (
U :
'M[R]_(m, n)).
-
Lemma rstab_morphim :
rstab rG U = G :&: f @*^-1 rstab rGf U.
+
Lemma rstab_morphim :
rstab rG U = G :&: f @*^-1 rstab rGf U.
End Stabiliser.
-
Lemma rker_morphim :
rker rG = G :&: f @*^-1 (rker rGf).
+
Lemma rker_morphim :
rker rG = G :&: f @*^-1 (rker rGf).
End Morphim.
@@ -625,36 +642,36 @@
Section Conjugate.
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
-
Variables (
rG :
mx_representation G n) (
B :
'M[R]_n).
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
+
Variables (
rG :
mx_representation G n) (
B :
'M[R]_n).
-
Definition rconj_mx of B \in unitmx :=
fun x ⇒
B ×m rG x ×m invmx B.
+
Definition rconj_mx of B \in unitmx :=
fun x ⇒
B ×m rG x ×m invmx B.
-
Hypothesis uB :
B \in unitmx.
+
Hypothesis uB :
B \in unitmx.
Lemma rconj_mx_repr :
mx_repr G (
rconj_mx uB).
Canonical rconj_repr :=
MxRepresentation rconj_mx_repr.
-
Lemma rconj_mxE x :
rGB x = B ×m rG x ×m invmx B.
+
Lemma rconj_mxE x :
rGB x = B ×m rG x ×m invmx B.
-
Lemma rconj_mxJ m (
W :
'M_(m, n))
x :
W ×m rGB x ×m B = W ×m B ×m rG x.
+
Lemma rconj_mxJ m (
W :
'M_(m, n))
x :
W ×m rGB x ×m B = W ×m B ×m rG x.
-
Lemma rcent_conj A :
rcent rGB A = rcent rG (
invmx B ×m A ×m B).
+
Lemma rcent_conj A :
rcent rGB A = rcent rG (
invmx B ×m A ×m B).
-
Lemma rstab_conj m (
U :
'M_(m, n)) :
rstab rGB U = rstab rG (
U ×m B).
+
Lemma rstab_conj m (
U :
'M_(m, n)) :
rstab rGB U = rstab rG (
U ×m B).
-
Lemma rker_conj :
rker rGB = rker rG.
+
Lemma rker_conj :
rker rGB = rker rG.
-
Lemma conj_mx_faithful :
mx_faithful rGB = mx_faithful rG.
+
Lemma conj_mx_faithful :
mx_faithful rGB = mx_faithful rG.
End Conjugate.
@@ -663,53 +680,53 @@
Section Quotient.
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
Variable rG :
mx_representation G n.
-
Definition quo_mx (
H :
{set gT})
of H \subset rker rG &
G \subset 'N(H) :=
+
Definition quo_mx (
H :
{set gT})
of H \subset rker rG &
G \subset 'N(H) :=
fun Hx :
coset_of H ⇒
rG (
repr Hx).
Section SubQuotient.
-
Variable H :
{group gT}.
-
Hypotheses (
krH :
H \subset rker rG) (
nHG :
G \subset 'N(H)).
+
Variable H :
{group gT}.
+
Hypotheses (
krH :
H \subset rker rG) (
nHG :
G \subset 'N(H)).
Let nHGs :=
subsetP nHG.
-
Lemma quo_mx_coset x :
x \in G → quo_mx krH nHG (
coset H x)
= rG x.
+
Lemma quo_mx_coset x :
x \in G → quo_mx krH nHG (
coset H x)
= rG x.
-
Lemma quo_mx_repr :
mx_repr (
G / H)%
g (
quo_mx krH nHG).
+
Lemma quo_mx_repr :
mx_repr (
G / H)%
g (
quo_mx krH nHG).
Canonical quo_repr :=
MxRepresentation quo_mx_repr.
-
Lemma quo_repr_coset x :
x \in G → rGH (
coset H x)
= rG x.
+
Lemma quo_repr_coset x :
x \in G → rGH (
coset H x)
= rG x.
-
Lemma rcent_quo A :
rcent rGH A = (
rcent rG A / H)%
g.
+
Lemma rcent_quo A :
rcent rGH A = (
rcent rG A / H)%
g.
-
Lemma rstab_quo m (
U :
'M_(m, n)) :
rstab rGH U = (
rstab rG U / H)%
g.
+
Lemma rstab_quo m (
U :
'M_(m, n)) :
rstab rGH U = (
rstab rG U / H)%
g.
-
Lemma rker_quo :
rker rGH = (
rker rG / H)%
g.
+
Lemma rker_quo :
rker rGH = (
rker rG / H)%
g.
End SubQuotient.
Definition kquo_mx :=
quo_mx (
subxx (
rker rG)) (
rker_norm rG).
-
Lemma kquo_mxE :
kquo_mx = quo_mx (
subxx (
rker rG)) (
rker_norm rG).
+
Lemma kquo_mxE :
kquo_mx = quo_mx (
subxx (
rker rG)) (
rker_norm rG).
Canonical kquo_repr := @
MxRepresentation _ _ _ kquo_mx (
quo_mx_repr _ _).
Lemma kquo_repr_coset x :
-
x \in G → kquo_repr (
coset (
rker rG)
x)
= rG x.
+
x \in G → kquo_repr (
coset (
rker rG)
x)
= rG x.
Lemma kquo_mx_faithful :
mx_faithful kquo_repr.
@@ -721,20 +738,20 @@
Section Regular.
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
Definition gring_index (
x :
gT) :=
enum_rank_in (
group1 G)
x.
-
Lemma gring_valK :
cancel enum_val gring_index.
+
Lemma gring_valK :
cancel enum_val gring_index.
-
Lemma gring_indexK :
{in G, cancel gring_index enum_val}.
+
Lemma gring_indexK :
{in G, cancel gring_index enum_val}.
-
Definition regular_mx x :
'M[R]_nG :=
-
\matrix_i delta_mx 0 (
gring_index (
enum_val i × x)).
+
Definition regular_mx x :
'M[R]_nG :=
+
\matrix_i delta_mx 0 (
gring_index (
enum_val i × x)).
Lemma regular_mx_repr :
mx_repr G regular_mx.
@@ -744,18 +761,18 @@
Definition group_ring :=
enveloping_algebra_mx aG.
-
Definition gring_row :
'M[R]_nG → 'rV_nG :=
row (
gring_index 1).
-
Canonical gring_row_linear :=
[linear of gring_row].
+
Definition gring_row :
'M[R]_nG → 'rV_nG :=
row (
gring_index 1).
+
Canonical gring_row_linear :=
[linear of gring_row].
-
Lemma gring_row_mul A B :
gring_row (
A ×m B)
= gring_row A ×m B.
+
Lemma gring_row_mul A B :
gring_row (
A ×m B)
= gring_row A ×m B.
-
Definition gring_proj x :=
row (
gring_index x)
\o trmx \o gring_row.
-
Canonical gring_proj_linear x :=
[linear of gring_proj x].
+
Definition gring_proj x :=
row (
gring_index x)
\o trmx \o gring_row.
+
Canonical gring_proj_linear x :=
[linear of gring_proj x].
-
Lemma gring_projE :
{in G &, ∀ x y,
gring_proj x (
aG y)
= (x == y)%:R}.
+
Lemma gring_projE :
{in G &, ∀ x y,
gring_proj x (
aG y)
= (x == y)%:R}.
Lemma regular_mx_faithful :
mx_faithful aG.
@@ -764,51 +781,51 @@
Section GringMx.
-
Variables (
n :
nat) (
rG :
mx_representation G n).
+
Variables (
n :
nat) (
rG :
mx_representation G n).
-
Definition gring_mx :=
vec_mx \o mulmxr (
enveloping_algebra_mx rG).
-
Canonical gring_mx_linear :=
[linear of gring_mx].
+
Definition gring_mx :=
vec_mx \o mulmxr (
enveloping_algebra_mx rG).
+
Canonical gring_mx_linear :=
[linear of gring_mx].
Lemma gring_mxJ a x :
-
x \in G → gring_mx (
a ×m aG x)
= gring_mx a ×m rG x.
+
x \in G → gring_mx (
a ×m aG x)
= gring_mx a ×m rG x.
End GringMx.
-
Lemma gring_mxK :
cancel (
gring_mx aG)
gring_row.
+
Lemma gring_mxK :
cancel (
gring_mx aG)
gring_row.
Section GringOp.
-
Variables (
n :
nat) (
rG :
mx_representation G n).
+
Variables (
n :
nat) (
rG :
mx_representation G n).
-
Definition gring_op :=
gring_mx rG \o gring_row.
-
Canonical gring_op_linear :=
[linear of gring_op].
+
Definition gring_op :=
gring_mx rG \o gring_row.
+
Canonical gring_op_linear :=
[linear of gring_op].
-
Lemma gring_opE a :
gring_op a = gring_mx rG (
gring_row a).
+
Lemma gring_opE a :
gring_op a = gring_mx rG (
gring_row a).
-
Lemma gring_opG x :
x \in G → gring_op (
aG x)
= rG x.
+
Lemma gring_opG x :
x \in G → gring_op (
aG x)
= rG x.
-
Lemma gring_op1 :
gring_op 1
%:M = 1
%:M.
+
Lemma gring_op1 :
gring_op 1
%:M = 1
%:M.
Lemma gring_opJ A b :
-
gring_op (
A ×m gring_mx aG b)
= gring_op A ×m gring_mx rG b.
+
gring_op (
A ×m gring_mx aG b)
= gring_op A ×m gring_mx rG b.
-
Lemma gring_op_mx b :
gring_op (
gring_mx aG b)
= gring_mx rG b.
+
Lemma gring_op_mx b :
gring_op (
gring_mx aG b)
= gring_mx rG b.
Lemma gring_mxA a b :
-
gring_mx rG (
a ×m gring_mx aG b)
= gring_mx rG a ×m gring_mx rG b.
+
gring_mx rG (
a ×m gring_mx aG b)
= gring_mx rG a ×m gring_mx rG b.
End GringOp.
@@ -827,55 +844,55 @@
Section ChangeOfRing.
-
Variables (
aR rR :
comUnitRingType) (
f :
{rmorphism aR → rR}).
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
aR rR :
comUnitRingType) (
f :
{rmorphism aR → rR}).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
-
Lemma map_regular_mx x :
(regular_mx aR G x)^f = regular_mx rR G x.
+
Lemma map_regular_mx x :
(regular_mx aR G x)^f = regular_mx rR G x.
-
Lemma map_gring_row (
A :
'M_#|G|) :
(gring_row A)^f = gring_row A^f.
+
Lemma map_gring_row (
A :
'M_#|G|) :
(gring_row A)^f = gring_row A^f.
-
Lemma map_gring_proj x (
A :
'M_#|G|) :
(gring_proj x A)^f = gring_proj x A^f.
+
Lemma map_gring_proj x (
A :
'M_#|G|) :
(gring_proj x A)^f = gring_proj x A^f.
Section OneRepresentation.
-
Variables (
n :
nat) (
rG :
mx_representation aR G n).
+
Variables (
n :
nat) (
rG :
mx_representation aR G n).
-
Definition map_repr_mx (
f0 :
aR → rR)
rG0 (
g :
gT) :
'M_n :=
map_mx f0 (
rG0 g).
+
Definition map_repr_mx (
f0 :
aR → rR)
rG0 (
g :
gT) :
'M_n :=
map_mx f0 (
rG0 g).
Lemma map_mx_repr :
mx_repr G (
map_repr_mx f rG).
Canonical map_repr :=
MxRepresentation map_mx_repr.
-
Lemma map_reprE x :
rGf x = (rG x)^f.
+
Lemma map_reprE x :
rGf x = (rG x)^f.
-
Lemma map_reprJ m (
A :
'M_(m, n))
x :
(A ×m rG x)^f = A^f ×m rGf x.
+
Lemma map_reprJ m (
A :
'M_(m, n))
x :
(A ×m rG x)^f = A^f ×m rGf x.
Lemma map_enveloping_algebra_mx :
-
(enveloping_algebra_mx rG)^f = enveloping_algebra_mx rGf.
+
(enveloping_algebra_mx rG)^f = enveloping_algebra_mx rGf.
-
Lemma map_gring_mx a :
(gring_mx rG a)^f = gring_mx rGf a^f.
+
Lemma map_gring_mx a :
(gring_mx rG a)^f = gring_mx rGf a^f.
-
Lemma map_gring_op A :
(gring_op rG A)^f = gring_op rGf A^f.
+
Lemma map_gring_op A :
(gring_op rG A)^f = gring_op rGf A^f.
End OneRepresentation.
-
Lemma map_regular_repr :
map_repr (
regular_repr aR G)
=1 regular_repr rR G.
+
Lemma map_regular_repr :
map_repr (
regular_repr aR G)
=1 regular_repr rR G.
-
Lemma map_group_ring :
(group_ring aR G)^f = group_ring rR G.
+
Lemma map_group_ring :
(group_ring aR G)^f = group_ring rR G.
@@ -901,92 +918,92 @@
Variable gT :
finGroupType.
-
Variables (
G :
{group gT}) (
n :
nat) (
rG :
mx_representation F G n).
+
Variables (
G :
{group gT}) (
n :
nat) (
rG :
mx_representation F G n).
-
Lemma repr_mx_free x :
x \in G → row_free (
rG x).
+
Lemma repr_mx_free x :
x \in G → row_free (
rG x).
Section Stabilisers.
-
Variables (
m :
nat) (
U :
'M[F]_(m, n)).
+
Variables (
m :
nat) (
U :
'M[F]_(m, n)).
-
Definition rstabs :=
[set x in G | U ×m rG x ≤ U]%
MS.
+
Definition rstabs :=
[set x in G | U ×m rG x ≤ U]%
MS.
-
Lemma rstabs_sub :
rstabs \subset G.
+
Lemma rstabs_sub :
rstabs \subset G.
Lemma rstabs_group_set :
group_set rstabs.
Canonical rstabs_group :=
Group rstabs_group_set.
-
Lemma rstab_act x m1 (
W :
'M_(m1, n)) :
-
x \in rstab rG U → (
W ≤ U)%
MS → W ×m rG x = W.
+
Lemma rstab_act x m1 (
W :
'M_(m1, n)) :
+
x \in rstab rG U → (
W ≤ U)%
MS → W ×m rG x = W.
-
Lemma rstabs_act x m1 (
W :
'M_(m1, n)) :
-
x \in rstabs → (
W ≤ U)%
MS → (
W ×m rG x ≤ U)%
MS.
+
Lemma rstabs_act x m1 (
W :
'M_(m1, n)) :
+
x \in rstabs → (
W ≤ U)%
MS → (
W ×m rG x ≤ U)%
MS.
-
Definition mxmodule :=
G \subset rstabs.
+
Definition mxmodule :=
G \subset rstabs.
-
Lemma mxmoduleP :
reflect {in G, ∀ x,
U ×m rG x ≤ U}%
MS mxmodule.
+
Lemma mxmoduleP :
reflect {in G, ∀ x,
U ×m rG x ≤ U}%
MS mxmodule.
End Stabilisers.
-
Lemma rstabS m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
- (
U ≤ V)%
MS → rstab rG V \subset rstab rG U.
+
Lemma rstabS m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
+ (
U ≤ V)%
MS → rstab rG V \subset rstab rG U.
-
Lemma eqmx_rstab m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
- (
U :=: V)%
MS → rstab rG U = rstab rG V.
+
Lemma eqmx_rstab m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
+ (
U :=: V)%
MS → rstab rG U = rstab rG V.
-
Lemma eqmx_rstabs m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
- (
U :=: V)%
MS → rstabs U = rstabs V.
+
Lemma eqmx_rstabs m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
+ (
U :=: V)%
MS → rstabs U = rstabs V.
-
Lemma eqmx_module m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
- (
U :=: V)%
MS → mxmodule U = mxmodule V.
+
Lemma eqmx_module m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
+ (
U :=: V)%
MS → mxmodule U = mxmodule V.
-
Lemma mxmodule0 m :
mxmodule (0
: 'M_(m, n)).
+
Lemma mxmodule0 m :
mxmodule (0
: 'M_(m, n)).
-
Lemma mxmodule1 :
mxmodule 1
%:M.
+
Lemma mxmodule1 :
mxmodule 1
%:M.
-
Lemma mxmodule_trans m1 m2 (
U :
'M_(m1, n)) (
W :
'M_(m2, n))
x :
-
mxmodule U → x \in G → (
W ≤ U → W ×m rG x ≤ U)%
MS.
+
Lemma mxmodule_trans m1 m2 (
U :
'M_(m1, n)) (
W :
'M_(m2, n))
x :
+
mxmodule U → x \in G → (
W ≤ U → W ×m rG x ≤ U)%
MS.
-
Lemma mxmodule_eigenvector m (
U :
'M_(m, n)) :
-
mxmodule U → \rank U = 1%
N →
-
{u : 'rV_n & {a | (
U :=: u)%
MS & {in G, ∀ x,
u ×m rG x = a x *: u}}}.
+
Lemma mxmodule_eigenvector m (
U :
'M_(m, n)) :
+
mxmodule U → \rank U = 1%
N →
+
{u : 'rV_n & {a | (
U :=: u)%
MS & {in G, ∀ x,
u ×m rG x = a x *: u}}}.
Lemma addsmx_module m1 m2 U V :
- @
mxmodule m1 U → @
mxmodule m2 V → mxmodule (
U + V)%
MS.
+ @
mxmodule m1 U → @
mxmodule m2 V → mxmodule (
U + V)%
MS.
-
Lemma sumsmx_module I r (
P :
pred I)
U :
-
(∀ i,
P i → mxmodule (
U i)
) → mxmodule (
\sum_(i <- r | P i) U i)%
MS.
+
Lemma sumsmx_module I r (
P :
pred I)
U :
+
(∀ i,
P i → mxmodule (
U i)
) → mxmodule (
\sum_(i <- r | P i) U i)%
MS.
Lemma capmx_module m1 m2 U V :
- @
mxmodule m1 U → @
mxmodule m2 V → mxmodule (
U :&: V)%
MS.
+ @
mxmodule m1 U → @
mxmodule m2 V → mxmodule (
U :&: V)%
MS.
-
Lemma bigcapmx_module I r (
P :
pred I)
U :
-
(∀ i,
P i → mxmodule (
U i)
) → mxmodule (
\bigcap_(i <- r | P i) U i)%
MS.
+
Lemma bigcapmx_module I r (
P :
pred I)
U :
+
(∀ i,
P i → mxmodule (
U i)
) → mxmodule (
\bigcap_(i <- r | P i) U i)%
MS.
-Variable U : 'M[F]_n.
+Variable U : 'M[F]_n.
-Definition val_submod m : 'M_(m, \rank U) → 'M_(m, n) := mulmxr (row_base U).
-Definition in_submod m : 'M_(m, n) → 'M_(m, \rank U) :=
- mulmxr (invmx (row_ebase U) ×m pid_mx (\rank U)).
-Canonical val_submod_linear m := [linear of @val_submod m].
-Canonical in_submod_linear m := [linear of @in_submod m].
+Definition val_submod m : 'M_(m, \rank U) → 'M_(m, n) := mulmxr (row_base U).
+Definition in_submod m : 'M_(m, n) → 'M_(m, \rank U) :=
+ mulmxr (invmx (row_ebase U) ×m pid_mx (\rank U)).
+Canonical val_submod_linear m := [linear of @val_submod m].
+Canonical in_submod_linear m := [linear of @in_submod m].
-Lemma val_submodE m W : @val_submod m W = W ×m val_submod 1%:M.
+Lemma val_submodE m W : @val_submod m W = W ×m val_submod 1%:M.
-Lemma in_submodE m W : @in_submod m W = W ×m in_submod 1%:M.
+Lemma in_submodE m W : @in_submod m W = W ×m in_submod 1%:M.
-Lemma val_submod1 : (val_submod 1%:M :=: U)%MS.
+Lemma val_submod1 : (val_submod 1%:M :=: U)%MS.
-Lemma val_submodP m W : (@val_submod m W ≤ U)%MS.
+Lemma val_submodP m W : (@val_submod m W ≤ U)%MS.
-Lemma val_submodK m : cancel (@val_submod m) (@in_submod m).
+Lemma val_submodK m : cancel (@val_submod m) (@in_submod m).
-Lemma val_submod_inj m : injective (@val_submod m).
+Lemma val_submod_inj m : injective (@val_submod m).
-Lemma val_submodS m1 m2 (V : 'M_(m1, \rank U)) (W : 'M_(m2, \rank U)) :
- (val_submod V ≤ val_submod W)%MS = (V ≤ W)%MS.
+Lemma val_submodS m1 m2 (V : 'M_(m1, \rank U)) (W : 'M_(m2, \rank U)) :
+ (val_submod V ≤ val_submod W)%MS = (V ≤ W)%MS.
-Lemma in_submodK m W : (W ≤ U)%MS → val_submod (@in_submod m W) = W.
+Lemma in_submodK m W : (W ≤ U)%MS → val_submod (@in_submod m W) = W.
-Lemma val_submod_eq0 m W : (@val_submod m W == 0) = (W == 0).
+Lemma val_submod_eq0 m W : (@val_submod m W == 0) = (W == 0).
-Lemma in_submod_eq0 m W : (@in_submod m W == 0) = (W ≤ U^C)%MS.
+Lemma in_submod_eq0 m W : (@in_submod m W == 0) = (W ≤ U^C)%MS.
-Lemma mxrank_in_submod m (W : 'M_(m, n)) :
- (W ≤ U)%MS → \rank (in_submod W) = \rank W.
+Lemma mxrank_in_submod m (W : 'M_(m, n)) :
+ (W ≤ U)%MS → \rank (in_submod W) = \rank W.
-Definition val_factmod m : _ → 'M_(m, n) :=
- mulmxr (row_base (cokermx U) ×m row_ebase U).
-Definition in_factmod m : 'M_(m, n) → _ := mulmxr (col_base (cokermx U)).
-Canonical val_factmod_linear m := [linear of @val_factmod m].
-Canonical in_factmod_linear m := [linear of @in_factmod m].
+Definition val_factmod m : _ → 'M_(m, n) :=
+ mulmxr (row_base (cokermx U) ×m row_ebase U).
+Definition in_factmod m : 'M_(m, n) → _ := mulmxr (col_base (cokermx U)).
+Canonical val_factmod_linear m := [linear of @val_factmod m].
+Canonical in_factmod_linear m := [linear of @in_factmod m].
-Lemma val_factmodE m W : @val_factmod m W = W ×m val_factmod 1%:M.
+Lemma val_factmodE m W : @val_factmod m W = W ×m val_factmod 1%:M.
-Lemma in_factmodE m W : @in_factmod m W = W ×m in_factmod 1%:M.
+Lemma in_factmodE m W : @in_factmod m W = W ×m in_factmod 1%:M.
-Lemma val_factmodP m W : (@val_factmod m W ≤ U^C)%MS.
+Lemma val_factmodP m W : (@val_factmod m W ≤ U^C)%MS.
-Lemma val_factmodK m : cancel (@val_factmod m) (@in_factmod m).
+Lemma val_factmodK m : cancel (@val_factmod m) (@in_factmod m).
-Lemma val_factmod_inj m : injective (@val_factmod m).
+Lemma val_factmod_inj m : injective (@val_factmod m).
-Lemma val_factmodS m1 m2 (V : 'M_(m1, _)) (W : 'M_(m2, _)) :
- (val_factmod V ≤ val_factmod W)%MS = (V ≤ W)%MS.
+Lemma val_factmodS m1 m2 (V : 'M_(m1, _)) (W : 'M_(m2, _)) :
+ (val_factmod V ≤ val_factmod W)%MS = (V ≤ W)%MS.
-Lemma val_factmod_eq0 m W : (@val_factmod m W == 0) = (W == 0).
+Lemma val_factmod_eq0 m W : (@val_factmod m W == 0) = (W == 0).
-Lemma in_factmod_eq0 m (W : 'M_(m, n)) : (in_factmod W == 0) = (W ≤ U)%MS.
+Lemma in_factmod_eq0 m (W : 'M_(m, n)) : (in_factmod W == 0) = (W ≤ U)%MS.
-Lemma in_factmodK m (W : 'M_(m, n)) :
- (W ≤ U^C)%MS → val_factmod (in_factmod W) = W.
+Lemma in_factmodK m (W : 'M_(m, n)) :
+ (W ≤ U^C)%MS → val_factmod (in_factmod W) = W.
-Lemma in_factmod_addsK m (W : 'M_(m, n)) :
- (in_factmod (U + W)%MS :=: in_factmod W)%MS.
+Lemma in_factmod_addsK m (W : 'M_(m, n)) :
+ (in_factmod (U + W)%MS :=: in_factmod W)%MS.
-Lemma add_sub_fact_mod m (W : 'M_(m, n)) :
- val_submod (in_submod W) + val_factmod (in_factmod W) = W.
+Lemma add_sub_fact_mod m (W : 'M_(m, n)) :
+ val_submod (in_submod W) + val_factmod (in_factmod W) = W.
-Lemma proj_factmodS m (W : 'M_(m, n)) :
- (val_factmod (in_factmod W) ≤ U + W)%MS.
+Lemma proj_factmodS m (W : 'M_(m, n)) :
+ (val_factmod (in_factmod W) ≤ U + W)%MS.
-Lemma in_factmodsK m (W : 'M_(m, n)) :
- (U ≤ W)%MS → (U + val_factmod (in_factmod W) :=: W)%MS.
+Lemma in_factmodsK m (W : 'M_(m, n)) :
+ (U ≤ W)%MS → (U + val_factmod (in_factmod W) :=: W)%MS.
-Lemma mxrank_in_factmod m (W : 'M_(m, n)) :
- (\rank (in_factmod W) + \rank U)%N = \rank (U + W).
+Lemma mxrank_in_factmod m (W : 'M_(m, n)) :
+ (\rank (in_factmod W) + \rank U)%N = \rank (U + W).
Definition submod_mx of mxmodule U :=
- fun x ⇒ in_submod (val_submod 1%:M ×m rG x).
+ fun x ⇒ in_submod (val_submod 1%:M ×m rG x).
Definition factmod_mx of mxmodule U :=
- fun x ⇒ in_factmod (val_factmod 1%:M ×m rG x).
+ fun x ⇒ in_factmod (val_factmod 1%:M ×m rG x).
Hypothesis Umod : mxmodule U.
-Lemma in_submodJ m (W : 'M_(m, n)) x :
- (W ≤ U)%MS → in_submod (W ×m rG x) = in_submod W ×m submod_mx Umod x.
+Lemma in_submodJ m (W : 'M_(m, n)) x :
+ (W ≤ U)%MS → in_submod (W ×m rG x) = in_submod W ×m submod_mx Umod x.
-Lemma val_submodJ m (W : 'M_(m, \rank U)) x :
- x \in G → val_submod (W ×m submod_mx Umod x) = val_submod W ×m rG x.
+Lemma val_submodJ m (W : 'M_(m, \rank U)) x :
+ x \in G → val_submod (W ×m submod_mx Umod x) = val_submod W ×m rG x.
Lemma submod_mx_repr : mx_repr G (submod_mx Umod).
@@ -1124,14 +1141,14 @@
Canonical submod_repr := MxRepresentation submod_mx_repr.
-Lemma in_factmodJ m (W : 'M_(m, n)) x :
- x \in G → in_factmod (W ×m rG x) = in_factmod W ×m factmod_mx Umod x.
+Lemma in_factmodJ m (W : 'M_(m, n)) x :
+ x \in G → in_factmod (W ×m rG x) = in_factmod W ×m factmod_mx Umod x.
-Lemma val_factmodJ m (W : 'M_(m, \rank (cokermx U))) x :
- x \in G →
- val_factmod (W ×m factmod_mx Umod x) =
- val_factmod (in_factmod (val_factmod W ×m rG x)).
+Lemma val_factmodJ m (W : 'M_(m, \rank (cokermx U))) x :
+ x \in G →
+ val_factmod (W ×m factmod_mx Umod x) =
+ val_factmod (in_factmod (val_factmod W ×m rG x)).
Lemma factmod_mx_repr : mx_repr G (factmod_mx Umod).
@@ -1145,7 +1162,7 @@
- Properties of enveloping algebra as a subspace of 'rV(n ^ 2).
+ Properties of enveloping algebra as a subspace of 'rV(n ^ 2).
@@ -1185,40 +1202,40 @@
-
Definition dom_hom_mx f :
'M_n :=
-
kermx (
lin1_mx (
mxvec \o mulmx (
cent_mx_fun E_G f)
\o lin_mul_row)).
+
Definition dom_hom_mx f :
'M_n :=
+
kermx (
lin1_mx (
mxvec \o mulmx (
cent_mx_fun E_G f)
\o lin_mul_row)).
-
Lemma hom_mxP m f (
W :
'M_(m, n)) :
-
reflect (
∀ x,
x \in G → W ×m rG x ×m f = W ×m f ×m rG x)
- (
W ≤ dom_hom_mx f)%
MS.
+
Lemma hom_mxP m f (
W :
'M_(m, n)) :
+
reflect (
∀ x,
x \in G → W ×m rG x ×m f = W ×m f ×m rG x)
+ (
W ≤ dom_hom_mx f)%
MS.
-
Lemma hom_envelop_mxC m f (
W :
'M_(m, n))
A :
- (
W ≤ dom_hom_mx f → A \in E_G → W ×m A ×m f = W ×m f ×m A)%
MS.
+
Lemma hom_envelop_mxC m f (
W :
'M_(m, n))
A :
+ (
W ≤ dom_hom_mx f → A \in E_G → W ×m A ×m f = W ×m f ×m A)%
MS.
Lemma dom_hom_invmx f :
-
f \in unitmx → (
dom_hom_mx (
invmx f)
:=: dom_hom_mx f ×m f)%
MS.
+
f \in unitmx → (
dom_hom_mx (
invmx f)
:=: dom_hom_mx f ×m f)%
MS.
Lemma dom_hom_mx_module f :
mxmodule (
dom_hom_mx f).
-
Lemma hom_mxmodule m (
U :
'M_(m, n))
f :
- (
U ≤ dom_hom_mx f)%
MS → mxmodule U → mxmodule (
U ×m f).
+
Lemma hom_mxmodule m (
U :
'M_(m, n))
f :
+ (
U ≤ dom_hom_mx f)%
MS → mxmodule U → mxmodule (
U ×m f).
-
Lemma kermx_hom_module m (
U :
'M_(m, n))
f :
- (
U ≤ dom_hom_mx f)%
MS → mxmodule U → mxmodule (
U :&: kermx f)%
MS.
+
Lemma kermx_hom_module m (
U :
'M_(m, n))
f :
+ (
U ≤ dom_hom_mx f)%
MS → mxmodule U → mxmodule (
U :&: kermx f)%
MS.
-
Lemma scalar_mx_hom a m (
U :
'M_(m, n)) : (
U ≤ dom_hom_mx a%:M)%
MS.
+
Lemma scalar_mx_hom a m (
U :
'M_(m, n)) : (
U ≤ dom_hom_mx a%:M)%
MS.
-
Lemma proj_mx_hom (
U V :
'M_n) :
- (
U :&: V = 0)%
MS → mxmodule U → mxmodule V →
- (
U + V ≤ dom_hom_mx (
proj_mx U V))%
MS.
+
Lemma proj_mx_hom (
U V :
'M_n) :
+ (
U :&: V = 0)%
MS → mxmodule U → mxmodule V →
+ (
U + V ≤ dom_hom_mx (
proj_mx U V))%
MS.
@@ -1233,37 +1250,37 @@
@@ -1272,28 +1289,28 @@
The cyclic module generated by a single vector.
@@ -1304,11 +1321,11 @@
@@ -1320,11 +1337,11 @@
Definition row_hom_mx u :=
- (\bigcap_j kermx (vec_mx (row j (annihilator_mx u))))%MS.
+ (\bigcap_j kermx (vec_mx (row j (annihilator_mx u))))%MS.
Lemma row_hom_mxP u v :
- reflect (exists2 f, u ≤ dom_hom_mx f & u ×m f = v)%MS (v ≤ row_hom_mx u)%MS.
+ reflect (exists2 f, u ≤ dom_hom_mx f & u ×m f = v)%MS (v ≤ row_hom_mx u)%MS.
@@ -1342,26 +1359,26 @@
@@ -1372,31 +1389,31 @@
-
Definition mxsimple (
V :
'M_n) :=
-
[/\ mxmodule V, V != 0
&
-
∀ U :
'M_n,
mxmodule U → (
U ≤ V)%
MS → U != 0
→ (
V ≤ U)%
MS].
+
Definition mxsimple (
V :
'M_n) :=
+
[/\ mxmodule V, V != 0
&
+
∀ U :
'M_n,
mxmodule U → (
U ≤ V)%
MS → U != 0
→ (
V ≤ U)%
MS].
-
Definition mxnonsimple (
U :
'M_n) :=
-
∃ V :
'M_n, [&& mxmodule V, (
V ≤ U)%
MS, V != 0
& \rank V < \rank U].
+
Definition mxnonsimple (
U :
'M_n) :=
+
∃ V :
'M_n, [&& mxmodule V, (
V ≤ U)%
MS, V != 0
& \rank V < \rank U].
Lemma mxsimpleP U :
-
[/\ mxmodule U, U != 0
& ¬ mxnonsimple U] ↔ mxsimple U.
+
[/\ mxmodule U, U != 0
& ¬ mxnonsimple U] ↔ mxsimple U.
-
Lemma mxsimple_module U :
mxsimple U → mxmodule U.
+
Lemma mxsimple_module U :
mxsimple U → mxmodule U.
-
Lemma mxsimple_exists m (
U :
'M_(m, n)) :
-
mxmodule U → U != 0
→ classically (
exists2 V, mxsimple V & V ≤ U)%
MS.
+
Lemma mxsimple_exists m (
U :
'M_(m, n)) :
+
mxmodule U → U != 0
→ classically (
exists2 V, mxsimple V & V ≤ U)%
MS.
-
Lemma mx_iso_simple U V :
mx_iso U V → mxsimple U → mxsimple V.
+
Lemma mx_iso_simple U V :
mx_iso U V → mxsimple U → mxsimple V.
Lemma mxsimple_cyclic u U :
-
mxsimple U → u != 0
→ (
u ≤ U)%
MS → (
U :=: cyclic_mx u)%
MS.
+
mxsimple U → u != 0
→ (
u ≤ U)%
MS → (
U :=: cyclic_mx u)%
MS.
@@ -1405,9 +1422,9 @@
The surjective part of Schur's lemma.
@@ -1417,7 +1434,7 @@
@@ -1427,7 +1444,7 @@
@@ -1437,8 +1454,8 @@
@@ -1450,19 +1467,19 @@
@@ -1478,9 +1495,9 @@
Implicit Type I : finType.
-CoInductive mxsemisimple (V : 'M_n) :=
- MxSemisimple I U (W := (\sum_(i : I) U i)%MS) of
- ∀ i, mxsimple (U i) & (W :=: V)%MS & mxdirect W.
+Variant mxsemisimple (V : 'M_n) :=
+ MxSemisimple I U (W := (\sum_(i : I) U i)%MS) of
+ ∀ i, mxsimple (U i) & (W :=: V)%MS & mxdirect W.
@@ -1489,45 +1506,45 @@
This is a slight generalization of Aschbacher 12.5 for finite sets.
-
Lemma sum_mxsimple_direct_compl m I W (
U :
'M_(m, n)) :
-
let V := (
\sum_(i : I) W i)%
MS in
-
(∀ i :
I,
mxsimple (
W i)
) → mxmodule U → (
U ≤ V)%
MS →
-
{J : {set I} | let S :=
U + \sum_(i in J) W i in S :=: V ∧ mxdirect S}%
MS.
+
Lemma sum_mxsimple_direct_compl m I W (
U :
'M_(m, n)) :
+
let V := (
\sum_(i : I) W i)%
MS in
+
(∀ i :
I,
mxsimple (
W i)
) → mxmodule U → (
U ≤ V)%
MS →
+
{J : {set I} | let S :=
U + \sum_(i in J) W i in S :=: V ∧ mxdirect S}%
MS.
-
Lemma sum_mxsimple_direct_sub I W (
V :
'M_n) :
-
(∀ i :
I,
mxsimple (
W i)
) → (
\sum_i W i :=: V)%
MS →
-
{J : {set I} | let S :=
\sum_(i in J) W i in S :=: V ∧ mxdirect S}%
MS.
+
Lemma sum_mxsimple_direct_sub I W (
V :
'M_n) :
+
(∀ i :
I,
mxsimple (
W i)
) → (
\sum_i W i :=: V)%
MS →
+
{J : {set I} | let S :=
\sum_(i in J) W i in S :=: V ∧ mxdirect S}%
MS.
Lemma mxsemisimple0 :
mxsemisimple 0.
-
Lemma intro_mxsemisimple (
I :
Type)
r (
P :
pred I)
W V :
- (
\sum_(i <- r | P i) W i :=: V)%
MS →
-
(∀ i,
P i → W i != 0
→ mxsimple (
W i)
) →
+
Lemma intro_mxsemisimple (
I :
Type)
r (
P :
pred I)
W V :
+ (
\sum_(i <- r | P i) W i :=: V)%
MS →
+
(∀ i,
P i → W i != 0
→ mxsimple (
W i)
) →
mxsemisimple V.
-
Lemma mxsimple_semisimple U :
mxsimple U → mxsemisimple U.
+
Lemma mxsimple_semisimple U :
mxsimple U → mxsemisimple U.
Lemma addsmx_semisimple U V :
-
mxsemisimple U → mxsemisimple V → mxsemisimple (
U + V)%
MS.
+
mxsemisimple U → mxsemisimple V → mxsemisimple (
U + V)%
MS.
-
Lemma sumsmx_semisimple (
I :
finType) (
P :
pred I)
V :
-
(∀ i,
P i → mxsemisimple (
V i)
) → mxsemisimple (
\sum_(i | P i) V i)%
MS.
+
Lemma sumsmx_semisimple (
I :
finType) (
P :
pred I)
V :
+
(∀ i,
P i → mxsemisimple (
V i)
) → mxsemisimple (
\sum_(i | P i) V i)%
MS.
-
Lemma eqmx_semisimple U V : (
U :=: V)%
MS → mxsemisimple U → mxsemisimple V.
+
Lemma eqmx_semisimple U V : (
U :=: V)%
MS → mxsemisimple U → mxsemisimple V.
-
Lemma hom_mxsemisimple (
V f :
'M_n) :
-
mxsemisimple V → (
V ≤ dom_hom_mx f)%
MS → mxsemisimple (
V ×m f).
+
Lemma hom_mxsemisimple (
V f :
'M_n) :
+
mxsemisimple V → (
V ≤ dom_hom_mx f)%
MS → mxsemisimple (
V ×m f).
-
Lemma mxsemisimple_module U :
mxsemisimple U → mxmodule U.
+
Lemma mxsemisimple_module U :
mxsemisimple U → mxmodule U.
-Fact component_mx_key : unit.
-Definition component_mx_expr (U : 'M[F]_n) :=
- (\sum_i cyclic_mx (row i (row_hom_mx (nz_row U))))%MS.
-Definition component_mx := locked_with component_mx_key component_mx_expr.
-Canonical component_mx_unfoldable := [unlockable fun component_mx].
+Fact component_mx_key : unit.
+Definition component_mx_expr (U : 'M[F]_n) :=
+ (\sum_i cyclic_mx (row i (row_hom_mx (nz_row U))))%MS.
+Definition component_mx := locked_with component_mx_key component_mx_expr.
+Canonical component_mx_unfoldable := [unlockable fun component_mx].
-Variable U : 'M[F]_n.
+Variable U : 'M[F]_n.
Hypothesis simU : mxsimple U.
Let u := nz_row U.
Let iso_u := row_hom_mx u.
-Let nz_u : u != 0 := nz_row_mxsimple simU.
-Let Uu : (u ≤ U)%MS := nz_row_sub U.
-Let defU : (U :=: cyclic_mx u)%MS := mxsimple_cyclic simU nz_u Uu.
+Let nz_u : u != 0 := nz_row_mxsimple simU.
+Let Uu : (u ≤ U)%MS := nz_row_sub U.
+Let defU : (U :=: cyclic_mx u)%MS := mxsimple_cyclic simU nz_u Uu.
Lemma component_mx_module : mxmodule compU.
-Lemma genmx_component : <<compU>>%MS = compU.
+Lemma genmx_component : <<compU>>%MS = compU.
-Lemma component_mx_def : {I : finType & {W : I → 'M_n |
- ∀ i, mx_iso U (W i) & compU = \sum_i W i}}%MS.
+Lemma component_mx_def : {I : finType & {W : I → 'M_n |
+ ∀ i, mx_iso U (W i) & compU = \sum_i W i}}%MS.
Lemma component_mx_semisimple : mxsemisimple compU.
-Lemma mx_iso_component V : mx_iso U V → (V ≤ compU)%MS.
+Lemma mx_iso_component V : mx_iso U V → (V ≤ compU)%MS.
-Lemma component_mx_id : (U ≤ compU)%MS.
+Lemma component_mx_id : (U ≤ compU)%MS.
Lemma hom_component_mx_iso f V :
- mxsimple V → (compU ≤ dom_hom_mx f)%MS → (V ≤ compU ×m f)%MS →
+ mxsimple V → (compU ≤ dom_hom_mx f)%MS → (V ≤ compU ×m f)%MS →
mx_iso U V.
-Lemma component_mx_iso V : mxsimple V → (V ≤ compU)%MS → mx_iso U V.
+Lemma component_mx_iso V : mxsimple V → (V ≤ compU)%MS → mx_iso U V.
Lemma hom_component_mx f :
- (compU ≤ dom_hom_mx f)%MS → (compU ×m f ≤ compU)%MS.
+ (compU ≤ dom_hom_mx f)%MS → (compU ×m f ≤ compU)%MS.
End Components.
Lemma component_mx_isoP U V :
- mxsimple U → mxsimple V →
- reflect (mx_iso U V) (component_mx U == component_mx V).
+ mxsimple U → mxsimple V →
+ reflect (mx_iso U V) (component_mx U == component_mx V).
Lemma component_mx_disjoint U V :
- mxsimple U → mxsimple V → component_mx U != component_mx V →
- (component_mx U :&: component_mx V = 0)%MS.
+ mxsimple U → mxsimple V → component_mx U != component_mx V →
+ (component_mx U :&: component_mx V = 0)%MS.
Section Socle.
Record socleType := EnumSocle {
- socle_base_enum : seq 'M[F]_n;
- _ : ∀ M, M \in socle_base_enum → mxsimple M;
- _ : ∀ M, mxsimple M → has (mxsimple_iso M) socle_base_enum
+ socle_base_enum : seq 'M[F]_n;
+ _ : ∀ M, M \in socle_base_enum → mxsimple M;
+ _ : ∀ M, mxsimple M → has (mxsimple_iso M) socle_base_enum
}.
-Lemma socle_exists : classically socleType.
+Lemma socle_exists : classically socleType.
Section SocleDef.
@@ -1667,21 +1684,21 @@
Definition socle_enum := map component_mx (socle_base_enum sG0).
-Lemma component_socle M : mxsimple M → component_mx M \in socle_enum.
+Lemma component_socle M : mxsimple M → component_mx M \in socle_enum.
-Inductive socle_sort : predArgType := PackSocle W of W \in socle_enum.
+Inductive socle_sort : predArgType := PackSocle W of W \in socle_enum.
-Definition socle_base W := let: PackSocle W _ := W in e0`_(index W socle_enum).
+Definition socle_base W := let: PackSocle W _ := W in e0`_(index W socle_enum).
-Coercion socle_val W : 'M[F]_n := component_mx (socle_base W).
+Coercion socle_val W : 'M[F]_n := component_mx (socle_base W).
-Definition socle_mult (W : sG) := (\rank W %/ \rank (socle_base W))%N.
+Definition socle_mult (W : sG) := (\rank W %/ \rank (socle_base W))%N.
Lemma socle_simple W : mxsimple (socle_base W).
@@ -1693,35 +1710,35 @@
Definition socle_repr W := submod_repr (socle_module W).
-Lemma nz_socle (W : sG) : W != 0 :> 'M_n.
+Lemma nz_socle (W : sG) : W != 0 :> 'M_n.
-Lemma socle_mem (W : sG) : (W : 'M_n) \in socle_enum.
+Lemma socle_mem (W : sG) : (W : 'M_n) \in socle_enum.
-Lemma PackSocleK W e0W : @PackSocle W e0W = W :> 'M_n.
+Lemma PackSocleK W e0W : @PackSocle W e0W = W :> 'M_n.
Canonical socle_subType := SubType _ _ _ socle_sort_rect PackSocleK.
-Definition socle_eqMixin := Eval hnf in [eqMixin of sG by <:].
+Definition socle_eqMixin := Eval hnf in [eqMixin of sG by <:].
Canonical socle_eqType := Eval hnf in EqType sG socle_eqMixin.
-Definition socle_choiceMixin := Eval hnf in [choiceMixin of sG by <:].
+Definition socle_choiceMixin := Eval hnf in [choiceMixin of sG by <:].
Canonical socle_choiceType := ChoiceType sG socle_choiceMixin.
-Lemma socleP (W W' : sG) : reflect (W = W') (W == W')%MS.
+Lemma socleP (W W' : sG) : reflect (W = W') (W == W')%MS.
Fact socle_finType_subproof :
- cancel (fun W ⇒ SeqSub (socle_mem W)) (fun s ⇒ PackSocle (valP s)).
+ cancel (fun W ⇒ SeqSub (socle_mem W)) (fun s ⇒ PackSocle (valP s)).
Definition socle_countMixin := CanCountMixin socle_finType_subproof.
Canonical socle_countType := CountType sG socle_countMixin.
-Canonical socle_subCountType := [subCountType of sG].
+Canonical socle_subCountType := [subCountType of sG].
Definition socle_finMixin := CanFinMixin socle_finType_subproof.
Canonical socle_finType := FinType sG socle_finMixin.
-Canonical socle_subFinType := [subFinType of sG].
+Canonical socle_subFinType := [subFinType of sG].
End SocleDef.
@@ -1736,8 +1753,8 @@
Section SubSocle.
-Variable P : pred sG.
-Notation S := (\sum_(W : sG | P W) socle_val W)%MS.
+Variable P : pred sG.
+Notation S := (\sum_(W : sG | P W) socle_val W)%MS.
Lemma subSocle_module : mxmodule S.
@@ -1747,36 +1764,36 @@
Lemma subSocle_iso M :
- mxsimple M → (M ≤ S)%MS → {W : sG | P W & mx_iso (socle_base W) M}.
+ mxsimple M → (M ≤ S)%MS → {W : sG | P W & mx_iso (socle_base W) M}.
-Lemma capmx_subSocle m (M : 'M_(m, n)) :
- mxmodule M → (M :&: S :=: \sum_(W : sG | P W) (M :&: W))%MS.
+Lemma capmx_subSocle m (M : 'M_(m, n)) :
+ mxmodule M → (M :&: S :=: \sum_(W : sG | P W) (M :&: W))%MS.
End SubSocle.
-Lemma subSocle_direct P : mxdirect (\sum_(W : sG | P W) W).
+Lemma subSocle_direct P : mxdirect (\sum_(W : sG | P W) W).
-Definition Socle := (\sum_(W : sG) W)%MS.
+Definition Socle := (\sum_(W : sG) W)%MS.
-Lemma simple_Socle M : mxsimple M → (M ≤ Socle)%MS.
+Lemma simple_Socle M : mxsimple M → (M ≤ Socle)%MS.
-Lemma semisimple_Socle U : mxsemisimple U → (U ≤ Socle)%MS.
+Lemma semisimple_Socle U : mxsemisimple U → (U ≤ Socle)%MS.
Lemma reducible_Socle U :
- mxmodule U → mx_completely_reducible U → (U ≤ Socle)%MS.
+ mxmodule U → mx_completely_reducible U → (U ≤ Socle)%MS.
-Lemma genmx_Socle : <<Socle>>%MS = Socle.
+Lemma genmx_Socle : <<Socle>>%MS = Socle.
-Lemma reducible_Socle1 : mx_completely_reducible 1%:M → Socle = 1%:M.
+Lemma reducible_Socle1 : mx_completely_reducible 1%:M → Socle = 1%:M.
Lemma Socle_module : mxmodule Socle.
@@ -1788,7 +1805,7 @@
Lemma Socle_direct : mxdirect Socle.
-Lemma Socle_iso M : mxsimple M → {W : sG | mx_iso (socle_base W) M}.
+Lemma Socle_iso M : mxsimple M → {W : sG | mx_iso (socle_base W) M}.
End Socle.
@@ -1803,19 +1820,19 @@
Section CentHom.
-Variable f : 'M[F]_n.
+Variable f : 'M[F]_n.
-Lemma row_full_dom_hom : row_full (dom_hom_mx f) = centgmx rG f.
+Lemma row_full_dom_hom : row_full (dom_hom_mx f) = centgmx rG f.
-Lemma memmx_cent_envelop : (f \in 'C(E_G))%MS = centgmx rG f.
+Lemma memmx_cent_envelop : (f \in 'C(E_G))%MS = centgmx rG f.
-Lemma kermx_centg_module : centgmx rG f → mxmodule (kermx f).
+Lemma kermx_centg_module : centgmx rG f → mxmodule (kermx f).
-Lemma centgmx_hom m (U : 'M_(m, n)) : centgmx rG f → (U ≤ dom_hom_mx f)%MS.
+Lemma centgmx_hom m (U : 'M_(m, n)) : centgmx rG f → (U ≤ dom_hom_mx f)%MS.
End CentHom.
@@ -1830,11 +1847,11 @@
@@ -1844,28 +1861,28 @@
Lemma mx_Schur :
-
mx_irreducible → ∀ f,
centgmx rG f → f != 0
→ f \in unitmx.
+
mx_irreducible → ∀ f,
centgmx rG f → f != 0
→ f \in unitmx.
-
Definition mx_absolutely_irreducible :=
(n > 0
) && row_full E_G.
+
Definition mx_absolutely_irreducible :=
(n > 0
) && row_full E_G.
Lemma mx_abs_irrP :
-
reflect (
n > 0
∧ ∃ a_, ∀ A,
A = \sum_(x in G) a_ x A *: rG x)
+
reflect (
n > 0
∧ ∃ a_, ∀ A,
A = \sum_(x in G) a_ x A *: rG x)
mx_absolutely_irreducible.
Lemma mx_abs_irr_cent_scalar :
-
mx_absolutely_irreducible → ∀ A,
centgmx rG A → is_scalar_mx A.
+
mx_absolutely_irreducible → ∀ A,
centgmx rG A → is_scalar_mx A.
-
Lemma mx_abs_irrW :
mx_absolutely_irreducible → mx_irreducible.
+
Lemma mx_abs_irrW :
mx_absolutely_irreducible → mx_irreducible.
-
Lemma linear_mx_abs_irr :
n = 1%
N → mx_absolutely_irreducible.
+
Lemma linear_mx_abs_irr :
n = 1%
N → mx_absolutely_irreducible.
-
Lemma abelian_abs_irr :
abelian G → mx_absolutely_irreducible = (n == 1%
N).
+
Lemma abelian_abs_irr :
abelian G → mx_absolutely_irreducible = (n == 1%
N).
End OneRepresentation.
@@ -1880,7 +1897,7 @@
Section Proper.
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n' :
nat).
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n' :
nat).
Variable rG :
mx_representation F G n.
@@ -1893,17 +1910,17 @@
Section JacobsonDensity.
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
Variable rG :
mx_representation F G n.
Hypothesis irrG :
mx_irreducible rG.
-
Lemma mx_Jacobson_density : (
'C(Hom_G) ≤ E_G)%
MS.
+
Lemma mx_Jacobson_density : (
'C(Hom_G) ≤ E_G)%
MS.
-
Lemma cent_mx_scalar_abs_irr :
\rank Hom_G ≤ 1
→ mx_absolutely_irreducible rG.
+
Lemma cent_mx_scalar_abs_irr :
\rank Hom_G ≤ 1
→ mx_absolutely_irreducible rG.
End JacobsonDensity.
@@ -1912,44 +1929,44 @@
Section ChangeGroup.
-
Variables (
gT :
finGroupType) (
G H :
{group gT}) (
n :
nat).
+
Variables (
gT :
finGroupType) (
G H :
{group gT}) (
n :
nat).
Variables (
rG :
mx_representation F G n).
Section SubGroup.
-
Hypothesis sHG :
H \subset G.
+
Hypothesis sHG :
H \subset G.
-
Lemma rfix_subg :
rfix_mx rH = rfix_mx rG.
+
Lemma rfix_subg :
rfix_mx rH = rfix_mx rG.
Section Stabilisers.
-
Variables (
m :
nat) (
U :
'M[F]_(m, n)).
+
Variables (
m :
nat) (
U :
'M[F]_(m, n)).
-
Lemma rstabs_subg :
rstabs rH U = H :&: rstabs rG U.
+
Lemma rstabs_subg :
rstabs rH U = H :&: rstabs rG U.
-
Lemma mxmodule_subg :
mxmodule rG U → mxmodule rH U.
+
Lemma mxmodule_subg :
mxmodule rG U → mxmodule rH U.
End Stabilisers.
-
Lemma mxsimple_subg M :
mxmodule rG M → mxsimple rH M → mxsimple rG M.
+
Lemma mxsimple_subg M :
mxmodule rG M → mxsimple rH M → mxsimple rG M.
-
Lemma subg_mx_irr :
mx_irreducible rH → mx_irreducible rG.
+
Lemma subg_mx_irr :
mx_irreducible rH → mx_irreducible rG.
Lemma subg_mx_abs_irr :
-
mx_absolutely_irreducible rH → mx_absolutely_irreducible rG.
+
mx_absolutely_irreducible rH → mx_absolutely_irreducible rG.
End SubGroup.
@@ -1958,37 +1975,37 @@
Section SameGroup.
-
Hypothesis eqGH :
G :==: H.
+
Hypothesis eqGH :
G :==: H.
-
Lemma rfix_eqg :
rfix_mx rH = rfix_mx rG.
+
Lemma rfix_eqg :
rfix_mx rH = rfix_mx rG.
Section Stabilisers.
-
Variables (
m :
nat) (
U :
'M[F]_(m, n)).
+
Variables (
m :
nat) (
U :
'M[F]_(m, n)).
-
Lemma rstabs_eqg :
rstabs rH U = rstabs rG U.
+
Lemma rstabs_eqg :
rstabs rH U = rstabs rG U.
-
Lemma mxmodule_eqg :
mxmodule rH U = mxmodule rG U.
+
Lemma mxmodule_eqg :
mxmodule rH U = mxmodule rG U.
End Stabilisers.
-
Lemma mxsimple_eqg M :
mxsimple rH M ↔ mxsimple rG M.
+
Lemma mxsimple_eqg M :
mxsimple rH M ↔ mxsimple rG M.
-
Lemma eqg_mx_irr :
mx_irreducible rH ↔ mx_irreducible rG.
+
Lemma eqg_mx_irr :
mx_irreducible rH ↔ mx_irreducible rG.
Lemma eqg_mx_abs_irr :
-
mx_absolutely_irreducible rH = mx_absolutely_irreducible rG.
+
mx_absolutely_irreducible rH = mx_absolutely_irreducible rG.
End SameGroup.
@@ -2000,36 +2017,36 @@
Section Morphpre.
-
Variables (
aT rT :
finGroupType) (
D :
{group aT}) (
f :
{morphism D >-> rT}).
-
Variables (
G :
{group rT}) (
n :
nat) (
rG :
mx_representation F G n).
+
Variables (
aT rT :
finGroupType) (
D :
{group aT}) (
f :
{morphism D >-> rT}).
+
Variables (
G :
{group rT}) (
n :
nat) (
rG :
mx_representation F G n).
Section Stabilisers.
-
Variables (
m :
nat) (
U :
'M[F]_(m, n)).
+
Variables (
m :
nat) (
U :
'M[F]_(m, n)).
-
Lemma rstabs_morphpre :
rstabs rGf U = f @*^-1 (rstabs rG U).
+
Lemma rstabs_morphpre :
rstabs rGf U = f @*^-1 (rstabs rG U).
-
Lemma mxmodule_morphpre :
G \subset f @* D → mxmodule rGf U = mxmodule rG U.
+
Lemma mxmodule_morphpre :
G \subset f @* D → mxmodule rGf U = mxmodule rG U.
End Stabilisers.
-
Lemma rfix_morphpre (
H :
{set aT}) :
-
H \subset D → (
rfix_mx rGf H :=: rfix_mx rG (
f @* H))%
MS.
+
Lemma rfix_morphpre (
H :
{set aT}) :
+
H \subset D → (
rfix_mx rGf H :=: rfix_mx rG (
f @* H))%
MS.
Lemma morphpre_mx_irr :
-
G \subset f @* D → (mx_irreducible rGf ↔ mx_irreducible rG).
+
G \subset f @* D → (mx_irreducible rGf ↔ mx_irreducible rG).
Lemma morphpre_mx_abs_irr :
-
G \subset f @* D →
-
mx_absolutely_irreducible rGf = mx_absolutely_irreducible rG.
+
G \subset f @* D →
+
mx_absolutely_irreducible rGf = mx_absolutely_irreducible rG.
End Morphpre.
@@ -2038,43 +2055,43 @@
Section Morphim.
-
Variables (
aT rT :
finGroupType) (
G D :
{group aT}) (
f :
{morphism D >-> rT}).
-
Variables (
n :
nat) (
rGf :
mx_representation F (
f @* G)
n).
+
Variables (
aT rT :
finGroupType) (
G D :
{group aT}) (
f :
{morphism D >-> rT}).
+
Variables (
n :
nat) (
rGf :
mx_representation F (
f @* G)
n).
-
Hypothesis sGD :
G \subset D.
+
Hypothesis sGD :
G \subset D.
-
Let sG_f'fG :
G \subset f @*^-1 (f @* G).
+
Let sG_f'fG :
G \subset f @*^-1 (f @* G).
Section Stabilisers.
-
Variables (
m :
nat) (
U :
'M[F]_(m, n)).
+
Variables (
m :
nat) (
U :
'M[F]_(m, n)).
-
Lemma rstabs_morphim :
rstabs rG U = G :&: f @*^-1 rstabs rGf U.
+
Lemma rstabs_morphim :
rstabs rG U = G :&: f @*^-1 rstabs rGf U.
-
Lemma mxmodule_morphim :
mxmodule rG U = mxmodule rGf U.
+
Lemma mxmodule_morphim :
mxmodule rG U = mxmodule rGf U.
End Stabilisers.
-
Lemma rfix_morphim (
H :
{set aT}) :
-
H \subset D → (
rfix_mx rG H :=: rfix_mx rGf (
f @* H))%
MS.
+
Lemma rfix_morphim (
H :
{set aT}) :
+
H \subset D → (
rfix_mx rG H :=: rfix_mx rGf (
f @* H))%
MS.
-
Lemma mxsimple_morphim M :
mxsimple rG M ↔ mxsimple rGf M.
+
Lemma mxsimple_morphim M :
mxsimple rG M ↔ mxsimple rGf M.
-
Lemma morphim_mx_irr : (
mx_irreducible rG ↔ mx_irreducible rGf).
+
Lemma morphim_mx_irr : (
mx_irreducible rG ↔ mx_irreducible rGf).
Lemma morphim_mx_abs_irr :
-
mx_absolutely_irreducible rG = mx_absolutely_irreducible rGf.
+
mx_absolutely_irreducible rG = mx_absolutely_irreducible rGf.
End Morphim.
@@ -2083,69 +2100,69 @@
Section Submodule.
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
-
Variables (
rG :
mx_representation F G n) (
U :
'M[F]_n) (
Umod :
mxmodule rG U).
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
+
Variables (
rG :
mx_representation F G n) (
U :
'M[F]_n) (
Umod :
mxmodule rG U).
-
Lemma rfix_submod (
H :
{set gT}) :
-
H \subset G → (
rfix_mx rU H :=: in_submod U (
U :&: rfix_mx rG H))%
MS.
+
Lemma rfix_submod (
H :
{set gT}) :
+
H \subset G → (
rfix_mx rU H :=: in_submod U (
U :&: rfix_mx rG H))%
MS.
-
Lemma rfix_factmod (
H :
{set gT}) :
-
H \subset G → (
in_factmod U (
rfix_mx rG H)
≤ rfix_mx rU' H)%
MS.
+
Lemma rfix_factmod (
H :
{set gT}) :
+
H \subset G → (
in_factmod U (
rfix_mx rG H)
≤ rfix_mx rU' H)%
MS.
-
Lemma rstab_submod m (
W :
'M_(m, \rank U)) :
-
rstab rU W = rstab rG (
val_submod W).
+
Lemma rstab_submod m (
W :
'M_(m, \rank U)) :
+
rstab rU W = rstab rG (
val_submod W).
-
Lemma rstabs_submod m (
W :
'M_(m, \rank U)) :
-
rstabs rU W = rstabs rG (
val_submod W).
+
Lemma rstabs_submod m (
W :
'M_(m, \rank U)) :
+
rstabs rU W = rstabs rG (
val_submod W).
-
Lemma val_submod_module m (
W :
'M_(m, \rank U)) :
-
mxmodule rG (
val_submod W)
= mxmodule rU W.
+
Lemma val_submod_module m (
W :
'M_(m, \rank U)) :
+
mxmodule rG (
val_submod W)
= mxmodule rU W.
-
Lemma in_submod_module m (
V :
'M_(m, n)) :
- (
V ≤ U)%
MS → mxmodule rU (
in_submod U V)
= mxmodule rG V.
+
Lemma in_submod_module m (
V :
'M_(m, n)) :
+ (
V ≤ U)%
MS → mxmodule rU (
in_submod U V)
= mxmodule rG V.
-
Lemma rstab_factmod m (
W :
'M_(m, n)) :
-
rstab rG W \subset rstab rU' (
in_factmod U W).
+
Lemma rstab_factmod m (
W :
'M_(m, n)) :
+
rstab rG W \subset rstab rU' (
in_factmod U W).
-
Lemma rstabs_factmod m (
W :
'M_(m, \rank (cokermx U))) :
-
rstabs rU' W = rstabs rG (
U + val_factmod W)%
MS.
+
Lemma rstabs_factmod m (
W :
'M_(m, \rank (cokermx U))) :
+
rstabs rU' W = rstabs rG (
U + val_factmod W)%
MS.
-
Lemma val_factmod_module m (
W :
'M_(m, \rank (cokermx U))) :
-
mxmodule rG (
U + val_factmod W)%
MS = mxmodule rU' W.
+
Lemma val_factmod_module m (
W :
'M_(m, \rank (cokermx U))) :
+
mxmodule rG (
U + val_factmod W)%
MS = mxmodule rU' W.
-
Lemma in_factmod_module m (
V :
'M_(m, n)) :
-
mxmodule rU' (
in_factmod U V)
= mxmodule rG (
U + V)%
MS.
+
Lemma in_factmod_module m (
V :
'M_(m, n)) :
+
mxmodule rU' (
in_factmod U V)
= mxmodule rG (
U + V)%
MS.
-
Lemma rker_submod :
rker rU = rstab rG U.
+
Lemma rker_submod :
rker rU = rstab rG U.
-
Lemma rstab_norm :
G \subset 'N(rstab rG U).
+
Lemma rstab_norm :
G \subset 'N(rstab rG U).
-
Lemma rstab_normal :
rstab rG U <| G.
+
Lemma rstab_normal :
rstab rG U <| G.
-
Lemma submod_mx_faithful :
mx_faithful rU → mx_faithful rG.
+
Lemma submod_mx_faithful :
mx_faithful rU → mx_faithful rG.
-
Lemma rker_factmod :
rker rG \subset rker rU'.
+
Lemma rker_factmod :
rker rG \subset rker rU'.
-
Lemma factmod_mx_faithful :
mx_faithful rU' → mx_faithful rG.
+
Lemma factmod_mx_faithful :
mx_faithful rU' → mx_faithful rG.
-
Lemma submod_mx_irr :
mx_irreducible rU ↔ mxsimple rG U.
+
Lemma submod_mx_irr :
mx_irreducible rU ↔ mxsimple rG U.
End Submodule.
@@ -2154,26 +2171,26 @@
Section Conjugate.
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
-
Variables (
rG :
mx_representation F G n) (
B :
'M[F]_n).
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
+
Variables (
rG :
mx_representation F G n) (
B :
'M[F]_n).
-
Hypothesis uB :
B \in unitmx.
+
Hypothesis uB :
B \in unitmx.
-
Lemma rfix_conj (
H :
{set gT}) :
- (
rfix_mx rGB H :=: B ×m rfix_mx rG H ×m invmx B)%
MS.
+
Lemma rfix_conj (
H :
{set gT}) :
+ (
rfix_mx rGB H :=: B ×m rfix_mx rG H ×m invmx B)%
MS.
-
Lemma rstabs_conj m (
U :
'M_(m, n)) :
rstabs rGB U = rstabs rG (
U ×m B).
+
Lemma rstabs_conj m (
U :
'M_(m, n)) :
rstabs rGB U = rstabs rG (
U ×m B).
-
Lemma mxmodule_conj m (
U :
'M_(m, n)) :
mxmodule rGB U = mxmodule rG (
U ×m B).
+
Lemma mxmodule_conj m (
U :
'M_(m, n)) :
mxmodule rGB U = mxmodule rG (
U ×m B).
-
Lemma conj_mx_irr :
mx_irreducible rGB ↔ mx_irreducible rG.
+
Lemma conj_mx_irr :
mx_irreducible rGB ↔ mx_irreducible rG.
End Conjugate.
@@ -2182,28 +2199,28 @@
Section Quotient.
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
-
Variables (
rG :
mx_representation F G n) (
H :
{group gT}).
-
Hypotheses (
krH :
H \subset rker rG) (
nHG :
G \subset 'N(H)).
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
+
Variables (
rG :
mx_representation F G n) (
H :
{group gT}).
+
Hypotheses (
krH :
H \subset rker rG) (
nHG :
G \subset 'N(H)).
Let nHGs :=
subsetP nHG.
-
Lemma quo_mx_quotient : (
E_ rGH :=: E_ rG)%
MS.
+
Lemma quo_mx_quotient : (
E_ rGH :=: E_ rG)%
MS.
-
Lemma rfix_quo (
K :
{group gT}) :
-
K \subset G → (
rfix_mx rGH (
K / H)%
g :=: rfix_mx rG K)%
MS.
+
Lemma rfix_quo (
K :
{group gT}) :
+
K \subset G → (
rfix_mx rGH (
K / H)%
g :=: rfix_mx rG K)%
MS.
-
Lemma rstabs_quo m (
U :
'M_(m, n)) :
rstabs rGH U = (
rstabs rG U / H)%
g.
+
Lemma rstabs_quo m (
U :
'M_(m, n)) :
rstabs rGH U = (
rstabs rG U / H)%
g.
-
Lemma mxmodule_quo m (
U :
'M_(m, n)) :
mxmodule rGH U = mxmodule rG U.
+
Lemma mxmodule_quo m (
U :
'M_(m, n)) :
mxmodule rGH U = mxmodule rG U.
-
Lemma quo_mx_irr :
mx_irreducible rGH ↔ mx_irreducible rG.
+
Lemma quo_mx_irr :
mx_irreducible rGH ↔ mx_irreducible rG.
End Quotient.
@@ -2215,21 +2232,21 @@
Implicit Type gT :
finGroupType.
-
Definition group_splitting_field gT (
G :
{group gT}) :=
+
Definition group_splitting_field gT (
G :
{group gT}) :=
∀ n (
rG :
mx_representation F G n),
-
mx_irreducible rG → mx_absolutely_irreducible rG.
+
mx_irreducible rG → mx_absolutely_irreducible rG.
Definition group_closure_field gT :=
-
∀ G :
{group gT},
group_splitting_field G.
+
∀ G :
{group gT},
group_splitting_field G.
-
Lemma quotient_splitting_field gT (
G :
{group gT}) (
H :
{set gT}) :
-
G \subset 'N(H) → group_splitting_field G → group_splitting_field (
G / H).
+
Lemma quotient_splitting_field gT (
G :
{group gT}) (
H :
{set gT}) :
+
G \subset 'N(H) → group_splitting_field G → group_splitting_field (
G / H).
-
Lemma coset_splitting_field gT (
H :
{set gT}) :
-
group_closure_field gT → group_closure_field (
coset_groupType H).
+
Lemma coset_splitting_field gT (
H :
{set gT}) :
+
group_closure_field gT → group_closure_field (
coset_groupType H).
End SplittingField.
@@ -2238,30 +2255,30 @@
Section Abelian.
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
Lemma mx_faithful_irr_center_cyclic n (
rG :
mx_representation F G n) :
-
mx_faithful rG → mx_irreducible rG → cyclic 'Z(G).
+
mx_faithful rG → mx_irreducible rG → cyclic 'Z(G).
Lemma mx_faithful_irr_abelian_cyclic n (
rG :
mx_representation F G n) :
-
mx_faithful rG → mx_irreducible rG → abelian G → cyclic G.
+
mx_faithful rG → mx_irreducible rG → abelian G → cyclic G.
Hypothesis splitG :
group_splitting_field G.
Lemma mx_irr_abelian_linear n (
rG :
mx_representation F G n) :
-
mx_irreducible rG → abelian G → n = 1%
N.
+
mx_irreducible rG → abelian G → n = 1%
N.
Lemma mxsimple_abelian_linear n (
rG :
mx_representation F G n)
M :
-
abelian G → mxsimple rG M → \rank M = 1%
N.
+
abelian G → mxsimple rG M → \rank M = 1%
N.
-
Lemma linear_mxsimple n (
rG :
mx_representation F G n) (
M :
'M_n) :
-
mxmodule rG M → \rank M = 1%
N → mxsimple rG M.
+
Lemma linear_mxsimple n (
rG :
mx_representation F G n) (
M :
'M_n) :
+
mxmodule rG M → \rank M = 1%
N → mxsimple rG M.
End Abelian.
@@ -2270,16 +2287,16 @@
Section AbelianQuotient.
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
-
Variables (
n :
nat) (
rG :
mx_representation F G n).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
n :
nat) (
rG :
mx_representation F G n).
-
Lemma center_kquo_cyclic :
mx_irreducible rG → cyclic 'Z(G / rker rG)%
g.
+
Lemma center_kquo_cyclic :
mx_irreducible rG → cyclic 'Z(G / rker rG)%
g.
Lemma der1_sub_rker :
-
group_splitting_field G → mx_irreducible rG →
- (
G^`(1
) \subset rker rG)%
g = (
n == 1)%
N.
+
group_splitting_field G → mx_irreducible rG →
+ (
G^`(1
) \subset rker rG)%
g = (
n == 1)%
N.
End AbelianQuotient.
@@ -2288,70 +2305,70 @@
Section Similarity.
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
-
CoInductive mx_rsim n1 (
rG1 :
reprG n1)
n2 (
rG2 :
reprG n2) :
Prop :=
-
MxReprSim B of n1 = n2 &
row_free B
- &
∀ x,
x \in G → rG1 x ×m B = B ×m rG2 x.
+
Variant mx_rsim n1 (
rG1 :
reprG n1)
n2 (
rG2 :
reprG n2) :
Prop :=
+
MxReprSim B of n1 = n2 &
row_free B
+ &
∀ x,
x \in G → rG1 x ×m B = B ×m rG2 x.
Lemma mxrank_rsim n1 n2 (
rG1 :
reprG n1) (
rG2 :
reprG n2) :
-
mx_rsim rG1 rG2 → n1 = n2.
+
mx_rsim rG1 rG2 → n1 = n2.
Lemma mx_rsim_refl n (
rG :
reprG n) :
mx_rsim rG rG.
Lemma mx_rsim_sym n1 n2 (
rG1 :
reprG n1) (
rG2 :
reprG n2) :
-
mx_rsim rG1 rG2 → mx_rsim rG2 rG1.
+
mx_rsim rG1 rG2 → mx_rsim rG2 rG1.
Lemma mx_rsim_trans n1 n2 n3
(
rG1 :
reprG n1) (
rG2 :
reprG n2) (
rG3 :
reprG n3) :
-
mx_rsim rG1 rG2 → mx_rsim rG2 rG3 → mx_rsim rG1 rG3.
+
mx_rsim rG1 rG2 → mx_rsim rG2 rG3 → mx_rsim rG1 rG3.
Lemma mx_rsim_def n1 n2 (
rG1 :
reprG n1) (
rG2 :
reprG n2) :
-
mx_rsim rG1 rG2 →
-
∃ B, exists2 B', B' ×m B = 1
%:M &
-
∀ x,
x \in G → rG1 x = B ×m rG2 x ×m B'.
+
mx_rsim rG1 rG2 →
+
∃ B, exists2 B', B' ×m B = 1
%:M &
+
∀ x,
x \in G → rG1 x = B ×m rG2 x ×m B'.
-
Lemma mx_rsim_iso n (
rG :
reprG n) (
U V :
'M_n)
+
Lemma mx_rsim_iso n (
rG :
reprG n) (
U V :
'M_n)
(
modU :
mxmodule rG U) (
modV :
mxmodule rG V) :
-
mx_rsim (
submod_repr modU) (
submod_repr modV)
↔ mx_iso rG U V.
+
mx_rsim (
submod_repr modU) (
submod_repr modV)
↔ mx_iso rG U V.
Lemma mx_rsim_irr n1 n2 (
rG1 :
reprG n1) (
rG2 :
reprG n2) :
-
mx_rsim rG1 rG2 → mx_irreducible rG1 → mx_irreducible rG2.
+
mx_rsim rG1 rG2 → mx_irreducible rG1 → mx_irreducible rG2.
Lemma mx_rsim_abs_irr n1 n2 (
rG1 :
reprG n1) (
rG2 :
reprG n2) :
-
mx_rsim rG1 rG2 →
-
mx_absolutely_irreducible rG1 = mx_absolutely_irreducible rG2.
+
mx_rsim rG1 rG2 →
+
mx_absolutely_irreducible rG1 = mx_absolutely_irreducible rG2.
Lemma rker_mx_rsim n1 n2 (
rG1 :
reprG n1) (
rG2 :
reprG n2) :
-
mx_rsim rG1 rG2 → rker rG1 = rker rG2.
+
mx_rsim rG1 rG2 → rker rG1 = rker rG2.
Lemma mx_rsim_faithful n1 n2 (
rG1 :
reprG n1) (
rG2 :
reprG n2) :
-
mx_rsim rG1 rG2 → mx_faithful rG1 = mx_faithful rG2.
+
mx_rsim rG1 rG2 → mx_faithful rG1 = mx_faithful rG2.
Lemma mx_rsim_factmod n (
rG :
reprG n)
U V
(
modU :
mxmodule rG U) (
modV :
mxmodule rG V) :
- (
U + V :=: 1
%:M)%
MS → mxdirect (
U + V)
→
+ (
U + V :=: 1
%:M)%
MS → mxdirect (
U + V)
→
mx_rsim (
factmod_repr modV) (
submod_repr modU).
Lemma mxtrace_rsim n1 n2 (
rG1 :
reprG n1) (
rG2 :
reprG n2) :
-
mx_rsim rG1 rG2 → {in G, ∀ x,
\tr (rG1 x) = \tr (rG2 x)}.
+
mx_rsim rG1 rG2 → {in G, ∀ x,
\tr (rG1 x) = \tr (rG2 x)}.
Lemma mx_rsim_scalar n1 n2 (
rG1 :
reprG n1) (
rG2 :
reprG n2)
x c :
-
x \in G → mx_rsim rG1 rG2 → rG1 x = c%:M → rG2 x = c%:M.
+
x \in G → mx_rsim rG1 rG2 → rG1 x = c%:M → rG2 x = c%:M.
End Similarity.
@@ -2360,52 +2377,52 @@
Section Socle.
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
-
Variables (
n :
nat) (
rG :
mx_representation F G n) (
sG :
socleType rG).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
n :
nat) (
rG :
mx_representation F G n) (
sG :
socleType rG).
Lemma socle_irr (
W :
sG) :
mx_irreducible (
socle_repr W).
Lemma socle_rsimP (
W1 W2 :
sG) :
-
reflect (
mx_rsim (
socle_repr W1) (
socle_repr W2)) (
W1 == W2).
+
reflect (
mx_rsim (
socle_repr W1) (
socle_repr W2)) (
W1 == W2).
Lemma mx_rsim_in_submod U V (
modU :
mG U) (
modV :
mG V) :
-
let U' :=
<<in_submod V U>>%
MS in
- (
U ≤ V)%
MS →
-
∃ modU' :
mxmodule (
sr modV)
U', mx_rsim (
sr modU) (
sr modU').
+
let U' :=
<<in_submod V U>>%
MS in
+ (
U ≤ V)%
MS →
+
∃ modU' :
mxmodule (
sr modV)
U', mx_rsim (
sr modU) (
sr modU').
-
Lemma rsim_submod1 U (
modU :
mG U) : (
U :=: 1
%:M)%
MS → mx_rsim (
sr modU)
rG.
+
Lemma rsim_submod1 U (
modU :
mG U) : (
U :=: 1
%:M)%
MS → mx_rsim (
sr modU)
rG.
Lemma mxtrace_submod1 U (
modU :
mG U) :
- (
U :=: 1
%:M)%
MS → {in G, ∀ x,
\tr (sr modU x) = \tr (rG x)}.
+ (
U :=: 1
%:M)%
MS → {in G, ∀ x,
\tr (sr modU x) = \tr (rG x)}.
Lemma mxtrace_dadd_mod U V W (
modU :
mG U) (
modV :
mG V) (
modW :
mG W) :
- (
U + V :=: W)%
MS → mxdirect (
U + V)
→
-
{in G, ∀ x,
\tr (sr modU x) + \tr (sr modV x) = \tr (sr modW x)}.
+ (
U + V :=: W)%
MS → mxdirect (
U + V)
→
+
{in G, ∀ x,
\tr (sr modU x) + \tr (sr modV x) = \tr (sr modW x)}.
-
Lemma mxtrace_dsum_mod (
I :
finType) (
P :
pred I)
U W
+
Lemma mxtrace_dsum_mod (
I :
finType) (
P :
pred I)
U W
(
modU :
∀ i,
mG (
U i)) (
modW :
mG W) :
-
let S := (
\sum_(i | P i) U i)%
MS in (
S :=: W)%
MS → mxdirect S →
-
{in G, ∀ x,
\sum_(i | P i) \tr (sr (
modU i)
x) = \tr (sr modW x)}.
+
let S := (
\sum_(i | P i) U i)%
MS in (
S :=: W)%
MS → mxdirect S →
+
{in G, ∀ x,
\sum_(i | P i) \tr (sr (
modU i)
x) = \tr (sr modW x)}.
Lemma mxtrace_component U (
simU :
mxsimple rG U) :
let V :=
component_mx rG U in
let modV :=
component_mx_module rG U in let modU :=
mxsimple_module simU in
-
{in G, ∀ x,
\tr (sr modV x) = \tr (sr modU x) *+ (\rank V %/ \rank U)}.
+
{in G, ∀ x,
\tr (sr modV x) = \tr (sr modU x) *+ (\rank V %/ \rank U)}.
Lemma mxtrace_Socle :
let modS :=
Socle_module sG in
-
{in G, ∀ x,
-
\tr (sr modS x) = \sum_(W : sG) \tr (socle_repr W x) *+ socle_mult W}.
+
{in G, ∀ x,
+
\tr (sr modS x) = \sum_(W : sG) \tr (socle_repr W x) *+ socle_mult W}.
End Socle.
@@ -2414,39 +2431,39 @@
Section Clifford.
-
Variables (
gT :
finGroupType) (
G H :
{group gT}).
-
Hypothesis nsHG :
H <| G.
-
Variables (
n :
nat) (
rG :
mx_representation F G n).
+
Variables (
gT :
finGroupType) (
G H :
{group gT}).
+
Hypothesis nsHG :
H <| G.
+
Variables (
n :
nat) (
rG :
mx_representation F G n).
Let sHG :=
normal_sub nsHG.
Let nHG :=
normal_norm nsHG.
Let rH :=
subg_repr rG sHG.
-
Lemma Clifford_simple M x :
mxsimple rH M → x \in G → mxsimple rH (
M ×m rG x).
+
Lemma Clifford_simple M x :
mxsimple rH M → x \in G → mxsimple rH (
M ×m rG x).
-
Lemma Clifford_hom x m (
U :
'M_(m, n)) :
-
x \in 'C_G(H) → (
U ≤ dom_hom_mx rH (
rG x))%
MS.
+
Lemma Clifford_hom x m (
U :
'M_(m, n)) :
+
x \in 'C_G(H) → (
U ≤ dom_hom_mx rH (
rG x))%
MS.
-
Lemma Clifford_iso x U :
x \in 'C_G(H) → mx_iso rH U (
U ×m rG x).
+
Lemma Clifford_iso x U :
x \in 'C_G(H) → mx_iso rH U (
U ×m rG x).
Lemma Clifford_iso2 x U V :
-
mx_iso rH U V → x \in G → mx_iso rH (
U ×m rG x) (
V ×m rG x).
+
mx_iso rH U V → x \in G → mx_iso rH (
U ×m rG x) (
V ×m rG x).
Lemma Clifford_componentJ M x :
-
mxsimple rH M → x \in G →
- (
component_mx rH (
M ×m rG x)
:=: component_mx rH M ×m rG x)%
MS.
+
mxsimple rH M → x \in G →
+ (
component_mx rH (
M ×m rG x)
:=: component_mx rH M ×m rG x)%
MS.
Hypothesis irrG :
mx_irreducible rG.
-
Lemma Clifford_basis M :
mxsimple rH M →
-
{X : {set gT} | X \subset G &
-
let S :=
\sum_(x in X) M ×m rG x in S :=: 1
%:M ∧ mxdirect S}%
MS.
+
Lemma Clifford_basis M :
mxsimple rH M →
+
{X : {set gT} | X \subset G &
+
let S :=
\sum_(x in X) M ×m rG x in S :=: 1
%:M ∧ mxdirect S}%
MS.
Variable sH :
socleType rH.
@@ -2457,7 +2474,7 @@
PackSocle (
component_socle sH (
Clifford_simple (
socle_simple W)
Gx)).
-
Let valWact W x : (
Clifford_act W x :=: W ×m rG (
sgval (
subg G x)))%
MS.
+
Let valWact W x : (
Clifford_act W x :=: W ×m rG (
sgval (
subg G x)))%
MS.
Fact Clifford_is_action :
is_action G Clifford_act.
@@ -2468,28 +2485,28 @@
-
Lemma val_Clifford_act W x :
x \in G → (
'Cl%
act W x :=: W ×m rG x)%
MS.
+
Lemma val_Clifford_act W x :
x \in G → (
'Cl%
act W x :=: W ×m rG x)%
MS.
-
Lemma Clifford_atrans :
[transitive G, on [set: sH] | 'Cl].
+
Lemma Clifford_atrans :
[transitive G, on [set: sH] | 'Cl].
-
Lemma Clifford_Socle1 :
Socle sH = 1
%:M.
+
Lemma Clifford_Socle1 :
Socle sH = 1
%:M.
-
Lemma Clifford_rank_components (
W :
sH) : (
#|sH| × \rank W)%
N = n.
+
Lemma Clifford_rank_components (
W :
sH) : (
#|sH| × \rank W)%
N = n.
-
Theorem Clifford_component_basis M :
mxsimple rH M →
-
{t : nat & {x_ : sH → 'I_t → gT |
-
∀ W,
let sW := (
\sum_j M ×m rG (
x_ W j))%
MS in
-
[/\ ∀ j,
x_ W j \in G, (
sW :=: W)%
MS & mxdirect sW]}}.
+
Theorem Clifford_component_basis M :
mxsimple rH M →
+
{t : nat & {x_ : sH → 'I_t → gT |
+
∀ W,
let sW := (
\sum_j M ×m rG (
x_ W j))%
MS in
+
[/\ ∀ j,
x_ W j \in G, (
sW :=: W)%
MS & mxdirect sW]}}.
-
Lemma Clifford_astab :
H <*> 'C_G(H) \subset 'C([set: sH] | 'Cl).
+
Lemma Clifford_astab :
H <*> 'C_G(H) \subset 'C([set: sH] | 'Cl).
-
Lemma Clifford_astab1 (
W :
sH) :
'C[W | 'Cl] = rstabs rG W.
+
Lemma Clifford_astab1 (
W :
sH) :
'C[W | 'Cl] = rstabs rG W.
Lemma Clifford_rstabs_simple (
W :
sH) :
@@ -2502,12 +2519,12 @@
Section JordanHolder.
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
-
Variables (
n :
nat) (
rG :
mx_representation F G n).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
n :
nat) (
rG :
mx_representation F G n).
-
Lemma section_module (
U V :
'M_n) (
modU :
modG U) (
modV :
modG V) :
-
mxmodule (
factmod_repr modU)
<<in_factmod U V>>%
MS.
+
Lemma section_module (
U V :
'M_n) (
modU :
modG U) (
modV :
modG V) :
+
mxmodule (
factmod_repr modU)
<<in_factmod U V>>%
MS.
Definition section_repr U V (
modU :
modG U) (
modV :
modG V) :=
@@ -2518,29 +2535,29 @@
mx_rsim (@
section_repr U _ modU (
mxmodule1 rG)) (
factmod_repr modU).
-
Definition max_submod (
U V :
'M_n) :=
- (
U < V)%
MS ∧ (
∀ W,
¬ [/\ modG W, U < W & W < V])%
MS.
+
Definition max_submod (
U V :
'M_n) :=
+ (
U < V)%
MS ∧ (
∀ W,
¬ [/\ modG W, U < W & W < V])%
MS.
Lemma max_submodP U V (
modU :
modG U) (
modV :
modG V) :
- (
U ≤ V)%
MS → (max_submod U V ↔ mx_irreducible (
section_repr modU modV)
).
+ (
U ≤ V)%
MS → (max_submod U V ↔ mx_irreducible (
section_repr modU modV)
).
Lemma max_submod_eqmx U1 U2 V1 V2 :
- (
U1 :=: U2)%
MS → (
V1 :=: V2)%
MS → max_submod U1 V1 → max_submod U2 V2.
+ (
U1 :=: U2)%
MS → (
V1 :=: V2)%
MS → max_submod U1 V1 → max_submod U2 V2.
Definition mx_subseries :=
all modG.
Definition mx_composition_series V :=
-
mx_subseries V ∧ (∀ i,
i < size V → max_submod (0
:: V)`_i V`_i).
+
mx_subseries V ∧ (∀ i,
i < size V → max_submod (0
:: V)`_i V`_i).
-
Fact mx_subseries_module V i :
mx_subseries V → mxmodule rG V`_i.
+
Fact mx_subseries_module V i :
mx_subseries V → mxmodule rG V`_i.
-
Fact mx_subseries_module' V i :
mx_subseries V → mxmodule rG (0
:: V)`_i.
+
Fact mx_subseries_module' V i :
mx_subseries V → mxmodule rG (0
:: V)`_i.
Definition subseries_repr V i (
modV :
all modG V) :=
@@ -2548,27 +2565,27 @@
Definition series_repr V i (
compV :
mx_composition_series V) :=
-
subseries_repr i (
proj1 compV).
+
subseries_repr i (
proj1 compV).
-
Lemma mx_series_lt V :
mx_composition_series V → path ltmx 0
V.
+
Lemma mx_series_lt V :
mx_composition_series V → path ltmx 0
V.
-
Lemma max_size_mx_series (
V :
seq 'M[F]_n) :
-
path ltmx 0
V → size V ≤ \rank (last 0
V).
+
Lemma max_size_mx_series (
V :
seq 'M[F]_n) :
+
path ltmx 0
V → size V ≤ \rank (last 0
V).
Lemma mx_series_repr_irr V i (
compV :
mx_composition_series V) :
-
i < size V → mx_irreducible (
series_repr i compV).
+
i < size V → mx_irreducible (
series_repr i compV).
Lemma mx_series_rcons U V :
-
mx_series (
rcons U V)
↔ [/\ mx_series U, modG V & max_submod (
last 0
U)
V].
+
mx_series (
rcons U V)
↔ [/\ mx_series U, modG V & max_submod (
last 0
U)
V].
Theorem mx_Schreier U :
-
mx_subseries U → path ltmx 0
U →
-
classically (
∃ V, [/\ mx_series V, last 0
V :=: 1
%:M & subseq U V])%
MS.
+
mx_subseries U → path ltmx 0
U →
+
classically (
∃ V, [/\ mx_series V, last 0
V :=: 1
%:M & subseq U V])%
MS.
Lemma mx_second_rsim U V (
modU :
modG U) (
modV :
modG V) :
@@ -2577,28 +2594,28 @@
Lemma section_eqmx_add U1 U2 V1 V2 modU1 modU2 modV1 modV2 :
- (
U1 :=: U2)%
MS → (
U1 + V1 :=: U2 + V2)%
MS →
+ (
U1 :=: U2)%
MS → (
U1 + V1 :=: U2 + V2)%
MS →
mx_rsim (@
section_repr U1 V1 modU1 modV1) (@
section_repr U2 V2 modU2 modV2).
Lemma section_eqmx U1 U2 V1 V2 modU1 modU2 modV1 modV2
- (
eqU : (
U1 :=: U2)%
MS) (
eqV : (
V1 :=: V2)%
MS) :
+ (
eqU : (
U1 :=: U2)%
MS) (
eqV : (
V1 :=: V2)%
MS) :
mx_rsim (@
section_repr U1 V1 modU1 modV1) (@
section_repr U2 V2 modU2 modV2).
Lemma mx_butterfly U V W modU modV modW :
-
~~ (
U == V)%
MS → max_submod U W → max_submod V W →
+
~~ (
U == V)%
MS → max_submod U W → max_submod V W →
let modUV :=
capmx_module modU modV in
-
max_submod (
U :&: V)%
MS U
-
∧ mx_rsim (@
section_repr V W modV modW) (@
section_repr _ U modUV modU).
+
max_submod (
U :&: V)%
MS U
+
∧ mx_rsim (@
section_repr V W modV modW) (@
section_repr _ U modUV modU).
Lemma mx_JordanHolder_exists U V :
-
mx_composition_series U → modG V → max_submod V (
last 0
U)
→
-
{W : seq 'M_n | mx_composition_series W & last 0
W = V}.
+
mx_composition_series U → modG V → max_submod V (
last 0
U)
→
+
{W : seq 'M_n | mx_composition_series W & last 0
W = V}.
-
Let rsim_rcons U V compU compUV i :
i < size U →
+
Let rsim_rcons U V compU compUV i :
i < size U →
mx_rsim (@
series_repr U i compU) (@
series_repr (
rcons U V)
i compUV).
@@ -2611,14 +2628,14 @@
Lemma mx_JordanHolder U V compU compV :
-
let m :=
size U in (
last 0
U :=: last 0
V)%
MS →
-
m = size V ∧ (∃ p :
'S_m, ∀ i :
'I_m,
-
mx_rsim (@
series_repr U i compU) (@
series_repr V (
p i)
compV)
).
+
let m :=
size U in (
last 0
U :=: last 0
V)%
MS →
+
m = size V ∧ (∃ p :
'S_m, ∀ i :
'I_m,
+
mx_rsim (@
series_repr U i compU) (@
series_repr V (
p i)
compV)
).
Lemma mx_JordanHolder_max U (
m :=
size U)
V compU modV :
- (
last 0
U :=: 1
%:M)%
MS → mx_irreducible (@
factmod_repr _ G n rG V modV)
→
-
∃ i :
'I_m, mx_rsim (
factmod_repr modV) (@
series_repr U i compU).
+ (
last 0
U :=: 1
%:M)%
MS → mx_irreducible (@
factmod_repr _ G n rG V modV)
→
+
∃ i :
'I_m, mx_rsim (
factmod_repr modV) (@
series_repr U i compU).
End JordanHolder.
@@ -2629,7 +2646,7 @@
Section Regular.
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
@@ -2637,74 +2654,74 @@
Lemma gring_free :
row_free R_G.
-
Lemma gring_op_id A : (
A \in R_G)%
MS → gring_op aG A = A.
+
Lemma gring_op_id A : (
A \in R_G)%
MS → gring_op aG A = A.
-
Lemma gring_rowK A : (
A \in R_G)%
MS → gring_mx aG (
gring_row A)
= A.
+
Lemma gring_rowK A : (
A \in R_G)%
MS → gring_mx aG (
gring_row A)
= A.
-
Lemma mem_gring_mx m a (
M :
'M_(m, nG)) :
- (
gring_mx aG a \in M ×m R_G)%
MS = (
a ≤ M)%
MS.
+
Lemma mem_gring_mx m a (
M :
'M_(m, nG)) :
+ (
gring_mx aG a \in M ×m R_G)%
MS = (
a ≤ M)%
MS.
-
Lemma mem_sub_gring m A (
M :
'M_(m, nG)) :
- (
A \in M ×m R_G)%
MS = (
A \in R_G)%
MS && (
gring_row A ≤ M)%
MS.
+
Lemma mem_sub_gring m A (
M :
'M_(m, nG)) :
+ (
A \in M ×m R_G)%
MS = (
A \in R_G)%
MS && (
gring_row A ≤ M)%
MS.
Section GringMx.
-
Variables (
n :
nat) (
rG :
mx_representation F G n).
+
Variables (
n :
nat) (
rG :
mx_representation F G n).
-
Lemma gring_mxP a : (
gring_mx rG a \in enveloping_algebra_mx rG)%
MS.
+
Lemma gring_mxP a : (
gring_mx rG a \in enveloping_algebra_mx rG)%
MS.
Lemma gring_opM A B :
- (
B \in R_G)%
MS → gring_op rG (
A ×m B)
= gring_op rG A ×m gring_op rG B.
+ (
B \in R_G)%
MS → gring_op rG (
A ×m B)
= gring_op rG A ×m gring_op rG B.
Hypothesis irrG :
mx_irreducible rG.
Lemma rsim_regular_factmod :
-
{U : 'M_nG & {modU : mxmodule aG U & mx_rsim rG (
factmod_repr modU)
}}.
+
{U : 'M_nG & {modU : mxmodule aG U & mx_rsim rG (
factmod_repr modU)
}}.
Lemma rsim_regular_series U (
compU :
mx_composition_series aG U) :
- (
last 0
U :=: 1
%:M)%
MS →
-
∃ i :
'I_(size U), mx_rsim rG (
series_repr i compU).
+ (
last 0
U :=: 1
%:M)%
MS →
+
∃ i :
'I_(size U), mx_rsim rG (
series_repr i compU).
-
Hypothesis F'G :
[char F]^'.-group G.
+
Hypothesis F'G :
[char F]^'.-group G.
Lemma rsim_regular_submod :
-
{U : 'M_nG & {modU : mxmodule aG U & mx_rsim rG (
submod_repr modU)
}}.
+
{U : 'M_nG & {modU : mxmodule aG U & mx_rsim rG (
submod_repr modU)
}}.
End GringMx.
-
Definition gset_mx (
A :
{set gT}) :=
\sum_(x in A) aG x.
+
Definition gset_mx (
A :
{set gT}) :=
\sum_(x in A) aG x.
-
Definition classg_base :=
\matrix_(k < tG) mxvec (
gset_mx (
enum_val k)).
+
Definition classg_base :=
\matrix_(k < tG) mxvec (
gset_mx (
enum_val k)).
-
Let groupCl :
{in G, ∀ x,
{subset x ^: G ≤ G}}.
+
Let groupCl :
{in G, ∀ x,
{subset x ^: G ≤ G}}.
Lemma classg_base_free :
row_free classg_base.
-
Lemma classg_base_center : (
classg_base :=: 'Z(R_G))%
MS.
+
Lemma classg_base_center : (
classg_base :=: 'Z(R_G))%
MS.
-
Lemma regular_module_ideal m (
M :
'M_(m, nG)) :
-
mxmodule aG M = right_mx_ideal R_G (
M ×m R_G).
+
Lemma regular_module_ideal m (
M :
'M_(m, nG)) :
+
mxmodule aG M = right_mx_ideal R_G (
M ×m R_G).
Definition irrType :=
socleType aG.
@@ -2714,95 +2731,95 @@
Variable sG :
irrType.
-
Definition irr_degree (
i :
sG) :=
\rank (socle_base i).
+
Definition irr_degree (
i :
sG) :=
\rank (socle_base i).
Local Open Scope group_ring_scope.
-
Lemma irr_degreeE i :
'n_i = \rank (socle_base i).
-
Lemma irr_degree_gt0 i :
'n_i > 0.
+
Lemma irr_degreeE i :
'n_i = \rank (socle_base i).
+
Lemma irr_degree_gt0 i :
'n_i > 0.
-
Definition irr_repr i :
mx_representation F G 'n_i :=
socle_repr i.
-
Lemma irr_reprE i x :
irr_repr i x = submod_mx (
socle_module i)
x.
+
Definition irr_repr i :
mx_representation F G 'n_i :=
socle_repr i.
+
Lemma irr_reprE i x :
irr_repr i x = submod_mx (
socle_module i)
x.
-
Lemma rfix_regular : (
rfix_mx aG G :=: gring_row (
gset_mx G))%
MS.
+
Lemma rfix_regular : (
rfix_mx aG G :=: gring_row (
gset_mx G))%
MS.
Lemma principal_comp_subproof :
mxsimple aG (
rfix_mx aG G).
-
Fact principal_comp_key :
unit.
+
Fact principal_comp_key :
unit.
Definition principal_comp_def :=
PackSocle (
component_socle sG principal_comp_subproof).
-
Definition principal_comp :=
locked_with principal_comp_key principal_comp_def.
+
Definition principal_comp :=
locked_with principal_comp_key principal_comp_def.
-
Lemma irr1_rfix : (1%
irr :=: rfix_mx aG G)%
MS.
+
Lemma irr1_rfix : (1%
irr :=: rfix_mx aG G)%
MS.
-
Lemma rank_irr1 :
\rank 1%
irr = 1%
N.
+
Lemma rank_irr1 :
\rank 1%
irr = 1%
N.
-
Lemma degree_irr1 :
'n_1 = 1%
N.
+
Lemma degree_irr1 :
'n_1 = 1%
N.
-
Definition Wedderburn_subring (
i :
sG) :=
<<i ×m R_G>>%
MS.
+
Definition Wedderburn_subring (
i :
sG) :=
<<i ×m R_G>>%
MS.
-
Let sums_R : (
\sum_i 'R_i :=: Socle sG ×m R_G)%
MS.
+
Let sums_R : (
\sum_i 'R_i :=: Socle sG ×m R_G)%
MS.
-
Lemma Wedderburn_ideal i :
mx_ideal R_G 'R_i.
+
Lemma Wedderburn_ideal i :
mx_ideal R_G 'R_i.
-
Lemma Wedderburn_direct :
mxdirect (
\sum_i 'R_i)%
MS.
+
Lemma Wedderburn_direct :
mxdirect (
\sum_i 'R_i)%
MS.
-
Lemma Wedderburn_disjoint i j :
i != j → (
'R_i :&: 'R_j)%
MS = 0.
+
Lemma Wedderburn_disjoint i j :
i != j → (
'R_i :&: 'R_j)%
MS = 0.
-
Lemma Wedderburn_annihilate i j :
i != j → (
'R_i × 'R_j)%
MS = 0.
+
Lemma Wedderburn_annihilate i j :
i != j → (
'R_i × 'R_j)%
MS = 0.
Lemma Wedderburn_mulmx0 i j A B :
-
i != j → (
A \in 'R_i)%
MS → (
B \in 'R_j)%
MS → A ×m B = 0.
+
i != j → (
A \in 'R_i)%
MS → (
B \in 'R_j)%
MS → A ×m B = 0.
-
Hypothesis F'G :
[char F]^'.-group G.
+
Hypothesis F'G :
[char F]^'.-group G.
-
Lemma irr_mx_sum : (
\sum_(i : sG) i = 1
%:M)%
MS.
+
Lemma irr_mx_sum : (
\sum_(i : sG) i = 1
%:M)%
MS.
-
Lemma Wedderburn_sum : (
\sum_i 'R_i :=: R_G)%
MS.
+
Lemma Wedderburn_sum : (
\sum_i 'R_i :=: R_G)%
MS.
Definition Wedderburn_id i :=
-
vec_mx (
mxvec 1
%:M ×m proj_mx 'R_i (
\sum_(j | j != i) 'R_j)%
MS).
+
vec_mx (
mxvec 1
%:M ×m proj_mx 'R_i (
\sum_(j | j != i) 'R_j)%
MS).
-
Lemma Wedderburn_sum_id :
\sum_i 'e_i = 1
%:M.
+
Lemma Wedderburn_sum_id :
\sum_i 'e_i = 1
%:M.
-
Lemma Wedderburn_id_mem i : (
'e_i \in 'R_i)%
MS.
+
Lemma Wedderburn_id_mem i : (
'e_i \in 'R_i)%
MS.
-
Lemma Wedderburn_is_id i :
mxring_id 'R_i 'e_i.
+
Lemma Wedderburn_is_id i :
mxring_id 'R_i 'e_i.
-
Lemma Wedderburn_closed i : (
'R_i × 'R_i = 'R_i)%
MS.
+
Lemma Wedderburn_closed i : (
'R_i × 'R_i = 'R_i)%
MS.
-
Lemma Wedderburn_is_ring i :
mxring 'R_i.
+
Lemma Wedderburn_is_ring i :
mxring 'R_i.
-
Lemma Wedderburn_min_ideal m i (
E :
'A_(m, nG)) :
-
E != 0
→ (
E ≤ 'R_i)%
MS → mx_ideal R_G E → (
E :=: 'R_i)%
MS.
+
Lemma Wedderburn_min_ideal m i (
E :
'A_(m, nG)) :
+
E != 0
→ (
E ≤ 'R_i)%
MS → mx_ideal R_G E → (
E :=: 'R_i)%
MS.
Section IrrComponent.
@@ -2817,15 +2834,15 @@
-
Variables (
n :
nat) (
rG :
mx_representation F G n).
+
Variables (
n :
nat) (
rG :
mx_representation F G n).
Let not_rsim_op0 (
iG j :
sG)
A :
-
mx_rsim rG (
socle_repr iG)
→ iG != j → (
A \in 'R_j)%
MS →
-
gring_op rG A = 0.
+
mx_rsim rG (
socle_repr iG)
→ iG != j → (
A \in 'R_j)%
MS →
+
gring_op rG A = 0.
-
Definition irr_comp :=
odflt 1%
irr [pick i | gring_op rG 'e_i != 0
].
+
Definition irr_comp :=
odflt 1%
irr [pick i | gring_op rG 'e_i != 0
].
Hypothesis irrG :
mx_irreducible rG.
@@ -2834,79 +2851,79 @@
Lemma rsim_irr_comp :
mx_rsim rG (
irr_repr iG).
-
Lemma irr_comp'_op0 j A :
j != iG → (
A \in 'R_j)%
MS → gring_op rG A = 0.
+
Lemma irr_comp'_op0 j A :
j != iG → (
A \in 'R_j)%
MS → gring_op rG A = 0.
-
Lemma irr_comp_envelop : (
'R_iG ×m lin_mx (
gring_op rG)
:=: E_G)%
MS.
+
Lemma irr_comp_envelop : (
'R_iG ×m lin_mx (
gring_op rG)
:=: E_G)%
MS.
-
Lemma ker_irr_comp_op : (
'R_iG :&: kermx (
lin_mx (
gring_op rG)))%
MS = 0.
+
Lemma ker_irr_comp_op : (
'R_iG :&: kermx (
lin_mx (
gring_op rG)))%
MS = 0.
Lemma regular_op_inj :
-
{in [pred A | (
A \in 'R_iG)%
MS] &, injective (
gring_op rG)
}.
+
{in [pred A | (
A \in 'R_iG)%
MS] &, injective (
gring_op rG)
}.
-
Lemma rank_irr_comp :
\rank 'R_iG = \rank E_G.
+
Lemma rank_irr_comp :
\rank 'R_iG = \rank E_G.
End IrrComponent.
Lemma irr_comp_rsim n1 n2 rG1 rG2 :
- @
mx_rsim _ G n1 rG1 n2 rG2 → irr_comp rG1 = irr_comp rG2.
+ @
mx_rsim _ G n1 rG1 n2 rG2 → irr_comp rG1 = irr_comp rG2.
-
Lemma irr_reprK i :
irr_comp (
irr_repr i)
= i.
+
Lemma irr_reprK i :
irr_comp (
irr_repr i)
= i.
Lemma irr_repr'_op0 i j A :
-
j != i → (
A \in 'R_j)%
MS → gring_op (
irr_repr i)
A = 0.
+
j != i → (
A \in 'R_j)%
MS → gring_op (
irr_repr i)
A = 0.
-
Lemma op_Wedderburn_id i :
gring_op (
irr_repr i)
'e_i = 1
%:M.
+
Lemma op_Wedderburn_id i :
gring_op (
irr_repr i)
'e_i = 1
%:M.
-
Lemma irr_comp_id (
M :
'M_nG) (
modM :
mxmodule aG M) (
iM :
sG) :
-
mxsimple aG M → (
M ≤ iM)%
MS → irr_comp (
submod_repr modM)
= iM.
+
Lemma irr_comp_id (
M :
'M_nG) (
modM :
mxmodule aG M) (
iM :
sG) :
+
mxsimple aG M → (
M ≤ iM)%
MS → irr_comp (
submod_repr modM)
= iM.
-
Lemma irr1_repr x :
x \in G → irr_repr 1
x = 1
%:M.
+
Lemma irr1_repr x :
x \in G → irr_repr 1
x = 1
%:M.
Hypothesis splitG :
group_splitting_field G.
-
Lemma rank_Wedderburn_subring i :
\rank 'R_i = (
'n_i ^ 2)%
N.
+
Lemma rank_Wedderburn_subring i :
\rank 'R_i = (
'n_i ^ 2)%
N.
-
Lemma sum_irr_degree : (
\sum_i 'n_i ^ 2
= nG)%
N.
+
Lemma sum_irr_degree : (
\sum_i 'n_i ^ 2
= nG)%
N.
-
Lemma irr_mx_mult i :
socle_mult i = 'n_i.
+
Lemma irr_mx_mult i :
socle_mult i = 'n_i.
Lemma mxtrace_regular :
-
{in G, ∀ x,
\tr (aG x) = \sum_i \tr (socle_repr i x) *+ 'n_i}.
+
{in G, ∀ x,
\tr (aG x) = \sum_i \tr (socle_repr i x) *+ 'n_i}.
-
Definition linear_irr :=
[set i | 'n_i == 1%
N].
+
Definition linear_irr :=
[set i | 'n_i == 1%
N].
-
Lemma irr_degree_abelian :
abelian G → ∀ i,
'n_i = 1%
N.
+
Lemma irr_degree_abelian :
abelian G → ∀ i,
'n_i = 1%
N.
-
Lemma linear_irr_comp i :
'n_i = 1%
N → (
i :=: socle_base i)%
MS.
+
Lemma linear_irr_comp i :
'n_i = 1%
N → (
i :=: socle_base i)%
MS.
-
Lemma Wedderburn_subring_center i : (
'Z('R_i) :=: mxvec 'e_i)%
MS.
+
Lemma Wedderburn_subring_center i : (
'Z('R_i) :=: mxvec 'e_i)%
MS.
Lemma Wedderburn_center :
- (
'Z(R_G) :=: \matrix_(i < #|sG|) mxvec 'e_(enum_val i))%
MS.
+ (
'Z(R_G) :=: \matrix_(i < #|sG|) mxvec 'e_(enum_val i))%
MS.
-
Lemma card_irr :
#|sG| = tG.
+
Lemma card_irr :
#|sG| = tG.
Section CenterMode.
@@ -2921,31 +2938,31 @@
Definition irr_mode x :=
irr_repr i x i0 i0.
-
Lemma irr_mode1 :
irr_mode 1
= 1.
+
Lemma irr_mode1 :
irr_mode 1
= 1.
-
Lemma irr_center_scalar :
{in 'Z(G), ∀ x,
irr_repr i x = (irr_mode x)%:M}.
+
Lemma irr_center_scalar :
{in 'Z(G), ∀ x,
irr_repr i x = (irr_mode x)%:M}.
-
Lemma irr_modeM :
{in 'Z(G) &, {morph irr_mode : x y / (
x × y)%
g >-> x × y}}.
+
Lemma irr_modeM :
{in 'Z(G) &, {morph irr_mode : x y / (
x × y)%
g >-> x × y}}.
-
Lemma irr_modeX n :
{in 'Z(G), {morph irr_mode : x / (
x ^+ n)%
g >-> x ^+ n}}.
+
Lemma irr_modeX n :
{in 'Z(G), {morph irr_mode : x / (
x ^+ n)%
g >-> x ^+ n}}.
-
Lemma irr_mode_unit :
{in 'Z(G), ∀ x,
irr_mode x \is a GRing.unit}.
+
Lemma irr_mode_unit :
{in 'Z(G), ∀ x,
irr_mode x \is a GRing.unit}.
-
Lemma irr_mode_neq0 :
{in 'Z(G), ∀ x,
irr_mode x != 0
}.
+
Lemma irr_mode_neq0 :
{in 'Z(G), ∀ x,
irr_mode x != 0
}.
-
Lemma irr_modeV :
{in 'Z(G), {morph irr_mode : x / (
x^-1)%
g >-> x^-1}}.
+
Lemma irr_modeV :
{in 'Z(G), {morph irr_mode : x / (
x^-1)%
g >-> x^-1}}.
End CenterMode.
-
Lemma irr1_mode x :
x \in G → irr_mode 1
x = 1.
+
Lemma irr1_mode x :
x \in G → irr_mode 1
x = 1.
End Regular.
@@ -2956,31 +2973,31 @@
Section LinearIrr.
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
Lemma card_linear_irr (
sG :
irrType G) :
-
[char F]^'.-group G → group_splitting_field G →
-
#|linear_irr sG| = #|G : G^`(1
)|%
g.
+
[char F]^'.-group G → group_splitting_field G →
+
#|linear_irr sG| = #|G : G^`(1
)|%
g.
Lemma primitive_root_splitting_abelian (
z :
F) :
-
#|G|.-primitive_root z → abelian G → group_splitting_field G.
+
#|G|.-primitive_root z → abelian G → group_splitting_field G.
Lemma cycle_repr_structure x (
sG :
irrType G) :
-
G :=: <[x]> → [char F]^'.-group G → group_splitting_field G →
-
exists2 w : F, #|G|.-primitive_root w &
-
∃ iphi :
'I_#|G| → sG,
-
[/\ bijective iphi,
-
#|sG| = #|G|,
-
∀ i,
irr_mode (
iphi i)
x = w ^+ i
-
& ∀ i,
irr_repr (
iphi i)
x = (w ^+ i)%:M].
+
G :=: <[x]> → [char F]^'.-group G → group_splitting_field G →
+
exists2 w : F, #|G|.-primitive_root w &
+
∃ iphi :
'I_#|G| → sG,
+
[/\ bijective iphi,
+
#|sG| = #|G|,
+
∀ i,
irr_mode (
iphi i)
x = w ^+ i
+
& ∀ i,
irr_repr (
iphi i)
x = (w ^+ i)%:M].
Lemma splitting_cyclic_primitive_root :
-
cyclic G → [char F]^'.-group G → group_splitting_field G →
-
classically {z : F | #|G|.-primitive_root z}.
+
cyclic G → [char F]^'.-group G → group_splitting_field G →
+
classically {z : F | #|G|.-primitive_root z}.
End LinearIrr.
@@ -2995,13 +3012,17 @@
-
Notation "'Cl" := (
Clifford_action _) :
action_scope.
-
Notation "[ 1 sG ]" := (
principal_comp sG) :
irrType_scope.
-
Notation "''n_' i" := (
irr_degree i) :
group_ring_scope.
-
Notation "''R_' i" := (
Wedderburn_subring i) :
group_ring_scope.
-
Notation "''e_' i" := (
Wedderburn_id i) :
group_ring_scope.
+
Notation "'Cl" := (
Clifford_action _) :
action_scope.
+
+
+
+
+
Notation "[ 1 sG ]" := (
principal_comp sG) :
irrType_scope.
+
Notation "''n_' i" := (
irr_degree i) :
group_ring_scope.
+
Notation "''R_' i" := (
Wedderburn_subring i) :
group_ring_scope.
+
Notation "''e_' i" := (
Wedderburn_id i) :
group_ring_scope.
Section DecideRed.
@@ -3013,49 +3034,49 @@
Section Definitions.
-
Variables (
F :
fieldType) (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
+
Variables (
F :
fieldType) (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
Variable rG :
mx_representation F G n.
-
Definition mxmodule_form (
U :
'M[term F]_n) :=
-
\big[And/True]_(x in G) submx_form (
mulmx_term U (
mx_term (
rG x)))
U.
+
Definition mxmodule_form (
U :
'M[term F]_n) :=
+
\big[And/True]_(x in G) submx_form (
mulmx_term U (
mx_term (
rG x)))
U.
Lemma mxmodule_form_qf U :
qf_form (
mxmodule_form U).
Lemma eval_mxmodule U e :
-
qf_eval e (
mxmodule_form U)
= mxmodule rG (
eval_mx e U).
+
qf_eval e (
mxmodule_form U)
= mxmodule rG (
eval_mx e U).
-
Definition mxnonsimple_form (
U :
'M[term F]_n) :=
-
let V :=
vec_mx (
row_var F (
n × n) 0)
in
-
let nzV := (
¬ mxrank_form 0
V)%
T in
-
let properVU := (
submx_form V U ∧ ¬ submx_form U V)%
T in
- (
Exists_row_form (
n × n) 0 (
mxmodule_form V ∧ nzV ∧ properVU))%
T.
+
Definition mxnonsimple_form (
U :
'M[term F]_n) :=
+
let V :=
vec_mx (
row_var F (
n × n) 0)
in
+
let nzV := (
¬ mxrank_form 0
V)%
T in
+
let properVU := (
submx_form V U ∧ ¬ submx_form U V)%
T in
+ (
Exists_row_form (
n × n) 0 (
mxmodule_form V ∧ nzV ∧ properVU))%
T.
End Definitions.
-
Variables (
F :
decFieldType) (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
+
Variables (
F :
decFieldType) (
gT :
finGroupType) (
G :
{group gT}) (
n :
nat).
Variable rG :
mx_representation F G n.
Definition mxnonsimple_sat U :=
-
GRing.sat (@
row_env _ (
n × n)
[::]) (
mxnonsimple_form rG (
mx_term U)).
+
GRing.sat (@
row_env _ (
n × n)
[::]) (
mxnonsimple_form rG (
mx_term U)).
Lemma mxnonsimpleP U :
-
U != 0
→ reflect (
mxnonsimple rG U) (
mxnonsimple_sat U).
+
U != 0
→ reflect (
mxnonsimple rG U) (
mxnonsimple_sat U).
-
Lemma dec_mxsimple_exists (
U :
'M_n) :
-
mxmodule rG U → U != 0
→ {V | mxsimple rG V & V ≤ U}%
MS.
+
Lemma dec_mxsimple_exists (
U :
'M_n) :
+
mxmodule rG U → U != 0
→ {V | mxsimple rG V & V ≤ U}%
MS.
Lemma dec_mx_reducible_semisimple U :
-
mxmodule rG U → mx_completely_reducible rG U → mxsemisimple rG U.
+
mxmodule rG U → mx_completely_reducible rG U → mxsemisimple rG U.
Lemma DecSocleType :
socleType rG.
@@ -3063,6 +3084,8 @@
End DecideRed.
+
+
@@ -3073,71 +3096,71 @@
Section ChangeOfField.
-
Variables (
aF rF :
fieldType) (
f :
{rmorphism aF → rF}).
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
aF rF :
fieldType) (
f :
{rmorphism aF → rF}).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
Section OneRepresentation.
-
Variables (
n :
nat) (
rG :
mx_representation aF G n).
+
Variables (
n :
nat) (
rG :
mx_representation aF G n).
-
Lemma map_rfix_mx H :
(rfix_mx rG H)^f = rfix_mx rGf H.
+
Lemma map_rfix_mx H :
(rfix_mx rG H)^f = rfix_mx rGf H.
-
Lemma rcent_map A :
rcent rGf A^f = rcent rG A.
+
Lemma rcent_map A :
rcent rGf A^f = rcent rG A.
-
Lemma rstab_map m (
U :
'M_(m, n)) :
rstab rGf U^f = rstab rG U.
+
Lemma rstab_map m (
U :
'M_(m, n)) :
rstab rGf U^f = rstab rG U.
-
Lemma rstabs_map m (
U :
'M_(m, n)) :
rstabs rGf U^f = rstabs rG U.
+
Lemma rstabs_map m (
U :
'M_(m, n)) :
rstabs rGf U^f = rstabs rG U.
-
Lemma centgmx_map A :
centgmx rGf A^f = centgmx rG A.
+
Lemma centgmx_map A :
centgmx rGf A^f = centgmx rG A.
-
Lemma mxmodule_map m (
U :
'M_(m, n)) :
mxmodule rGf U^f = mxmodule rG U.
+
Lemma mxmodule_map m (
U :
'M_(m, n)) :
mxmodule rGf U^f = mxmodule rG U.
-
Lemma mxsimple_map (
U :
'M_n) :
mxsimple rGf U^f → mxsimple rG U.
+
Lemma mxsimple_map (
U :
'M_n) :
mxsimple rGf U^f → mxsimple rG U.
-
Lemma mx_irr_map :
mx_irreducible rGf → mx_irreducible rG.
+
Lemma mx_irr_map :
mx_irreducible rGf → mx_irreducible rG.
-
Lemma rker_map :
rker rGf = rker rG.
+
Lemma rker_map :
rker rGf = rker rG.
-
Lemma map_mx_faithful :
mx_faithful rGf = mx_faithful rG.
+
Lemma map_mx_faithful :
mx_faithful rGf = mx_faithful rG.
Lemma map_mx_abs_irr :
-
mx_absolutely_irreducible rGf = mx_absolutely_irreducible rG.
+
mx_absolutely_irreducible rGf = mx_absolutely_irreducible rG.
End OneRepresentation.
Lemma mx_rsim_map n1 n2 rG1 rG2 :
- @
mx_rsim _ _ G n1 rG1 n2 rG2 → mx_rsim (
map_repr f rG1) (
map_repr f rG2).
+ @
mx_rsim _ _ G n1 rG1 n2 rG2 → mx_rsim (
map_repr f rG1) (
map_repr f rG2).
Lemma map_section_repr n (
rG :
mx_representation aF G n)
rGf U V
(
modU :
mxmodule rG U) (
modV :
mxmodule rG V)
- (
modUf :
mxmodule rGf U^f) (
modVf :
mxmodule rGf V^f) :
-
map_repr f rG =1 rGf →
+ (
modUf :
mxmodule rGf U^f) (
modVf :
mxmodule rGf V^f) :
+
map_repr f rG =1 rGf →
mx_rsim (
map_repr f (
section_repr modU modV)) (
section_repr modUf modVf).
Lemma map_regular_subseries U i (
modU :
mx_subseries (
regular_repr aF G)
U)
- (
modUf :
mx_subseries (
regular_repr rF G)
[seq M^f | M <- U]) :
+ (
modUf :
mx_subseries (
regular_repr rF G)
[seq M^f | M <- U]) :
mx_rsim (
map_repr f (
subseries_repr i modU)) (
subseries_repr i modUf).
Lemma extend_group_splitting_field :
-
group_splitting_field aF G → group_splitting_field rF G.
+
group_splitting_field aF G → group_splitting_field rF G.
End ChangeOfField.
@@ -3157,17 +3180,30 @@
Module Import MatrixGenField.
-
Section GenField.
+
+
+
+ The type definition must come before the main section so that the Bind
+ Scope directive applies to all lemmas and definition discharged at the
+ of the section.
+
+
+
Record gen_of {
F :
fieldType} {
gT :
finGroupType} {
G :
{group gT}} {
n' :
nat}
+ {
rG :
mx_representation F G n'.+1} {
A :
'M[F]_n'.+1}
+ (
irrG :
mx_irreducible rG) (
cGA :
centgmx rG A) :=
+
Gen {
rVval :
'rV[F]_(degree_mxminpoly A)}.
-
Variables (
F :
fieldType) (
gT :
finGroupType) (
G :
{group gT}) (
n' :
nat).
-
Variables (
rG :
mx_representation F G n) (
A :
'M[F]_n).
-
Let d_gt0 :=
mxminpoly_nonconstant A.
+
Section GenField.
-
Record gen_of (
irrG :
irr rG) (
cGA :
centgmx rG A) :=
Gen {
rVval :
'rV[F]_d}.
+
Variables (
F :
fieldType) (
gT :
finGroupType) (
G :
{group gT}) (
n' :
nat).
+
Variables (
rG :
mx_representation F G n) (
A :
'M[F]_n).
+
+
+
Let d_gt0 :=
mxminpoly_nonconstant A.
Hypotheses (
irrG :
irr rG) (
cGA :
centgmx rG A).
@@ -3177,28 +3213,28 @@
Let inFA :=
Gen irrG cGA.
-
Canonical gen_subType :=
Eval hnf in [newType for @
rVval irrG cGA].
-
Definition gen_eqMixin :=
Eval hnf in [eqMixin of FA by <:].
+
Canonical gen_subType :=
Eval hnf in [newType for rVval : FA → 'rV_d].
+
Definition gen_eqMixin :=
Eval hnf in [eqMixin of FA by <:].
Canonical gen_eqType :=
Eval hnf in EqType FA gen_eqMixin.
-
Definition gen_choiceMixin :=
[choiceMixin of FA by <:].
+
Definition gen_choiceMixin :=
[choiceMixin of FA by <:].
Canonical gen_choiceType :=
Eval hnf in ChoiceType FA gen_choiceMixin.
Definition gen0 :=
inFA 0.
-
Definition genN (
x :
FA) :=
inFA (
- val x).
-
Definition genD (
x y :
FA) :=
inFA (
val x + val y).
+
Definition genN (
x :
FA) :=
inFA (
- val x).
+
Definition genD (
x y :
FA) :=
inFA (
val x + val y).
-
Lemma gen_addA :
associative genD.
+
Lemma gen_addA :
associative genD.
-
Lemma gen_addC :
commutative genD.
+
Lemma gen_addC :
commutative genD.
-
Lemma gen_add0r :
left_id gen0 genD.
+
Lemma gen_add0r :
left_id gen0 genD.
-
Lemma gen_addNr :
left_inverse gen0 genN genD.
+
Lemma gen_addNr :
left_inverse gen0 genN genD.
Definition gen_zmodMixin :=
ZmodMixin gen_addA gen_addC gen_add0r gen_addNr.
@@ -3211,54 +3247,54 @@
Definition mxval (
x :
FA) :=
horner_mx A (
pval x).
-
Definition gen (
x :
F) :=
inFA (
poly_rV x%:P).
+
Definition gen (
x :
F) :=
inFA (
poly_rV x%:P).
-
Lemma genK x :
mxval (
gen x)
= x%:M.
+
Lemma genK x :
mxval (
gen x)
= x%:M.
-
Lemma mxval_inj :
injective mxval.
+
Lemma mxval_inj :
injective mxval.
-
Lemma mxval0 :
mxval 0
= 0.
+
Lemma mxval0 :
mxval 0
= 0.
-
Lemma mxvalN :
{morph mxval : x / - x}.
+
Lemma mxvalN :
{morph mxval : x / - x}.
-
Lemma mxvalD :
{morph mxval : x y / x + y}.
+
Lemma mxvalD :
{morph mxval : x y / x + y}.
Definition mxval_sum :=
big_morph mxval mxvalD mxval0.
Definition gen1 :=
inFA (
poly_rV 1).
-
Definition genM x y :=
inFA (
poly_rV (
pval x × pval y %% pA)).
-
Definition genV x :=
inFA (
poly_rV (
mx_inv_horner A (mxval x)^-1)).
+
Definition genM x y :=
inFA (
poly_rV (
pval x × pval y %% pA)).
+
Definition genV x :=
inFA (
poly_rV (
mx_inv_horner A (mxval x)^-1)).
-
Lemma mxval_gen1 :
mxval gen1 = 1
%:M.
+
Lemma mxval_gen1 :
mxval gen1 = 1
%:M.
-
Lemma mxval_genM :
{morph mxval : x y / genM x y >-> x ×m y}.
+
Lemma mxval_genM :
{morph mxval : x y / genM x y >-> x ×m y}.
-
Lemma mxval_genV :
{morph mxval : x / genV x >-> invmx x}.
+
Lemma mxval_genV :
{morph mxval : x / genV x >-> invmx x}.
-
Lemma gen_mulA :
associative genM.
+
Lemma gen_mulA :
associative genM.
-
Lemma gen_mulC :
commutative genM.
+
Lemma gen_mulC :
commutative genM.
-
Lemma gen_mul1r :
left_id gen1 genM.
+
Lemma gen_mul1r :
left_id gen1 genM.
-
Lemma gen_mulDr :
left_distributive genM +%R.
+
Lemma gen_mulDr :
left_distributive genM +%R.
-
Lemma gen_ntriv :
gen1 != 0.
+
Lemma gen_ntriv :
gen1 != 0.
Definition gen_ringMixin :=
@@ -3267,10 +3303,10 @@
Canonical gen_comRingType :=
Eval hnf in ComRingType FA gen_mulC.
-
Lemma mxval1 :
mxval 1
= 1
%:M.
+
Lemma mxval1 :
mxval 1
= 1
%:M.
-
Lemma mxvalM :
{morph mxval : x y / x × y >-> x ×m y}.
+
Lemma mxvalM :
{morph mxval : x y / x × y >-> x ×m y}.
Lemma mxval_sub :
additive mxval.
@@ -3287,20 +3323,21 @@
Lemma gen_mulVr :
GRing.Field.axiom genV.
-
Lemma gen_invr0 :
genV 0
= 0.
+
Lemma gen_invr0 :
genV 0
= 0.
Definition gen_unitRingMixin :=
FieldUnitMixin gen_mulVr gen_invr0.
-
Canonical gen_unitRingType :=
Eval hnf in UnitRingType FA gen_unitRingMixin.
-
Canonical gen_comUnitRingType :=
Eval hnf in [comUnitRingType of FA].
+
Canonical gen_unitRingType :=
+
Eval hnf in UnitRingType FA gen_unitRingMixin.
+
Canonical gen_comUnitRingType :=
Eval hnf in [comUnitRingType of FA].
Definition gen_fieldMixin :=
- @
FieldMixin _ _ _ _ : GRing.Field.mixin_of gen_unitRingType.
+ @
FieldMixin _ _ _ _ : GRing.Field.mixin_of gen_unitRingType.
Definition gen_idomainMixin :=
FieldIdomainMixin gen_fieldMixin.
Canonical gen_idomainType :=
Eval hnf in IdomainType FA gen_idomainMixin.
Canonical gen_fieldType :=
Eval hnf in FieldType FA gen_fieldMixin.
-
Lemma mxvalV :
{morph mxval : x / x^-1 >-> invmx x}.
+
Lemma mxvalV :
{morph mxval : x / x^-1 >-> invmx x}.
Lemma gen_is_rmorphism :
rmorphism gen.
@@ -3317,16 +3354,16 @@
@@ -3339,7 +3376,7 @@
Lemma non_linear_gen_reducible :
-
d > 1
→ mxnonsimple (
map_repr gen_rmorphism rG) 1
%:M.
+
d > 1
→ mxnonsimple (
map_repr gen_rmorphism rG) 1
%:M.
-
Definition subbase m (
B :
'rV_m) :
'M_(m × d, n) :=
-
\matrix_ik mxvec (
\matrix_(i, k) (row (
B 0
i) (
A ^+ k)
)) 0
ik.
+
Definition subbase nA (
B :
'rV_nA) :
'M_(nA × d, n) :=
+
\matrix_ik mxvec (
\matrix_(i, k) (row (
B 0
i) (
A ^+ k)
)) 0
ik.
-
Lemma gen_dim_ex_proof :
∃ m, [∃ B : 'rV_m, row_free (
subbase B)
].
+
Lemma gen_dim_ex_proof :
∃ nA, [∃ B : 'rV_nA, row_free (
subbase B)
].
-
Lemma gen_dim_ub_proof m :
-
[∃ B : 'rV_m, row_free (
subbase B)
] → (
m ≤ n)%
N.
+
Lemma gen_dim_ub_proof nA :
+
[∃ B : 'rV_nA, row_free (
subbase B)
] → (
nA ≤ n)%
N.
Definition gen_dim :=
ex_maxn gen_dim_ex_proof gen_dim_ub_proof.
-
Notation m :=
gen_dim.
+
Notation nA :=
gen_dim.
-
Definition gen_base :
'rV_m :=
odflt 0
[pick B | row_free (
subbase B)
].
+
Definition gen_base :
'rV_nA :=
odflt 0
[pick B | row_free (
subbase B)
].
Definition base :=
subbase gen_base.
@@ -3383,55 +3420,55 @@
Lemma base_full :
row_full base.
-
Lemma gen_dim_factor : (
m × d)%
N = n.
+
Lemma gen_dim_factor : (
nA × d)%
N = n.
-
Lemma gen_dim_gt0 :
m > 0.
+
Lemma gen_dim_gt0 :
nA > 0.
Section Bijection.
-
Variable m1 :
nat.
+
Variable m :
nat.
-
Definition in_gen (
W :
'M[F]_(m1, n)) :
'M[FA]_(m1, m) :=
-
\matrix_(i, j) inFA (
row j (
vec_mx (
row i W ×m pinvmx base))).
+
Definition in_gen (
W :
'M[F]_(m, n)) :
'M[FA]_(m, nA) :=
+
\matrix_(i, j) inFA (
row j (
vec_mx (
row i W ×m pinvmx base))).
-
Definition val_gen (
W :
'M[FA]_(m1, m)) :
'M[F]_(m1, n) :=
-
\matrix_i (mxvec (
\matrix_j val (
W i j))
×m base).
+
Definition val_gen (
W :
'M[FA]_(m, nA)) :
'M[F]_(m, n) :=
+
\matrix_i (mxvec (
\matrix_j val (
W i j))
×m base).
-
Lemma in_genK :
cancel in_gen val_gen.
+
Lemma in_genK :
cancel in_gen val_gen.
-
Lemma val_genK :
cancel val_gen in_gen.
+
Lemma val_genK :
cancel val_gen in_gen.
-
Lemma in_gen0 :
in_gen 0
= 0.
+
Lemma in_gen0 :
in_gen 0
= 0.
-
Lemma val_gen0 :
val_gen 0
= 0.
+
Lemma val_gen0 :
val_gen 0
= 0.
-
Lemma in_genN :
{morph in_gen : W / - W}.
+
Lemma in_genN :
{morph in_gen : W / - W}.
-
Lemma val_genN :
{morph val_gen : W / - W}.
+
Lemma val_genN :
{morph val_gen : W / - W}.
-
Lemma in_genD :
{morph in_gen : U V / U + V}.
+
Lemma in_genD :
{morph in_gen : U V / U + V}.
-
Lemma val_genD :
{morph val_gen : U V / U + V}.
+
Lemma val_genD :
{morph val_gen : U V / U + V}.
Definition in_gen_sum :=
big_morph in_gen in_genD in_gen0.
Definition val_gen_sum :=
big_morph val_gen val_genD val_gen0.
-
Lemma in_genZ a :
{morph in_gen : W / a *: W >-> gen a *: W}.
+
Lemma in_genZ a :
{morph in_gen : W / a *: W >-> gen a *: W}.
End Bijection.
@@ -3439,45 +3476,45 @@
-
Lemma val_gen_rV (
w :
'rV_m) :
-
val_gen w = mxvec (
\matrix_j val (
w 0
j))
×m base.
+
Lemma val_gen_rV (
w :
'rV_nA) :
+
val_gen w = mxvec (
\matrix_j val (
w 0
j))
×m base.
Section Bijection2.
-
Variable m1 :
nat.
+
Variable m :
nat.
-
Lemma val_gen_row W (
i :
'I_m1) :
val_gen (
row i W)
= row i (
val_gen W).
+
Lemma val_gen_row W (
i :
'I_m) :
val_gen (
row i W)
= row i (
val_gen W).
-
Lemma in_gen_row W (
i :
'I_m1) :
in_gen (
row i W)
= row i (
in_gen W).
+
Lemma in_gen_row W (
i :
'I_m) :
in_gen (
row i W)
= row i (
in_gen W).
-
Lemma row_gen_sum_mxval W (
i :
'I_m1) :
-
row i (
val_gen W)
= \sum_j row (
gen_base 0
j) (
mxval (
W i j)).
+
Lemma row_gen_sum_mxval W (
i :
'I_m) :
+
row i (
val_gen W)
= \sum_j row (
gen_base 0
j) (
mxval (
W i j)).
-
Lemma val_genZ x :
{morph @
val_gen m1 : W / x *: W >-> W ×m mxval x}.
+
Lemma val_genZ x :
{morph @
val_gen m : W / x *: W >-> W ×m mxval x}.
End Bijection2.
-
Lemma submx_in_gen m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
- (
U ≤ V → in_gen U ≤ in_gen V)%
MS.
+
Lemma submx_in_gen m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
+ (
U ≤ V → in_gen U ≤ in_gen V)%
MS.
-
Lemma submx_in_gen_eq m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
- (
V ×m A ≤ V → (in_gen U ≤ in_gen V) = (U ≤ V))%
MS.
+
Lemma submx_in_gen_eq m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, n)) :
+ (
V ×m A ≤ V → (in_gen U ≤ in_gen V) = (U ≤ V))%
MS.
-
Definition gen_mx g :=
\matrix_i in_gen (
row (
gen_base 0
i) (
rG g)).
+
Definition gen_mx g :=
\matrix_i in_gen (
row (
gen_base 0
i) (
rG g)).
Let val_genJmx m :
-
{in G, ∀ g,
{morph @
val_gen m : W / W ×m gen_mx g >-> W ×m rG g}}.
+
{in G, ∀ g,
{morph @
val_gen m : W / W ×m gen_mx g >-> W ×m rG g}}.
Lemma gen_mx_repr :
mx_repr G gen_mx.
@@ -3485,55 +3522,55 @@
Lemma val_genJ m :
-
{in G, ∀ g,
{morph @
val_gen m : W / W ×m rGA g >-> W ×m rG g}}.
+
{in G, ∀ g,
{morph @
val_gen m : W / W ×m rGA g >-> W ×m rG g}}.
Lemma in_genJ m :
-
{in G, ∀ g,
{morph @
in_gen m : v / v ×m rG g >-> v ×m rGA g}}.
+
{in G, ∀ g,
{morph @
in_gen m : v / v ×m rG g >-> v ×m rGA g}}.
-
Lemma rfix_gen (
H :
{set gT}) :
-
H \subset G → (
rfix_mx rGA H :=: in_gen (
rfix_mx rG H))%
MS.
+
Lemma rfix_gen (
H :
{set gT}) :
+
H \subset G → (
rfix_mx rGA H :=: in_gen (
rfix_mx rG H))%
MS.
-
Definition rowval_gen m1 U :=
-
<<\matrix_ik
-
mxvec (
\matrix_(i < m1, k < d) (row i (
val_gen U)
×m A ^+ k)) 0
ik>>%
MS.
+
Definition rowval_gen m U :=
+
<<\matrix_ik
+
mxvec (
\matrix_(i < m, k < d) (row i (
val_gen U)
×m A ^+ k)) 0
ik>>%
MS.
-
Lemma submx_rowval_gen m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, m)) :
- (
U ≤ rowval_gen V)%
MS = (
in_gen U ≤ V)%
MS.
+
Lemma submx_rowval_gen m1 m2 (
U :
'M_(m1, n)) (
V :
'M_(m2, nA)) :
+ (
U ≤ rowval_gen V)%
MS = (
in_gen U ≤ V)%
MS.
-
Lemma rowval_genK m1 (
U :
'M_(m1, m)) : (
in_gen (
rowval_gen U)
:=: U)%
MS.
+
Lemma rowval_genK m (
U :
'M_(m, nA)) : (
in_gen (
rowval_gen U)
:=: U)%
MS.
-
Lemma rowval_gen_stable m1 (
U :
'M_(m1, m)) :
- (
rowval_gen U ×m A ≤ rowval_gen U)%
MS.
+
Lemma rowval_gen_stable m (
U :
'M_(m, nA)) :
+ (
rowval_gen U ×m A ≤ rowval_gen U)%
MS.
-
Lemma rstab_in_gen m1 (
U :
'M_(m1, n)) :
rstab rGA (
in_gen U)
= rstab rG U.
+
Lemma rstab_in_gen m (
U :
'M_(m, n)) :
rstab rGA (
in_gen U)
= rstab rG U.
-
Lemma rstabs_in_gen m1 (
U :
'M_(m1, n)) :
-
rstabs rG U \subset rstabs rGA (
in_gen U).
+
Lemma rstabs_in_gen m (
U :
'M_(m, n)) :
+
rstabs rG U \subset rstabs rGA (
in_gen U).
-
Lemma rstabs_rowval_gen m1 (
U :
'M_(m1, m)) :
-
rstabs rG (
rowval_gen U)
= rstabs rGA U.
+
Lemma rstabs_rowval_gen m (
U :
'M_(m, nA)) :
+
rstabs rG (
rowval_gen U)
= rstabs rGA U.
-
Lemma mxmodule_rowval_gen m1 (
U :
'M_(m1, m)) :
-
mxmodule rG (
rowval_gen U)
= mxmodule rGA U.
+
Lemma mxmodule_rowval_gen m (
U :
'M_(m, nA)) :
+
mxmodule rG (
rowval_gen U)
= mxmodule rGA U.
Lemma gen_mx_irr :
mx_irreducible rGA.
-
Lemma rker_gen :
rker rGA = rker rG.
+
Lemma rker_gen :
rker rGA = rker rG.
-
Lemma gen_mx_faithful :
mx_faithful rGA = mx_faithful rG.
+
Lemma gen_mx_faithful :
mx_faithful rGA = mx_faithful rG.
End GenField.
@@ -3552,77 +3589,70 @@
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n' :
nat).
-
Variables (
rG :
mx_representation F G n) (
A :
'M[F]_n).
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
n' :
nat).
+
Variables (
rG :
mx_representation F G n) (
A :
'M[F]_n).
Hypotheses (
irrG :
mx_irreducible rG) (
cGA :
centgmx rG A).
-
Let d_gt0 :
d > 0 :=
mxminpoly_nonconstant A.
+
Let d_gt0 :
d > 0 :=
mxminpoly_nonconstant A.
-
Let mxT (
u :
'rV_d) :=
vec_mx (
mulmx_term u (
mx_term Ad)).
+
Let mxT (
u :
'rV_d) :=
vec_mx (
mulmx_term u (
mx_term Ad)).
-
Let eval_mxT e u :
eval_mx e (
mxT u)
= mxval (
inFA (
eval_mx e u)).
+
Let eval_mxT e u :
eval_mx e (
mxT u)
= mxval (
inFA (
eval_mx e u)).
Let Ad'T :=
mx_term (
pinvmx Ad).
-
Let mulT (
u v :
'rV_d) :=
mulmx_term (
mxvec (
mulmx_term (
mxT u) (
mxT v)))
Ad'T.
+
Let mulT (
u v :
'rV_d) :=
mulmx_term (
mxvec (
mulmx_term (
mxT u) (
mxT v)))
Ad'T.
Lemma eval_mulT e u v :
-
eval_mx e (
mulT u v)
= val (
inFA (
eval_mx e u)
× inFA (
eval_mx e v)).
+
eval_mx e (
mulT u v)
= val (
inFA (
eval_mx e u)
× inFA (
eval_mx e v)).
Fixpoint gen_term t :=
match t with
-|
'X_k ⇒
row_var _ d k
-|
x%:T ⇒
mx_term (
val (
x : FA))
-|
n1%:R ⇒
mx_term (
val (
n1%:R : FA))%
R
-|
t1 + t2 ⇒
\row_i (gen_term t1 0%
R i + gen_term t2 0%
R i)
-|
- t1 ⇒
\row_i (- gen_term t1 0%
R i)
-|
t1 *+ n1 ⇒
mulmx_term (
mx_term n1%:R%:M)%
R (
gen_term t1)
-|
t1 × t2 ⇒
mulT (
gen_term t1) (
gen_term t2)
-|
t1^-1 ⇒
gen_term t1
-|
t1 ^+ n1 ⇒
iter n1 (
mulT (
gen_term t1)) (
mx_term (
val (1%
R : FA)))
+|
'X_k ⇒
row_var _ d k
+|
x%:T ⇒
mx_term (
val (
x : FA))
+|
n1%:R ⇒
mx_term (
val (
n1%:R : FA))%
R
+|
t1 + t2 ⇒
\row_i (gen_term t1 0%
R i + gen_term t2 0%
R i)
+|
- t1 ⇒
\row_i (- gen_term t1 0%
R i)
+|
t1 *+ n1 ⇒
mulmx_term (
mx_term n1%:R%:M)%
R (
gen_term t1)
+|
t1 × t2 ⇒
mulT (
gen_term t1) (
gen_term t2)
+|
t1^-1 ⇒
gen_term t1
+|
t1 ^+ n1 ⇒
iter n1 (
mulT (
gen_term t1)) (
mx_term (
val (1%
R : FA)))
end%
T.
Definition gen_env (
e :
seq FA) :=
row_env (
map val e).
-
Lemma nth_map_rVval (
e :
seq FA)
j :
(map val e)`_j = val e`_j.
+
Lemma nth_map_rVval (
e :
seq FA)
j :
(map val e)`_j = val e`_j.
Lemma set_nth_map_rVval (
e :
seq FA)
j v :
-
set_nth 0 (
map val e)
j v = map val (
set_nth 0
e j (
inFA v)).
+
set_nth 0 (
map val e)
j v = map val (
set_nth 0
e j (
inFA v)).
Lemma eval_gen_term e t :
-
GRing.rterm t → eval_mx (
gen_env e) (
gen_term t)
= val (
GRing.eval e t).
+
GRing.rterm t → eval_mx (
gen_env e) (
gen_term t)
= val (
GRing.eval e t).
-
-
-
- WARNING: Coq will core dump if the Notation Bool is used in the match
- pattern here.
-
-