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.fingroup.automorphism.html | 181 +++++++++++------------
1 file changed, 90 insertions(+), 91 deletions(-)
(limited to 'docs/htmldoc/mathcomp.fingroup.automorphism.html')
diff --git a/docs/htmldoc/mathcomp.fingroup.automorphism.html b/docs/htmldoc/mathcomp.fingroup.automorphism.html
index bff22e2..bac4533 100644
--- a/docs/htmldoc/mathcomp.fingroup.automorphism.html
+++ b/docs/htmldoc/mathcomp.fingroup.automorphism.html
@@ -21,7 +21,6 @@
@@ -73,20 +72,20 @@
Variable gT : finGroupType.
-Implicit Type A : {set gT}.
-Implicit Types a b : {perm gT}.
+Implicit Type A : {set gT}.
+Implicit Types a b : {perm gT}.
-Definition Aut A := [set a | perm_on A a & morphic A a].
+Definition Aut A := [set a | perm_on A a & morphic A a].
-Lemma Aut_morphic A a : a \in Aut A → morphic A a.
+Lemma Aut_morphic A a : a \in Aut A → morphic A a.
-Lemma out_Aut A a x : a \in Aut A → x \notin A → a x = x.
+Lemma out_Aut A a x : a \in Aut A → x \notin A → a x = x.
-Lemma eq_Aut A : {in Aut A &, ∀ a b, {in A, a =1 b} → a = b}.
+Lemma eq_Aut A : {in Aut A &, ∀ a b, {in A, a =1 b} → a = b}.
@@ -97,17 +96,17 @@
-
Definition autm A a (
AutAa :
a \in Aut A) :=
morphm (
Aut_morphic AutAa).
-
Lemma autmE A a (
AutAa :
a \in Aut A) :
autm AutAa = a.
+
Definition autm A a (
AutAa :
a \in Aut A) :=
morphm (
Aut_morphic AutAa).
+
Lemma autmE A a (
AutAa :
a \in Aut A) :
autm AutAa = a.
-
Canonical autm_morphism A a aM :=
Eval hnf in [morphism of @
autm A a aM].
+
Canonical autm_morphism A a aM :=
Eval hnf in [morphism of @
autm A a aM].
Section AutGroup.
-
Variable G :
{group gT}.
+
Variable G :
{group gT}.
Lemma Aut_group_set :
group_set (
Aut G).
@@ -116,35 +115,35 @@
Canonical Aut_group :=
group Aut_group_set.
-
Variable (
a :
{perm gT}) (
AutGa :
a \in Aut G).
+
Variable (
a :
{perm gT}) (
AutGa :
a \in Aut G).
Notation f := (
autm AutGa).
Notation fE := (
autmE AutGa).
-
Lemma injm_autm :
'injm f.
+
Lemma injm_autm :
'injm f.
-
Lemma ker_autm :
'ker f = 1.
+
Lemma ker_autm :
'ker f = 1.
-
Lemma im_autm :
f @* G = G.
+
Lemma im_autm :
f @* G = G.
-
Lemma Aut_closed x :
x \in G → a x \in G.
+
Lemma Aut_closed x :
x \in G → a x \in G.
End AutGroup.
-
Lemma Aut1 :
Aut 1
= 1.
+
Lemma Aut1 :
Aut 1
= 1.
End Automorphism.
-
Notation "[ 'Aut' G ]" := (
Aut_group G)
+
Notation "[ 'Aut' G ]" := (
Aut_group G)
(
at level 0,
format "[ 'Aut' G ]") :
Group_scope.
-
Notation "[ 'Aut' G ]" := (
Aut G)
+
Notation "[ 'Aut' G ]" := (
Aut G)
(
at level 0,
only parsing) :
group_scope.
@@ -162,13 +161,13 @@
Section PermIn.
-
Variables (
T :
finType) (
A :
{set T}) (
f :
T → T).
+
Variables (
T :
finType) (
A :
{set T}) (
f :
T → T).
-
Hypotheses (
injf :
{in A &, injective f}) (
sBf :
f @: A \subset A).
+
Hypotheses (
injf :
{in A &, injective f}) (
sBf :
f @: A \subset A).
-
Lemma perm_in_inj :
injective (
fun x ⇒
if x \in A then f x else x).
+
Lemma perm_in_inj :
injective (
fun x ⇒
if x \in A then f x else x).
Definition perm_in :=
perm perm_in_inj.
@@ -177,7 +176,7 @@
Lemma perm_in_on :
perm_on A perm_in.
-
Lemma perm_inE :
{in A, perm_in =1 f}.
+
Lemma perm_inE :
{in A, perm_in =1 f}.
End PermIn.
@@ -194,38 +193,38 @@
Section MakeAut.
-
Variables (
gT :
finGroupType) (
G :
{group gT}) (
f :
{morphism G >-> gT}).
-
Implicit Type A :
{set gT}.
+
Variables (
gT :
finGroupType) (
G :
{group gT}) (
f :
{morphism G >-> gT}).
+
Implicit Type A :
{set gT}.
-
Hypothesis injf :
'injm f.
+
Hypothesis injf :
'injm f.
-
Lemma morphim_fixP A :
A \subset G → reflect (
f @* A = A) (
f @* A \subset A).
+
Lemma morphim_fixP A :
A \subset G → reflect (
f @* A = A) (
f @* A \subset A).
-
Hypothesis Gf :
f @* G = G.
+
Hypothesis Gf :
f @* G = G.
-
Lemma aut_closed :
f @: G \subset G.
+
Lemma aut_closed :
f @: G \subset G.
Definition aut :=
perm_in (
injmP injf)
aut_closed.
-
Lemma autE :
{in G, aut =1 f}.
+
Lemma autE :
{in G, aut =1 f}.
Lemma morphic_aut :
morphic G aut.
-
Lemma Aut_aut :
aut \in Aut G.
+
Lemma Aut_aut :
aut \in Aut G.
-
Lemma imset_autE A :
A \subset G → aut @: A = f @* A.
+
Lemma imset_autE A :
A \subset G → aut @: A = f @* A.
-
Lemma preim_autE A :
A \subset G → aut @^-1: A = f @*^-1 A.
+
Lemma preim_autE A :
A \subset G → aut @^-1: A = f @*^-1 A.
End MakeAut.
@@ -236,31 +235,31 @@
Section AutIsom.
-
Variables (
gT rT :
finGroupType) (
G D :
{group gT}) (
f :
{morphism D >-> rT}).
+
Variables (
gT rT :
finGroupType) (
G D :
{group gT}) (
f :
{morphism D >-> rT}).
-
Hypotheses (
injf :
'injm f) (
sGD :
G \subset D).
+
Hypotheses (
injf :
'injm f) (
sGD :
G \subset D).
Let domG :=
subsetP sGD.
Lemma Aut_isom_subproof a :
-
{a' | a' \in Aut (
f @* G)
& a \in Aut G → {in G, a' \o f =1 f \o a}}.
+
{a' | a' \in Aut (
f @* G)
& a \in Aut G → {in G, a' \o f =1 f \o a}}.
Definition Aut_isom a :=
s2val (
Aut_isom_subproof a).
-
Lemma Aut_Aut_isom a :
Aut_isom a \in Aut (
f @* G).
+
Lemma Aut_Aut_isom a :
Aut_isom a \in Aut (
f @* G).
-
Lemma Aut_isomE a :
a \in Aut G → {in G, ∀ x,
Aut_isom a (
f x)
= f (
a x)
}.
+
Lemma Aut_isomE a :
a \in Aut G → {in G, ∀ x,
Aut_isom a (
f x)
= f (
a x)
}.
-
Lemma Aut_isomM :
{in Aut G &, {morph Aut_isom: x y / x × y}}.
+
Lemma Aut_isomM :
{in Aut G &, {morph Aut_isom: x y / x × y}}.
Canonical Aut_isom_morphism :=
Morphism Aut_isomM.
-
Lemma injm_Aut_isom :
'injm Aut_isom.
+
Lemma injm_Aut_isom :
'injm Aut_isom.
End AutIsom.
@@ -269,20 +268,20 @@
Section InjmAut.
-
Variables (
gT rT :
finGroupType) (
G D :
{group gT}) (
f :
{morphism D >-> rT}).
+
Variables (
gT rT :
finGroupType) (
G D :
{group gT}) (
f :
{morphism D >-> rT}).
-
Hypotheses (
injf :
'injm f) (
sGD :
G \subset D).
+
Hypotheses (
injf :
'injm f) (
sGD :
G \subset D).
Let domG :=
subsetP sGD.
-
Lemma im_Aut_isom :
Aut_isom injf sGD @* Aut G = Aut (
f @* G).
+
Lemma im_Aut_isom :
Aut_isom injf sGD @* Aut G = Aut (
f @* G).
-
Lemma Aut_isomP :
isom (
Aut G) (
Aut (
f @* G)) (
Aut_isom injf sGD).
+
Lemma Aut_isomP :
isom (
Aut G) (
Aut (
f @* G)) (
Aut_isom injf sGD).
-
Lemma injm_Aut :
Aut (
f @* G)
\isog Aut G.
+
Lemma injm_Aut :
Aut (
f @* G)
\isog Aut G.
End InjmAut.
@@ -300,59 +299,59 @@
Variable gT :
finGroupType.
-
Implicit Type A :
{set gT}.
+
Implicit Type A :
{set gT}.
-
Definition conjgm of {set gT} :=
fun x y :
gT ⇒
y ^ x.
+
Definition conjgm of {set gT} :=
fun x y :
gT ⇒
y ^ x.
-
Lemma conjgmE A x y :
conjgm A x y = y ^ x.
+
Lemma conjgmE A x y :
conjgm A x y = y ^ x.
Canonical conjgm_morphism A x :=
- @
Morphism _ _ A (
conjgm A x) (
in2W (
fun y z ⇒
conjMg y z x)).
+ @
Morphism _ _ A (
conjgm A x) (
in2W (
fun y z ⇒
conjMg y z x)).
-
Lemma morphim_conj A x B :
conjgm A x @* B = (A :&: B) :^ x.
+
Lemma morphim_conj A x B :
conjgm A x @* B = (A :&: B) :^ x.
-
Variable G :
{group gT}.
+
Variable G :
{group gT}.
-
Lemma injm_conj x :
'injm (conjgm G x).
+
Lemma injm_conj x :
'injm (conjgm G x).
-
Lemma conj_isom x :
isom G (
G :^ x) (
conjgm G x).
+
Lemma conj_isom x :
isom G (
G :^ x) (
conjgm G x).
-
Lemma conj_isog x :
G \isog G :^ x.
+
Lemma conj_isog x :
G \isog G :^ x.
-
Lemma norm_conjg_im x :
x \in 'N(G) → conjgm G x @* G = G.
+
Lemma norm_conjg_im x :
x \in 'N(G) → conjgm G x @* G = G.
-
Lemma norm_conj_isom x :
x \in 'N(G) → isom G G (
conjgm G x).
+
Lemma norm_conj_isom x :
x \in 'N(G) → isom G G (
conjgm G x).
Definition conj_aut x :=
aut (
injm_conj _) (
norm_conjg_im (
subgP (
subg _ x))).
-
Lemma norm_conj_autE :
{in 'N(G) & G, ∀ x y,
conj_aut x y = y ^ x}.
+
Lemma norm_conj_autE :
{in 'N(G) & G, ∀ x y,
conj_aut x y = y ^ x}.
-
Lemma conj_autE :
{in G &, ∀ x y,
conj_aut x y = y ^ x}.
+
Lemma conj_autE :
{in G &, ∀ x y,
conj_aut x y = y ^ x}.
-
Lemma conj_aut_morphM :
{in 'N(G) &, {morph conj_aut : x y / x × y}}.
+
Lemma conj_aut_morphM :
{in 'N(G) &, {morph conj_aut : x y / x × y}}.
Canonical conj_aut_morphism :=
Morphism conj_aut_morphM.
-
Lemma ker_conj_aut :
'ker conj_aut = 'C(G).
+
Lemma ker_conj_aut :
'ker conj_aut = 'C(G).
-
Lemma Aut_conj_aut A :
conj_aut @* A \subset Aut G.
+
Lemma Aut_conj_aut A :
conj_aut @* A \subset Aut G.
End ConjugationMorphism.
@@ -375,20 +374,20 @@
Variable gT :
finGroupType.
-
Implicit Types A B :
{set gT}.
-
Implicit Types G H K L :
{group gT}.
+
Implicit Types A B :
{set gT}.
+
Implicit Types G H K L :
{group gT}.
Definition characteristic A B :=
-
(A \subset B) && [∀ f in Aut B, f @: A \subset A].
+
(A \subset B) && [∀ f in Aut B, f @: A \subset A].
-
Infix "\char" :=
characteristic.
+
Infix "\char" :=
characteristic.
Lemma charP H G :
-
let fixH (
f :
{morphism G >-> gT}) :=
'injm f → f @* G = G → f @* H = H in
-
reflect [/\ H \subset G & ∀ f,
fixH f] (
H \char G).
+
let fixH (
f :
{morphism G >-> gT}) :=
'injm f → f @* G = G → f @* H = H in
+
reflect [/\ H \subset G & ∀ f,
fixH f] (
H \char G).
@@ -399,65 +398,65 @@