Monomorphisms and epimorphisms in Group
#
In this file, we prove monomorphisms in the category of groups are injective homomorphisms and epimorphisms are surjective homomorphisms.
instance
Grp.SurjectiveOfEpiAuxs.instSMulCarrierXWithInfinity
{A B : Grp}
(f : A ⟶ B)
:
SMul (↑B) (XWithInfinity f)
Equations
- One or more equations did not get rendered due to their size.
Let τ
be the permutation on X'
exchanging f.hom.range
and the point at infinity.
Equations
Instances For
Let g : B ⟶ S(X')
be defined as such that, for any β : B
, g(β)
is the function sending
point at infinity to point at infinity and sending coset y
to β • y
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The strategy is the following: assuming epi f