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× N
;
Monoid homomorphisms between submonoid #
Submonoid.subtype
: embedding of a submonoid into the ambient monoid.Submonoid.inclusion
: given two submonoidsS
,T
such thatS ≤ T≤ 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× 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.
Additive submonoids of an additive monoid Additive M
are isomorphic to submonoids of M
.
Equations
- AddSubmonoid.toSubmonoid' = OrderIso.symm Submonoid.toAddSubmonoid
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.
Submonoids of a monoid Multiplicative A
are isomorphic to additive submonoids of A
.
Equations
- Submonoid.toAddSubmonoid' = OrderIso.symm AddSubmonoid.toSubmonoid
The preimage of an AddSubmonoid
along an AddMonoid
homomorphism is an AddSubmonoid
.
The preimage of a submonoid along a monoid homomorphism is a submonoid.
The image of an AddSubmonoid
along an AddMonoid
homomorphism is an AddSubmonoid
.
Equations
- One or more equations did not get rendered due to their size.
The image of a submonoid along a monoid homomorphism is a submonoid.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : x ∈ AddSubmonoid.comap f (AddSubmonoid.map f S) → x ∈ S) = (_ : x ∈ AddSubmonoid.comap f (AddSubmonoid.map f S) → x ∈ S)
map f
and comap f
form a GaloisCoinsertion
when f
is injective.
Equations
- One or more equations did not get rendered due to their size.
map f
and comap f
form a GaloisCoinsertion
when f
is injective.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : x ∈ AddSubmonoid.map f (AddSubmonoid.comap f S)) = (_ : x ∈ AddSubmonoid.map f (AddSubmonoid.comap f S))
map f
and comap f
form a GaloisInsertion
when f
is surjective.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddSubmonoid.giMapComap.match_1 x motive x h_1 = Exists.casesOn x fun w h => h_1 w h
map f
and comap f
form a GaloisInsertion
when f
is surjective.
Equations
- One or more equations did not get rendered due to their size.
An AddSubmonoid
of an AddMonoid
inherits a zero.
Equations
- ZeroMemClass.zero S' = { zero := { val := 0, property := (_ : 0 ∈ S') } }
A submonoid of a monoid inherits a 1.
Equations
- OneMemClass.one S' = { one := { val := 1, property := (_ : 1 ∈ S') } }
An AddSubmonoid
of an AddMonoid
inherits a scalar multiplication.
Equations
- AddSubmonoidClass.nSMul S = { smul := fun n a => { val := n • ↑a, property := (_ : n • ↑a ∈ S) } }
A submonoid of a monoid inherits a power operator.
Equations
- SubmonoidClass.nPow S = { pow := fun a n => { val := ↑a ^ n, property := (_ : ↑a ^ n ∈ S) } }
An AddSubmonoid
of an unital additive magma inherits an unital additive magma structure.
Equations
- AddSubmonoidClass.toAddZeroClass S = Function.Injective.addZeroClass Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ↑0 = ↑0) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1))
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
A submonoid of a unital magma inherits a unital magma structure.
Equations
- SubmonoidClass.toMulOneClass S = Function.Injective.mulOneClass Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ↑1 = ↑1) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x * x_1) = ↑(x * x_1))
An AddSubmonoid
of an AddMonoid
inherits an AddMonoid
structure.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
A submonoid of a monoid inherits a monoid structure.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
An AddSubmonoid
of an AddCommMonoid
is an AddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)
A submonoid of a CommMonoid
is a CommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
An AddSubmonoid
of an OrderedAddCommMonoid
is an OrderedAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
Equations
- (_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)
A submonoid of an OrderedCommMonoid
is an OrderedCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
An AddSubmonoid
of a LinearOrderedAddCommMonoid
is a LinearOrderedAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)
A submonoid of a LinearOrderedCommMonoid
is a LinearOrderedCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
An AddSubmonoid
of an OrderedCancelAddCommMonoid
is an OrderedCancelAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)
A submonoid of an OrderedCancelCommMonoid
is an OrderedCancelCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
An AddSubmonoid
of a LinearOrderedCancelAddCommMonoid
is
a LinearOrderedCancelAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
Equations
- (_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)
A submonoid of a LinearOrderedCancelCommMonoid
is a LinearOrderedCancelCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
The natural monoid hom from an AddSubmonoid
of AddMonoid
M
to M
.
The natural monoid hom from a submonoid of monoid M
to M
.
An AddSubmonoid
of an AddMonoid
inherits an addition.
Equations
- AddSubmonoid.add S = { add := fun a b => { val := ↑a + ↑b, property := (_ : ↑a + ↑b ∈ S) } }
A submonoid of a monoid inherits a multiplication.
Equations
- Submonoid.mul S = { mul := fun a b => { val := ↑a * ↑b, property := (_ : ↑a * ↑b ∈ S) } }
An AddSubmonoid
of an AddMonoid
inherits a zero.
Equations
- AddSubmonoid.zero S = { zero := { val := 0, property := (_ : 0 ∈ S) } }
A submonoid of a monoid inherits a 1.
Equations
- Submonoid.one S = { one := { val := 1, property := (_ : 1 ∈ S) } }
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
An AddSubmonoid
of an unital additive magma inherits an unital additive magma structure.
Equations
- AddSubmonoid.toAddZeroClass S = Function.Injective.addZeroClass Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ↑0 = ↑0) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1))
A submonoid of a unital magma inherits a unital magma structure.
Equations
- Submonoid.toMulOneClass S = Function.Injective.mulOneClass Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ↑1 = ↑1) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x * x_1) = ↑(x * x_1))
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
Equations
- (_ : AddSubmonoidClass (AddSubmonoid M) M) = (_ : AddSubmonoidClass (AddSubmonoid M) M)
An AddSubmonoid
of an AddMonoid
inherits an AddMonoid
structure.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
Equations
- (_ : AddSubmonoidClass (AddSubmonoid M) M) = (_ : AddSubmonoidClass (AddSubmonoid M) M)
An AddSubmonoid
of an AddCommMonoid
is an AddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
A submonoid of a CommMonoid
is a CommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : AddSubmonoidClass (AddSubmonoid M) M) = (_ : AddSubmonoidClass (AddSubmonoid M) M)
An AddSubmonoid
of an OrderedAddCommMonoid
is an OrderedAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
A submonoid of an OrderedCommMonoid
is an OrderedCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
Equations
- (_ : AddSubmonoidClass (AddSubmonoid M) M) = (_ : AddSubmonoidClass (AddSubmonoid M) M)
An AddSubmonoid
of a LinearOrderedAddCommMonoid
is a LinearOrderedAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
A submonoid of a LinearOrderedCommMonoid
is a LinearOrderedCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : AddSubmonoidClass (AddSubmonoid M) M) = (_ : AddSubmonoidClass (AddSubmonoid M) M)
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
An AddSubmonoid
of an OrderedCancelAddCommMonoid
is an OrderedCancelAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
A submonoid of an OrderedCancelCommMonoid
is an OrderedCancelCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)
An AddSubmonoid
of a LinearOrderedCancelAddCommMonoid
is
a LinearOrderedCancelAddCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : AddSubmonoidClass (AddSubmonoid M) M) = (_ : AddSubmonoidClass (AddSubmonoid M) M)
A submonoid of a LinearOrderedCancelCommMonoid
is a LinearOrderedCancelCommMonoid
.
Equations
- One or more equations did not get rendered due to their size.
The natural monoid hom from an AddSubmonoid
of AddMonoid
M
to M
.
The natural monoid hom from a submonoid of monoid M
to M
.
The top additive submonoid is isomorphic to the additive monoid.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The top submonoid is isomorphic to the monoid.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
use MulEquiv.submonoidMap
for better definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
Given AddSubmonoid
s s
, t
of AddMonoid
s A
, B
respectively, s × t× t
as an AddSubmonoid
of A × B× B
.
Equations
- One or more equations did not get rendered due to their size.
Given submonoids s
, t
of monoids M
, N
respectively, s × t× t
as a submonoid
of M × N× N
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun) = (_ : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun)
The product of additive submonoids is isomorphic to their product as additive monoids
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun) = (_ : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun)
Equations
- One or more equations did not get rendered due to their size.
The product of submonoids is isomorphic to their product as monoids.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddSubmonoid.map_inl.match_1 s p motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right
Equations
- AddSubmonoid.map_inl.match_2 s p motive x h_1 = And.casesOn x fun left right => h_1 left right
Equations
- AddSubmonoid.map_inr.match_2 s p motive x h_1 = And.casesOn x fun left right => h_1 left right
Equations
- AddSubmonoid.map_inr.match_1 s p motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right