mathlib documentation

group_theory.subsemigroup.operations

Operations on subsemigroups #

In this file we define various operations on subsemigroups and mul_homs.

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) semigroup structure on a subsemigroup #

Operations on subsemigroups #

Semigroup homomorphisms between subsemigroups #

Operations on mul_homs #

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
def add_subsemigroup.comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (S : add_subsemigroup N) :

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]
theorem add_subsemigroup.coe_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup N) (f : add_hom M N) :
@[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} :
@[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 : add_hom M N} {x : M} :
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 : add_hom N P) (f : add_hom M N) :
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) :
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
def add_subsemigroup.map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (S : add_subsemigroup M) :

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) :
@[simp]
theorem add_subsemigroup.coe_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (S : add_subsemigroup M) :
@[simp]
theorem add_subsemigroup.mem_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} {S : add_subsemigroup M} {y : N} :
y add_subsemigroup.map f S ∃ (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 subsemigroup.map f S ∃ (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 : add_hom M N) {S : add_subsemigroup M} {x : M} (hx : x S) :
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) :
theorem add_subsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M 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) :
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 : add_hom N P) (f : add_hom M N) :
theorem add_subsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.injective f) {S : add_subsemigroup M} {x : M} :
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} :
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} :
theorem add_subsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} {S : add_subsemigroup M} {T : add_subsemigroup N} :
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.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) {T : add_subsemigroup N} {f : add_hom M 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} :
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} :
theorem add_subsemigroup.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) {T : add_subsemigroup N} {f : add_hom M N} :
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} :
theorem add_subsemigroup.le_comap_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) {f : add_hom M N} :
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} :
theorem add_subsemigroup.map_comap_le {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {S : add_subsemigroup N} {f : add_hom M N} :
theorem add_subsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M 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 : add_hom M N} :
@[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} :
@[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} :
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 : add_hom M N) :
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) :
theorem add_subsemigroup.map_supr {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Sort u_3} (f : add_hom M N) (s : ι → add_subsemigroup M) :
add_subsemigroup.map f (supr s) = ⨆ (i : ι), add_subsemigroup.map f (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 : ι → subsemigroup M) :
subsemigroup.map f (supr s) = ⨆ (i : ι), subsemigroup.map f (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 : add_hom M N) :
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) :
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 : ι → subsemigroup N) :
subsemigroup.comap f (infi s) = ⨅ (i : ι), subsemigroup.comap f (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 : add_hom M N) (s : ι → add_subsemigroup N) :
@[simp]
theorem add_subsemigroup.map_bot {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M 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 : add_hom M N) :
@[simp]
theorem add_subsemigroup.map_id {M : Type u_1} [has_add M] (S : add_subsemigroup M) :
@[simp]
theorem subsemigroup.map_id {M : Type u_1} [has_mul M] (S : subsemigroup M) :

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) :
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 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) :
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 : add_hom M N} (hf : function.injective f) (S : ι → add_subsemigroup M) :
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 : ι → subsemigroup M) :
subsemigroup.comap f (⨅ (i : ι), subsemigroup.map f (S i)) = infi S
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) :
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 : add_hom M N} (hf : function.injective f) (S : ι → add_subsemigroup M) :
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 : ι → subsemigroup M) :
subsemigroup.comap f (⨆ (i : ι), subsemigroup.map f (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} :
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) :
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

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

Equations
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) :
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) :
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 : add_hom M N} (hf : function.surjective f) (S : ι → add_subsemigroup N) :
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 : ι → subsemigroup N) :
subsemigroup.map f (⨅ (i : ι), subsemigroup.comap f (S i)) = infi S
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) :
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 : ι → subsemigroup N) :
subsemigroup.map f (⨆ (i : ι), subsemigroup.comap f (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 : add_hom M N} (hf : function.surjective f) (S : ι → add_subsemigroup N) :
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} :
@[protected, instance]
def add_mem_class.has_add {M : Type u_1} {A : Type u_5} [has_add M] [set_like A M] [hA : add_mem_class A M] (S' : A) :

An additive submagma of an additive magma inherits an addition.

Equations
@[protected, instance]
def mul_mem_class.has_mul {M : Type u_1} {A : Type u_5} [has_mul M] [set_like A M] [hA : mul_mem_class A 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] [set_like A M] [hA : add_mem_class A 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] [set_like A M] [hA : mul_mem_class A 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] [set_like A M] [hA : add_mem_class A 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] [set_like A M] [hA : mul_mem_class A 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] [set_like A M] [hA : add_mem_class A 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] [set_like A M] [hA : mul_mem_class A M] (S' : A) (x y : S') :
x * y = x * y, _⟩
@[protected, instance]
def add_mem_class.to_add_semigroup {M : Type u_1} [add_semigroup M] {A : Type u_2} [set_like A M] [add_mem_class A 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} [set_like A M] [mul_mem_class A 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} [comm_semigroup M] {A : Type u_2} [set_like A M] [mul_mem_class A M] (S : A) :

A subsemigroup of a comm_semigroup is a comm_semigroup.

Equations
def mul_mem_class.subtype {M : Type u_1} {A : Type u_5} [has_mul M] [set_like A M] [hA : mul_mem_class A 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] [set_like A M] [hA : add_mem_class A 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] [set_like A M] [hA : add_mem_class A M] (S' : A) :
@[simp]
theorem mul_mem_class.coe_subtype {M : Type u_1} {A : Type u_5} [has_mul M] [set_like A M] [hA : mul_mem_class A M] (S' : A) :
@[simp]
theorem subsemigroup.top_equiv_symm_apply_coe {M : Type u_1} [has_mul M] (x : M) :
@[simp]
def add_subsemigroup.top_equiv {M : Type u_1} [has_add M] :

The top additive subsemigroup is isomorphic to the additive semigroup.

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

The top subsemigroup is isomorphic to the semigroup.

Equations
@[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 : add_hom M 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) :
@[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 : add_hom M N) (hf : function.injective f) (x : S) :
@[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 subsemigroups s, t of semigroups M, N respectively, s × t as a subsemigroup of M × N.

Equations
def add_subsemigroup.prod {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (s : add_subsemigroup M) (t : add_subsemigroup N) :

Given add_subsemigroups s, t of add_semigroups A, B respectively, s × t as an add_subsemigroup of A × B.

Equations
theorem add_subsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (s : add_subsemigroup M) (t : add_subsemigroup N) :
(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 add_subsemigroup.prod_top {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (s : add_subsemigroup M) :
theorem subsemigroup.prod_top {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (s : subsemigroup M) :
theorem subsemigroup.top_prod {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (s : subsemigroup N) :
theorem add_subsemigroup.top_prod {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (s : add_subsemigroup N) :
@[simp]
theorem subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :
@[simp]
theorem add_subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] :
theorem subsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :
theorem add_subsemigroup.bot_sum_bot {M : Type u_1} {N : Type u_2} [has_add M] [has_add 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
def add_subsemigroup.prod_equiv {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (s : add_subsemigroup M) (t : add_subsemigroup N) :

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} :
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} :
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 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) :
@[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)} :
theorem add_subsemigroup.le_prod_iff {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {s : add_subsemigroup M} {t : add_subsemigroup N} {u : add_subsemigroup (M × N)} :
def add_hom.srange {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M 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 : add_hom M 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 : add_hom M 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 : add_hom M 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 : add_hom N P) (f : add_hom M N) :
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) :
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 : add_hom M 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 : add_hom M 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 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 : add_hom M 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] [set_like σ M] [mul_mem_class σ 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] [set_like σ M] [add_mem_class σ M] (f : add_hom M N) (S : σ) :

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] [set_like σ M] [add_mem_class σ M] (f : add_hom M 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] [set_like σ M] [mul_mem_class σ 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] [set_like σ N] [add_mem_class σ N] (f : add_hom M N) (S : σ) (h : ∀ (x : M), f x 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] [set_like σ N] [mul_mem_class σ 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] [set_like σ N] [add_mem_class σ N] (f : add_hom M 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] [set_like σ N] [mul_mem_class σ 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 : add_hom M 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 : add_hom M 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 : add_hom M N) :
theorem mul_hom.srange_restrict_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :
theorem add_hom.sum_map_comap_sum' {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {M' : Type u_3} {N' : Type u_4} [has_add M'] [has_add N'] (f : add_hom M N) (g : add_hom M' N') (S : add_subsemigroup N) (S' : add_subsemigroup N') :
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') :
@[simp]
theorem add_hom.subsemigroup_comap_apply_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (N' : add_subsemigroup N) (x : (add_subsemigroup.comap f N')) :
def add_hom.subsemigroup_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (N' : add_subsemigroup 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 : (subsemigroup.comap f 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_equivs.

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

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

Equations
@[simp]
theorem add_hom.subsemigroup_map_apply_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M 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) :
theorem add_hom.subsemigroup_map_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (M' : add_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 =
theorem add_subsemigroup.sum_eq_top_iff {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] [nonempty M] [nonempty N] {s : add_subsemigroup M} {t : add_subsemigroup N} :
s.prod t = s = t =
def add_subsemigroup.inclusion {M : Type u_1} [has_add M] {S T : add_subsemigroup M} (h : S 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
theorem add_subsemigroup.eq_top_iff' {M : Type u_1} [has_add M] (S : add_subsemigroup M) :
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 : add_hom M N) {g : N → M} (h : function.left_inverse g f) (ᾰ : M) :
def add_equiv.of_left_inverse {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) {g : N → M} (h : function.left_inverse g 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 : function.left_inverse g 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 : function.left_inverse g f) (ᾰ : (f.srange)) :
@[simp]
theorem add_equiv.of_left_inverse_symm_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) {g : N → M} (h : function.left_inverse g f) (ᾰ : (f.srange)) :
@[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 : function.left_inverse g f) (ᾰ : M) :
@[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_homs.

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 : (add_subsemigroup.map e.to_add_hom S)) :
@[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 : (subsemigroup.map e.to_mul_hom S)) :
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_homs.

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) :