Operations on Submonoid
s #
In this file we define various operations on Submonoid
s and MonoidHom
s.
Main definitions #
Conversion between multiplicative and additive definitions #
Submonoid.toAddSubmonoid
,Submonoid.toAddSubmonoid'
,AddSubmonoid.toSubmonoid
,AddSubmonoid.toSubmonoid'
: convert between multiplicative and additive submonoids ofM
,Multiplicative M
, andAdditive M
. These are stated asOrderIso
s.
(Commutative) monoid structure on a submonoid #
Submonoid.toMonoid
,Submonoid.toCommMonoid
: a submonoid inherits a (commutative) monoid structure.
Group actions by submonoids #
Submonoid.MulAction
,Submonoid.DistribMulAction
: a submonoid inherits (distributive) multiplicative actions.
Operations on submonoids #
Submonoid.comap
: preimage of a submonoid under a monoid homomorphism as a submonoid of the domain;Submonoid.map
: image of a submonoid under a monoid homomorphism as a submonoid of the codomain;Submonoid.prod
: product of two submonoidss : Submonoid M
andt : Submonoid N
as a submonoid ofM × N
;
Monoid homomorphisms between submonoid #
Submonoid.subtype
: embedding of a submonoid into the ambient monoid.Submonoid.inclusion
: given two submonoidsS
,T
such thatS ≤ T
,S.inclusion T
is the inclusion ofS
intoT
as a monoid homomorphism;MulEquiv.submonoidCongr
: converts a proof ofS = T
into a monoid isomorphism betweenS
andT
.Submonoid.prodEquiv
: monoid isomorphism betweens.prod t
ands × t
;
Operations on MonoidHom
s #
MonoidHom.mrange
: range of a monoid homomorphism as a submonoid of the codomain;MonoidHom.mker
: kernel of a monoid homomorphism as a submonoid of the domain;MonoidHom.restrict
: restrict a monoid homomorphism to a submonoid;MonoidHom.codRestrict
: restrict the codomain of a monoid homomorphism to a submonoid;MonoidHom.mrangeRestrict
: restrict a monoid homomorphism to its range;
Tags #
submonoid, range, product, map, comap
Conversion to/from Additive
/Multiplicative
#
Submonoids of monoid M
are isomorphic to additive submonoids of Additive M
.
Instances For
Additive submonoids of an additive monoid Additive M
are isomorphic to submonoids of M
.
Instances For
Additive submonoids of an additive monoid A
are isomorphic to
multiplicative submonoids of Multiplicative A
.
Instances For
Submonoids of a monoid Multiplicative A
are isomorphic to additive submonoids of A
.
Instances For
The preimage of an AddSubmonoid
along an AddMonoid
homomorphism is an AddSubmonoid
.
Instances For
The preimage of a submonoid along a monoid homomorphism is a submonoid.
Instances For
The image of an AddSubmonoid
along an AddMonoid
homomorphism is an AddSubmonoid
.
Instances For
The image of a submonoid along a monoid homomorphism is a submonoid.
Instances For
Instances For
map f
and comap f
form a GaloisCoinsertion
when f
is injective.
Instances For
map f
and comap f
form a GaloisCoinsertion
when f
is injective.
Instances For
map f
and comap f
form a GaloisInsertion
when f
is surjective.
Instances For
Instances For
map f
and comap f
form a GaloisInsertion
when f
is surjective.
Instances For
An AddSubmonoid
of an AddMonoid
inherits a zero.
A submonoid of a monoid inherits a 1.
An AddSubmonoid
of an AddMonoid
inherits a scalar multiplication.
A submonoid of a monoid inherits a power operator.
An AddSubmonoid
of a unital additive magma inherits a unital additive magma structure.
A submonoid of a unital magma inherits a unital magma structure.
An AddSubmonoid
of an AddMonoid
inherits an AddMonoid
structure.
A submonoid of a monoid inherits a monoid structure.
An AddSubmonoid
of an AddCommMonoid
is an AddCommMonoid
.
A submonoid of a CommMonoid
is a CommMonoid
.
An AddSubmonoid
of an OrderedAddCommMonoid
is an OrderedAddCommMonoid
.
A submonoid of an OrderedCommMonoid
is an OrderedCommMonoid
.
An AddSubmonoid
of a LinearOrderedAddCommMonoid
is a LinearOrderedAddCommMonoid
.
A submonoid of a LinearOrderedCommMonoid
is a LinearOrderedCommMonoid
.
An AddSubmonoid
of an OrderedCancelAddCommMonoid
is an OrderedCancelAddCommMonoid
.
A submonoid of an OrderedCancelCommMonoid
is an OrderedCancelCommMonoid
.
An AddSubmonoid
of a LinearOrderedCancelAddCommMonoid
is
a LinearOrderedCancelAddCommMonoid
.
A submonoid of a LinearOrderedCancelCommMonoid
is a LinearOrderedCancelCommMonoid
.
The natural monoid hom from an AddSubmonoid
of AddMonoid
M
to M
.
Instances For
The natural monoid hom from a submonoid of monoid M
to M
.
Instances For
An AddSubmonoid
of an AddMonoid
inherits an addition.
A submonoid of a monoid inherits a multiplication.
An AddSubmonoid
of an AddMonoid
inherits a zero.
A submonoid of a monoid inherits a 1.
An AddSubmonoid
of a unital additive magma inherits a unital additive magma structure.
A submonoid of a unital magma inherits a unital magma structure.
An AddSubmonoid
of an AddMonoid
inherits an AddMonoid
structure.
An AddSubmonoid
of an AddCommMonoid
is an AddCommMonoid
.
A submonoid of a CommMonoid
is a CommMonoid
.
An AddSubmonoid
of an OrderedAddCommMonoid
is an OrderedAddCommMonoid
.
A submonoid of an OrderedCommMonoid
is an OrderedCommMonoid
.
An AddSubmonoid
of a LinearOrderedAddCommMonoid
is a LinearOrderedAddCommMonoid
.
A submonoid of a LinearOrderedCommMonoid
is a LinearOrderedCommMonoid
.
An AddSubmonoid
of an OrderedCancelAddCommMonoid
is an OrderedCancelAddCommMonoid
.
A submonoid of an OrderedCancelCommMonoid
is an OrderedCancelCommMonoid
.
An AddSubmonoid
of a LinearOrderedCancelAddCommMonoid
is
a LinearOrderedCancelAddCommMonoid
.
A submonoid of a LinearOrderedCancelCommMonoid
is a LinearOrderedCancelCommMonoid
.
The natural monoid hom from an AddSubmonoid
of AddMonoid
M
to M
.
Instances For
The natural monoid hom from a submonoid of monoid M
to M
.
Instances For
The top additive submonoid is isomorphic to the additive monoid.
Instances For
The top submonoid is isomorphic to the monoid.
Instances For
An additive subgroup is isomorphic to its image under an injective function. If you
have an isomorphism, use AddEquiv.addSubmonoidMap
for better definitional equalities.
Instances For
A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
use MulEquiv.submonoidMap
for better definitional equalities.
Instances For
Given AddSubmonoid
s s
, t
of AddMonoid
s A
, B
respectively, s × t
as an AddSubmonoid
of A × B
.
Instances For
Given submonoids s
, t
of monoids M
, N
respectively, s × t
as a submonoid
of M × N
.
Instances For
The product of additive submonoids is isomorphic to their product as additive monoids
Instances For
The product of submonoids is isomorphic to their product as monoids.
Instances For
Instances For
Instances For
Instances For
Instances For
The range of an AddMonoidHom
is an AddSubmonoid
.
Instances For
The range of a monoid homomorphism is a submonoid. See Note [range copy pattern].
Instances For
The range of a surjective AddMonoid
hom is the whole of the codomain.
The range of a surjective monoid hom is the whole of the codomain.
The image under an AddMonoid
hom of the AddSubmonoid
generated by a set equals
the AddSubmonoid
generated by the image of the set.
The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set.
Restriction of an AddMonoid
hom to an AddSubmonoid
of the domain.
Instances For
Restriction of a monoid hom to a submonoid of the domain.
Instances For
Restriction of an AddMonoid
hom to an AddSubmonoid
of the codomain.
Instances For
Restriction of a monoid hom to a submonoid of the codomain.
Instances For
Restriction of an AddMonoid
hom to its range interpreted as a submonoid.
Instances For
Restriction of a monoid hom to its range interpreted as a submonoid.
Instances For
Instances For
The additive kernel of an AddMonoid
hom is the AddSubmonoid
of
elements such that f x = 0
Instances For
The multiplicative kernel of a monoid hom is the submonoid of elements x : G
such
that f x = 1