-
Variables (
pi :
nat_pred) (
gT :
finGroupType) (
A :
{set gT}).
+
Variables (
pi :
nat_pred) (
gT :
finGroupType) (
A :
{set gT}).
-
Definition pcore :=
\bigcap_(G | [max G | pi.-subgroup(A) G]) G.
+
Definition pcore :=
\bigcap_(G | [max G | pi.-subgroup(A) G]) G.
-
Canonical pcore_group :
{group gT} :=
Eval hnf in [group of pcore].
+
Canonical pcore_group :
{group gT} :=
Eval hnf in [group of pcore].
End PcoreDef.
-
Notation "''O_' pi ( G )" := (
pcore pi G)
+
Notation "''O_' pi ( G )" := (
pcore pi G)
(
at level 8,
pi at level 2,
format "''O_' pi ( G )") :
group_scope.
-
Notation "''O_' pi ( G )" := (
pcore_group pi G) :
Group_scope.
+
Notation "''O_' pi ( G )" := (
pcore_group pi G) :
Group_scope.
Section PseriesDefs.
-
Variables (
pis :
seq nat_pred) (
gT :
finGroupType) (
A :
{set gT}).
+
Variables (
pis :
seq nat_pred) (
gT :
finGroupType) (
A :
{set gT}).
-
Definition pcore_mod pi B :=
coset B @*^-1 'O_pi(A / B).
-
Canonical pcore_mod_group pi B :
{group gT} :=
-
Eval hnf in [group of pcore_mod pi B].
+
Definition pcore_mod pi B :=
coset B @*^-1 'O_pi(A / B).
+
Canonical pcore_mod_group pi B :
{group gT} :=
+
Eval hnf in [group of pcore_mod pi B].
Definition pseries :=
foldr pcore_mod 1 (
rev pis).
@@ -694,71 +693,71 @@
Lemma pseries_group_set :
group_set pseries.
-
Canonical pseries_group :
{group gT} :=
group pseries_group_set.
+
Canonical pseries_group :
{group gT} :=
group pseries_group_set.
End PseriesDefs.
-
Notation "''O_{' p1 , .. , pn } ( A )" :=
- (
pseries (
ConsPred p1 .. (
ConsPred pn [::]) ..)
A)
+
Notation "''O_{' p1 , .. , pn } ( A )" :=
+ (
pseries (
ConsPred p1 .. (
ConsPred pn [::]) ..)
A)
(
at level 8,
format "''O_{' p1 , .. , pn } ( A )") :
group_scope.
-
Notation "''O_{' p1 , .. , pn } ( A )" :=
- (
pseries_group (
ConsPred p1 .. (
ConsPred pn [::]) ..)
A) :
Group_scope.
+
Notation "''O_{' p1 , .. , pn } ( A )" :=
+ (
pseries_group (
ConsPred p1 .. (
ConsPred pn [::]) ..)
A) :
Group_scope.
Section PCoreProps.
Variables (
pi :
nat_pred) (
gT :
finGroupType).
-
Implicit Types (
A :
{set gT}) (
G H M K :
{group gT}).
+
Implicit Types (
A :
{set gT}) (
G H M K :
{group gT}).
-
Lemma pcore_psubgroup G :
pi.-subgroup(G) 'O_pi(G).
+
Lemma pcore_psubgroup G :
pi.-subgroup(G) 'O_pi(G).
-
Lemma pcore_pgroup G :
pi.-group 'O_pi(G).
+
Lemma pcore_pgroup G :
pi.-group 'O_pi(G).
-
Lemma pcore_sub G :
'O_pi(G) \subset G.
+
Lemma pcore_sub G :
'O_pi(G) \subset G.
-
Lemma pcore_sub_Hall G H :
pi.-Hall(G) H → 'O_pi(G) \subset H.
+
Lemma pcore_sub_Hall G H :
pi.-Hall(G) H → 'O_pi(G) \subset H.
-
Lemma pcore_max G H :
pi.-group H → H <| G → H \subset 'O_pi(G).
+
Lemma pcore_max G H :
pi.-group H → H <| G → H \subset 'O_pi(G).
-
Lemma pcore_pgroup_id G :
pi.-group G → 'O_pi(G) = G.
+
Lemma pcore_pgroup_id G :
pi.-group G → 'O_pi(G) = G.
-
Lemma pcore_normal G :
'O_pi(G) <| G.
+
Lemma pcore_normal G :
'O_pi(G) <| G.
-
Lemma normal_Hall_pcore H G :
pi.-Hall(G) H → H <| G → 'O_pi(G) = H.
+
Lemma normal_Hall_pcore H G :
pi.-Hall(G) H → H <| G → 'O_pi(G) = H.
Lemma eq_Hall_pcore G H :
-
pi.-Hall(G) 'O_pi(G) → pi.-Hall(G) H → H :=: 'O_pi(G).
+
pi.-Hall(G) 'O_pi(G) → pi.-Hall(G) H → H :=: 'O_pi(G).
Lemma sub_Hall_pcore G K :
-
pi.-Hall(G) 'O_pi(G) → K \subset G → (K \subset 'O_pi(G)) = pi.-group K.
+
pi.-Hall(G) 'O_pi(G) → K \subset G → (K \subset 'O_pi(G)) = pi.-group K.
Lemma mem_Hall_pcore G x :
-
pi.-Hall(G) 'O_pi(G) → x \in G → (x \in 'O_pi(G)) = pi.-elt x.
+
pi.-Hall(G) 'O_pi(G) → x \in G → (x \in 'O_pi(G)) = pi.-elt x.
Lemma sdprod_Hall_pcoreP H G :
-
pi.-Hall(G) 'O_pi(G) → reflect (
'O_pi(G) ><| H = G) (
pi^'.-Hall(G) H).
+
pi.-Hall(G) 'O_pi(G) → reflect (
'O_pi(G) ><| H = G) (
pi^'.-Hall(G) H).
Lemma sdprod_pcore_HallP H G :
-
pi^'.-Hall(G) H → reflect (
'O_pi(G) ><| H = G) (
pi.-Hall(G) 'O_pi(G)).
+
pi^'.-Hall(G) H → reflect (
'O_pi(G) ><| H = G) (
pi.-Hall(G) 'O_pi(G)).
-
Lemma pcoreJ G x :
'O_pi(G :^ x) = 'O_pi(G) :^ x.
+
Lemma pcoreJ G x :
'O_pi(G :^ x) = 'O_pi(G) :^ x.
End PCoreProps.
@@ -770,19 +769,19 @@
Implicit Types (
pi :
nat_pred) (
gT rT :
finGroupType).
-
Lemma morphim_pcore pi :
GFunctor.pcontinuous (
pcore pi).
+
Lemma morphim_pcore pi :
GFunctor.pcontinuous (@
pcore pi).
-
Lemma pcoreS pi gT (
G H :
{group gT}) :
-
H \subset G → H :&: 'O_pi(G) \subset 'O_pi(H).
+
Lemma pcoreS pi gT (
G H :
{group gT}) :
+
H \subset G → H :&: 'O_pi(G) \subset 'O_pi(H).
-
Canonical pcore_igFun pi :=
[igFun by pcore_sub pi & morphim_pcore pi].
-
Canonical pcore_gFun pi :=
[gFun by morphim_pcore pi].
-
Canonical pcore_pgFun pi :=
[pgFun by morphim_pcore pi].
+
Canonical pcore_igFun pi :=
[igFun by pcore_sub pi & morphim_pcore pi].
+
Canonical pcore_gFun pi :=
[gFun by morphim_pcore pi].
+
Canonical pcore_pgFun pi :=
[pgFun by morphim_pcore pi].
-
Lemma pcore_char pi gT (
G :
{group gT}) :
'O_pi(G) \char G.
+
Lemma pcore_char pi gT (
G :
{group gT}) :
'O_pi(G) \char G.
Section PcoreMod.
@@ -791,124 +790,124 @@
Variable F :
GFunctor.pmap.
-
Lemma pcore_mod_sub pi gT (
G :
{group gT}) :
pcore_mod G pi (
F _ G)
\subset G.
+
Lemma pcore_mod_sub pi gT (
G :
{group gT}) :
pcore_mod G pi (
F _ G)
\subset G.
-
Lemma quotient_pcore_mod pi gT (
G :
{group gT}) (
B :
{set gT}) :
-
pcore_mod G pi B / B = 'O_pi(G / B).
+
Lemma quotient_pcore_mod pi gT (
G :
{group gT}) (
B :
{set gT}) :
+
pcore_mod G pi B / B = 'O_pi(G / B).
-
Lemma morphim_pcore_mod pi gT rT (
D G :
{group gT}) (
f :
{morphism D >-> rT}) :
-
f @* pcore_mod G pi (
F _ G)
\subset pcore_mod (
f @* G)
pi (
F _ (
f @* G)).
+
Lemma morphim_pcore_mod pi gT rT (
D G :
{group gT}) (
f :
{morphism D >-> rT}) :
+
f @* pcore_mod G pi (
F _ G)
\subset pcore_mod (
f @* G)
pi (
F _ (
f @* G)).
-
Lemma pcore_mod_res pi gT rT (
D :
{group gT}) (
f :
{morphism D >-> rT}) :
-
f @* pcore_mod D pi (
F _ D)
\subset pcore_mod (
f @* D)
pi (
F _ (
f @* D)).
+
Lemma pcore_mod_res pi gT rT (
D :
{group gT}) (
f :
{morphism D >-> rT}) :
+
f @* pcore_mod D pi (
F _ D)
\subset pcore_mod (
f @* D)
pi (
F _ (
f @* D)).
-
Lemma pcore_mod1 pi gT (
G :
{group gT}) :
pcore_mod G pi 1
= 'O_pi(G).
+
Lemma pcore_mod1 pi gT (
G :
{group gT}) :
pcore_mod G pi 1
= 'O_pi(G).
End PcoreMod.
-
Lemma pseries_rcons pi pis gT (
A :
{set gT}) :
-
pseries (
rcons pis pi)
A = pcore_mod A pi (
pseries pis A).
+
Lemma pseries_rcons pi pis gT (
A :
{set gT}) :
+
pseries (
rcons pis pi)
A = pcore_mod A pi (
pseries pis A).
Lemma pseries_subfun pis :
-
GFunctor.closed (
pseries pis)
∧ GFunctor.pcontinuous (
pseries pis).
+
GFunctor.closed (@
pseries pis)
∧ GFunctor.pcontinuous (@
pseries pis).
-
Lemma pseries_sub pis :
GFunctor.closed (
pseries pis).
+
Lemma pseries_sub pis :
GFunctor.closed (@
pseries pis).
-
Lemma morphim_pseries pis :
GFunctor.pcontinuous (
pseries pis).
+
Lemma morphim_pseries pis :
GFunctor.pcontinuous (@
pseries pis).
-
Lemma pseriesS pis :
GFunctor.hereditary (
pseries pis).
+
Lemma pseriesS pis :
GFunctor.hereditary (@
pseries pis).
-
Canonical pseries_igFun pis :=
[igFun by pseries_sub pis & morphim_pseries pis].
-
Canonical pseries_gFun pis :=
[gFun by morphim_pseries pis].
-
Canonical pseries_pgFun pis :=
[pgFun by morphim_pseries pis].
+
Canonical pseries_igFun pis :=
[igFun by pseries_sub pis & morphim_pseries pis].
+
Canonical pseries_gFun pis :=
[gFun by morphim_pseries pis].
+
Canonical pseries_pgFun pis :=
[pgFun by morphim_pseries pis].
-
Lemma pseries_char pis gT (
G :
{group gT}) :
pseries pis G \char G.
+
Lemma pseries_char pis gT (
G :
{group gT}) :
pseries pis G \char G.
-
Lemma pseries_normal pis gT (
G :
{group gT}) :
pseries pis G <| G.
+
Lemma pseries_normal pis gT (
G :
{group gT}) :
pseries pis G <| G.
-
Lemma pseriesJ pis gT (
G :
{group gT})
x :
-
pseries pis (
G :^ x)
= pseries pis G :^ x.
+
Lemma pseriesJ pis gT (
G :
{group gT})
x :
+
pseries pis (
G :^ x)
= pseries pis G :^ x.
-
Lemma pseries1 pi gT (
G :
{group gT}) :
'O_{pi}(G) = 'O_pi(G).
+
Lemma pseries1 pi gT (
G :
{group gT}) :
'O_{pi}(G) = 'O_pi(G).
-
Lemma pseries_pop pi pis gT (
G :
{group gT}) :
-
'O_pi(G) = 1
→ pseries (
pi :: pis)
G = pseries pis G.
+
Lemma pseries_pop pi pis gT (
G :
{group gT}) :
+
'O_pi(G) = 1
→ pseries (
pi :: pis)
G = pseries pis G.
-
Lemma pseries_pop2 pi1 pi2 gT (
G :
{group gT}) :
-
'O_pi1(G) = 1
→ 'O_{pi1, pi2}(G) = 'O_pi2(G).
+
Lemma pseries_pop2 pi1 pi2 gT (
G :
{group gT}) :
+
'O_pi1(G) = 1
→ 'O_{pi1, pi2}(G) = 'O_pi2(G).
-
Lemma pseries_sub_catl pi1s pi2s gT (
G :
{group gT}) :
-
pseries pi1s G \subset pseries (
pi1s ++ pi2s)
G.
+
Lemma pseries_sub_catl pi1s pi2s gT (
G :
{group gT}) :
+
pseries pi1s G \subset pseries (
pi1s ++ pi2s)
G.
-
Lemma quotient_pseries pis pi gT (
G :
{group gT}) :
-
pseries (
rcons pis pi)
G / pseries pis G = 'O_pi(G / pseries pis G).
+
Lemma quotient_pseries pis pi gT (
G :
{group gT}) :
+
pseries (
rcons pis pi)
G / pseries pis G = 'O_pi(G / pseries pis G).
-
Lemma pseries_norm2 pi1s pi2s gT (
G :
{group gT}) :
-
pseries pi2s G \subset 'N(pseries pi1s G).
+
Lemma pseries_norm2 pi1s pi2s gT (
G :
{group gT}) :
+
pseries pi2s G \subset 'N(pseries pi1s G).
-
Lemma pseries_sub_catr pi1s pi2s gT (
G :
{group gT}) :
-
pseries pi2s G \subset pseries (
pi1s ++ pi2s)
G.
+
Lemma pseries_sub_catr pi1s pi2s gT (
G :
{group gT}) :
+
pseries pi2s G \subset pseries (
pi1s ++ pi2s)
G.
-
Lemma quotient_pseries2 pi1 pi2 gT (
G :
{group gT}) :
-
'O_{pi1, pi2}(G) / 'O_pi1(G) = 'O_pi2(G / 'O_pi1(G)).
+
Lemma quotient_pseries2 pi1 pi2 gT (
G :
{group gT}) :
+
'O_{pi1, pi2}(G) / 'O_pi1(G) = 'O_pi2(G / 'O_pi1(G)).
-
Lemma quotient_pseries_cat pi1s pi2s gT (
G :
{group gT}) :
-
pseries (
pi1s ++ pi2s)
G / pseries pi1s G
-
= pseries pi2s (
G / pseries pi1s G).
+
Lemma quotient_pseries_cat pi1s pi2s gT (
G :
{group gT}) :
+
pseries (
pi1s ++ pi2s)
G / pseries pi1s G
+
= pseries pi2s (
G / pseries pi1s G).
-
Lemma pseries_catl_id pi1s pi2s gT (
G :
{group gT}) :
-
pseries pi1s (
pseries (
pi1s ++ pi2s)
G)
= pseries pi1s G.
+
Lemma pseries_catl_id pi1s pi2s gT (
G :
{group gT}) :
+
pseries pi1s (
pseries (
pi1s ++ pi2s)
G)
= pseries pi1s G.
-
Lemma pseries_char_catl pi1s pi2s gT (
G :
{group gT}) :
-
pseries pi1s G \char pseries (
pi1s ++ pi2s)
G.
+
Lemma pseries_char_catl pi1s pi2s gT (
G :
{group gT}) :
+
pseries pi1s G \char pseries (
pi1s ++ pi2s)
G.
-
Lemma pseries_catr_id pi1s pi2s gT (
G :
{group gT}) :
-
pseries pi2s (
pseries (
pi1s ++ pi2s)
G)
= pseries pi2s G.
+
Lemma pseries_catr_id pi1s pi2s gT (
G :
{group gT}) :
+
pseries pi2s (
pseries (
pi1s ++ pi2s)
G)
= pseries pi2s G.
-
Lemma pseries_char_catr pi1s pi2s gT (
G :
{group gT}) :
-
pseries pi2s G \char pseries (
pi1s ++ pi2s)
G.
+
Lemma pseries_char_catr pi1s pi2s gT (
G :
{group gT}) :
+
pseries pi2s G \char pseries (
pi1s ++ pi2s)
G.
-
Lemma pcore_modp pi gT (
G H :
{group gT}) :
-
H <| G → pi.-group H → pcore_mod G pi H = 'O_pi(G).
+
Lemma pcore_modp pi gT (
G H :
{group gT}) :
+
H <| G → pi.-group H → pcore_mod G pi H = 'O_pi(G).
-
Lemma pquotient_pcore pi gT (
G H :
{group gT}) :
-
H <| G → pi.-group H → 'O_pi(G / H) = 'O_pi(G) / H.
+
Lemma pquotient_pcore pi gT (
G H :
{group gT}) :
+
H <| G → pi.-group H → 'O_pi(G / H) = 'O_pi(G) / H.
-
Lemma trivg_pcore_quotient pi gT (
G :
{group gT}) :
'O_pi(G / 'O_pi(G)) = 1.
+
Lemma trivg_pcore_quotient pi gT (
G :
{group gT}) :
'O_pi(G / 'O_pi(G)) = 1.
-
Lemma pseries_rcons_id pis pi gT (
G :
{group gT}) :
-
pseries (
rcons (
rcons pis pi)
pi)
G = pseries (
rcons pis pi)
G.
+
Lemma pseries_rcons_id pis pi gT (
G :
{group gT}) :
+
pseries (
rcons (
rcons pis pi)
pi)
G = pseries (
rcons pis pi)
G.
End MorphPcore.
@@ -918,51 +917,51 @@
Variables gT :
finGroupType.
-
Implicit Types (
pi rho :
nat_pred) (
G H :
{group gT}).
+
Implicit Types (
pi rho :
nat_pred) (
G H :
{group gT}).
Lemma sub_in_pcore pi rho G :
-
{in \pi(G), {subset pi ≤ rho}} → 'O_pi(G) \subset 'O_rho(G).
+
{in \pi(G), {subset pi ≤ rho}} → 'O_pi(G) \subset 'O_rho(G).
-
Lemma sub_pcore pi rho G :
{subset pi ≤ rho} → 'O_pi(G) \subset 'O_rho(G).
+
Lemma sub_pcore pi rho G :
{subset pi ≤ rho} → 'O_pi(G) \subset 'O_rho(G).
-
Lemma eq_in_pcore pi rho G :
{in \pi(G), pi =i rho} → 'O_pi(G) = 'O_rho(G).
+
Lemma eq_in_pcore pi rho G :
{in \pi(G), pi =i rho} → 'O_pi(G) = 'O_rho(G).
-
Lemma eq_pcore pi rho G :
pi =i rho → 'O_pi(G) = 'O_rho(G).
+
Lemma eq_pcore pi rho G :
pi =i rho → 'O_pi(G) = 'O_rho(G).
-
Lemma pcoreNK pi G :
'O_pi^'^'(G) = 'O_pi(G).
+
Lemma pcoreNK pi G :
'O_pi^'^'(G) = 'O_pi(G).
-
Lemma eq_p'core pi rho G :
pi =i rho → 'O_pi^'(G) = 'O_rho^'(G).
+
Lemma eq_p'core pi rho G :
pi =i rho → 'O_pi^'(G) = 'O_rho^'(G).
Lemma sdprod_Hall_p'coreP pi H G :
-
pi^'.-Hall(G) 'O_pi^'(G) → reflect (
'O_pi^'(G) ><| H = G) (
pi.-Hall(G) H).
+
pi^'.-Hall(G) 'O_pi^'(G) → reflect (
'O_pi^'(G) ><| H = G) (
pi.-Hall(G) H).
Lemma sdprod_p'core_HallP pi H G :
-
pi.-Hall(G) H → reflect (
'O_pi^'(G) ><| H = G) (
pi^'.-Hall(G) 'O_pi^'(G)).
+
pi.-Hall(G) H → reflect (
'O_pi^'(G) ><| H = G) (
pi^'.-Hall(G) 'O_pi^'(G)).
-
Lemma pcoreI pi rho G :
'O_[predI pi & rho](G) = 'O_pi('O_rho(G)).
+
Lemma pcoreI pi rho G :
'O_[predI pi & rho](G) = 'O_pi('O_rho(G)).
Lemma bigcap_p'core pi G :
-
G :&: \bigcap_(p < #|G|.+1 | (p : nat) \in pi) 'O_p^'(G) = 'O_pi^'(G).
+
G :&: \bigcap_(p < #|G|.+1 | (p : nat) \in pi) 'O_p^'(G) = 'O_pi^'(G).
-
Lemma coprime_pcoreC (
rT :
finGroupType)
pi G (
R :
{group rT}) :
-
coprime #|'O_pi(G)| #|'O_pi^'(R)|.
+
Lemma coprime_pcoreC (
rT :
finGroupType)
pi G (
R :
{group rT}) :
+
coprime #|'O_pi(G)| #|'O_pi^'(R)|.
-
Lemma TI_pcoreC pi G H :
'O_pi(G) :&: 'O_pi^'(H) = 1.
+
Lemma TI_pcoreC pi G H :
'O_pi(G) :&: 'O_pi^'(H) = 1.
-
Lemma pcore_setI_normal pi G H :
H <| G → 'O_pi(G) :&: H = 'O_pi(H).
+
Lemma pcore_setI_normal pi G H :
H <| G → 'O_pi(G) :&: H = 'O_pi(H).
End EqPcore.
@@ -973,26 +972,26 @@
Section Injm.
-
Variables (
aT rT :
finGroupType) (
D :
{group aT}) (
f :
{morphism D >-> rT}).
-
Hypothesis injf :
'injm f.
-
Implicit Types (
A :
{set aT}) (
G H :
{group aT}).
+
Variables (
aT rT :
finGroupType) (
D :
{group aT}) (
f :
{morphism D >-> rT}).
+
Hypothesis injf :
'injm f.
+
Implicit Types (
A :
{set aT}) (
G H :
{group aT}).
-
Lemma injm_pgroup pi A :
A \subset D → pi.-group (
f @* A)
= pi.-group A.
+
Lemma injm_pgroup pi A :
A \subset D → pi.-group (
f @* A)
= pi.-group A.
-
Lemma injm_pelt pi x :
x \in D → pi.-elt (
f x)
= pi.-elt x.
+
Lemma injm_pelt pi x :
x \in D → pi.-elt (
f x)
= pi.-elt x.
Lemma injm_pHall pi G H :
-
G \subset D → H \subset D → pi.-Hall(f @* G) (
f @* H)
= pi.-Hall(G) H.
+
G \subset D → H \subset D → pi.-Hall(f @* G) (
f @* H)
= pi.-Hall(G) H.
-
Lemma injm_pcore pi G :
G \subset D → f @* 'O_pi(G) = 'O_pi(f @* G).
+
Lemma injm_pcore pi G :
G \subset D → f @* 'O_pi(G) = 'O_pi(f @* G).
Lemma injm_pseries pis G :
-
G \subset D → f @* pseries pis G = pseries pis (
f @* G).
+
G \subset D → f @* pseries pis G = pseries pis (
f @* G).
End Injm.
@@ -1001,16 +1000,16 @@
Section Isog.
-
Variables (
aT rT :
finGroupType) (
G :
{group aT}) (
H :
{group rT}).
+
Variables (
aT rT :
finGroupType) (
G :
{group aT}) (
H :
{group rT}).
-
Lemma isog_pgroup pi :
G \isog H → pi.-group G = pi.-group H.
+
Lemma isog_pgroup pi :
G \isog H → pi.-group G = pi.-group H.
-
Lemma isog_pcore pi :
G \isog H → 'O_pi(G) \isog 'O_pi(H).
+
Lemma isog_pcore pi :
G \isog H → 'O_pi(G) \isog 'O_pi(H).
-
Lemma isog_pseries pis :
G \isog H → pseries pis G \isog pseries pis H.
+
Lemma isog_pseries pis :
G \isog H → pseries pis G \isog pseries pis H.
End Isog.
--
cgit v1.2.3