Adjoining a zero/one to semigroups and related algebraic structures #
This file contains different results about adjoining an element to an algebraic structure which then
behaves like a zero or a one. An example is adjoining a one to a semigroup to obtain a monoid. That
this provides an example of an adjunction is proved in Algebra.Category.MonCat.Adjunctions
.
Another result says that adjoining to a group an element zero
gives a GroupWithZero
. For more
information about these structures (which are not that standard in informal mathematics, see
Algebra.GroupWithZero.Basic
)
Porting notes #
In Lean 3, we use id
here and there to get correct types of proofs. This is required because
WithOne
and WithZero
are marked as Irreducible
at the end of algebra.group.with_one.defs
,
so proofs that use Option α
instead of WithOne α
no longer typecheck. In Lean 4, both types are
plain def
s, so we don't need these id
s.
The canonical map from α
into WithZero α
Instances For
The canonical map from α
into WithOne α
Instances For
if G
is a group then WithZero G
is a group with zero.