# mathlib3documentation

group_theory.subsemigroup.operations

# Operations on `subsemigroup`s #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define various operations on `subsemigroup`s and `mul_hom`s.

## Main definitions #

### Conversion between multiplicative and additive definitions #

• `subsemigroup.to_add_subsemigroup`, `subsemigroup.to_add_subsemigroup'`, `add_subsemigroup.to_subsemigroup`, `add_subsemigroup.to_subsemigroup'`: convert between multiplicative and additive subsemigroups of `M`, `multiplicative M`, and `additive M`. These are stated as `order_iso`s.

### (Commutative) semigroup structure on a subsemigroup #

• `subsemigroup.to_semigroup`, `subsemigroup.to_comm_semigroup`: 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 subsemigroups `s : subsemigroup M` and `t : subsemigroup N` as a subsemigroup of `M × N`;

### Semigroup homomorphisms between subsemigroups #

• `subsemigroup.subtype`: embedding of a subsemigroup into the ambient semigroup.
• `subsemigroup.inclusion`: given two subsemigroups `S`, `T` such that `S ≤ T`, `S.inclusion T` is the inclusion of `S` into `T` as a semigroup homomorphism;
• `mul_equiv.subsemigroup_congr`: converts a proof of `S = T` into a semigroup isomorphism between `S` and `T`.
• `subsemigroup.prod_equiv`: semigroup isomorphism between `s.prod t` and `s × t`;

### Operations on `mul_hom`s #

• `mul_hom.srange`: range of a semigroup homomorphism as a subsemigroup of the codomain;
• `mul_hom.restrict`: restrict a semigroup homomorphism to a subsemigroup;
• `mul_hom.cod_restrict`: restrict the codomain of a semigroup homomorphism to a subsemigroup;
• `mul_hom.srange_restrict`: restrict a semigroup homomorphism to its range;

### Implementation notes #

This file follows closely `group_theory/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
@[reducible]

Additive subsemigroups of an additive semigroup `additive M` are isomorphic to subsemigroups of `M`.

Additive subsemigroups of an additive semigroup `A` are isomorphic to multiplicative subsemigroups of `multiplicative A`.

Equations
@[reducible]

Subsemigroups of a semigroup `multiplicative A` are isomorphic to additive subsemigroups of `A`.

### `comap` and `map`#

def subsemigroup.comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (S : subsemigroup N) :

The preimage of a subsemigroup along a semigroup homomorphism is a subsemigroup.

Equations

The preimage of an `add_subsemigroup` along an `add_semigroup` homomorphism is an `add_subsemigroup`.

Equations
@[simp]
theorem subsemigroup.coe_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S : subsemigroup N) (f : M →ₙ* N) :
@[simp]
@[simp]
theorem subsemigroup.mem_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {S : subsemigroup N} {f : M →ₙ* N} {x : M} :
x f x S
@[simp]
theorem add_subsemigroup.mem_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {S : add_subsemigroup N} {f : N} {x : M} :
f x S
theorem add_subsemigroup.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (S : add_subsemigroup P) (g : P) (f : N) :
= S
theorem subsemigroup.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] (S : subsemigroup P) (g : N →ₙ* P) (f : M →ₙ* N) :
@[simp]
@[simp]
theorem subsemigroup.comap_id {P : Type u_3} [has_mul P] (S : subsemigroup P) :
= S
def subsemigroup.map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (S : subsemigroup M) :

The image of a subsemigroup along a semigroup homomorphism is a subsemigroup.

Equations

The image of an `add_subsemigroup` along an `add_semigroup` homomorphism is an `add_subsemigroup`.

Equations
@[simp]
theorem subsemigroup.coe_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (S : subsemigroup M) :
S) = f '' S
@[simp]
S) = f '' S
@[simp]
theorem add_subsemigroup.mem_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} {S : add_subsemigroup M} {y : N} :
(x : M) (H : x S), f x = y
@[simp]
theorem subsemigroup.mem_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} {S : subsemigroup M} {y : N} :
y (x : M) (H : x S), f x = y
theorem add_subsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) {S : add_subsemigroup M} {x : M} (hx : x S) :
f x
theorem subsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) {S : subsemigroup M} {x : M} (hx : x S) :
f x
theorem add_subsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (S : add_subsemigroup M) (x : S) :
theorem subsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (S : subsemigroup M) (x : S) :
theorem subsemigroup.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] (S : subsemigroup M) (g : N →ₙ* P) (f : M →ₙ* N) :
S) = subsemigroup.map (g.comp f) S
theorem add_subsemigroup.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (S : add_subsemigroup M) (g : P) (f : N) :
theorem add_subsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.injective f) {S : add_subsemigroup M} {x : M} :
f x x S
theorem subsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective f) {S : subsemigroup M} {x : M} :
f x x S
theorem subsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} {S : subsemigroup M} {T : subsemigroup N} :
T S
theorem subsemigroup.gc_map_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :
theorem add_subsemigroup.gc_map_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) :
theorem subsemigroup.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S : subsemigroup M) {T : subsemigroup N} {f : M →ₙ* N} :
S T
theorem subsemigroup.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S : subsemigroup M) {T : subsemigroup N} {f : M →ₙ* N} :
T S
theorem subsemigroup.le_comap_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S : subsemigroup M) {f : M →ₙ* N} :
S
theorem subsemigroup.map_comap_le {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {S : subsemigroup N} {f : M →ₙ* N} :
S
theorem add_subsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} :
theorem subsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} :
theorem subsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} :
theorem add_subsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} :
@[simp]
@[simp]
theorem subsemigroup.map_comap_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S : subsemigroup M) {f : M →ₙ* N} :
S)) =
@[simp]
@[simp]
theorem subsemigroup.comap_map_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {S : subsemigroup N} {f : M →ₙ* N} :
S)) =
theorem add_subsemigroup.map_sup {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S T : add_subsemigroup M) (f : N) :
(S T) =
theorem subsemigroup.map_sup {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S T : subsemigroup M) (f : M →ₙ* N) :
(S T) =
theorem add_subsemigroup.map_supr {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Sort u_3} (f : N) (s : ι ) :
(supr s) = (i : ι), (s i)
theorem subsemigroup.map_supr {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Sort u_3} (f : M →ₙ* N) (s : ι ) :
(supr s) = (i : ι), (s i)
theorem add_subsemigroup.comap_inf {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S T : add_subsemigroup N) (f : N) :
(S T) =
theorem subsemigroup.comap_inf {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S T : subsemigroup N) (f : M →ₙ* N) :
(S T) =
theorem subsemigroup.comap_infi {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Sort u_3} (f : M →ₙ* N) (s : ι ) :
(infi s) = (i : ι), (s i)
theorem add_subsemigroup.comap_infi {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Sort u_3} (f : N) (s : ι ) :
= (i : ι), (s i)
@[simp]
theorem add_subsemigroup.map_bot {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) :
@[simp]
theorem subsemigroup.map_bot {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :
@[simp]
theorem subsemigroup.comap_top {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :
@[simp]
theorem add_subsemigroup.comap_top {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) :
@[simp]
= S
@[simp]
theorem subsemigroup.map_id {M : Type u_1} [has_mul M] (S : subsemigroup M) :
= S
def add_subsemigroup.gci_map_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.injective f) :

`map f` and `comap f` form a `galois_coinsertion` when `f` is injective.

Equations
def subsemigroup.gci_map_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective f) :

`map f` and `comap f` form a `galois_coinsertion` when `f` is injective.

Equations
theorem subsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective f) (S : subsemigroup M) :
= S
theorem add_subsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.injective f) (S : add_subsemigroup M) :
theorem subsemigroup.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective f) :
theorem add_subsemigroup.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.injective f) :
theorem subsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective f) :
theorem add_subsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.injective f) :
theorem add_subsemigroup.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.injective f) (S T : add_subsemigroup M) :
= S T
theorem subsemigroup.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective f) (S T : subsemigroup M) :
S T) = S T
theorem add_subsemigroup.comap_infi_map_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Type u_5} {f : N} (hf : function.injective f) (S : ι ) :
( (i : ι), (S i)) = infi S
theorem subsemigroup.comap_infi_map_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : function.injective f) (S : ι ) :
( (i : ι), (S i)) = infi S
theorem add_subsemigroup.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.injective f) (S T : add_subsemigroup M) :
= S T
theorem subsemigroup.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective f) (S T : subsemigroup M) :
S T) = S T
theorem add_subsemigroup.comap_supr_map_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Type u_5} {f : N} (hf : function.injective f) (S : ι ) :
( (i : ι), (S i)) = supr S
theorem subsemigroup.comap_supr_map_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : function.injective f) (S : ι ) :
( (i : ι), (S i)) = supr S
theorem subsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective f) {S T : subsemigroup M} :
S T
theorem add_subsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.injective f) {S T : add_subsemigroup M} :
S T
theorem subsemigroup.map_strict_mono_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective f) :
theorem add_subsemigroup.map_strict_mono_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.injective f) :
def subsemigroup.gi_map_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective f) :

`map f` and `comap f` form a `galois_insertion` when `f` is surjective.

Equations
def add_subsemigroup.gi_map_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.surjective f) :

`map f` and `comap f` form a `galois_insertion` when `f` is surjective.

Equations
theorem add_subsemigroup.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.surjective f) (S : add_subsemigroup N) :
theorem subsemigroup.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective f) (S : subsemigroup N) :
= S
theorem add_subsemigroup.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.surjective f) :
theorem subsemigroup.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective f) :
theorem add_subsemigroup.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.surjective f) :
theorem subsemigroup.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective f) :
theorem add_subsemigroup.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.surjective f) (S T : add_subsemigroup N) :
= S T
theorem subsemigroup.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective f) (S T : subsemigroup N) :
= S T
theorem add_subsemigroup.map_infi_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Type u_5} {f : N} (hf : function.surjective f) (S : ι ) :
( (i : ι), (S i)) = infi S
theorem subsemigroup.map_infi_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : function.surjective f) (S : ι ) :
( (i : ι), (S i)) = infi S
theorem add_subsemigroup.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.surjective f) (S T : add_subsemigroup N) :
= S T
theorem subsemigroup.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective f) (S T : subsemigroup N) :
= S T
theorem subsemigroup.map_supr_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : function.surjective f) (S : ι ) :
( (i : ι), (S i)) = supr S
theorem add_subsemigroup.map_supr_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Type u_5} {f : N} (hf : function.surjective f) (S : ι ) :
( (i : ι), (S i)) = supr S
theorem add_subsemigroup.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} (hf : function.surjective f) {S T : add_subsemigroup N} :
S T
theorem subsemigroup.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective f) {S T : subsemigroup N} :
S T
@[protected, instance]
def add_mem_class.has_add {M : Type u_1} {A : Type u_5} [has_add M] [ M] [hA : M] (S' : A) :

Equations
@[protected, instance]
def mul_mem_class.has_mul {M : Type u_1} {A : Type u_5} [has_mul M] [ M] [hA : M] (S' : A) :

A submagma of a magma inherits a multiplication.

Equations
@[simp, norm_cast]
theorem add_mem_class.coe_add {M : Type u_1} {A : Type u_5} [has_add M] [ M] [hA : M] (S' : A) (x y : S') :
(x + y) = x + y
@[simp, norm_cast]
theorem mul_mem_class.coe_mul {M : Type u_1} {A : Type u_5} [has_mul M] [ M] [hA : M] (S' : A) (x y : S') :
(x * y) = x * y
@[simp]
theorem add_mem_class.mk_add_mk {M : Type u_1} {A : Type u_5} [has_add M] [ M] [hA : M] (S' : A) (x y : M) (hx : x S') (hy : y S') :
x, hx⟩ + y, hy⟩ = x + y, _⟩
@[simp]
theorem mul_mem_class.mk_mul_mk {M : Type u_1} {A : Type u_5} [has_mul M] [ M] [hA : M] (S' : A) (x y : M) (hx : x S') (hy : y S') :
x, hx⟩ * y, hy⟩ = x * y, _⟩
theorem add_mem_class.add_def {M : Type u_1} {A : Type u_5} [has_add M] [ M] [hA : M] (S' : A) (x y : S') :
x + y = x + y, _⟩
theorem mul_mem_class.mul_def {M : Type u_1} {A : Type u_5} [has_mul M] [ M] [hA : M] (S' : A) (x y : S') :
x * y = x * y, _⟩
@[protected, instance]
def add_mem_class.to_add_semigroup {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

An `add_subsemigroup` of an `add_semigroup` inherits an `add_semigroup` structure.

Equations
@[protected, instance]
def mul_mem_class.to_semigroup {M : Type u_1} [semigroup M] {A : Type u_2} [ M] [ M] (S : A) :

A subsemigroup of a semigroup inherits a semigroup structure.

Equations
@[protected, instance]
def mul_mem_class.to_comm_semigroup {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

A subsemigroup of a `comm_semigroup` is a `comm_semigroup`.

Equations
@[protected, instance]
def add_mem_class.to_add_comm_semigroup {M : Type u_1} {A : Type u_2} [ M] [ M] (S : A) :

An `add_subsemigroup` of an `add_comm_semigroup` is an `add_comm_semigroup`.

Equations
def mul_mem_class.subtype {M : Type u_1} {A : Type u_5} [has_mul M] [ M] [hA : M] (S' : A) :

The natural semigroup hom from a subsemigroup of semigroup `M` to `M`.

Equations
def add_mem_class.subtype {M : Type u_1} {A : Type u_5} [has_add M] [ M] [hA : M] (S' : A) :

The natural semigroup hom from an `add_subsemigroup` of `add_semigroup` `M` to `M`.

Equations
@[simp]
theorem add_mem_class.coe_subtype {M : Type u_1} {A : Type u_5} [has_add M] [ M] [hA : M] (S' : A) :
@[simp]
theorem mul_mem_class.coe_subtype {M : Type u_1} {A : Type u_5} [has_mul M] [ M] [hA : M] (S' : A) :
@[simp]
theorem add_subsemigroup.top_equiv_apply {M : Type u_1} [has_add M] (x : ) :
@[simp]
theorem add_subsemigroup.top_equiv_symm_apply_coe {M : Type u_1} [has_add M] (x : M) :

Equations
def subsemigroup.top_equiv {M : Type u_1} [has_mul M] :

The top subsemigroup is isomorphic to the semigroup.

Equations
@[simp]
theorem subsemigroup.top_equiv_apply {M : Type u_1} [has_mul M] (x : ) :
@[simp]
@[simp]
noncomputable def add_subsemigroup.equiv_map_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) (f : N) (hf : function.injective f) :

An additive subsemigroup is isomorphic to its image under an injective function

Equations
noncomputable def subsemigroup.equiv_map_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S : subsemigroup M) (f : M →ₙ* N) (hf : function.injective f) :

A subsemigroup is isomorphic to its image under an injective function

Equations
@[simp]
theorem subsemigroup.coe_equiv_map_of_injective_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S : subsemigroup M) (f : M →ₙ* N) (hf : function.injective f) (x : S) :
( hf) x) = f x
@[simp]
theorem add_subsemigroup.coe_equiv_map_of_injective_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) (f : N) (hf : function.injective f) (x : S) :
( hf) x) = f x
@[simp]
theorem subsemigroup.closure_closure_coe_preimage {M : Type u_1} [has_mul M] {s : set M} :
@[simp]
def subsemigroup.prod {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (s : subsemigroup M) (t : subsemigroup N) :

Given `subsemigroup`s `s`, `t` of semigroups `M`, `N` respectively, `s × t` as a subsemigroup of `M × N`.

Equations

Given `add_subsemigroup`s `s`, `t` of `add_semigroup`s `A`, `B` respectively, `s × t` as an `add_subsemigroup` of `A × B`.

Equations
(s.prod t) = s ×ˢ t
theorem subsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (s : subsemigroup M) (t : subsemigroup N) :
(s.prod t) = s ×ˢ t
theorem subsemigroup.mem_prod {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {s : subsemigroup M} {t : subsemigroup N} {p : M × N} :
p s.prod t p.fst s p.snd t
theorem add_subsemigroup.mem_prod {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {s : add_subsemigroup M} {t : add_subsemigroup N} {p : M × N} :
p s.prod t p.fst s p.snd t
theorem subsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {s₁ s₂ : subsemigroup M} {t₁ t₂ : subsemigroup N} (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.prod t₁ s₂.prod t₂
theorem add_subsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {s₁ s₂ : add_subsemigroup M} {t₁ t₂ : add_subsemigroup N} (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.prod t₁ s₂.prod t₂
theorem subsemigroup.prod_top {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (s : subsemigroup M) :
s.prod = s
theorem subsemigroup.top_prod {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (s : subsemigroup N) :
.prod s = s
@[simp]
theorem subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :
@[simp]
theorem subsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :
def subsemigroup.prod_equiv {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (s : subsemigroup M) (t : subsemigroup N) :

The product of subsemigroups is isomorphic to their product as semigroups.

Equations

The product of additive subsemigroups is isomorphic to their product as additive semigroups

Equations
theorem add_subsemigroup.mem_map_equiv {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : M ≃+ N} {K : add_subsemigroup M} {x : N} :
(f.symm) x K
theorem subsemigroup.mem_map_equiv {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M ≃* N} {K : subsemigroup M} {x : N} :
(f.symm) x K
theorem subsemigroup.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M ≃* N) (K : subsemigroup M) :
theorem add_subsemigroup.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : M ≃+ N) (K : add_subsemigroup M) :
theorem subsemigroup.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : N ≃* M) (K : subsemigroup M) :
theorem add_subsemigroup.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N ≃+ M) (K : add_subsemigroup M) :
@[simp]
theorem subsemigroup.map_equiv_top {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M ≃* N) :
@[simp]
theorem add_subsemigroup.map_equiv_top {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : M ≃+ N) :
theorem subsemigroup.le_prod_iff {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {s : subsemigroup M} {t : subsemigroup N} {u : subsemigroup (M × N)} :
u s.prod t u s u t
u s.prod t u s u t
def add_hom.srange {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) :

The range of an `add_hom` is an `add_subsemigroup`.

Equations
def mul_hom.srange {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :

The range of a semigroup homomorphism is a subsemigroup. See Note [range copy pattern].

Equations
@[simp]
theorem add_hom.coe_srange {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) :
@[simp]
theorem mul_hom.coe_srange {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :
@[simp]
theorem mul_hom.mem_srange {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} {y : N} :
y f.srange (x : M), f x = y
@[simp]
theorem add_hom.mem_srange {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : N} {y : N} :
y f.srange (x : M), f x = y
theorem mul_hom.srange_eq_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :
theorem add_hom.srange_eq_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) :
theorem add_hom.map_srange {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (g : P) (f : N) :
= (g.comp f).srange
theorem mul_hom.map_srange {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul M] [has_mul N] [has_mul P] (g : N →ₙ* P) (f : M →ₙ* N) :
= (g.comp f).srange
theorem mul_hom.srange_top_iff_surjective {M : Type u_1} [has_mul M] {N : Type u_2} [has_mul N] {f : M →ₙ* N} :
theorem add_hom.srange_top_iff_surjective {M : Type u_1} [has_add M] {N : Type u_2} [has_add N] {f : N} :
theorem mul_hom.srange_top_of_surjective {M : Type u_1} [has_mul M] {N : Type u_2} [has_mul N] (f : M →ₙ* N) (hf : function.surjective f) :

The range of a surjective semigroup hom is the whole of the codomain.

theorem add_hom.srange_top_of_surjective {M : Type u_1} [has_add M] {N : Type u_2} [has_add N] (f : N) (hf : function.surjective f) :

The range of a surjective `add_semigroup` hom is the whole of the codomain.

theorem mul_hom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (s : set N) :
theorem add_hom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (s : set N) :
theorem mul_hom.map_mclosure {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (s : set M) :

The image under a semigroup hom of the subsemigroup generated by a set equals the subsemigroup generated by the image of the set.

theorem add_hom.map_mclosure {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (s : set M) :

The image under an `add_semigroup` hom of the `add_subsemigroup` generated by a set equals the `add_subsemigroup` generated by the image of the set.

def mul_hom.restrict {M : Type u_1} {σ : Type u_4} [has_mul M] {N : Type u_2} [has_mul N] [ M] [ M] (f : M →ₙ* N) (S : σ) :

Restriction of a semigroup hom to a subsemigroup of the domain.

Equations
def add_hom.restrict {M : Type u_1} {σ : Type u_4} [has_add M] {N : Type u_2} [has_add N] [ M] [ M] (f : N) (S : σ) :
N

Restriction of an add_semigroup hom to an `add_subsemigroup` of the domain.

Equations
@[simp]
theorem add_hom.restrict_apply {M : Type u_1} {σ : Type u_4} [has_add M] {N : Type u_2} [has_add N] [ M] [ M] (f : N) {S : σ} (x : S) :
(f.restrict S) x = f x
@[simp]
theorem mul_hom.restrict_apply {M : Type u_1} {σ : Type u_4} [has_mul M] {N : Type u_2} [has_mul N] [ M] [ M] (f : M →ₙ* N) {S : σ} (x : S) :
(f.restrict S) x = f x
def add_hom.cod_restrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [has_add M] [has_add N] [ N] [ N] (f : N) (S : σ) (h : (x : M), f x S) :
S

Restriction of an `add_semigroup` hom to an `add_subsemigroup` of the codomain.

Equations
def mul_hom.cod_restrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [has_mul M] [has_mul N] [ N] [ N] (f : M →ₙ* N) (S : σ) (h : (x : M), f x S) :

Restriction of a semigroup hom to a subsemigroup of the codomain.

Equations
@[simp]
theorem add_hom.cod_restrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_4} [has_add M] [has_add N] [ N] [ N] (f : N) (S : σ) (h : (x : M), f x S) (n : M) :
((f.cod_restrict S h) n) = f n
@[simp]
theorem mul_hom.cod_restrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_4} [has_mul M] [has_mul N] [ N] [ N] (f : M →ₙ* N) (S : σ) (h : (x : M), f x S) (n : M) :
((f.cod_restrict S h) n) = f n
def mul_hom.srange_restrict {M : Type u_1} [has_mul M] {N : Type u_2} [has_mul N] (f : M →ₙ* N) :

Restriction of a semigroup hom to its range interpreted as a subsemigroup.

Equations
def add_hom.srange_restrict {M : Type u_1} [has_add M] {N : Type u_2} [has_add N] (f : N) :

Restriction of an `add_semigroup` hom to its range interpreted as a subsemigroup.

Equations
@[simp]
theorem add_hom.coe_srange_restrict {M : Type u_1} [has_add M] {N : Type u_2} [has_add N] (f : N) (x : M) :
@[simp]
theorem mul_hom.coe_srange_restrict {M : Type u_1} [has_mul M] {N : Type u_2} [has_mul N] (f : M →ₙ* N) (x : M) :
theorem add_hom.srange_restrict_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) :
theorem mul_hom.srange_restrict_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :
(S.prod S') = .prod S')
theorem mul_hom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {M' : Type u_3} {N' : Type u_4} [has_mul M'] [has_mul N'] (f : M →ₙ* N) (g : M' →ₙ* N') (S : subsemigroup N) (S' : subsemigroup N') :
(S.prod S') = S).prod S')
@[simp]
theorem add_hom.subsemigroup_comap_apply_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (N' : add_subsemigroup N) (x : N')) :
N'

the `add_hom` from the preimage of an additive subsemigroup to itself.

Equations
@[simp]
theorem mul_hom.subsemigroup_comap_apply_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (N' : subsemigroup N) (x : N')) :
def mul_hom.subsemigroup_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (N' : subsemigroup N) :

The `mul_hom` from the preimage of a subsemigroup to itself.

Equations
def mul_hom.subsemigroup_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (M' : subsemigroup M) :

The `mul_hom` from a subsemigroup to its image. See `mul_equiv.subsemigroup_map` for a variant for `mul_equiv`s.

Equations

the `add_hom` from an additive subsemigroup to its image. See `add_equiv.add_subsemigroup_map` for a variant for `add_equiv`s.

Equations
@[simp]
theorem add_hom.subsemigroup_map_apply_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (M' : add_subsemigroup M) (x : M') :
@[simp]
theorem mul_hom.subsemigroup_map_apply_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (M' : subsemigroup M) (x : M') :
theorem mul_hom.subsemigroup_map_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (M' : subsemigroup M) :
@[simp]
theorem subsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] [nonempty N] :
@[simp]
theorem add_subsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] [nonempty N] :
@[simp]
theorem add_subsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] [nonempty M] :
@[simp]
theorem subsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] [nonempty M] :
theorem subsemigroup.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] [nonempty M] [nonempty N] {s : subsemigroup M} {t : subsemigroup N} :
s.prod t = s = t =
s.prod t = s = t =
def add_subsemigroup.inclusion {M : Type u_1} [has_add M] {S T : add_subsemigroup M} (h : S T) :
T

The `add_semigroup` hom associated to an inclusion of subsemigroups.

Equations
def subsemigroup.inclusion {M : Type u_1} [has_mul M] {S T : subsemigroup M} (h : S T) :

The semigroup hom associated to an inclusion of subsemigroups.

Equations
@[simp]
@[simp]
theorem subsemigroup.range_subtype {M : Type u_1} [has_mul M] (s : subsemigroup M) :
theorem subsemigroup.eq_top_iff' {M : Type u_1} [has_mul M] (S : subsemigroup M) :
S = (x : M), x S
S = (x : M), x S
def mul_equiv.subsemigroup_congr {M : Type u_1} [has_mul M] {S T : subsemigroup M} (h : S = T) :

Makes the identity isomorphism from a proof that two subsemigroups of a multiplicative semigroup are equal.

Equations
def add_equiv.subsemigroup_congr {M : Type u_1} [has_add M] {S T : add_subsemigroup M} (h : S = T) :

Makes the identity additive isomorphism from a proof two subsemigroups of an additive semigroup are equal.

Equations
@[simp]
theorem add_equiv.of_left_inverse_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) {g : N M} (h : f) (ᾰ : M) :
= (f.srange_restrict) ᾰ
def add_equiv.of_left_inverse {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) {g : N M} (h : f) :

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 `add_hom.srange_restrict`.

Equations
def mul_equiv.of_left_inverse {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) {g : N M} (h : f) :

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 `mul_hom.srange_restrict`.

Equations
@[simp]
theorem mul_equiv.of_left_inverse_symm_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) {g : N M} (h : f) (ᾰ : (f.srange)) :
.symm) = g
@[simp]
theorem add_equiv.of_left_inverse_symm_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) {g : N M} (h : f) (ᾰ : (f.srange)) :
.symm) = g
@[simp]
theorem mul_equiv.of_left_inverse_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) {g : N M} (h : f) (ᾰ : M) :
= (f.srange_restrict) ᾰ
@[simp]
theorem mul_equiv.subsemigroup_map_apply_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (e : M ≃* N) (S : subsemigroup M) (x : S) :
def add_equiv.subsemigroup_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (e : M ≃+ N) (S : add_subsemigroup M) :

An `add_equiv` `φ` between two additive semigroups `M` and `N` induces an `add_equiv` between a subsemigroup `S ≤ M` and the subsemigroup `φ(S) ≤ N`. See `add_hom.add_subsemigroup_map` for a variant for `add_hom`s.

Equations
@[simp]
theorem add_equiv.subsemigroup_map_symm_apply_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (e : M ≃+ N) (S : add_subsemigroup M) (x : ) :
@[simp]
theorem mul_equiv.subsemigroup_map_symm_apply_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (e : M ≃* N) (S : subsemigroup M) (x : ) :
def mul_equiv.subsemigroup_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (e : M ≃* N) (S : subsemigroup M) :

A `mul_equiv` `φ` between two semigroups `M` and `N` induces a `mul_equiv` between a subsemigroup `S ≤ M` and the subsemigroup `φ(S) ≤ N`. See `mul_hom.subsemigroup_map` for a variant for `mul_hom`s.

Equations
@[simp]
theorem add_equiv.subsemigroup_map_apply_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (e : M ≃+ N) (S : add_subsemigroup M) (x : S) :