From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.solvable.center.html | 269 ++++++++++++++---------------
1 file changed, 134 insertions(+), 135 deletions(-)
(limited to 'docs/htmldoc/mathcomp.solvable.center.html')
diff --git a/docs/htmldoc/mathcomp.solvable.center.html b/docs/htmldoc/mathcomp.solvable.center.html
index 7d9adbd..1a276f1 100644
--- a/docs/htmldoc/mathcomp.solvable.center.html
+++ b/docs/htmldoc/mathcomp.solvable.center.html
@@ -21,7 +21,6 @@
@@ -71,26 +70,26 @@
Variable gT : finGroupType.
-Definition center (A : {set gT}) := 'C_A(A).
+Definition center (A : {set gT}) := 'C_A(A).
-Canonical center_group (G : {group gT}) : {group gT} :=
- Eval hnf in [group of center G].
+Canonical center_group (G : {group gT}) : {group gT} :=
+ Eval hnf in [group of center G].
End Defs.
-Notation "''Z' ( A )" := (center A) : group_scope.
-Notation "''Z' ( H )" := (center_group H) : Group_scope.
+Notation "''Z' ( A )" := (center A) : group_scope.
+Notation "''Z' ( H )" := (center_group H) : Group_scope.
-Lemma morphim_center : GFunctor.pcontinuous center.
+Lemma morphim_center : GFunctor.pcontinuous (@center).
-Canonical center_igFun := [igFun by fun _ _ ⇒ subsetIl _ _ & morphim_center].
-Canonical center_gFun := [gFun by morphim_center].
-Canonical center_pgFun := [pgFun by morphim_center].
+Canonical center_igFun := [igFun by fun _ _ ⇒ subsetIl _ _ & morphim_center].
+Canonical center_gFun := [gFun by morphim_center].
+Canonical center_pgFun := [pgFun by morphim_center].
Section Center.
@@ -98,74 +97,74 @@
Variables gT : finGroupType.
Implicit Type rT : finGroupType.
-Implicit Types (x y : gT) (A B : {set gT}) (G H K D : {group gT}).
+Implicit Types (x y : gT) (A B : {set gT}) (G H K D : {group gT}).
-Lemma subcentP A B x : reflect (x \in A ∧ centralises x B) (x \in 'C_A(B)).
+Lemma subcentP A B x : reflect (x \in A ∧ centralises x B) (x \in 'C_A(B)).
-Lemma subcent_sub A B : 'C_A(B) \subset 'N_A(B).
+Lemma subcent_sub A B : 'C_A(B) \subset 'N_A(B).
-Lemma subcent_norm G B : 'N_G(B) \subset 'N('C_G(B)).
+Lemma subcent_norm G B : 'N_G(B) \subset 'N('C_G(B)).
-Lemma subcent_normal G B : 'C_G(B) <| 'N_G(B).
+Lemma subcent_normal G B : 'C_G(B) <| 'N_G(B).
-Lemma subcent_char G H K : H \char G → K \char G → 'C_H(K) \char G.
+Lemma subcent_char G H K : H \char G → K \char G → 'C_H(K) \char G.
-Lemma centerP A x : reflect (x \in A ∧ centralises x A) (x \in 'Z(A)).
+Lemma centerP A x : reflect (x \in A ∧ centralises x A) (x \in 'Z(A)).
-Lemma center_sub A : 'Z(A) \subset A.
+Lemma center_sub A : 'Z(A) \subset A.
-Lemma center1 : 'Z(1) = 1 :> {set gT}.
+Lemma center1 : 'Z(1) = 1 :> {set gT}.
-Lemma centerC A : {in A, centralised 'Z(A)}.
+Lemma centerC A : {in A, centralised 'Z(A)}.
-Lemma center_normal G : 'Z(G) <| G.
+Lemma center_normal G : 'Z(G) <| G.
-Lemma sub_center_normal H G : H \subset 'Z(G) → H <| G.
+Lemma sub_center_normal H G : H \subset 'Z(G) → H <| G.
-Lemma center_abelian G : abelian 'Z(G).
+Lemma center_abelian G : abelian 'Z(G).
-Lemma center_char G : 'Z(G) \char G.
+Lemma center_char G : 'Z(G) \char G.
-Lemma center_idP A : reflect ('Z(A) = A) (abelian A).
+Lemma center_idP A : reflect ('Z(A) = A) (abelian A).
Lemma center_class_formula G :
- #|G| = #|'Z(G)| + \sum_(xG in [set x ^: G | x in G :\: 'C(G)]) #|xG|.
+ #|G| = #|'Z(G)| + \sum_(xG in [set x ^: G | x in G :\: 'C(G)]) #|xG|.
-Lemma subcent1P A x y : reflect (y \in A ∧ commute x y) (y \in 'C_A[x]).
+Lemma subcent1P A x y : reflect (y \in A ∧ commute x y) (y \in 'C_A[x]).
-Lemma subcent1_id x G : x \in G → x \in 'C_G[x].
+Lemma subcent1_id x G : x \in G → x \in 'C_G[x].
-Lemma subcent1_sub x G : 'C_G[x] \subset G.
+Lemma subcent1_sub x G : 'C_G[x] \subset G.
-Lemma subcent1C x y G : x \in G → y \in 'C_G[x] → x \in 'C_G[y].
+Lemma subcent1C x y G : x \in G → y \in 'C_G[x] → x \in 'C_G[y].
-Lemma subcent1_cycle_sub x G : x \in G → <[x]> \subset 'C_G[x].
+Lemma subcent1_cycle_sub x G : x \in G → <[x]> \subset 'C_G[x].
-Lemma subcent1_cycle_norm x G : 'C_G[x] \subset 'N(<[x]>).
+Lemma subcent1_cycle_norm x G : 'C_G[x] \subset 'N(<[x]>).
-Lemma subcent1_cycle_normal x G : x \in G → <[x]> <| 'C_G[x].
+Lemma subcent1_cycle_normal x G : x \in G → <[x]> <| 'C_G[x].
@@ -174,23 +173,23 @@
Gorenstein. 1.3.4
-
Lemma cyclic_center_factor_abelian G :
cyclic (
G / 'Z(G))
→ abelian G.
+
Lemma cyclic_center_factor_abelian G :
cyclic (
G / 'Z(G))
→ abelian G.
Lemma cyclic_factor_abelian H G :
-
H \subset 'Z(G) → cyclic (
G / H)
→ abelian G.
+
H \subset 'Z(G) → cyclic (
G / H)
→ abelian G.
Section Injm.
-
Variables (
rT :
finGroupType) (
D :
{group gT}) (
f :
{morphism D >-> rT}).
+
Variables (
rT :
finGroupType) (
D :
{group gT}) (
f :
{morphism D >-> rT}).
-
Hypothesis injf :
'injm f.
+
Hypothesis injf :
'injm f.
-
Lemma injm_center G :
G \subset D → f @* 'Z(G) = 'Z(f @* G).
+
Lemma injm_center G :
G \subset D → f @* 'Z(G) = 'Z(f @* G).
End Injm.
@@ -201,44 +200,44 @@
-
Lemma isog_center (
aT rT :
finGroupType) (
G :
{group aT}) (
H :
{group rT}) :
-
G \isog H → 'Z(G) \isog 'Z(H).
+
Lemma isog_center (
aT rT :
finGroupType) (
G :
{group aT}) (
H :
{group rT}) :
+
G \isog H → 'Z(G) \isog 'Z(H).
Section Product.
Variable gT :
finGroupType.
-
Implicit Types (
A B C :
{set gT}) (
G H K :
{group gT}).
+
Implicit Types (
A B C :
{set gT}) (
G H K :
{group gT}).
-
Lemma center_prod H K :
K \subset 'C(H) → 'Z(H) × 'Z(K) = 'Z(H × K).
+
Lemma center_prod H K :
K \subset 'C(H) → 'Z(H) × 'Z(K) = 'Z(H × K).
-
Lemma center_cprod A B G :
A \* B = G → 'Z(A) \* 'Z(B) = 'Z(G).
+
Lemma center_cprod A B G :
A \* B = G → 'Z(A) \* 'Z(B) = 'Z(G).
-
Lemma center_bigcprod I r P (
F :
I → {set gT})
G :
-
\big[cprod/1
]_(i <- r | P i) F i = G →
-
\big[cprod/1
]_(i <- r | P i) 'Z(F i) = 'Z(G).
+
Lemma center_bigcprod I r P (
F :
I → {set gT})
G :
+
\big[cprod/1
]_(i <- r | P i) F i = G →
+
\big[cprod/1
]_(i <- r | P i) 'Z(F i) = 'Z(G).
-
Lemma cprod_center_id G :
G \* 'Z(G) = G.
+
Lemma cprod_center_id G :
G \* 'Z(G) = G.
-
Lemma center_dprod A B G :
A \x B = G → 'Z(A) \x 'Z(B) = 'Z(G).
+
Lemma center_dprod A B G :
A \x B = G → 'Z(A) \x 'Z(B) = 'Z(G).
-
Lemma center_bigdprod I r P (
F:
I → {set gT})
G :
-
\big[dprod/1
]_(i <- r | P i) F i = G →
-
\big[dprod/1
]_(i <- r | P i) 'Z(F i) = 'Z(G).
+
Lemma center_bigdprod I r P (
F:
I → {set gT})
G :
+
\big[dprod/1
]_(i <- r | P i) F i = G →
+
\big[dprod/1
]_(i <- r | P i) 'Z(F i) = 'Z(G).
Lemma Aut_cprod_full G H K :
-
H \* K = G → 'Z(H) = 'Z(K) →
-
Aut_in (
Aut H)
'Z(H) \isog Aut 'Z(H) →
-
Aut_in (
Aut K)
'Z(K) \isog Aut 'Z(K) →
-
Aut_in (
Aut G)
'Z(G) \isog Aut 'Z(G).
+
H \* K = G → 'Z(H) = 'Z(K) →
+
Aut_in (
Aut H)
'Z(H) \isog Aut 'Z(H) →
+
Aut_in (
Aut K)
'Z(K) \isog Aut 'Z(K) →
+
Aut_in (
Aut G)
'Z(G) \isog Aut 'Z(G).
End Product.
@@ -248,87 +247,87 @@
Variables gTH gTK :
finGroupType.
-
Variables (
H :
{group gTH}) (
K :
{group gTK}) (
gz :
{morphism 'Z(H) >-> gTK}).
+
Variables (
H :
{group gTH}) (
K :
{group gTK}) (
gz :
{morphism 'Z(H) >-> gTK}).
-
Definition ker_cprod_by of isom 'Z(H) 'Z(K) gz :=
-
[set xy | let:
(x, y) :=
xy in (x \in 'Z(H)) && (y == (gz x)^-1)].
+
Definition ker_cprod_by of isom 'Z(H) 'Z(K) gz :=
+
[set xy | let:
(x, y) :=
xy in (x \in 'Z(H)) && (y == (gz x)^-1)].
-
Hypothesis isoZ :
isom 'Z(H) 'Z(K) gz.
+
Hypothesis isoZ :
isom 'Z(H) 'Z(K) gz.
Let kerHK :=
ker_cprod_by isoZ.
-
Let injgz :
'injm gz.
-
Let gzZ :
gz @* 'Z(H) = 'Z(K).
-
Let gzZchar :
gz @* 'Z(H) \char 'Z(K).
-
Let sgzZZ :
gz @* 'Z(H) \subset 'Z(K) :=
char_sub gzZchar.
+
Let injgz :
'injm gz.
+
Let gzZ :
gz @* 'Z(H) = 'Z(K).
+
Let gzZchar :
gz @* 'Z(H) \char 'Z(K).
+
Let sgzZZ :
gz @* 'Z(H) \subset 'Z(K) :=
char_sub gzZchar.
Let sZH :=
center_sub H.
Let sZK :=
center_sub K.
-
Let sgzZG :
gz @* 'Z(H) \subset K :=
subset_trans sgzZZ sZK.
+
Let sgzZG :
gz @* 'Z(H) \subset K :=
subset_trans sgzZZ sZK.
Lemma ker_cprod_by_is_group :
group_set kerHK.
Canonical ker_cprod_by_group :=
Group ker_cprod_by_is_group.
-
Lemma ker_cprod_by_central :
kerHK \subset 'Z(setX H K).
+
Lemma ker_cprod_by_central :
kerHK \subset 'Z(setX H K).
-
Fact cprod_by_key :
unit.
-
Definition cprod_by_def :=
subFinGroupType [group of setX H K / kerHK].
-
Definition cprod_by :=
locked_with cprod_by_key cprod_by_def.
+
Fact cprod_by_key :
unit.
+
Definition cprod_by_def :=
subFinGroupType [group of setX H K / kerHK].
+
Definition cprod_by :=
locked_with cprod_by_key cprod_by_def.
-
Definition in_cprod :
gTH × gTK → cprod_by :=
-
let:
tt as k :=
cprod_by_key return _ → locked_with k cprod_by_def in
-
subg _ \o coset kerHK.
+
Definition in_cprod :
gTH × gTK → cprod_by :=
+
let:
tt as k :=
cprod_by_key return _ → locked_with k cprod_by_def in
+
subg _ \o coset kerHK.
-
Lemma in_cprodM :
{in setX H K &, {morph in_cprod : u v / u × v}}.
+
Lemma in_cprodM :
{in setX H K &, {morph in_cprod : u v / u × v}}.
Canonical in_cprod_morphism :=
Morphism in_cprodM.
-
Lemma ker_in_cprod :
'ker in_cprod = kerHK.
+
Lemma ker_in_cprod :
'ker in_cprod = kerHK.
-
Lemma cpairg1_dom :
H \subset 'dom (in_cprod \o @
pairg1 gTH gTK).
+
Lemma cpairg1_dom :
H \subset 'dom (in_cprod \o @
pairg1 gTH gTK).
-
Lemma cpair1g_dom :
K \subset 'dom (in_cprod \o @
pair1g gTH gTK).
+
Lemma cpair1g_dom :
K \subset 'dom (in_cprod \o @
pair1g gTH gTK).
-
Definition cpairg1 :=
tag (
restrmP _ cpairg1_dom).
-
Definition cpair1g :=
tag (
restrmP _ cpair1g_dom).
+
Definition cpairg1 :=
tag (
restrmP _ cpairg1_dom).
+
Definition cpair1g :=
tag (
restrmP _ cpair1g_dom).
-
Lemma injm_cpairg1 :
'injm cpairg1.
+
Lemma injm_cpairg1 :
'injm cpairg1.
Let injH :=
injm_cpairg1.
-
Lemma injm_cpair1g :
'injm cpair1g.
+
Lemma injm_cpair1g :
'injm cpair1g.
Let injK :=
injm_cpair1g.
-
Lemma im_cpair_cent :
CK \subset 'C(CH).
-
Hint Resolve im_cpair_cent.
+
Lemma im_cpair_cent :
CK \subset 'C(CH).
+
Hint Resolve im_cpair_cent :
core.
-
Lemma im_cpair :
CH × CK = C.
+
Lemma im_cpair :
CH × CK = C.
-
Lemma im_cpair_cprod :
CH \* CK = C.
+
Lemma im_cpair_cprod :
CH \* CK = C.
-
Lemma eq_cpairZ :
{in 'Z(H), cpairg1 =1 cpair1g \o gz}.
+
Lemma eq_cpairZ :
{in 'Z(H), cpairg1 =1 cpair1g \o gz}.
-
Lemma setI_im_cpair :
CH :&: CK = 'Z(CH).
+
Lemma setI_im_cpair :
CH :&: CK = 'Z(CH).
-
Lemma cpair1g_center :
cpair1g @* 'Z(K) = 'Z(C).
+
Lemma cpair1g_center :
cpair1g @* 'Z(K) = 'Z(C).
-
Lemma cpairg1_center :
cpairg1 @* 'Z(H) = 'Z(C).
+
Lemma cpairg1_center :
cpairg1 @* 'Z(H) = 'Z(C).
Section ExtCprodm.
Variable rT :
finGroupType.
-
Variables (
fH :
{morphism H >-> rT}) (
fK :
{morphism K >-> rT}).
-
Hypothesis cfHK :
fK @* K \subset 'C(fH @* H).
-
Hypothesis eq_fHK :
{in 'Z(H), fH =1 fK \o gz}.
+
Variables (
fH :
{morphism H >-> rT}) (
fK :
{morphism K >-> rT}).
+
Hypothesis cfHK :
fK @* K \subset 'C(fH @* H).
+
Hypothesis eq_fHK :
{in 'Z(H), fH =1 fK \o gz}.
Let gH :=
ifactm fH injm_cpairg1.
Let gK :=
ifactm fK injm_cpair1g.
-
Lemma xcprodm_cent :
gK @* CK \subset 'C(gH @* CH).
+
Lemma xcprodm_cent :
gK @* CK \subset 'C(gH @* CH).
-
Lemma xcprodmI :
{in CH :&: CK, gH =1 gK}.
+
Lemma xcprodmI :
{in CH :&: CK, gH =1 gK}.
Definition xcprodm :=
cprodm im_cpair_cprod xcprodm_cent xcprodmI.
-
Canonical xcprod_morphism :=
[morphism of xcprodm].
+
Canonical xcprod_morphism :=
[morphism of xcprodm].
-
Lemma xcprodmEl :
{in H, ∀ x,
xcprodm (
cpairg1 x)
= fH x}.
+
Lemma xcprodmEl :
{in H, ∀ x,
xcprodm (
cpairg1 x)
= fH x}.
-
Lemma xcprodmEr :
{in K, ∀ y,
xcprodm (
cpair1g y)
= fK y}.
+
Lemma xcprodmEr :
{in K, ∀ y,
xcprodm (
cpair1g y)
= fK y}.
Lemma xcprodmE :
-
{in H & K, ∀ x y,
xcprodm (
cpairg1 x × cpair1g y)
= fH x × fK y}.
+
{in H & K, ∀ x y,
xcprodm (
cpairg1 x × cpair1g y)
= fH x × fK y}.
-
Lemma im_xcprodm :
xcprodm @* C = fH @* H × fK @* K.
+
Lemma im_xcprodm :
xcprodm @* C = fH @* H × fK @* K.
-
Lemma im_xcprodml A :
xcprodm @* (cpairg1 @* A) = fH @* A.
+
Lemma im_xcprodml A :
xcprodm @* (cpairg1 @* A) = fH @* A.
-
Lemma im_xcprodmr A :
xcprodm @* (cpair1g @* A) = fK @* A.
+
Lemma im_xcprodmr A :
xcprodm @* (cpair1g @* A) = fK @* A.
-
Lemma injm_xcprodm :
'injm xcprodm = 'injm fH && 'injm fK.
+
Lemma injm_xcprodm :
'injm xcprodm = 'injm fH && 'injm fK.
End ExtCprodm.
@@ -404,22 +403,22 @@