-
Definition morphism_for D of phant rT :=
morphism D.
+
Definition morphism_for D of phant rT :=
morphism D.
Definition clone_morphism D f :=
let:
Morphism _ fM :=
f
-
return {type of @
Morphism D for f} → morphism_for D (
Phant rT)
+
return {type of @
Morphism D for f} → morphism_for D (
Phant rT)
in fun k ⇒
k fM.
-
Variables (
D A :
{set aT}) (
R :
{set rT}) (
x :
aT) (
y :
rT) (
f :
aT → rT).
+
Variables (
D A :
{set aT}) (
R :
{set rT}) (
x :
aT) (
y :
rT) (
f :
aT → rT).
-
CoInductive morphim_spec :
Prop :=
MorphimSpec z &
z \in D &
z \in A &
y = f z.
+
Variant morphim_spec :
Prop :=
MorphimSpec z &
z \in D &
z \in A &
y = f z.
-
Lemma morphimP :
reflect morphim_spec (
y \in f @: (D :&: A)).
+
Lemma morphimP :
reflect morphim_spec (
y \in f @: (D :&: A)).
-
Lemma morphpreP :
reflect (
x \in D ∧ f x \in R) (
x \in D :&: f @^-1: R).
+
Lemma morphpreP :
reflect (
x \in D ∧ f x \in R) (
x \in D :&: f @^-1: R).
End MorphismStructure.
-
Notation "{ 'morphism' D >-> T }" := (
morphism_for D (
Phant T))
+
Notation "{ 'morphism' D >-> T }" := (
morphism_for D (
Phant T))
(
at level 0,
format "{ 'morphism' D >-> T }") :
group_scope.
-
Notation "[ 'morphism' D 'of' f ]" :=
+
Notation "[ 'morphism' D 'of' f ]" :=
(@
clone_morphism _ _ D _ (
fun fM ⇒ @
Morphism _ _ D f fM))
(
at level 0,
format "[ 'morphism' D 'of' f ]") :
form_scope.
-
Notation "[ 'morphism' 'of' f ]" := (
clone_morphism (@
Morphism _ _ _ f))
+
Notation "[ 'morphism' 'of' f ]" := (
clone_morphism (@
Morphism _ _ _ f))
(
at level 0,
format "[ 'morphism' 'of' f ]") :
form_scope.
@@ -178,23 +177,23 @@
Section MorphismOps1.
-
Variables (
aT rT :
finGroupType) (
D :
{set aT}) (
f :
{morphism D >-> rT}).
+
Variables (
aT rT :
finGroupType) (
D :
{set aT}) (
f :
{morphism D >-> rT}).
-
Lemma morphM :
{in D &, {morph f : x y / x × y}}.
+
Lemma morphM :
{in D &, {morph f : x y / x × y}}.
-
Notation morPhantom := (
phantom (
aT → rT)).
-
Definition MorPhantom :=
Phantom (
aT → rT).
+
Notation morPhantom := (
phantom (
aT → rT)).
+
Definition MorPhantom :=
Phantom (
aT → rT).
Definition dom of morPhantom f :=
D.
-
Definition morphim of morPhantom f :=
fun A ⇒
f @: (D :&: A).
+
Definition morphim of morPhantom f :=
fun A ⇒
f @: (D :&: A).
-
Definition morphpre of morPhantom f :=
fun R :
{set rT} ⇒
D :&: f @^-1: R.
+
Definition morphpre of morPhantom f :=
fun R :
{set rT} ⇒
D :&: f @^-1: R.
Definition ker mph :=
morphpre mph 1.
@@ -205,28 +204,28 @@
-
Notation "''dom' f" := (
dom (
MorPhantom f))
+
Notation "''dom' f" := (
dom (
MorPhantom f))
(
at level 10,
f at level 8,
format "''dom' f") :
group_scope.
-
Notation "''ker' f" := (
ker (
MorPhantom f))
+
Notation "''ker' f" := (
ker (
MorPhantom f))
(
at level 10,
f at level 8,
format "''ker' f") :
group_scope.
-
Notation "''ker_' H f" := (
H :&: 'ker f)
+
Notation "''ker_' H f" := (
H :&: 'ker f)
(
at level 10,
H at level 2,
f at level 8,
format "''ker_' H f")
:
group_scope.
-
Notation "f @* A" := (
morphim (
MorPhantom f)
A)
+
Notation "f @* A" := (
morphim (
MorPhantom f)
A)
(
at level 24,
format "f @* A") :
group_scope.
-
Notation "f @*^-1 R" := (
morphpre (
MorPhantom f)
R)
+
Notation "f @*^-1 R" := (
morphpre (
MorPhantom f)
R)
(
at level 24,
format "f @*^-1 R") :
group_scope.
-
Notation "''injm' f" := (
pred_of_set (
'ker f)
\subset pred_of_set 1)
+
Notation "''injm' f" := (
pred_of_set (
'ker f)
\subset pred_of_set 1)
(
at level 10,
f at level 8,
format "''injm' f") :
group_scope.
@@ -234,10 +233,10 @@
Variables aT rT :
finGroupType.
-
Implicit Types A B :
{set aT}.
-
Implicit Types G H :
{group aT}.
-
Implicit Types R S :
{set rT}.
-
Implicit Types M :
{group rT}.
+
Implicit Types A B :
{set aT}.
+
Implicit Types G H :
{group aT}.
+
Implicit Types R S :
{set rT}.
+
Implicit Types M :
{group rT}.
@@ -246,27 +245,27 @@
Most properties of morphims hold only when the domain is a group.