-
Variables (
k :
unit) (
F1 F2 :
object_map).
+
Variables (
k :
unit) (
F1 F2 :
object_map).
-
Definition comp_head :
object_map :=
fun gT A ⇒
let:
tt :=
k in F1 (
F2 A).
+
Definition comp_head :
object_map :=
fun gT A ⇒
let:
tt :=
k in F1 (
F2 A).
Definition modulo :
object_map :=
-
fun gT A ⇒
coset (
F2 A)
@*^-1 (F1 (
A / (F2 A))
).
+
fun gT A ⇒
coset (
F2 A)
@*^-1 (F1 (
A / (F2 A))
).
End Definitions.
@@ -257,25 +256,25 @@
Definition clone_iso (
F :
object_map) :=
fun Fgrp Fsub Fcont (
isoF := @
IsoMap F Fgrp Fsub Fcont) ⇒
-
fun isoF0 &
phant_id (
apply isoF0)
F &
phant_id isoF isoF0 ⇒
isoF.
+
fun isoF0 &
phant_id (
apply isoF0)
F &
phant_id isoF isoF0 ⇒
isoF.
Definition clone (
F :
object_map) :=
-
fun isoF &
phant_id (
apply isoF)
F ⇒
-
fun (
funF0 :
map) &
phant_id (
apply funF0)
F ⇒
-
fun Fcont (
funF := @
Map isoF Fcont) &
phant_id funF0 funF ⇒
funF.
+
fun isoF &
phant_id (
apply isoF)
F ⇒
+
fun (
funF0 :
map) &
phant_id (
apply funF0)
F ⇒
+
fun Fcont (
funF := @
Map isoF Fcont) &
phant_id funF0 funF ⇒
funF.
Definition clone_pmap (
F :
object_map) :=
-
fun (
funF :
map) &
phant_id (
apply funF)
F ⇒
-
fun (
pfunF0 :
pmap) &
phant_id (
apply pfunF0)
F ⇒
-
fun Fher (
pfunF := @
Pmap funF Fher) &
phant_id pfunF0 pfunF ⇒
pfunF.
+
fun (
funF :
map) &
phant_id (
apply funF)
F ⇒
+
fun (
pfunF0 :
pmap) &
phant_id (
apply pfunF0)
F ⇒
+
fun Fher (
pfunF := @
Pmap funF Fher) &
phant_id pfunF0 pfunF ⇒
pfunF.
Definition clone_mono (
F :
object_map) :=
-
fun (
funF :
map) &
phant_id (
apply funF)
F ⇒
-
fun (
mfunF0 :
mono_map) &
phant_id (
apply mfunF0)
F ⇒
-
fun Fmon (
mfunF := @
MonoMap funF Fmon) &
phant_id mfunF0 mfunF ⇒
mfunF.
+
fun (
funF :
map) &
phant_id (
apply funF)
F ⇒
+
fun (
mfunF0 :
mono_map) &
phant_id (
apply mfunF0)
F ⇒
+
fun Fmon (
mfunF := @
MonoMap funF Fmon) &
phant_id mfunF0 mfunF ⇒
mfunF.
End ClassDefinitions.
@@ -294,41 +293,41 @@
Coercion pcontinuous_is_hereditary : pcontinuous >-> hereditary.
-
Notation "[ 'igFun' 'by' Fsub & Fcont ]" :=
+
Notation "[ 'igFun' 'by' Fsub & Fcont ]" :=
(
pack_iso (
continuous_is_iso_continuous Fcont) (
fun gT G ⇒
groupP _)
Fsub)
(
at level 0,
format "[ 'igFun' 'by' Fsub & Fcont ]") :
form_scope.
-
Notation "[ 'igFun' 'by' Fsub & ! Fcont ]" :=
+
Notation "[ 'igFun' 'by' Fsub & ! Fcont ]" :=
(
pack_iso Fcont (
fun gT G ⇒
groupP _)
Fsub)
(
at level 0,
format "[ 'igFun' 'by' Fsub & ! Fcont ]") :
form_scope.
-
Notation "[ 'igFun' 'of' F ]" := (@
clone_iso F _ _ _ _ id id)
+
Notation "[ 'igFun' 'of' F ]" := (@
clone_iso F _ _ _ _ id id)
(
at level 0,
format "[ 'igFun' 'of' F ]") :
form_scope.
-
Notation "[ 'gFun' 'by' Fcont ]" := (
Map Fcont)
+
Notation "[ 'gFun' 'by' Fcont ]" := (
Map Fcont)
(
at level 0,
format "[ 'gFun' 'by' Fcont ]") :
form_scope.
-
Notation "[ 'gFun' 'of' F ]" := (@
clone F _ id _ id _ id)
+
Notation "[ 'gFun' 'of' F ]" := (@
clone F _ id _ id _ id)
(
at level 0,
format "[ 'gFun' 'of' F ]") :
form_scope.
-
Notation "[ 'pgFun' 'by' Fher ]" := (
Pmap Fher)
+
Notation "[ 'pgFun' 'by' Fher ]" := (
Pmap Fher)
(
at level 0,
format "[ 'pgFun' 'by' Fher ]") :
form_scope.
-
Notation "[ 'pgFun' 'of' F ]" := (@
clone_pmap F _ id _ id _ id)
+
Notation "[ 'pgFun' 'of' F ]" := (@
clone_pmap F _ id _ id _ id)
(
at level 0,
format "[ 'pgFun' 'of' F ]") :
form_scope.
-
Notation "[ 'mgFun' 'by' Fmon ]" := (
MonoMap Fmon)
+
Notation "[ 'mgFun' 'by' Fmon ]" := (
MonoMap Fmon)
(
at level 0,
format "[ 'mgFun' 'by' Fmon ]") :
form_scope.
-
Notation "[ 'mgFun' 'of' F ]" := (@
clone_mono F _ id _ id _ id)
+
Notation "[ 'mgFun' 'of' F ]" := (@
clone_mono F _ id _ id _ id)
(
at level 0,
format "[ 'mgFun' 'of' F ]") :
form_scope.
@@ -341,14 +340,14 @@
-
Notation "F1 \o F2" := (
GFunctor.comp_head tt F1 F2) :
gFun_scope.
-
Notation "F1 %% F2" := (
GFunctor.modulo F1 F2) :
gFun_scope.
+
Notation "F1 \o F2" := (
GFunctor.comp_head tt F1 F2) :
gFun_scope.
+
Notation "F1 %% F2" := (
GFunctor.modulo F1 F2) :
gFun_scope.
Section FunctorGroup.
-
Variables (
F :
GFunctor.iso_map) (
gT :
finGroupType) (
G :
{group gT}).
+
Variables (
F :
GFunctor.iso_map) (
gT :
finGroupType) (
G :
{group gT}).
Lemma gFgroupset :
group_set (
F gT G).
Canonical gFgroup :=
Group gFgroupset.
@@ -358,8 +357,8 @@
Canonical gFmod_group
(
F1 :
GFunctor.iso_map) (
F2 :
GFunctor.object_map)
- (
gT :
finGroupType) (
G :
{group gT}) :=
-
[group of (
F1 %% F2)%
gF gT G].
+ (
gT :
finGroupType) (
G :
{group gT}) :=
+
[group of (
F1 %% F2)%
gF gT G].
Section IsoFunctorTheory.
@@ -369,55 +368,55 @@
Variable F :
GFunctor.iso_map.
-
Lemma gFsub gT (
G :
{group gT}) :
F gT G \subset G.
+
Lemma gFsub gT (
G :
{group gT}) :
F gT G \subset G.
-
Lemma gFsub_trans gT (
G :
{group gT}) (
A :
pred_class) :
-
G \subset A → F gT G \subset A.
+
Lemma gFsub_trans gT (
G :
{group gT}) (
A :
{pred gT}) :
+
G \subset A → F gT G \subset A.
-
Lemma gF1 gT :
F gT 1
= 1.
+
Lemma gF1 gT :
F gT 1
= 1.
Lemma gFiso_cont :
GFunctor.iso_continuous F.
-
Lemma gFchar gT (
G :
{group gT}) :
F gT G \char G.
+
Lemma gFchar gT (
G :
{group gT}) :
F gT G \char G.
-
Lemma gFnorm gT (
G :
{group gT}) :
G \subset 'N(F gT G).
+
Lemma gFnorm gT (
G :
{group gT}) :
G \subset 'N(F gT G).
-
Lemma gFnorms gT (
G :
{group gT}) :
'N(G) \subset 'N(F gT G).
+
Lemma gFnorms gT (
G :
{group gT}) :
'N(G) \subset 'N(F gT G).
-
Lemma gFnormal gT (
G :
{group gT}) :
F gT G <| G.
+
Lemma gFnormal gT (
G :
{group gT}) :
F gT G <| G.
-
Lemma gFchar_trans gT (
G H :
{group gT}) :
H \char G → F gT H \char G.
+
Lemma gFchar_trans gT (
G H :
{group gT}) :
H \char G → F gT H \char G.
-
Lemma gFnormal_trans gT (
G H :
{group gT}) :
H <| G → F gT H <| G.
+
Lemma gFnormal_trans gT (
G H :
{group gT}) :
H <| G → F gT H <| G.
-
Lemma gFnorm_trans gT (
A :
pred_class) (
G :
{group gT}) :
-
A \subset 'N(G) → A \subset 'N(F gT G).
+
Lemma gFnorm_trans gT (
A :
{pred gT}) (
G :
{group gT}) :
+
A \subset 'N(G) → A \subset 'N(F gT G).
-
Lemma injmF_sub gT rT (
G D :
{group gT}) (
f :
{morphism D >-> rT}) :
-
'injm f → G \subset D → f @* (F gT G) \subset F rT (
f @* G).
+
Lemma injmF_sub gT rT (
G D :
{group gT}) (
f :
{morphism D >-> rT}) :
+
'injm f → G \subset D → f @* (F gT G) \subset F rT (
f @* G).
-
Lemma injmF gT rT (
G D :
{group gT}) (
f :
{morphism D >-> rT}) :
-
'injm f → G \subset D → f @* (F gT G) = F rT (
f @* G).
+
Lemma injmF gT rT (
G D :
{group gT}) (
f :
{morphism D >-> rT}) :
+
'injm f → G \subset D → f @* (F gT G) = F rT (
f @* G).
-
Lemma gFisom gT rT (
G D :
{group gT})
R (
f :
{morphism D >-> rT}) :
-
G \subset D → isom G (
gval R)
f → isom (
F gT G) (
F rT R)
f.
+
Lemma gFisom gT rT (
G D :
{group gT})
R (
f :
{morphism D >-> rT}) :
+
G \subset D → isom G (
gval R)
f → isom (
F gT G) (
F rT R)
f.
-
Lemma gFisog gT rT (
G :
{group gT}) (
R :
{group rT}) :
-
G \isog R → F gT G \isog F rT R.
+
Lemma gFisog gT rT (
G :
{group gT}) (
R :
{group rT}) :
+
G \isog R → F gT G \isog F rT R.
End IsoFunctorTheory.
@@ -433,8 +432,8 @@
Lemma gFcont :
GFunctor.continuous F.
-
Lemma morphimF gT rT (
G D :
{group gT}) (
f :
{morphism D >-> rT}) :
-
G \subset D → f @* (F gT G) \subset F rT (
f @* G).
+
Lemma morphimF gT rT (
G D :
{group gT}) (
f :
{morphism D >-> rT}) :
+
G \subset D → f @* (F gT G) \subset F rT (
f @* G).
End FunctorTheory.
@@ -455,14 +454,14 @@
Lemma gFhereditary :
GFunctor.hereditary F.
-
Lemma gFunctorI gT (
G H :
{group gT}) :
-
F gT G :&: H = F gT G :&: F gT (
G :&: H).
+
Lemma gFunctorI gT (
G H :
{group gT}) :
+
F gT G :&: H = F gT G :&: F gT (
G :&: H).
Lemma pmorphimF :
GFunctor.pcontinuous F.
-
Lemma gFid gT (
G :
{group gT}) :
F gT (
F gT G)
= F gT G.
+
Lemma gFid gT (
G :
{group gT}) :
F gT (
F gT G)
= F gT G.
End BasicTheory.
@@ -474,14 +473,14 @@
Variables (
F1 :
GFunctor.pmap) (
F2 :
GFunctor.map).
-
Lemma gFmod_closed :
GFunctor.closed (
F1 %% F2).
+
Lemma gFmod_closed :
GFunctor.closed (
F1 %% F2).
-
Lemma gFmod_cont :
GFunctor.continuous (
F1 %% F2).
+
Lemma gFmod_cont :
GFunctor.continuous (
F1 %% F2).
-
Canonical gFmod_igFun :=
[igFun by gFmod_closed & gFmod_cont].
-
Canonical gFmod_gFun :=
[gFun by gFmod_cont].
+
Canonical gFmod_igFun :=
[igFun by gFmod_closed & gFmod_cont].
+
Canonical gFmod_gFun :=
[gFun by gFmod_cont].
End Modulo.
@@ -490,10 +489,10 @@
Variables F1 F2 :
GFunctor.pmap.
-
Lemma gFmod_hereditary :
GFunctor.hereditary (
F1 %% F2).
+
Lemma gFmod_hereditary :
GFunctor.hereditary (
F1 %% F2).
-
Canonical gFmod_pgFun :=
[pgFun by gFmod_hereditary].
+
Canonical gFmod_pgFun :=
[pgFun by gFmod_hereditary].
End PartialFunctorTheory.
@@ -514,14 +513,14 @@
Variables (
F1 :
GFunctor.mono_map) (
F2 :
GFunctor.map).
-
Lemma gFcomp_closed :
GFunctor.closed (
F1 \o F2).
+
Lemma gFcomp_closed :
GFunctor.closed (
F1 \o F2).
-
Lemma gFcomp_cont :
GFunctor.continuous (
F1 \o F2).
+
Lemma gFcomp_cont :
GFunctor.continuous (
F1 \o F2).
-
Canonical gFcomp_igFun :=
[igFun by gFcomp_closed & gFcomp_cont].
-
Canonical gFcomp_gFun :=
[gFun by gFcomp_cont].
+
Canonical gFcomp_igFun :=
[igFun by gFcomp_closed & gFcomp_cont].
+
Canonical gFcomp_gFun :=
[gFun by gFcomp_cont].
End Composition.
@@ -530,10 +529,10 @@
Variables F1 F2 :
GFunctor.mono_map.
-
Lemma gFcompS :
GFunctor.monotonic (
F1 \o F2).
+
Lemma gFcompS :
GFunctor.monotonic (
F1 \o F2).
-
Canonical gFcomp_mgFun :=
[mgFun by gFcompS].
+
Canonical gFcomp_mgFun :=
[mgFun by gFcompS].
End MonotonicFunctorTheory.
@@ -545,7 +544,7 @@
Implicit Types gT :
finGroupType.
-
Definition idGfun gT :=
@id {set gT}.
+
Definition idGfun gT :=
@id {set gT}.
Lemma idGfun_closed :
GFunctor.closed idGfun.
@@ -553,20 +552,20 @@
Lemma idGfun_monotonic :
GFunctor.monotonic idGfun.
-
Canonical bgFunc_id :=
[igFun by idGfun_closed & idGfun_cont].
-
Canonical gFunc_id :=
[gFun by idGfun_cont].
-
Canonical mgFunc_id :=
[mgFun by idGfun_monotonic].
+
Canonical bgFunc_id :=
[igFun by idGfun_closed & idGfun_cont].
+
Canonical gFunc_id :=
[gFun by idGfun_cont].
+
Canonical mgFunc_id :=
[mgFun by idGfun_monotonic].
-
Definition trivGfun gT of {set gT} :=
[1 gT].
+
Definition trivGfun gT of {set gT} :=
[1 gT].
Lemma trivGfun_cont :
GFunctor.pcontinuous trivGfun.
-
Canonical trivGfun_igFun :=
[igFun by sub1G & trivGfun_cont].
-
Canonical trivGfun_gFun :=
[gFun by trivGfun_cont].
-
Canonical trivGfun_pgFun :=
[pgFun by trivGfun_cont].
+
Canonical trivGfun_igFun :=
[igFun by sub1G & trivGfun_cont].
+
Canonical trivGfun_gFun :=
[gFun by trivGfun_cont].
+
Canonical trivGfun_pgFun :=
[pgFun by trivGfun_cont].
End GFunctorExamples.
--
cgit v1.2.3