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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Additive submonoids of an additive monoid Additive M
are isomorphic to submonoids of M
.
Equations
- AddSubmonoid.toSubmonoid' = Submonoid.toAddSubmonoid.symm
Instances For
Additive submonoids of an additive monoid A
are isomorphic to
multiplicative submonoids of Multiplicative A
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Submonoids of a monoid Multiplicative A
are isomorphic to additive submonoids of A
.
Equations
- Submonoid.toAddSubmonoid' = AddSubmonoid.toSubmonoid.symm
Instances For
The preimage of a submonoid along a monoid homomorphism is a submonoid.
Equations
- Submonoid.comap f S = { carrier := ⇑f ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
The preimage of an AddSubmonoid
along an AddMonoid
homomorphism is an AddSubmonoid
.
Equations
- AddSubmonoid.comap f S = { carrier := ⇑f ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
The image of a submonoid along a monoid homomorphism is a submonoid.
Equations
- Submonoid.map f S = { carrier := ⇑f '' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
The image of an AddSubmonoid
along an AddMonoid
homomorphism is an AddSubmonoid
.
Equations
- AddSubmonoid.map f S = { carrier := ⇑f '' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
map f
and comap f
form a GaloisCoinsertion
when f
is injective.
Equations
- Submonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯
Instances For
map f
and comap f
form a GaloisCoinsertion
when f
is injective.
Equations
- AddSubmonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯
Instances For
map f
and comap f
form a GaloisInsertion
when f
is surjective.
Equations
- Submonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯
Instances For
map f
and comap f
form a GaloisInsertion
when f
is surjective.
Equations
- AddSubmonoid.giMapComap hf = ⋯.toGaloisInsertion ⋯
Instances For
The top submonoid is isomorphic to the monoid.
Equations
Instances For
The top additive submonoid is isomorphic to the additive monoid.
Equations
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.
Equations
- S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_mul' := ⋯ }
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.
Equations
- S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_add' := ⋯ }
Instances For
Given submonoids s
, t
of monoids M
, N
respectively, s × t
as a submonoid
of M × N
.
Instances For
Given AddSubmonoid
s s
, t
of AddMonoid
s A
, B
respectively, s × t
as an AddSubmonoid
of A × B
.
Instances For
The product of submonoids is isomorphic to their product as monoids.
Equations
- s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_mul' := ⋯ }
Instances For
The product of additive submonoids is isomorphic to their product as additive monoids
Equations
- s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_add' := ⋯ }
Instances For
The range of a monoid homomorphism is a submonoid. See Note [range copy pattern].
Equations
- MonoidHom.mrange f = (Submonoid.map f ⊤).copy (Set.range ⇑f) ⋯
Instances For
The range of an AddMonoidHom
is an AddSubmonoid
.
Equations
- AddMonoidHom.mrange f = (AddSubmonoid.map f ⊤).copy (Set.range ⇑f) ⋯
Instances For
The range of a surjective monoid hom is the whole of the codomain.
The range of a surjective AddMonoid
hom is the whole of the codomain.
The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set.
The image under an AddMonoid
hom of the AddSubmonoid
generated by a set equals
the AddSubmonoid
generated by the image of the set.
Restriction of a monoid hom to a submonoid of the domain.
Equations
- f.restrict s = f.comp (SubmonoidClass.subtype s)
Instances For
Restriction of an AddMonoid
hom to an AddSubmonoid
of the domain.
Equations
- f.restrict s = f.comp (AddSubmonoidClass.subtype s)
Instances For
Restriction of a monoid hom to a submonoid of the codomain.
Equations
- f.codRestrict s h = { toFun := fun (n : M) => ⟨f n, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Restriction of an AddMonoid
hom to an AddSubmonoid
of the codomain.
Equations
- f.codRestrict s h = { toFun := fun (n : M) => ⟨f n, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Restriction of a monoid hom to its range interpreted as a submonoid.
Equations
- f.mrangeRestrict = f.codRestrict (MonoidHom.mrange f) ⋯
Instances For
Restriction of an AddMonoid
hom to its range interpreted as a submonoid.
Equations
- f.mrangeRestrict = f.codRestrict (AddMonoidHom.mrange f) ⋯
Instances For
The multiplicative kernel of a monoid hom is the submonoid of elements x : G
such
that f x = 1
Equations
Instances For
The additive kernel of an AddMonoid
hom is the AddSubmonoid
of
elements such that f x = 0
Equations
Instances For
Equations
- MonoidHom.decidableMemMker f x = decidable_of_iff (f x = 1) ⋯
Equations
- AddMonoidHom.decidableMemMker f x = decidable_of_iff (f x = 0) ⋯
The MonoidHom
from the preimage of a submonoid to itself.
Equations
- f.submonoidComap N' = { toFun := fun (x : ↥(Submonoid.comap f N')) => ⟨f ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
Instances For
the AddMonoidHom
from the preimage of an additive submonoid to itself.
Equations
- f.addSubmonoidComap N' = { toFun := fun (x : ↥(AddSubmonoid.comap f N')) => ⟨f ↑x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The MonoidHom
from a submonoid to its image.
See MulEquiv.SubmonoidMap
for a variant for MulEquiv
s.
Equations
- f.submonoidMap M' = { toFun := fun (x : ↥M') => ⟨f ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
Instances For
the AddMonoidHom
from an additive submonoid to its image. See
AddEquiv.AddSubmonoidMap
for a variant for AddEquiv
s.
Equations
- f.addSubmonoidMap M' = { toFun := fun (x : ↥M') => ⟨f ↑x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The monoid hom associated to an inclusion of submonoids.
Equations
- Submonoid.inclusion h = S.subtype.codRestrict T ⋯
Instances For
The AddMonoid
hom associated to an inclusion of submonoids.
Equations
- AddSubmonoid.inclusion h = S.subtype.codRestrict T ⋯
Instances For
A submonoid is either the trivial submonoid or nontrivial.
An additive submonoid is either the trivial additive submonoid or nontrivial.
A submonoid is either the trivial submonoid or contains a nonzero element.
An additive submonoid is either the trivial additive submonoid or contains a nonzero element.
Makes the identity isomorphism from a proof that two submonoids of a multiplicative monoid are equal.
Equations
- MulEquiv.submonoidCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }
Instances For
Makes the identity additive isomorphism from a proof two submonoids of an additive monoid are equal.
Equations
- AddEquiv.addSubmonoidCongr h = { toEquiv := Equiv.setCongr ⋯, map_add' := ⋯ }
Instances For
A monoid homomorphism f : M →* N
with a left-inverse g : N → M
defines a multiplicative
equivalence between M
and f.mrange
.
This is a bidirectional version of MonoidHom.mrange_restrict
.
Equations
- MulEquiv.ofLeftInverse' f h = { toFun := ⇑f.mrangeRestrict, invFun := g ∘ ⇑(MonoidHom.mrange f).subtype, left_inv := h, right_inv := ⋯, map_mul' := ⋯ }
Instances For
An additive monoid homomorphism f : M →+ N
with a left-inverse g : N → M
defines an additive equivalence between M
and f.mrange
.
This is a bidirectional version of AddMonoidHom.mrange_restrict
.
Equations
- AddEquiv.ofLeftInverse' f h = { toFun := ⇑f.mrangeRestrict, invFun := g ∘ ⇑(AddMonoidHom.mrange f).subtype, left_inv := h, right_inv := ⋯, map_add' := ⋯ }
Instances For
A MulEquiv
φ
between two monoids M
and N
induces a MulEquiv
between
a submonoid S ≤ M
and the submonoid φ(S) ≤ N
.
See MonoidHom.submonoidMap
for a variant for MonoidHom
s.
Equations
- e.submonoidMap S = { toEquiv := (↑e).image ↑S, map_mul' := ⋯ }
Instances For
An AddEquiv
φ
between two additive monoids M
and N
induces an AddEquiv
between a submonoid S ≤ M
and the submonoid φ(S) ≤ N
. See
AddMonoidHom.addSubmonoidMap
for a variant for AddMonoidHom
s.
Equations
- e.addSubmonoidMap S = { toEquiv := (↑e).image ↑S, map_add' := ⋯ }
Instances For
Actions by Submonoid
s #
These instances transfer the action by an element m : M
of a monoid M
written as m • a
onto
the action by an element s : S
of a submonoid S : Submonoid M
such that s • a = (s : M) • a
.
These instances work particularly well in conjunction with Monoid.toMulAction
, enabling
s • m
as an alias for ↑s * m
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Note that this provides IsScalarTower S M' M'
which is needed by SMulMulAssoc
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The action by a submonoid is the action by the underlying monoid.
Equations
- S.mulAction = MulAction.compHom α S.subtype
The additive action by an AddSubmonoid
is the action by the underlying AddMonoid
.
Equations
- S.addAction = AddAction.compHom α S.subtype
The multiplicative equivalence between the type of units of M
and the submonoid of unit
elements of M
.
Equations
- Submonoid.unitsTypeEquivIsUnitSubmonoid = { toFun := fun (x : Mˣ) => ⟨↑x, ⋯⟩, invFun := fun (x : ↥(IsUnit.submonoid M)) => IsUnit.unit ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
The additive equivalence between the type of additive units of M
and the additive submonoid whose elements are the additive units of M
.
Equations
- One or more equations did not get rendered due to their size.