Operations on Subsemigroup
s #
In this file we define various operations on Subsemigroup
s and MulHom
s.
Main definitions #
Conversion between multiplicative and additive definitions #
Subsemigroup.toAddSubsemigroup
,Subsemigroup.toAddSubsemigroup'
,AddSubsemigroup.toSubsemigroup
,AddSubsemigroup.toSubsemigroup'
: convert between multiplicative and additive subsemigroups ofM
,Multiplicative M
, andAdditive M
. These are stated asOrderIso
s.
(Commutative) semigroup structure on a subsemigroup #
Subsemigroup.toSemigroup
,Subsemigroup.toCommSemigroup
: a subsemigroup inherits a (commutative) semigroup structure.
Operations on subsemigroups #
Subsemigroup.comap
: preimage of a subsemigroup under a semigroup homomorphism as a subsemigroup of the domain;Subsemigroup.map
: image of a subsemigroup under a semigroup homomorphism as a subsemigroup of the codomain;Subsemigroup.prod
: product of two subsemigroupss : Subsemigroup M
andt : Subsemigroup N
as a subsemigroup ofM × N
;
Semigroup homomorphisms between subsemigroups #
Subsemigroup.subtype
: embedding of a subsemigroup into the ambient semigroup.Subsemigroup.inclusion
: given two subsemigroupsS
,T
such thatS ≤ T
,S.inclusion T
is the inclusion ofS
intoT
as a semigroup homomorphism;MulEquiv.subsemigroupCongr
: converts a proof ofS = T
into a semigroup isomorphism betweenS
andT
.Subsemigroup.prodEquiv
: semigroup isomorphism betweens.prod t
ands × t
;
Operations on MulHom
s #
MulHom.srange
: range of a semigroup homomorphism as a subsemigroup of the codomain;MulHom.restrict
: restrict a semigroup homomorphism to a subsemigroup;MulHom.codRestrict
: restrict the codomain of a semigroup homomorphism to a subsemigroup;MulHom.srangeRestrict
: restrict a semigroup homomorphism to its range;
Implementation notes #
This file follows closely GroupTheory/Submonoid/Operations.lean
, omitting only that which is
necessary.
Tags #
subsemigroup, range, product, map, comap
Conversion to/from Additive
/Multiplicative
#
Subsemigroups of semigroup M
are isomorphic to additive subsemigroups of Additive M
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Additive subsemigroups of an additive semigroup Additive M
are isomorphic to subsemigroups
of M
.
Equations
- AddSubsemigroup.toSubsemigroup' = Subsemigroup.toAddSubsemigroup.symm
Instances For
Additive subsemigroups of an additive semigroup A
are isomorphic to
multiplicative subsemigroups of Multiplicative A
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Subsemigroups of a semigroup Multiplicative A
are isomorphic to additive subsemigroups
of A
.
Equations
- Subsemigroup.toAddSubsemigroup' = AddSubsemigroup.toSubsemigroup.symm
Instances For
The preimage of an AddSubsemigroup
along an AddSemigroup
homomorphism is an
AddSubsemigroup
.
Equations
- AddSubsemigroup.comap f S = { carrier := ⇑f ⁻¹' ↑S, add_mem' := ⋯ }
Instances For
The preimage of a subsemigroup along a semigroup homomorphism is a subsemigroup.
Equations
- Subsemigroup.comap f S = { carrier := ⇑f ⁻¹' ↑S, mul_mem' := ⋯ }
Instances For
The image of an AddSubsemigroup
along an AddSemigroup
homomorphism is
an AddSubsemigroup
.
Equations
- AddSubsemigroup.map f S = { carrier := ⇑f '' ↑S, add_mem' := ⋯ }
Instances For
The image of a subsemigroup along a semigroup homomorphism is a subsemigroup.
Equations
- Subsemigroup.map f S = { carrier := ⇑f '' ↑S, mul_mem' := ⋯ }
Instances For
map f
and comap f
form a GaloisCoinsertion
when f
is injective.
Equations
- AddSubsemigroup.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯
Instances For
map f
and comap f
form a GaloisCoinsertion
when f
is injective.
Equations
- Subsemigroup.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯
Instances For
map f
and comap f
form a GaloisInsertion
when f
is surjective.
Equations
- AddSubsemigroup.giMapComap hf = ⋯.toGaloisInsertion ⋯
Instances For
map f
and comap f
form a GaloisInsertion
when f
is surjective.
Equations
- Subsemigroup.giMapComap hf = ⋯.toGaloisInsertion ⋯
Instances For
An additive submagma of an additive magma inherits an addition.
Equations
- AddMemClass.add S' = { add := fun (a b : ↥S') => ⟨↑a + ↑b, ⋯⟩ }
A submagma of a magma inherits a multiplication.
Equations
- MulMemClass.mul S' = { mul := fun (a b : ↥S') => ⟨↑a * ↑b, ⋯⟩ }
An AddSubsemigroup
of an AddSemigroup
inherits an AddSemigroup
structure.
Equations
- AddMemClass.toAddSemigroup S = Function.Injective.addSemigroup Subtype.val ⋯ ⋯
A subsemigroup of a semigroup inherits a semigroup structure.
Equations
- MulMemClass.toSemigroup S = Function.Injective.semigroup Subtype.val ⋯ ⋯
An AddSubsemigroup
of an AddCommSemigroup
is an AddCommSemigroup
.
Equations
- AddMemClass.toAddCommSemigroup S = Function.Injective.addCommSemigroup Subtype.val ⋯ ⋯
A subsemigroup of a CommSemigroup
is a CommSemigroup
.
Equations
- MulMemClass.toCommSemigroup S = Function.Injective.commSemigroup Subtype.val ⋯ ⋯
The natural semigroup hom from an AddSubsemigroup
of
AddSubsemigroup
M
to M
.
Equations
- AddMemClass.subtype S' = { toFun := Subtype.val, map_add' := ⋯ }
Instances For
The natural semigroup hom from a subsemigroup of semigroup M
to M
.
Equations
- MulMemClass.subtype S' = { toFun := Subtype.val, map_mul' := ⋯ }
Instances For
An additive subsemigroup is isomorphic to its image under an injective function
Equations
- S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_add' := ⋯ }
Instances For
A subsemigroup is isomorphic to its image under an injective function
Equations
- S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_mul' := ⋯ }
Instances For
Given AddSubsemigroup
s s
, t
of AddSemigroup
s A
, B
respectively,
s × t
as an AddSubsemigroup
of A × B
.
Instances For
Given Subsemigroup
s s
, t
of semigroups M
, N
respectively, s × t
as a subsemigroup
of M × N
.
Instances For
The product of additive subsemigroups is isomorphic to their product as additive semigroups
Equations
- s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_add' := ⋯ }
Instances For
The product of subsemigroups is isomorphic to their product as semigroups.
Equations
- s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_mul' := ⋯ }
Instances For
The range of an AddHom
is an AddSubsemigroup
.
Equations
- f.srange = (AddSubsemigroup.map f ⊤).copy (Set.range ⇑f) ⋯
Instances For
The range of a semigroup homomorphism is a subsemigroup. See Note [range copy pattern].
Equations
- f.srange = (Subsemigroup.map f ⊤).copy (Set.range ⇑f) ⋯
Instances For
The range of a surjective AddSemigroup
hom is the whole of the codomain.
The range of a surjective semigroup hom is the whole of the codomain.
The image under an AddSemigroup
hom of the AddSubsemigroup
generated by a set
equals the AddSubsemigroup
generated by the image of the set.
The image under a semigroup hom of the subsemigroup generated by a set equals the subsemigroup generated by the image of the set.
Restriction of an AddSemigroup hom to an AddSubsemigroup
of the domain.
Equations
- f.restrict S = f.comp (AddMemClass.subtype S)
Instances For
Restriction of a semigroup hom to a subsemigroup of the domain.
Equations
- f.restrict S = f.comp (MulMemClass.subtype S)
Instances For
Restriction of an AddSemigroup
hom to an AddSubsemigroup
of the codomain.
Equations
- f.codRestrict S h = { toFun := fun (n : M) => ⟨f n, ⋯⟩, map_add' := ⋯ }
Instances For
Restriction of a semigroup hom to a subsemigroup of the codomain.
Equations
- f.codRestrict S h = { toFun := fun (n : M) => ⟨f n, ⋯⟩, map_mul' := ⋯ }
Instances For
Restriction of an AddSemigroup
hom to its range interpreted as a subsemigroup.
Equations
- f.srangeRestrict = f.codRestrict f.srange ⋯
Instances For
The AddHom
from the preimage of an additive subsemigroup to itself.
Equations
- f.subsemigroupComap N' = { toFun := fun (x : ↥(AddSubsemigroup.comap f N')) => ⟨f ↑x, ⋯⟩, map_add' := ⋯ }
Instances For
The MulHom
from the preimage of a subsemigroup to itself.
Equations
- f.subsemigroupComap N' = { toFun := fun (x : ↥(Subsemigroup.comap f N')) => ⟨f ↑x, ⋯⟩, map_mul' := ⋯ }
Instances For
the AddHom
from an additive subsemigroup to its image. See
AddEquiv.addSubsemigroupMap
for a variant for AddEquiv
s.
Equations
- f.subsemigroupMap M' = { toFun := fun (x : ↥M') => ⟨f ↑x, ⋯⟩, map_add' := ⋯ }
Instances For
The MulHom
from a subsemigroup to its image.
See MulEquiv.subsemigroupMap
for a variant for MulEquiv
s.
Equations
- f.subsemigroupMap M' = { toFun := fun (x : ↥M') => ⟨f ↑x, ⋯⟩, map_mul' := ⋯ }
Instances For
The AddSemigroup
hom associated to an inclusion of subsemigroups.
Equations
- AddSubsemigroup.inclusion h = (AddMemClass.subtype S).codRestrict T ⋯
Instances For
The semigroup hom associated to an inclusion of subsemigroups.
Equations
- Subsemigroup.inclusion h = (MulMemClass.subtype S).codRestrict T ⋯
Instances For
Makes the identity additive isomorphism from a proof two subsemigroups of an additive semigroup are equal.
Equations
- AddEquiv.subsemigroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_add' := ⋯ }
Instances For
Makes the identity isomorphism from a proof that two subsemigroups of a multiplicative semigroup are equal.
Equations
- MulEquiv.subsemigroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }
Instances For
An additive semigroup homomorphism f : M →+ N
with a left-inverse
g : N → M
defines an additive equivalence between M
and f.srange
.
This is a bidirectional version of AddHom.srangeRestrict
.
Equations
- AddEquiv.ofLeftInverse f h = { toFun := ⇑f.srangeRestrict, invFun := g ∘ ⇑(AddMemClass.subtype f.srange), left_inv := h, right_inv := ⋯, map_add' := ⋯ }
Instances For
A semigroup homomorphism f : M →ₙ* N
with a left-inverse g : N → M
defines a multiplicative
equivalence between M
and f.srange
.
This is a bidirectional version of MulHom.srangeRestrict
.
Equations
- MulEquiv.ofLeftInverse f h = { toFun := ⇑f.srangeRestrict, invFun := g ∘ ⇑(MulMemClass.subtype f.srange), left_inv := h, right_inv := ⋯, map_mul' := ⋯ }
Instances For
An AddEquiv
φ
between two additive semigroups M
and N
induces an AddEquiv
between a subsemigroup S ≤ M
and the subsemigroup φ(S) ≤ N
.
See AddHom.addSubsemigroupMap
for a variant for AddHom
s.
Equations
- e.subsemigroupMap S = { toFun := fun (x : ↥S) => ⟨e ↑x, ⋯⟩, invFun := fun (x : ↥(AddSubsemigroup.map (↑e) S)) => ⟨e.symm ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
A MulEquiv
φ
between two semigroups M
and N
induces a MulEquiv
between
a subsemigroup S ≤ M
and the subsemigroup φ(S) ≤ N
.
See MulHom.subsemigroupMap
for a variant for MulHom
s.
Equations
- e.subsemigroupMap S = { toFun := fun (x : ↥S) => ⟨e ↑x, ⋯⟩, invFun := fun (x : ↥(Subsemigroup.map (↑e) S)) => ⟨e.symm ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }