Library Coq.Classes.Functions
Require
Import
Coq.Classes.RelationClasses
.
Require
Import
Coq.Classes.Morphisms
.
Class
Injective
`(
m
:
Morphism
(
A
->
B
) (
RA
++>
RB
)
f
) :
Prop
:=
injective
:
forall
x
y
:
A
,
RB
(
f
x
) (
f
y
) ->
RA
x
y
.
Class
Surjective
`(
m
:
Morphism
(
A
->
B
) (
RA
++>
RB
)
f
) :
Prop
:=
surjective
:
forall
y
,
exists
x
:
A
,
RB
y
(
f
x
).
Definition
Bijective
`(
m
:
Morphism
(
A
->
B
) (
RA
++>
RB
) (
f
:
A
->
B
)) :=
Injective
m
/\
Surjective
m
.
Class
MonoMorphism
`(
m
:
Morphism
(
A
->
B
) (
eqA
++>
eqB
)) :=
monic
:>
Injective
m
.
Class
EpiMorphism
`(
m
:
Morphism
(
A
->
B
) (
eqA
++>
eqB
)) :=
epic
:>
Surjective
m
.
Class
IsoMorphism
`(
m
:
Morphism
(
A
->
B
) (
eqA
++>
eqB
)) :=
{
monomorphism
:>
MonoMorphism
m
;
epimorphism
:>
EpiMorphism
m
}.
Class
AutoMorphism
`(
m
:
Morphism
(
A
->
A
) (
eqA
++>
eqA
)) {
I
:
IsoMorphism
m
}.